; @origtpdbfilename ./TRS/TRCSR/LISTUTILITIES_complete_GM.trs
; @xtcfilename "./TRS_Standard/Transformed_CSR_04/LISTUTILITIES_complete_GM.xml"
(format TRS)
(fun a__U101 3)
(fun tt 0)
(fun a__U102 2)
(fun a__isNatural 1)
(fun a__U103 1)
(fun a__isLNat 1)
(fun a__U11 3)
(fun a__snd 1)
(fun a__splitAt 2)
(fun mark 1)
(fun a__U111 2)
(fun a__U112 1)
(fun a__U121 2)
(fun a__U122 1)
(fun a__U131 3)
(fun a__U132 2)
(fun a__U133 1)
(fun a__U141 3)
(fun a__U142 2)
(fun a__U143 1)
(fun a__U151 3)
(fun a__U152 2)
(fun a__U153 1)
(fun a__U161 2)
(fun cons 2)
(fun natsFrom 1)
(fun s 1)
(fun a__U171 3)
(fun a__head 1)
(fun a__afterNth 2)
(fun a__U181 2)
(fun a__U191 2)
(fun pair 2)
(fun nil 0)
(fun a__U201 4)
(fun a__U202 2)
(fun a__U21 2)
(fun a__U211 2)
(fun a__U221 3)
(fun a__fst 1)
(fun a__U31 2)
(fun a__U41 3)
(fun a__U42 2)
(fun a__U43 1)
(fun a__U51 3)
(fun a__U52 2)
(fun a__U53 1)
(fun a__U61 2)
(fun a__U62 1)
(fun a__isPLNat 1)
(fun a__U71 2)
(fun a__U72 1)
(fun a__U81 2)
(fun a__U82 1)
(fun a__U91 2)
(fun a__U92 1)
(fun a__and 2)
(fun isNaturalKind 1)
(fun and 2)
(fun isLNat 1)
(fun isLNatKind 1)
(fun afterNth 2)
(fun a__isNaturalKind 1)
(fun fst 1)
(fun a__isPLNatKind 1)
(fun snd 1)
(fun tail 1)
(fun a__isLNatKind 1)
(fun take 2)
(fun |0| 0)
(fun head 1)
(fun sel 2)
(fun splitAt 2)
(fun a__natsFrom 1)
(fun a__sel 2)
(fun isNatural 1)
(fun a__tail 1)
(fun a__take 2)
(fun U101 3)
(fun U102 2)
(fun U103 1)
(fun U11 3)
(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 U171 3)
(fun U181 2)
(fun U191 2)
(fun U201 4)
(fun U202 2)
(fun U21 2)
(fun U211 2)
(fun U221 3)
(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 isPLNatKind 1)
(rule (a__U101 tt V1 V2) (a__U102 (a__isNatural V1) V2))
(rule (a__U102 tt V2) (a__U103 (a__isLNat V2)))
(rule (a__U103 tt) tt)
(rule (a__U11 tt N XS) (a__snd (a__splitAt (mark N) (mark XS))))
(rule (a__U111 tt V1) (a__U112 (a__isLNat V1)))
(rule (a__U112 tt) tt)
(rule (a__U121 tt V1) (a__U122 (a__isNatural V1)))
(rule (a__U122 tt) tt)
(rule (a__U131 tt V1 V2) (a__U132 (a__isNatural V1) V2))
(rule (a__U132 tt V2) (a__U133 (a__isLNat V2)))
(rule (a__U133 tt) tt)
(rule (a__U141 tt V1 V2) (a__U142 (a__isLNat V1) V2))
(rule (a__U142 tt V2) (a__U143 (a__isLNat V2)))
(rule (a__U143 tt) tt)
(rule (a__U151 tt V1 V2) (a__U152 (a__isNatural V1) V2))
(rule (a__U152 tt V2) (a__U153 (a__isLNat V2)))
(rule (a__U153 tt) tt)
(rule (a__U161 tt N) (cons (mark N) (natsFrom (s N))))
(rule (a__U171 tt N XS) (a__head (a__afterNth (mark N) (mark XS))))
(rule (a__U181 tt Y) (mark Y))
(rule (a__U191 tt XS) (pair nil (mark XS)))
(rule (a__U201 tt N X XS) (a__U202 (a__splitAt (mark N) (mark XS)) X))
(rule (a__U202 (pair YS ZS) X) (pair (cons (mark X) YS) (mark ZS)))
(rule (a__U21 tt X) (mark X))
(rule (a__U211 tt XS) (mark XS))
(rule (a__U221 tt N XS) (a__fst (a__splitAt (mark N) (mark XS))))
(rule (a__U31 tt N) (mark N))
(rule (a__U41 tt V1 V2) (a__U42 (a__isNatural V1) V2))
(rule (a__U42 tt V2) (a__U43 (a__isLNat V2)))
(rule (a__U43 tt) tt)
(rule (a__U51 tt V1 V2) (a__U52 (a__isNatural V1) V2))
(rule (a__U52 tt V2) (a__U53 (a__isLNat V2)))
(rule (a__U53 tt) tt)
(rule (a__U61 tt V1) (a__U62 (a__isPLNat V1)))
(rule (a__U62 tt) tt)
(rule (a__U71 tt V1) (a__U72 (a__isNatural V1)))
(rule (a__U72 tt) tt)
(rule (a__U81 tt V1) (a__U82 (a__isPLNat V1)))
(rule (a__U82 tt) tt)
(rule (a__U91 tt V1) (a__U92 (a__isLNat V1)))
(rule (a__U92 tt) tt)
(rule (a__afterNth N XS) (a__U11 (a__and (a__and (a__isNatural N) (isNaturalKind N)) (and (isLNat XS) (isLNatKind XS))) N XS))
(rule (a__and tt X) (mark X))
(rule (a__fst (pair X Y)) (a__U21 (a__and (a__and (a__isLNat X) (isLNatKind X)) (and (isLNat Y) (isLNatKind Y))) X))
(rule (a__head (cons N XS)) (a__U31 (a__and (a__and (a__isNatural N) (isNaturalKind N)) (and (isLNat XS) (isLNatKind XS))) N))
(rule (a__isLNat nil) tt)
(rule (a__isLNat (afterNth V1 V2)) (a__U41 (a__and (a__isNaturalKind V1) (isLNatKind V2)) V1 V2))
(rule (a__isLNat (cons V1 V2)) (a__U51 (a__and (a__isNaturalKind V1) (isLNatKind V2)) V1 V2))
(rule (a__isLNat (fst V1)) (a__U61 (a__isPLNatKind V1) V1))
(rule (a__isLNat (natsFrom V1)) (a__U71 (a__isNaturalKind V1) V1))
(rule (a__isLNat (snd V1)) (a__U81 (a__isPLNatKind V1) V1))
(rule (a__isLNat (tail V1)) (a__U91 (a__isLNatKind V1) V1))
(rule (a__isLNat (take V1 V2)) (a__U101 (a__and (a__isNaturalKind V1) (isLNatKind V2)) V1 V2))
(rule (a__isLNatKind nil) tt)
(rule (a__isLNatKind (afterNth V1 V2)) (a__and (a__isNaturalKind V1) (isLNatKind V2)))
(rule (a__isLNatKind (cons V1 V2)) (a__and (a__isNaturalKind V1) (isLNatKind V2)))
(rule (a__isLNatKind (fst V1)) (a__isPLNatKind V1))
(rule (a__isLNatKind (natsFrom V1)) (a__isNaturalKind V1))
(rule (a__isLNatKind (snd V1)) (a__isPLNatKind V1))
(rule (a__isLNatKind (tail V1)) (a__isLNatKind V1))
(rule (a__isLNatKind (take V1 V2)) (a__and (a__isNaturalKind V1) (isLNatKind V2)))
(rule (a__isNatural |0|) tt)
(rule (a__isNatural (head V1)) (a__U111 (a__isLNatKind V1) V1))
(rule (a__isNatural (s V1)) (a__U121 (a__isNaturalKind V1) V1))
(rule (a__isNatural (sel V1 V2)) (a__U131 (a__and (a__isNaturalKind V1) (isLNatKind V2)) V1 V2))
(rule (a__isNaturalKind |0|) tt)
(rule (a__isNaturalKind (head V1)) (a__isLNatKind V1))
(rule (a__isNaturalKind (s V1)) (a__isNaturalKind V1))
(rule (a__isNaturalKind (sel V1 V2)) (a__and (a__isNaturalKind V1) (isLNatKind V2)))
(rule (a__isPLNat (pair V1 V2)) (a__U141 (a__and (a__isLNatKind V1) (isLNatKind V2)) V1 V2))
(rule (a__isPLNat (splitAt V1 V2)) (a__U151 (a__and (a__isNaturalKind V1) (isLNatKind V2)) V1 V2))
(rule (a__isPLNatKind (pair V1 V2)) (a__and (a__isLNatKind V1) (isLNatKind V2)))
(rule (a__isPLNatKind (splitAt V1 V2)) (a__and (a__isNaturalKind V1) (isLNatKind V2)))
(rule (a__natsFrom N) (a__U161 (a__and (a__isNatural N) (isNaturalKind N)) N))
(rule (a__sel N XS) (a__U171 (a__and (a__and (a__isNatural N) (isNaturalKind N)) (and (isLNat XS) (isLNatKind XS))) N XS))
(rule (a__snd (pair X Y)) (a__U181 (a__and (a__and (a__isLNat X) (isLNatKind X)) (and (isLNat Y) (isLNatKind Y))) Y))
(rule (a__splitAt |0| XS) (a__U191 (a__and (a__isLNat XS) (isLNatKind XS)) XS))
(rule (a__splitAt (s N) (cons X XS)) (a__U201 (a__and (a__and (a__isNatural N) (isNaturalKind N)) (and (and (isNatural X) (isNaturalKind X)) (and (isLNat XS) (isLNatKind XS)))) N X XS))
(rule (a__tail (cons N XS)) (a__U211 (a__and (a__and (a__isNatural N) (isNaturalKind N)) (and (isLNat XS) (isLNatKind XS))) XS))
(rule (a__take N XS) (a__U221 (a__and (a__and (a__isNatural N) (isNaturalKind N)) (and (isLNat XS) (isLNatKind XS))) N XS))
(rule (mark (U101 X1 X2 X3)) (a__U101 (mark X1) X2 X3))
(rule (mark (U102 X1 X2)) (a__U102 (mark X1) X2))
(rule (mark (isNatural X)) (a__isNatural X))
(rule (mark (U103 X)) (a__U103 (mark X)))
(rule (mark (isLNat X)) (a__isLNat X))
(rule (mark (U11 X1 X2 X3)) (a__U11 (mark X1) X2 X3))
(rule (mark (snd X)) (a__snd (mark X)))
(rule (mark (splitAt X1 X2)) (a__splitAt (mark X1) (mark X2)))
(rule (mark (U111 X1 X2)) (a__U111 (mark X1) X2))
(rule (mark (U112 X)) (a__U112 (mark X)))
(rule (mark (U121 X1 X2)) (a__U121 (mark X1) X2))
(rule (mark (U122 X)) (a__U122 (mark X)))
(rule (mark (U131 X1 X2 X3)) (a__U131 (mark X1) X2 X3))
(rule (mark (U132 X1 X2)) (a__U132 (mark X1) X2))
(rule (mark (U133 X)) (a__U133 (mark X)))
(rule (mark (U141 X1 X2 X3)) (a__U141 (mark X1) X2 X3))
(rule (mark (U142 X1 X2)) (a__U142 (mark X1) X2))
(rule (mark (U143 X)) (a__U143 (mark X)))
(rule (mark (U151 X1 X2 X3)) (a__U151 (mark X1) X2 X3))
(rule (mark (U152 X1 X2)) (a__U152 (mark X1) X2))
(rule (mark (U153 X)) (a__U153 (mark X)))
(rule (mark (U161 X1 X2)) (a__U161 (mark X1) X2))
(rule (mark (natsFrom X)) (a__natsFrom (mark X)))
(rule (mark (U171 X1 X2 X3)) (a__U171 (mark X1) X2 X3))
(rule (mark (head X)) (a__head (mark X)))
(rule (mark (afterNth X1 X2)) (a__afterNth (mark X1) (mark X2)))
(rule (mark (U181 X1 X2)) (a__U181 (mark X1) X2))
(rule (mark (U191 X1 X2)) (a__U191 (mark X1) X2))
(rule (mark (U201 X1 X2 X3 X4)) (a__U201 (mark X1) X2 X3 X4))
(rule (mark (U202 X1 X2)) (a__U202 (mark X1) X2))
(rule (mark (U21 X1 X2)) (a__U21 (mark X1) X2))
(rule (mark (U211 X1 X2)) (a__U211 (mark X1) X2))
(rule (mark (U221 X1 X2 X3)) (a__U221 (mark X1) X2 X3))
(rule (mark (fst X)) (a__fst (mark X)))
(rule (mark (U31 X1 X2)) (a__U31 (mark X1) X2))
(rule (mark (U41 X1 X2 X3)) (a__U41 (mark X1) X2 X3))
(rule (mark (U42 X1 X2)) (a__U42 (mark X1) X2))
(rule (mark (U43 X)) (a__U43 (mark X)))
(rule (mark (U51 X1 X2 X3)) (a__U51 (mark X1) X2 X3))
(rule (mark (U52 X1 X2)) (a__U52 (mark X1) X2))
(rule (mark (U53 X)) (a__U53 (mark X)))
(rule (mark (U61 X1 X2)) (a__U61 (mark X1) X2))
(rule (mark (U62 X)) (a__U62 (mark X)))
(rule (mark (isPLNat X)) (a__isPLNat X))
(rule (mark (U71 X1 X2)) (a__U71 (mark X1) X2))
(rule (mark (U72 X)) (a__U72 (mark X)))
(rule (mark (U81 X1 X2)) (a__U81 (mark X1) X2))
(rule (mark (U82 X)) (a__U82 (mark X)))
(rule (mark (U91 X1 X2)) (a__U91 (mark X1) X2))
(rule (mark (U92 X)) (a__U92 (mark X)))
(rule (mark (and X1 X2)) (a__and (mark X1) X2))
(rule (mark (isNaturalKind X)) (a__isNaturalKind X))
(rule (mark (isLNatKind X)) (a__isLNatKind X))
(rule (mark (isPLNatKind X)) (a__isPLNatKind X))
(rule (mark (tail X)) (a__tail (mark X)))
(rule (mark (take X1 X2)) (a__take (mark X1) (mark X2)))
(rule (mark (sel X1 X2)) (a__sel (mark X1) (mark X2)))
(rule (mark tt) tt)
(rule (mark (cons X1 X2)) (cons (mark X1) X2))
(rule (mark (s X)) (s (mark X)))
(rule (mark (pair X1 X2)) (pair (mark X1) (mark X2)))
(rule (mark nil) nil)
(rule (mark |0|) |0|)
(rule (a__U101 X1 X2 X3) (U101 X1 X2 X3))
(rule (a__U102 X1 X2) (U102 X1 X2))
(rule (a__isNatural X) (isNatural X))
(rule (a__U103 X) (U103 X))
(rule (a__isLNat X) (isLNat X))
(rule (a__U11 X1 X2 X3) (U11 X1 X2 X3))
(rule (a__snd X) (snd X))
(rule (a__splitAt X1 X2) (splitAt X1 X2))
(rule (a__U111 X1 X2) (U111 X1 X2))
(rule (a__U112 X) (U112 X))
(rule (a__U121 X1 X2) (U121 X1 X2))
(rule (a__U122 X) (U122 X))
(rule (a__U131 X1 X2 X3) (U131 X1 X2 X3))
(rule (a__U132 X1 X2) (U132 X1 X2))
(rule (a__U133 X) (U133 X))
(rule (a__U141 X1 X2 X3) (U141 X1 X2 X3))
(rule (a__U142 X1 X2) (U142 X1 X2))
(rule (a__U143 X) (U143 X))
(rule (a__U151 X1 X2 X3) (U151 X1 X2 X3))
(rule (a__U152 X1 X2) (U152 X1 X2))
(rule (a__U153 X) (U153 X))
(rule (a__U161 X1 X2) (U161 X1 X2))
(rule (a__natsFrom X) (natsFrom X))
(rule (a__U171 X1 X2 X3) (U171 X1 X2 X3))
(rule (a__head X) (head X))
(rule (a__afterNth X1 X2) (afterNth X1 X2))
(rule (a__U181 X1 X2) (U181 X1 X2))
(rule (a__U191 X1 X2) (U191 X1 X2))
(rule (a__U201 X1 X2 X3 X4) (U201 X1 X2 X3 X4))
(rule (a__U202 X1 X2) (U202 X1 X2))
(rule (a__U21 X1 X2) (U21 X1 X2))
(rule (a__U211 X1 X2) (U211 X1 X2))
(rule (a__U221 X1 X2 X3) (U221 X1 X2 X3))
(rule (a__fst X) (fst X))
(rule (a__U31 X1 X2) (U31 X1 X2))
(rule (a__U41 X1 X2 X3) (U41 X1 X2 X3))
(rule (a__U42 X1 X2) (U42 X1 X2))
(rule (a__U43 X) (U43 X))
(rule (a__U51 X1 X2 X3) (U51 X1 X2 X3))
(rule (a__U52 X1 X2) (U52 X1 X2))
(rule (a__U53 X) (U53 X))
(rule (a__U61 X1 X2) (U61 X1 X2))
(rule (a__U62 X) (U62 X))
(rule (a__isPLNat X) (isPLNat X))
(rule (a__U71 X1 X2) (U71 X1 X2))
(rule (a__U72 X) (U72 X))
(rule (a__U81 X1 X2) (U81 X1 X2))
(rule (a__U82 X) (U82 X))
(rule (a__U91 X1 X2) (U91 X1 X2))
(rule (a__U92 X) (U92 X))
(rule (a__and X1 X2) (and X1 X2))
(rule (a__isNaturalKind X) (isNaturalKind X))
(rule (a__isLNatKind X) (isLNatKind X))
(rule (a__isPLNatKind X) (isPLNatKind X))
(rule (a__tail X) (tail X))
(rule (a__take X1 X2) (take X1 X2))
(rule (a__sel X1 X2) (sel X1 X2))