; @origtpdbfilename ./TRS/TRCSR/LISTUTILITIES_complete_L.trs
; @xtcfilename "./TRS_Standard/Transformed_CSR_04/LISTUTILITIES_complete_L.xml"
(format TRS)
(fun U11 1)
(fun tt 0)
(fun snd 1)
(fun splitAt 2)
(fun U161 1)
(fun cons 1)
(fun U171 1)
(fun head 1)
(fun afterNth 2)
(fun U181 1)
(fun U191 1)
(fun pair 2)
(fun nil 0)
(fun U201 1)
(fun U202 1)
(fun U21 1)
(fun U211 1)
(fun U221 1)
(fun fst 1)
(fun U31 1)
(fun and 1)
(fun U101 1)
(fun U102 1)
(fun isNatural 0)
(fun U103 1)
(fun isLNat 0)
(fun U111 1)
(fun U112 1)
(fun U121 1)
(fun U122 1)
(fun U131 1)
(fun U132 1)
(fun U133 1)
(fun U141 1)
(fun U142 1)
(fun U143 1)
(fun U151 1)
(fun U152 1)
(fun U153 1)
(fun U41 1)
(fun U42 1)
(fun U43 1)
(fun U51 1)
(fun U52 1)
(fun U53 1)
(fun U61 1)
(fun U62 1)
(fun isPLNat 0)
(fun U71 1)
(fun U72 1)
(fun U81 1)
(fun U82 1)
(fun U91 1)
(fun U92 1)
(fun isNaturalKind 0)
(fun isPLNatKind 0)
(fun isLNatKind 0)
(fun natsFrom 1)
(fun sel 2)
(fun |0| 0)
(fun s 1)
(fun tail 1)
(fun take 2)
(rule (U11 tt) (snd (splitAt N XS)))
(rule (U161 tt) (cons N))
(rule (U171 tt) (head (afterNth N XS)))
(rule (U181 tt) Y)
(rule (U191 tt) (pair nil XS))
(rule (U201 tt) (U202 (splitAt N XS)))
(rule (U202 (pair YS ZS)) (pair (cons X) ZS))
(rule (U21 tt) X)
(rule (U211 tt) XS)
(rule (U221 tt) (fst (splitAt N XS)))
(rule (U31 tt) N)
(rule (and tt) X)
(rule (U101 tt) (U102 isNatural))
(rule (U102 tt) (U103 isLNat))
(rule (U103 tt) tt)
(rule (U111 tt) (U112 isLNat))
(rule (U112 tt) tt)
(rule (U121 tt) (U122 isNatural))
(rule (U122 tt) tt)
(rule (U131 tt) (U132 isNatural))
(rule (U132 tt) (U133 isLNat))
(rule (U133 tt) tt)
(rule (U141 tt) (U142 isLNat))
(rule (U142 tt) (U143 isLNat))
(rule (U143 tt) tt)
(rule (U151 tt) (U152 isNatural))
(rule (U152 tt) (U153 isLNat))
(rule (U153 tt) tt)
(rule (U41 tt) (U42 isNatural))
(rule (U42 tt) (U43 isLNat))
(rule (U43 tt) tt)
(rule (U51 tt) (U52 isNatural))
(rule (U52 tt) (U53 isLNat))
(rule (U53 tt) tt)
(rule (U61 tt) (U62 isPLNat))
(rule (U62 tt) tt)
(rule (U71 tt) (U72 isNatural))
(rule (U72 tt) tt)
(rule (U81 tt) (U82 isPLNat))
(rule (U82 tt) tt)
(rule (U91 tt) (U92 isLNat))
(rule (U92 tt) tt)
(rule (afterNth N XS) (U11 (and (and isNatural))))
(rule (fst (pair X Y)) (U21 (and (and isLNat))))
(rule (head (cons N)) (U31 (and (and isNatural))))
(rule isLNat tt)
(rule isLNat (U41 (and isNaturalKind)))
(rule isLNat (U51 (and isNaturalKind)))
(rule isLNat (U61 isPLNatKind))
(rule isLNat (U71 isNaturalKind))
(rule isLNat (U81 isPLNatKind))
(rule isLNat (U91 isLNatKind))
(rule isLNat (U101 (and isNaturalKind)))
(rule isLNatKind tt)
(rule isLNatKind (and isNaturalKind))
(rule isLNatKind isPLNatKind)
(rule isLNatKind isNaturalKind)
(rule isLNatKind isLNatKind)
(rule isNatural tt)
(rule isNatural (U111 isLNatKind))
(rule isNatural (U121 isNaturalKind))
(rule isNatural (U131 (and isNaturalKind)))
(rule isNaturalKind tt)
(rule isNaturalKind isLNatKind)
(rule isNaturalKind isNaturalKind)
(rule isNaturalKind (and isNaturalKind))
(rule isPLNat (U141 (and isLNatKind)))
(rule isPLNat (U151 (and isNaturalKind)))
(rule isPLNatKind (and isLNatKind))
(rule isPLNatKind (and isNaturalKind))
(rule (natsFrom N) (U161 (and isNatural)))
(rule (sel N XS) (U171 (and (and isNatural))))
(rule (snd (pair X Y)) (U181 (and (and isLNat))))
(rule (splitAt |0| XS) (U191 (and isLNat)))
(rule (splitAt (s N) (cons X)) (U201 (and (and isNatural))))
(rule (tail (cons N)) (U211 (and (and isNatural))))
(rule (take N XS) (U221 (and (and isNatural))))