; @origtpdbfilename ./TRS/TRCSR/LISTUTILITIES_nokinds_C.trs
; @xtcfilename "./TRS_Standard/Transformed_CSR_04/LISTUTILITIES_nokinds_C.xml"
(format TRS)
(fun active 1)
(fun U101 3)
(fun tt 0)
(fun mark 1)
(fun fst 1)
(fun splitAt 2)
(fun U11 3)
(fun snd 1)
(fun U21 2)
(fun U31 2)
(fun U41 2)
(fun cons 2)
(fun natsFrom 1)
(fun s 1)
(fun U51 3)
(fun head 1)
(fun afterNth 2)
(fun U61 2)
(fun U71 2)
(fun pair 2)
(fun nil 0)
(fun U81 4)
(fun U82 2)
(fun U91 2)
(fun and 2)
(fun isNatural 1)
(fun isLNat 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 N XS)) (mark (fst (splitAt N XS))))
(rule (active (U11 tt N XS)) (mark (snd (splitAt N XS))))
(rule (active (U21 tt X)) (mark X))
(rule (active (U31 tt N)) (mark N))
(rule (active (U41 tt N)) (mark (cons N (natsFrom (s N)))))
(rule (active (U51 tt N XS)) (mark (head (afterNth N XS))))
(rule (active (U61 tt Y)) (mark Y))
(rule (active (U71 tt XS)) (mark (pair nil XS)))
(rule (active (U81 tt N X XS)) (mark (U82 (splitAt N XS) X)))
(rule (active (U82 (pair YS ZS) X)) (mark (pair (cons X YS) ZS)))
(rule (active (U91 tt XS)) (mark XS))
(rule (active (afterNth N XS)) (mark (U11 (and (isNatural N) (isLNat XS)) N XS)))
(rule (active (and tt X)) (mark X))
(rule (active (fst (pair X Y))) (mark (U21 (and (isLNat X) (isLNat Y)) X)))
(rule (active (head (cons N XS))) (mark (U31 (and (isNatural N) (isLNat XS)) N)))
(rule (active (isLNat nil)) (mark tt))
(rule (active (isLNat (afterNth V1 V2))) (mark (and (isNatural V1) (isLNat V2))))
(rule (active (isLNat (cons V1 V2))) (mark (and (isNatural V1) (isLNat V2))))
(rule (active (isLNat (fst V1))) (mark (isPLNat V1)))
(rule (active (isLNat (natsFrom V1))) (mark (isNatural V1)))
(rule (active (isLNat (snd V1))) (mark (isPLNat V1)))
(rule (active (isLNat (tail V1))) (mark (isLNat V1)))
(rule (active (isLNat (take V1 V2))) (mark (and (isNatural V1) (isLNat V2))))
(rule (active (isNatural |0|)) (mark tt))
(rule (active (isNatural (head V1))) (mark (isLNat V1)))
(rule (active (isNatural (s V1))) (mark (isNatural V1)))
(rule (active (isNatural (sel V1 V2))) (mark (and (isNatural V1) (isLNat V2))))
(rule (active (isPLNat (pair V1 V2))) (mark (and (isLNat V1) (isLNat V2))))
(rule (active (isPLNat (splitAt V1 V2))) (mark (and (isNatural V1) (isLNat V2))))
(rule (active (natsFrom N)) (mark (U41 (isNatural N) N)))
(rule (active (sel N XS)) (mark (U51 (and (isNatural N) (isLNat XS)) N XS)))
(rule (active (snd (pair X Y))) (mark (U61 (and (isLNat X) (isLNat Y)) Y)))
(rule (active (splitAt |0| XS)) (mark (U71 (isLNat XS) XS)))
(rule (active (splitAt (s N) (cons X XS))) (mark (U81 (and (isNatural N) (and (isNatural X) (isLNat XS))) N X XS)))
(rule (active (tail (cons N XS))) (mark (U91 (and (isNatural N) (isLNat XS)) XS)))
(rule (active (take N XS)) (mark (U101 (and (isNatural N) (isLNat XS)) N XS)))
(rule (active (U101 X1 X2 X3)) (U101 (active X1) X2 X3))
(rule (active (fst X)) (fst (active X)))
(rule (active (splitAt X1 X2)) (splitAt (active X1) X2))
(rule (active (splitAt X1 X2)) (splitAt X1 (active X2)))
(rule (active (U11 X1 X2 X3)) (U11 (active X1) X2 X3))
(rule (active (snd X)) (snd (active X)))
(rule (active (U21 X1 X2)) (U21 (active X1) X2))
(rule (active (U31 X1 X2)) (U31 (active X1) X2))
(rule (active (U41 X1 X2)) (U41 (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 (U51 X1 X2 X3)) (U51 (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 (U61 X1 X2)) (U61 (active X1) X2))
(rule (active (U71 X1 X2)) (U71 (active X1) X2))
(rule (active (pair X1 X2)) (pair (active X1) X2))
(rule (active (pair X1 X2)) (pair X1 (active X2)))
(rule (active (U81 X1 X2 X3 X4)) (U81 (active X1) X2 X3 X4))
(rule (active (U82 X1 X2)) (U82 (active X1) X2))
(rule (active (U91 X1 X2)) (U91 (active X1) X2))
(rule (active (and X1 X2)) (and (active X1) X2))
(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 X3) (mark (U101 X1 X2 X3)))
(rule (fst (mark X)) (mark (fst X)))
(rule (splitAt (mark X1) X2) (mark (splitAt X1 X2)))
(rule (splitAt X1 (mark X2)) (mark (splitAt X1 X2)))
(rule (U11 (mark X1) X2 X3) (mark (U11 X1 X2 X3)))
(rule (snd (mark X)) (mark (snd X)))
(rule (U21 (mark X1) X2) (mark (U21 X1 X2)))
(rule (U31 (mark X1) X2) (mark (U31 X1 X2)))
(rule (U41 (mark X1) X2) (mark (U41 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 (U51 (mark X1) X2 X3) (mark (U51 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 (U61 (mark X1) X2) (mark (U61 X1 X2)))
(rule (U71 (mark X1) X2) (mark (U71 X1 X2)))
(rule (pair (mark X1) X2) (mark (pair X1 X2)))
(rule (pair X1 (mark X2)) (mark (pair X1 X2)))
(rule (U81 (mark X1) X2 X3 X4) (mark (U81 X1 X2 X3 X4)))
(rule (U82 (mark X1) X2) (mark (U82 X1 X2)))
(rule (U91 (mark X1) X2) (mark (U91 X1 X2)))
(rule (and (mark X1) X2) (mark (and X1 X2)))
(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 X3)) (U101 (proper X1) (proper X2) (proper X3)))
(rule (proper tt) (ok tt))
(rule (proper (fst X)) (fst (proper X)))
(rule (proper (splitAt X1 X2)) (splitAt (proper X1) (proper X2)))
(rule (proper (U11 X1 X2 X3)) (U11 (proper X1) (proper X2) (proper X3)))
(rule (proper (snd X)) (snd (proper X)))
(rule (proper (U21 X1 X2)) (U21 (proper X1) (proper X2)))
(rule (proper (U31 X1 X2)) (U31 (proper X1) (proper X2)))
(rule (proper (U41 X1 X2)) (U41 (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 (U51 X1 X2 X3)) (U51 (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 (U61 X1 X2)) (U61 (proper X1) (proper X2)))
(rule (proper (U71 X1 X2)) (U71 (proper X1) (proper X2)))
(rule (proper (pair X1 X2)) (pair (proper X1) (proper X2)))
(rule (proper nil) (ok nil))
(rule (proper (U81 X1 X2 X3 X4)) (U81 (proper X1) (proper X2) (proper X3) (proper X4)))
(rule (proper (U82 X1 X2)) (U82 (proper X1) (proper X2)))
(rule (proper (U91 X1 X2)) (U91 (proper X1) (proper X2)))
(rule (proper (and X1 X2)) (and (proper X1) (proper X2)))
(rule (proper (isNatural X)) (isNatural (proper X)))
(rule (proper (isLNat X)) (isLNat (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 X3)) (ok (U101 X1 X2 X3)))
(rule (fst (ok X)) (ok (fst X)))
(rule (splitAt (ok X1) (ok X2)) (ok (splitAt X1 X2)))
(rule (U11 (ok X1) (ok X2) (ok X3)) (ok (U11 X1 X2 X3)))
(rule (snd (ok X)) (ok (snd X)))
(rule (U21 (ok X1) (ok X2)) (ok (U21 X1 X2)))
(rule (U31 (ok X1) (ok X2)) (ok (U31 X1 X2)))
(rule (U41 (ok X1) (ok X2)) (ok (U41 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 (U51 (ok X1) (ok X2) (ok X3)) (ok (U51 X1 X2 X3)))
(rule (head (ok X)) (ok (head X)))
(rule (afterNth (ok X1) (ok X2)) (ok (afterNth X1 X2)))
(rule (U61 (ok X1) (ok X2)) (ok (U61 X1 X2)))
(rule (U71 (ok X1) (ok X2)) (ok (U71 X1 X2)))
(rule (pair (ok X1) (ok X2)) (ok (pair X1 X2)))
(rule (U81 (ok X1) (ok X2) (ok X3) (ok X4)) (ok (U81 X1 X2 X3 X4)))
(rule (U82 (ok X1) (ok X2)) (ok (U82 X1 X2)))
(rule (U91 (ok X1) (ok X2)) (ok (U91 X1 X2)))
(rule (and (ok X1) (ok X2)) (ok (and X1 X2)))
(rule (isNatural (ok X)) (ok (isNatural X)))
(rule (isLNat (ok X)) (ok (isLNat 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)))