; @origtpdbfilename ./TRS/TRCSR/LISTUTILITIES_complete_Z.trs
; @xtcfilename "./TRS_Standard/Transformed_CSR_04/LISTUTILITIES_complete_Z.xml"
(format TRS)
(fun U101 3)
(fun tt 0)
(fun U102 2)
(fun isNatural 1)
(fun activate 1)
(fun U103 1)
(fun isLNat 1)
(fun U11 3)
(fun snd 1)
(fun splitAt 2)
(fun U111 2)
(fun U112 1)
(fun U121 2)
(fun U122 1)
(fun U131 3)
(fun U132 2)
(fun U133 1)
(fun U141 3)
(fun U142 2)
(fun U143 1)
(fun U151 3)
(fun U152 2)
(fun U153 1)
(fun U161 2)
(fun cons 2)
(fun n__natsFrom 1)
(fun s 1)
(fun U171 3)
(fun head 1)
(fun afterNth 2)
(fun U181 2)
(fun U191 2)
(fun pair 2)
(fun nil 0)
(fun U201 4)
(fun U202 2)
(fun U21 2)
(fun U211 2)
(fun U221 3)
(fun fst 1)
(fun U31 2)
(fun U41 3)
(fun U42 2)
(fun U43 1)
(fun U51 3)
(fun U52 2)
(fun U53 1)
(fun U61 2)
(fun U62 1)
(fun isPLNat 1)
(fun U71 2)
(fun U72 1)
(fun U81 2)
(fun U82 1)
(fun U91 2)
(fun U92 1)
(fun and 2)
(fun n__isNaturalKind 1)
(fun n__and 2)
(fun n__isLNatKind 1)
(fun n__nil 0)
(fun n__afterNth 2)
(fun isNaturalKind 1)
(fun n__cons 2)
(fun n__fst 1)
(fun isPLNatKind 1)
(fun n__snd 1)
(fun n__tail 1)
(fun isLNatKind 1)
(fun n__take 2)
(fun n__0 0)
(fun n__head 1)
(fun n__s 1)
(fun n__sel 2)
(fun n__pair 2)
(fun n__splitAt 2)
(fun natsFrom 1)
(fun sel 2)
(fun |0| 0)
(fun tail 1)
(fun take 2)
(rule (U101 tt V1 V2) (U102 (isNatural (activate V1)) (activate V2)))
(rule (U102 tt V2) (U103 (isLNat (activate V2))))
(rule (U103 tt) tt)
(rule (U11 tt N XS) (snd (splitAt (activate N) (activate XS))))
(rule (U111 tt V1) (U112 (isLNat (activate V1))))
(rule (U112 tt) tt)
(rule (U121 tt V1) (U122 (isNatural (activate V1))))
(rule (U122 tt) tt)
(rule (U131 tt V1 V2) (U132 (isNatural (activate V1)) (activate V2)))
(rule (U132 tt V2) (U133 (isLNat (activate V2))))
(rule (U133 tt) tt)
(rule (U141 tt V1 V2) (U142 (isLNat (activate V1)) (activate V2)))
(rule (U142 tt V2) (U143 (isLNat (activate V2))))
(rule (U143 tt) tt)
(rule (U151 tt V1 V2) (U152 (isNatural (activate V1)) (activate V2)))
(rule (U152 tt V2) (U153 (isLNat (activate V2))))
(rule (U153 tt) tt)
(rule (U161 tt N) (cons (activate N) (n__natsFrom (s (activate N)))))
(rule (U171 tt N XS) (head (afterNth (activate N) (activate XS))))
(rule (U181 tt Y) (activate Y))
(rule (U191 tt XS) (pair nil (activate XS)))
(rule (U201 tt N X XS) (U202 (splitAt (activate N) (activate XS)) (activate X)))
(rule (U202 (pair YS ZS) X) (pair (cons (activate X) YS) ZS))
(rule (U21 tt X) (activate X))
(rule (U211 tt XS) (activate XS))
(rule (U221 tt N XS) (fst (splitAt (activate N) (activate XS))))
(rule (U31 tt N) (activate N))
(rule (U41 tt V1 V2) (U42 (isNatural (activate V1)) (activate V2)))
(rule (U42 tt V2) (U43 (isLNat (activate V2))))
(rule (U43 tt) tt)
(rule (U51 tt V1 V2) (U52 (isNatural (activate V1)) (activate V2)))
(rule (U52 tt V2) (U53 (isLNat (activate V2))))
(rule (U53 tt) tt)
(rule (U61 tt V1) (U62 (isPLNat (activate V1))))
(rule (U62 tt) tt)
(rule (U71 tt V1) (U72 (isNatural (activate V1))))
(rule (U72 tt) tt)
(rule (U81 tt V1) (U82 (isPLNat (activate V1))))
(rule (U82 tt) tt)
(rule (U91 tt V1) (U92 (isLNat (activate V1))))
(rule (U92 tt) tt)
(rule (afterNth N XS) (U11 (and (and (isNatural N) (n__isNaturalKind N)) (n__and (isLNat XS) (n__isLNatKind XS))) N XS))
(rule (and tt X) (activate X))
(rule (fst (pair X Y)) (U21 (and (and (isLNat X) (n__isLNatKind X)) (n__and (isLNat Y) (n__isLNatKind Y))) X))
(rule (head (cons N XS)) (U31 (and (and (isNatural N) (n__isNaturalKind N)) (n__and (isLNat (activate XS)) (n__isLNatKind (activate XS)))) N))
(rule (isLNat n__nil) tt)
(rule (isLNat (n__afterNth V1 V2)) (U41 (and (isNaturalKind (activate V1)) (n__isLNatKind (activate V2))) (activate V1) (activate V2)))
(rule (isLNat (n__cons V1 V2)) (U51 (and (isNaturalKind (activate V1)) (n__isLNatKind (activate V2))) (activate V1) (activate V2)))
(rule (isLNat (n__fst V1)) (U61 (isPLNatKind (activate V1)) (activate V1)))
(rule (isLNat (n__natsFrom V1)) (U71 (isNaturalKind (activate V1)) (activate V1)))
(rule (isLNat (n__snd V1)) (U81 (isPLNatKind (activate V1)) (activate V1)))
(rule (isLNat (n__tail V1)) (U91 (isLNatKind (activate V1)) (activate V1)))
(rule (isLNat (n__take V1 V2)) (U101 (and (isNaturalKind (activate V1)) (n__isLNatKind (activate V2))) (activate V1) (activate V2)))
(rule (isLNatKind n__nil) tt)
(rule (isLNatKind (n__afterNth V1 V2)) (and (isNaturalKind (activate V1)) (n__isLNatKind (activate V2))))
(rule (isLNatKind (n__cons V1 V2)) (and (isNaturalKind (activate V1)) (n__isLNatKind (activate V2))))
(rule (isLNatKind (n__fst V1)) (isPLNatKind (activate V1)))
(rule (isLNatKind (n__natsFrom V1)) (isNaturalKind (activate V1)))
(rule (isLNatKind (n__snd V1)) (isPLNatKind (activate V1)))
(rule (isLNatKind (n__tail V1)) (isLNatKind (activate V1)))
(rule (isLNatKind (n__take V1 V2)) (and (isNaturalKind (activate V1)) (n__isLNatKind (activate V2))))
(rule (isNatural n__0) tt)
(rule (isNatural (n__head V1)) (U111 (isLNatKind (activate V1)) (activate V1)))
(rule (isNatural (n__s V1)) (U121 (isNaturalKind (activate V1)) (activate V1)))
(rule (isNatural (n__sel V1 V2)) (U131 (and (isNaturalKind (activate V1)) (n__isLNatKind (activate V2))) (activate V1) (activate V2)))
(rule (isNaturalKind n__0) tt)
(rule (isNaturalKind (n__head V1)) (isLNatKind (activate V1)))
(rule (isNaturalKind (n__s V1)) (isNaturalKind (activate V1)))
(rule (isNaturalKind (n__sel V1 V2)) (and (isNaturalKind (activate V1)) (n__isLNatKind (activate V2))))
(rule (isPLNat (n__pair V1 V2)) (U141 (and (isLNatKind (activate V1)) (n__isLNatKind (activate V2))) (activate V1) (activate V2)))
(rule (isPLNat (n__splitAt V1 V2)) (U151 (and (isNaturalKind (activate V1)) (n__isLNatKind (activate V2))) (activate V1) (activate V2)))
(rule (isPLNatKind (n__pair V1 V2)) (and (isLNatKind (activate V1)) (n__isLNatKind (activate V2))))
(rule (isPLNatKind (n__splitAt V1 V2)) (and (isNaturalKind (activate V1)) (n__isLNatKind (activate V2))))
(rule (natsFrom N) (U161 (and (isNatural N) (n__isNaturalKind N)) N))
(rule (sel N XS) (U171 (and (and (isNatural N) (n__isNaturalKind N)) (n__and (isLNat XS) (n__isLNatKind XS))) N XS))
(rule (snd (pair X Y)) (U181 (and (and (isLNat X) (n__isLNatKind X)) (n__and (isLNat Y) (n__isLNatKind Y))) Y))
(rule (splitAt |0| XS) (U191 (and (isLNat XS) (n__isLNatKind XS)) XS))
(rule (splitAt (s N) (cons X XS)) (U201 (and (and (isNatural N) (n__isNaturalKind N)) (n__and (and (isNatural X) (n__isNaturalKind X)) (n__and (isLNat (activate XS)) (n__isLNatKind (activate XS))))) N X (activate XS)))
(rule (tail (cons N XS)) (U211 (and (and (isNatural N) (n__isNaturalKind N)) (n__and (isLNat (activate XS)) (n__isLNatKind (activate XS)))) (activate XS)))
(rule (take N XS) (U221 (and (and (isNatural N) (n__isNaturalKind N)) (n__and (isLNat XS) (n__isLNatKind XS))) N XS))
(rule (natsFrom X) (n__natsFrom X))
(rule (isNaturalKind X) (n__isNaturalKind X))
(rule (and X1 X2) (n__and X1 X2))
(rule (isLNatKind X) (n__isLNatKind X))
(rule nil n__nil)
(rule (afterNth X1 X2) (n__afterNth X1 X2))
(rule (cons X1 X2) (n__cons X1 X2))
(rule (fst X) (n__fst X))
(rule (snd X) (n__snd X))
(rule (tail X) (n__tail X))
(rule (take X1 X2) (n__take X1 X2))
(rule |0| n__0)
(rule (head X) (n__head X))
(rule (s X) (n__s X))
(rule (sel X1 X2) (n__sel X1 X2))
(rule (pair X1 X2) (n__pair X1 X2))
(rule (splitAt X1 X2) (n__splitAt X1 X2))
(rule (activate (n__natsFrom X)) (natsFrom X))
(rule (activate (n__isNaturalKind X)) (isNaturalKind X))
(rule (activate (n__and X1 X2)) (and X1 X2))
(rule (activate (n__isLNatKind X)) (isLNatKind X))
(rule (activate n__nil) nil)
(rule (activate (n__afterNth X1 X2)) (afterNth X1 X2))
(rule (activate (n__cons X1 X2)) (cons X1 X2))
(rule (activate (n__fst X)) (fst X))
(rule (activate (n__snd X)) (snd X))
(rule (activate (n__tail X)) (tail X))
(rule (activate (n__take X1 X2)) (take X1 X2))
(rule (activate n__0) |0|)
(rule (activate (n__head X)) (head X))
(rule (activate (n__s X)) (s X))
(rule (activate (n__sel X1 X2)) (sel X1 X2))
(rule (activate (n__pair X1 X2)) (pair X1 X2))
(rule (activate (n__splitAt X1 X2)) (splitAt X1 X2))
(rule (activate X) X)