; @origtpdbfilename ./TRS/TRCSR/ExSec4_2_DLMMU04_C.trs
; @xtcfilename "./TRS_Standard/Transformed_CSR_04/ExSec4_2_DLMMU04_C.xml"
(format TRS)
(fun active 1)
(fun natsFrom 1)
(fun mark 1)
(fun cons 2)
(fun s 1)
(fun fst 1)
(fun pair 2)
(fun snd 1)
(fun splitAt 2)
(fun |0| 0)
(fun nil 0)
(fun u 4)
(fun head 1)
(fun tail 1)
(fun sel 2)
(fun afterNth 2)
(fun take 2)
(fun proper 1)
(fun ok 1)
(fun top 1)
(rule (active (natsFrom N)) (mark (cons N (natsFrom (s N)))))
(rule (active (fst (pair XS YS))) (mark XS))
(rule (active (snd (pair XS YS))) (mark YS))
(rule (active (splitAt |0| XS)) (mark (pair nil XS)))
(rule (active (splitAt (s N) (cons X XS))) (mark (u (splitAt N XS) N X XS)))
(rule (active (u (pair YS ZS) N X XS)) (mark (pair (cons X YS) ZS)))
(rule (active (head (cons N XS))) (mark N))
(rule (active (tail (cons N XS))) (mark XS))
(rule (active (sel N XS)) (mark (head (afterNth N XS))))
(rule (active (take N XS)) (mark (fst (splitAt N XS))))
(rule (active (afterNth N XS)) (mark (snd (splitAt N XS))))
(rule (active (natsFrom X)) (natsFrom (active X)))
(rule (active (cons X1 X2)) (cons (active X1) X2))
(rule (active (s X)) (s (active X)))
(rule (active (fst X)) (fst (active X)))
(rule (active (pair X1 X2)) (pair (active X1) X2))
(rule (active (pair X1 X2)) (pair X1 (active X2)))
(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 (u X1 X2 X3 X4)) (u (active X1) X2 X3 X4))
(rule (active (head X)) (head (active X)))
(rule (active (tail X)) (tail (active X)))
(rule (active (sel X1 X2)) (sel (active X1) X2))
(rule (active (sel X1 X2)) (sel X1 (active X2)))
(rule (active (afterNth X1 X2)) (afterNth (active X1) X2))
(rule (active (afterNth X1 X2)) (afterNth X1 (active X2)))
(rule (active (take X1 X2)) (take (active X1) X2))
(rule (active (take X1 X2)) (take X1 (active X2)))
(rule (natsFrom (mark X)) (mark (natsFrom X)))
(rule (cons (mark X1) X2) (mark (cons X1 X2)))
(rule (s (mark X)) (mark (s X)))
(rule (fst (mark X)) (mark (fst X)))
(rule (pair (mark X1) X2) (mark (pair X1 X2)))
(rule (pair X1 (mark X2)) (mark (pair X1 X2)))
(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 (u (mark X1) X2 X3 X4) (mark (u X1 X2 X3 X4)))
(rule (head (mark X)) (mark (head X)))
(rule (tail (mark X)) (mark (tail X)))
(rule (sel (mark X1) X2) (mark (sel X1 X2)))
(rule (sel X1 (mark X2)) (mark (sel X1 X2)))
(rule (afterNth (mark X1) X2) (mark (afterNth X1 X2)))
(rule (afterNth X1 (mark X2)) (mark (afterNth X1 X2)))
(rule (take (mark X1) X2) (mark (take X1 X2)))
(rule (take X1 (mark X2)) (mark (take X1 X2)))
(rule (proper (natsFrom X)) (natsFrom (proper X)))
(rule (proper (cons X1 X2)) (cons (proper X1) (proper X2)))
(rule (proper (s X)) (s (proper X)))
(rule (proper (fst X)) (fst (proper X)))
(rule (proper (pair X1 X2)) (pair (proper X1) (proper X2)))
(rule (proper (snd X)) (snd (proper X)))
(rule (proper (splitAt X1 X2)) (splitAt (proper X1) (proper X2)))
(rule (proper |0|) (ok |0|))
(rule (proper nil) (ok nil))
(rule (proper (u X1 X2 X3 X4)) (u (proper X1) (proper X2) (proper X3) (proper X4)))
(rule (proper (head X)) (head (proper X)))
(rule (proper (tail X)) (tail (proper X)))
(rule (proper (sel X1 X2)) (sel (proper X1) (proper X2)))
(rule (proper (afterNth X1 X2)) (afterNth (proper X1) (proper X2)))
(rule (proper (take X1 X2)) (take (proper X1) (proper X2)))
(rule (natsFrom (ok X)) (ok (natsFrom X)))
(rule (cons (ok X1) (ok X2)) (ok (cons X1 X2)))
(rule (s (ok X)) (ok (s X)))
(rule (fst (ok X)) (ok (fst X)))
(rule (pair (ok X1) (ok X2)) (ok (pair X1 X2)))
(rule (snd (ok X)) (ok (snd X)))
(rule (splitAt (ok X1) (ok X2)) (ok (splitAt X1 X2)))
(rule (u (ok X1) (ok X2) (ok X3) (ok X4)) (ok (u X1 X2 X3 X4)))
(rule (head (ok X)) (ok (head X)))
(rule (tail (ok X)) (ok (tail X)))
(rule (sel (ok X1) (ok X2)) (ok (sel X1 X2)))
(rule (afterNth (ok X1) (ok X2)) (ok (afterNth X1 X2)))
(rule (take (ok X1) (ok X2)) (ok (take X1 X2)))
(rule (top (mark X)) (top (proper X)))
(rule (top (ok X)) (top (active X)))