; @origtpdbfilename ./TRS/TRCSR/LISTUTILITIES_nokinds_noand_C.trs
; @xtcfilename "./TRS_Standard/Transformed_CSR_04/LISTUTILITIES_nokinds_noand_C.xml"
(format TRS)
(fun active 1)
(fun U101 2)
(fun tt 0)
(fun mark 1)
(fun U102 1)
(fun isLNat 1)
(fun U11 3)
(fun U12 3)
(fun U111 1)
(fun snd 1)
(fun splitAt 2)
(fun U121 1)
(fun U131 2)
(fun U132 1)
(fun U141 2)
(fun U142 1)
(fun U151 2)
(fun U152 1)
(fun U161 2)
(fun cons 2)
(fun natsFrom 1)
(fun s 1)
(fun U171 3)
(fun U172 3)
(fun head 1)
(fun afterNth 2)
(fun U181 2)
(fun U182 2)
(fun U191 2)
(fun pair 2)
(fun nil 0)
(fun U201 4)
(fun U202 4)
(fun isNatural 1)
(fun U203 4)
(fun U204 2)
(fun U21 3)
(fun U22 2)
(fun U211 2)
(fun U212 2)
(fun U221 3)
(fun U222 3)
(fun fst 1)
(fun U31 3)
(fun U32 2)
(fun U41 2)
(fun U42 1)
(fun U51 2)
(fun U52 1)
(fun U61 1)
(fun U71 1)
(fun U81 1)
(fun U91 1)
(fun isPLNat 1)
(fun tail 1)
(fun take 2)
(fun |0| 0)
(fun sel 2)
(fun proper 1)
(fun ok 1)
(fun top 1)
(rule (active (U101 tt V2)) (mark (U102 (isLNat V2))))
(rule (active (U102 tt)) (mark tt))
(rule (active (U11 tt N XS)) (mark (U12 (isLNat XS) N XS)))
(rule (active (U111 tt)) (mark tt))
(rule (active (U12 tt N XS)) (mark (snd (splitAt N XS))))
(rule (active (U121 tt)) (mark tt))
(rule (active (U131 tt V2)) (mark (U132 (isLNat V2))))
(rule (active (U132 tt)) (mark tt))
(rule (active (U141 tt V2)) (mark (U142 (isLNat V2))))
(rule (active (U142 tt)) (mark tt))
(rule (active (U151 tt V2)) (mark (U152 (isLNat V2))))
(rule (active (U152 tt)) (mark tt))
(rule (active (U161 tt N)) (mark (cons N (natsFrom (s N)))))
(rule (active (U171 tt N XS)) (mark (U172 (isLNat XS) N XS)))
(rule (active (U172 tt N XS)) (mark (head (afterNth N XS))))
(rule (active (U181 tt Y)) (mark (U182 (isLNat Y) Y)))
(rule (active (U182 tt Y)) (mark Y))
(rule (active (U191 tt XS)) (mark (pair nil XS)))
(rule (active (U201 tt N X XS)) (mark (U202 (isNatural X) N X XS)))
(rule (active (U202 tt N X XS)) (mark (U203 (isLNat XS) N X XS)))
(rule (active (U203 tt N X XS)) (mark (U204 (splitAt N XS) X)))
(rule (active (U204 (pair YS ZS) X)) (mark (pair (cons X YS) ZS)))
(rule (active (U21 tt X Y)) (mark (U22 (isLNat Y) X)))
(rule (active (U211 tt XS)) (mark (U212 (isLNat XS) XS)))
(rule (active (U212 tt XS)) (mark XS))
(rule (active (U22 tt X)) (mark X))
(rule (active (U221 tt N XS)) (mark (U222 (isLNat XS) N XS)))
(rule (active (U222 tt N XS)) (mark (fst (splitAt N XS))))
(rule (active (U31 tt N XS)) (mark (U32 (isLNat XS) N)))
(rule (active (U32 tt N)) (mark N))
(rule (active (U41 tt V2)) (mark (U42 (isLNat V2))))
(rule (active (U42 tt)) (mark tt))
(rule (active (U51 tt V2)) (mark (U52 (isLNat V2))))
(rule (active (U52 tt)) (mark tt))
(rule (active (U61 tt)) (mark tt))
(rule (active (U71 tt)) (mark tt))
(rule (active (U81 tt)) (mark tt))
(rule (active (U91 tt)) (mark tt))
(rule (active (afterNth N XS)) (mark (U11 (isNatural N) N XS)))
(rule (active (fst (pair X Y))) (mark (U21 (isLNat X) X Y)))
(rule (active (head (cons N XS))) (mark (U31 (isNatural N) N XS)))
(rule (active (isLNat nil)) (mark tt))
(rule (active (isLNat (afterNth V1 V2))) (mark (U41 (isNatural V1) V2)))
(rule (active (isLNat (cons V1 V2))) (mark (U51 (isNatural V1) V2)))
(rule (active (isLNat (fst V1))) (mark (U61 (isPLNat V1))))
(rule (active (isLNat (natsFrom V1))) (mark (U71 (isNatural V1))))
(rule (active (isLNat (snd V1))) (mark (U81 (isPLNat V1))))
(rule (active (isLNat (tail V1))) (mark (U91 (isLNat V1))))
(rule (active (isLNat (take V1 V2))) (mark (U101 (isNatural V1) V2)))
(rule (active (isNatural |0|)) (mark tt))
(rule (active (isNatural (head V1))) (mark (U111 (isLNat V1))))
(rule (active (isNatural (s V1))) (mark (U121 (isNatural V1))))
(rule (active (isNatural (sel V1 V2))) (mark (U131 (isNatural V1) V2)))
(rule (active (isPLNat (pair V1 V2))) (mark (U141 (isLNat V1) V2)))
(rule (active (isPLNat (splitAt V1 V2))) (mark (U151 (isNatural V1) V2)))
(rule (active (natsFrom N)) (mark (U161 (isNatural N) N)))
(rule (active (sel N XS)) (mark (U171 (isNatural N) N XS)))
(rule (active (snd (pair X Y))) (mark (U181 (isLNat X) Y)))
(rule (active (splitAt |0| XS)) (mark (U191 (isLNat XS) XS)))
(rule (active (splitAt (s N) (cons X XS))) (mark (U201 (isNatural N) N X XS)))
(rule (active (tail (cons N XS))) (mark (U211 (isNatural N) XS)))
(rule (active (take N XS)) (mark (U221 (isNatural N) N XS)))
(rule (active (U101 X1 X2)) (U101 (active X1) X2))
(rule (active (U102 X)) (U102 (active X)))
(rule (active (U11 X1 X2 X3)) (U11 (active X1) X2 X3))
(rule (active (U12 X1 X2 X3)) (U12 (active X1) X2 X3))
(rule (active (U111 X)) (U111 (active X)))
(rule (active (snd X)) (snd (active X)))
(rule (active (splitAt X1 X2)) (splitAt (active X1) X2))
(rule (active (splitAt X1 X2)) (splitAt X1 (active X2)))
(rule (active (U121 X)) (U121 (active X)))
(rule (active (U131 X1 X2)) (U131 (active X1) X2))
(rule (active (U132 X)) (U132 (active X)))
(rule (active (U141 X1 X2)) (U141 (active X1) X2))
(rule (active (U142 X)) (U142 (active X)))
(rule (active (U151 X1 X2)) (U151 (active X1) X2))
(rule (active (U152 X)) (U152 (active X)))
(rule (active (U161 X1 X2)) (U161 (active X1) X2))
(rule (active (cons X1 X2)) (cons (active X1) X2))
(rule (active (natsFrom X)) (natsFrom (active X)))
(rule (active (s X)) (s (active X)))
(rule (active (U171 X1 X2 X3)) (U171 (active X1) X2 X3))
(rule (active (U172 X1 X2 X3)) (U172 (active X1) X2 X3))
(rule (active (head X)) (head (active X)))
(rule (active (afterNth X1 X2)) (afterNth (active X1) X2))
(rule (active (afterNth X1 X2)) (afterNth X1 (active X2)))
(rule (active (U181 X1 X2)) (U181 (active X1) X2))
(rule (active (U182 X1 X2)) (U182 (active X1) X2))
(rule (active (U191 X1 X2)) (U191 (active X1) X2))
(rule (active (pair X1 X2)) (pair (active X1) X2))
(rule (active (pair X1 X2)) (pair X1 (active X2)))
(rule (active (U201 X1 X2 X3 X4)) (U201 (active X1) X2 X3 X4))
(rule (active (U202 X1 X2 X3 X4)) (U202 (active X1) X2 X3 X4))
(rule (active (U203 X1 X2 X3 X4)) (U203 (active X1) X2 X3 X4))
(rule (active (U204 X1 X2)) (U204 (active X1) X2))
(rule (active (U21 X1 X2 X3)) (U21 (active X1) X2 X3))
(rule (active (U22 X1 X2)) (U22 (active X1) X2))
(rule (active (U211 X1 X2)) (U211 (active X1) X2))
(rule (active (U212 X1 X2)) (U212 (active X1) X2))
(rule (active (U221 X1 X2 X3)) (U221 (active X1) X2 X3))
(rule (active (U222 X1 X2 X3)) (U222 (active X1) X2 X3))
(rule (active (fst X)) (fst (active X)))
(rule (active (U31 X1 X2 X3)) (U31 (active X1) X2 X3))
(rule (active (U32 X1 X2)) (U32 (active X1) X2))
(rule (active (U41 X1 X2)) (U41 (active X1) X2))
(rule (active (U42 X)) (U42 (active X)))
(rule (active (U51 X1 X2)) (U51 (active X1) X2))
(rule (active (U52 X)) (U52 (active X)))
(rule (active (U61 X)) (U61 (active X)))
(rule (active (U71 X)) (U71 (active X)))
(rule (active (U81 X)) (U81 (active X)))
(rule (active (U91 X)) (U91 (active X)))
(rule (active (tail X)) (tail (active X)))
(rule (active (take X1 X2)) (take (active X1) X2))
(rule (active (take X1 X2)) (take X1 (active X2)))
(rule (active (sel X1 X2)) (sel (active X1) X2))
(rule (active (sel X1 X2)) (sel X1 (active X2)))
(rule (U101 (mark X1) X2) (mark (U101 X1 X2)))
(rule (U102 (mark X)) (mark (U102 X)))
(rule (U11 (mark X1) X2 X3) (mark (U11 X1 X2 X3)))
(rule (U12 (mark X1) X2 X3) (mark (U12 X1 X2 X3)))
(rule (U111 (mark X)) (mark (U111 X)))
(rule (snd (mark X)) (mark (snd X)))
(rule (splitAt (mark X1) X2) (mark (splitAt X1 X2)))
(rule (splitAt X1 (mark X2)) (mark (splitAt X1 X2)))
(rule (U121 (mark X)) (mark (U121 X)))
(rule (U131 (mark X1) X2) (mark (U131 X1 X2)))
(rule (U132 (mark X)) (mark (U132 X)))
(rule (U141 (mark X1) X2) (mark (U141 X1 X2)))
(rule (U142 (mark X)) (mark (U142 X)))
(rule (U151 (mark X1) X2) (mark (U151 X1 X2)))
(rule (U152 (mark X)) (mark (U152 X)))
(rule (U161 (mark X1) X2) (mark (U161 X1 X2)))
(rule (cons (mark X1) X2) (mark (cons X1 X2)))
(rule (natsFrom (mark X)) (mark (natsFrom X)))
(rule (s (mark X)) (mark (s X)))
(rule (U171 (mark X1) X2 X3) (mark (U171 X1 X2 X3)))
(rule (U172 (mark X1) X2 X3) (mark (U172 X1 X2 X3)))
(rule (head (mark X)) (mark (head X)))
(rule (afterNth (mark X1) X2) (mark (afterNth X1 X2)))
(rule (afterNth X1 (mark X2)) (mark (afterNth X1 X2)))
(rule (U181 (mark X1) X2) (mark (U181 X1 X2)))
(rule (U182 (mark X1) X2) (mark (U182 X1 X2)))
(rule (U191 (mark X1) X2) (mark (U191 X1 X2)))
(rule (pair (mark X1) X2) (mark (pair X1 X2)))
(rule (pair X1 (mark X2)) (mark (pair X1 X2)))
(rule (U201 (mark X1) X2 X3 X4) (mark (U201 X1 X2 X3 X4)))
(rule (U202 (mark X1) X2 X3 X4) (mark (U202 X1 X2 X3 X4)))
(rule (U203 (mark X1) X2 X3 X4) (mark (U203 X1 X2 X3 X4)))
(rule (U204 (mark X1) X2) (mark (U204 X1 X2)))
(rule (U21 (mark X1) X2 X3) (mark (U21 X1 X2 X3)))
(rule (U22 (mark X1) X2) (mark (U22 X1 X2)))
(rule (U211 (mark X1) X2) (mark (U211 X1 X2)))
(rule (U212 (mark X1) X2) (mark (U212 X1 X2)))
(rule (U221 (mark X1) X2 X3) (mark (U221 X1 X2 X3)))
(rule (U222 (mark X1) X2 X3) (mark (U222 X1 X2 X3)))
(rule (fst (mark X)) (mark (fst X)))
(rule (U31 (mark X1) X2 X3) (mark (U31 X1 X2 X3)))
(rule (U32 (mark X1) X2) (mark (U32 X1 X2)))
(rule (U41 (mark X1) X2) (mark (U41 X1 X2)))
(rule (U42 (mark X)) (mark (U42 X)))
(rule (U51 (mark X1) X2) (mark (U51 X1 X2)))
(rule (U52 (mark X)) (mark (U52 X)))
(rule (U61 (mark X)) (mark (U61 X)))
(rule (U71 (mark X)) (mark (U71 X)))
(rule (U81 (mark X)) (mark (U81 X)))
(rule (U91 (mark X)) (mark (U91 X)))
(rule (tail (mark X)) (mark (tail X)))
(rule (take (mark X1) X2) (mark (take X1 X2)))
(rule (take X1 (mark X2)) (mark (take X1 X2)))
(rule (sel (mark X1) X2) (mark (sel X1 X2)))
(rule (sel X1 (mark X2)) (mark (sel X1 X2)))
(rule (proper (U101 X1 X2)) (U101 (proper X1) (proper X2)))
(rule (proper tt) (ok tt))
(rule (proper (U102 X)) (U102 (proper X)))
(rule (proper (isLNat X)) (isLNat (proper X)))
(rule (proper (U11 X1 X2 X3)) (U11 (proper X1) (proper X2) (proper X3)))
(rule (proper (U12 X1 X2 X3)) (U12 (proper X1) (proper X2) (proper X3)))
(rule (proper (U111 X)) (U111 (proper X)))
(rule (proper (snd X)) (snd (proper X)))
(rule (proper (splitAt X1 X2)) (splitAt (proper X1) (proper X2)))
(rule (proper (U121 X)) (U121 (proper X)))
(rule (proper (U131 X1 X2)) (U131 (proper X1) (proper X2)))
(rule (proper (U132 X)) (U132 (proper X)))
(rule (proper (U141 X1 X2)) (U141 (proper X1) (proper X2)))
(rule (proper (U142 X)) (U142 (proper X)))
(rule (proper (U151 X1 X2)) (U151 (proper X1) (proper X2)))
(rule (proper (U152 X)) (U152 (proper X)))
(rule (proper (U161 X1 X2)) (U161 (proper X1) (proper X2)))
(rule (proper (cons X1 X2)) (cons (proper X1) (proper X2)))
(rule (proper (natsFrom X)) (natsFrom (proper X)))
(rule (proper (s X)) (s (proper X)))
(rule (proper (U171 X1 X2 X3)) (U171 (proper X1) (proper X2) (proper X3)))
(rule (proper (U172 X1 X2 X3)) (U172 (proper X1) (proper X2) (proper X3)))
(rule (proper (head X)) (head (proper X)))
(rule (proper (afterNth X1 X2)) (afterNth (proper X1) (proper X2)))
(rule (proper (U181 X1 X2)) (U181 (proper X1) (proper X2)))
(rule (proper (U182 X1 X2)) (U182 (proper X1) (proper X2)))
(rule (proper (U191 X1 X2)) (U191 (proper X1) (proper X2)))
(rule (proper (pair X1 X2)) (pair (proper X1) (proper X2)))
(rule (proper nil) (ok nil))
(rule (proper (U201 X1 X2 X3 X4)) (U201 (proper X1) (proper X2) (proper X3) (proper X4)))
(rule (proper (U202 X1 X2 X3 X4)) (U202 (proper X1) (proper X2) (proper X3) (proper X4)))
(rule (proper (isNatural X)) (isNatural (proper X)))
(rule (proper (U203 X1 X2 X3 X4)) (U203 (proper X1) (proper X2) (proper X3) (proper X4)))
(rule (proper (U204 X1 X2)) (U204 (proper X1) (proper X2)))
(rule (proper (U21 X1 X2 X3)) (U21 (proper X1) (proper X2) (proper X3)))
(rule (proper (U22 X1 X2)) (U22 (proper X1) (proper X2)))
(rule (proper (U211 X1 X2)) (U211 (proper X1) (proper X2)))
(rule (proper (U212 X1 X2)) (U212 (proper X1) (proper X2)))
(rule (proper (U221 X1 X2 X3)) (U221 (proper X1) (proper X2) (proper X3)))
(rule (proper (U222 X1 X2 X3)) (U222 (proper X1) (proper X2) (proper X3)))
(rule (proper (fst X)) (fst (proper X)))
(rule (proper (U31 X1 X2 X3)) (U31 (proper X1) (proper X2) (proper X3)))
(rule (proper (U32 X1 X2)) (U32 (proper X1) (proper X2)))
(rule (proper (U41 X1 X2)) (U41 (proper X1) (proper X2)))
(rule (proper (U42 X)) (U42 (proper X)))
(rule (proper (U51 X1 X2)) (U51 (proper X1) (proper X2)))
(rule (proper (U52 X)) (U52 (proper X)))
(rule (proper (U61 X)) (U61 (proper X)))
(rule (proper (U71 X)) (U71 (proper X)))
(rule (proper (U81 X)) (U81 (proper X)))
(rule (proper (U91 X)) (U91 (proper X)))
(rule (proper (isPLNat X)) (isPLNat (proper X)))
(rule (proper (tail X)) (tail (proper X)))
(rule (proper (take X1 X2)) (take (proper X1) (proper X2)))
(rule (proper |0|) (ok |0|))
(rule (proper (sel X1 X2)) (sel (proper X1) (proper X2)))
(rule (U101 (ok X1) (ok X2)) (ok (U101 X1 X2)))
(rule (U102 (ok X)) (ok (U102 X)))
(rule (isLNat (ok X)) (ok (isLNat X)))
(rule (U11 (ok X1) (ok X2) (ok X3)) (ok (U11 X1 X2 X3)))
(rule (U12 (ok X1) (ok X2) (ok X3)) (ok (U12 X1 X2 X3)))
(rule (U111 (ok X)) (ok (U111 X)))
(rule (snd (ok X)) (ok (snd X)))
(rule (splitAt (ok X1) (ok X2)) (ok (splitAt X1 X2)))
(rule (U121 (ok X)) (ok (U121 X)))
(rule (U131 (ok X1) (ok X2)) (ok (U131 X1 X2)))
(rule (U132 (ok X)) (ok (U132 X)))
(rule (U141 (ok X1) (ok X2)) (ok (U141 X1 X2)))
(rule (U142 (ok X)) (ok (U142 X)))
(rule (U151 (ok X1) (ok X2)) (ok (U151 X1 X2)))
(rule (U152 (ok X)) (ok (U152 X)))
(rule (U161 (ok X1) (ok X2)) (ok (U161 X1 X2)))
(rule (cons (ok X1) (ok X2)) (ok (cons X1 X2)))
(rule (natsFrom (ok X)) (ok (natsFrom X)))
(rule (s (ok X)) (ok (s X)))
(rule (U171 (ok X1) (ok X2) (ok X3)) (ok (U171 X1 X2 X3)))
(rule (U172 (ok X1) (ok X2) (ok X3)) (ok (U172 X1 X2 X3)))
(rule (head (ok X)) (ok (head X)))
(rule (afterNth (ok X1) (ok X2)) (ok (afterNth X1 X2)))
(rule (U181 (ok X1) (ok X2)) (ok (U181 X1 X2)))
(rule (U182 (ok X1) (ok X2)) (ok (U182 X1 X2)))
(rule (U191 (ok X1) (ok X2)) (ok (U191 X1 X2)))
(rule (pair (ok X1) (ok X2)) (ok (pair X1 X2)))
(rule (U201 (ok X1) (ok X2) (ok X3) (ok X4)) (ok (U201 X1 X2 X3 X4)))
(rule (U202 (ok X1) (ok X2) (ok X3) (ok X4)) (ok (U202 X1 X2 X3 X4)))
(rule (isNatural (ok X)) (ok (isNatural X)))
(rule (U203 (ok X1) (ok X2) (ok X3) (ok X4)) (ok (U203 X1 X2 X3 X4)))
(rule (U204 (ok X1) (ok X2)) (ok (U204 X1 X2)))
(rule (U21 (ok X1) (ok X2) (ok X3)) (ok (U21 X1 X2 X3)))
(rule (U22 (ok X1) (ok X2)) (ok (U22 X1 X2)))
(rule (U211 (ok X1) (ok X2)) (ok (U211 X1 X2)))
(rule (U212 (ok X1) (ok X2)) (ok (U212 X1 X2)))
(rule (U221 (ok X1) (ok X2) (ok X3)) (ok (U221 X1 X2 X3)))
(rule (U222 (ok X1) (ok X2) (ok X3)) (ok (U222 X1 X2 X3)))
(rule (fst (ok X)) (ok (fst X)))
(rule (U31 (ok X1) (ok X2) (ok X3)) (ok (U31 X1 X2 X3)))
(rule (U32 (ok X1) (ok X2)) (ok (U32 X1 X2)))
(rule (U41 (ok X1) (ok X2)) (ok (U41 X1 X2)))
(rule (U42 (ok X)) (ok (U42 X)))
(rule (U51 (ok X1) (ok X2)) (ok (U51 X1 X2)))
(rule (U52 (ok X)) (ok (U52 X)))
(rule (U61 (ok X)) (ok (U61 X)))
(rule (U71 (ok X)) (ok (U71 X)))
(rule (U81 (ok X)) (ok (U81 X)))
(rule (U91 (ok X)) (ok (U91 X)))
(rule (isPLNat (ok X)) (ok (isPLNat X)))
(rule (tail (ok X)) (ok (tail X)))
(rule (take (ok X1) (ok X2)) (ok (take X1 X2)))
(rule (sel (ok X1) (ok X2)) (ok (sel X1 X2)))
(rule (top (mark X)) (top (proper X)))
(rule (top (ok X)) (top (active X)))