; @origtpdbfilename ./TRS/TRCSR/Ex4_DLMMU04_C.trs
; @xtcfilename "./TRS_Standard/Transformed_CSR_04/Ex4_DLMMU04_C.xml"
(format TRS)
(fun active 1)
(fun and 2)
(fun tt 0)
(fun mark 1)
(fun isNatIList 1)
(fun isNatList 1)
(fun isNat 1)
(fun |0| 0)
(fun s 1)
(fun length 1)
(fun zeros 0)
(fun cons 2)
(fun nil 0)
(fun take 2)
(fun uTake1 1)
(fun uTake2 4)
(fun uLength 2)
(fun proper 1)
(fun ok 1)
(fun top 1)
(rule (active (and tt T)) (mark T))
(rule (active (isNatIList IL)) (mark (isNatList IL)))
(rule (active (isNat |0|)) (mark tt))
(rule (active (isNat (s N))) (mark (isNat N)))
(rule (active (isNat (length L))) (mark (isNatList L)))
(rule (active (isNatIList zeros)) (mark tt))
(rule (active (isNatIList (cons N IL))) (mark (and (isNat N) (isNatIList IL))))
(rule (active (isNatList nil)) (mark tt))
(rule (active (isNatList (cons N L))) (mark (and (isNat N) (isNatList L))))
(rule (active (isNatList (take N IL))) (mark (and (isNat N) (isNatIList IL))))
(rule (active zeros) (mark (cons |0| zeros)))
(rule (active (take |0| IL)) (mark (uTake1 (isNatIList IL))))
(rule (active (uTake1 tt)) (mark nil))
(rule (active (take (s M) (cons N IL))) (mark (uTake2 (and (isNat M) (and (isNat N) (isNatIList IL))) M N IL)))
(rule (active (uTake2 tt M N IL)) (mark (cons N (take M IL))))
(rule (active (length (cons N L))) (mark (uLength (and (isNat N) (isNatList L)) L)))
(rule (active (uLength tt L)) (mark (s (length L))))
(rule (active (and X1 X2)) (and (active X1) X2))
(rule (active (and X1 X2)) (and X1 (active X2)))
(rule (active (s X)) (s (active X)))
(rule (active (length X)) (length (active X)))
(rule (active (cons X1 X2)) (cons (active X1) X2))
(rule (active (take X1 X2)) (take (active X1) X2))
(rule (active (take X1 X2)) (take X1 (active X2)))
(rule (active (uTake1 X)) (uTake1 (active X)))
(rule (active (uTake2 X1 X2 X3 X4)) (uTake2 (active X1) X2 X3 X4))
(rule (active (uLength X1 X2)) (uLength (active X1) X2))
(rule (and (mark X1) X2) (mark (and X1 X2)))
(rule (and X1 (mark X2)) (mark (and X1 X2)))
(rule (s (mark X)) (mark (s X)))
(rule (length (mark X)) (mark (length X)))
(rule (cons (mark X1) X2) (mark (cons X1 X2)))
(rule (take (mark X1) X2) (mark (take X1 X2)))
(rule (take X1 (mark X2)) (mark (take X1 X2)))
(rule (uTake1 (mark X)) (mark (uTake1 X)))
(rule (uTake2 (mark X1) X2 X3 X4) (mark (uTake2 X1 X2 X3 X4)))
(rule (uLength (mark X1) X2) (mark (uLength X1 X2)))
(rule (proper (and X1 X2)) (and (proper X1) (proper X2)))
(rule (proper tt) (ok tt))
(rule (proper (isNatIList X)) (isNatIList (proper X)))
(rule (proper (isNatList X)) (isNatList (proper X)))
(rule (proper (isNat X)) (isNat (proper X)))
(rule (proper |0|) (ok |0|))
(rule (proper (s X)) (s (proper X)))
(rule (proper (length X)) (length (proper X)))
(rule (proper zeros) (ok zeros))
(rule (proper (cons X1 X2)) (cons (proper X1) (proper X2)))
(rule (proper nil) (ok nil))
(rule (proper (take X1 X2)) (take (proper X1) (proper X2)))
(rule (proper (uTake1 X)) (uTake1 (proper X)))
(rule (proper (uTake2 X1 X2 X3 X4)) (uTake2 (proper X1) (proper X2) (proper X3) (proper X4)))
(rule (proper (uLength X1 X2)) (uLength (proper X1) (proper X2)))
(rule (and (ok X1) (ok X2)) (ok (and X1 X2)))
(rule (isNatIList (ok X)) (ok (isNatIList X)))
(rule (isNatList (ok X)) (ok (isNatList X)))
(rule (isNat (ok X)) (ok (isNat X)))
(rule (s (ok X)) (ok (s X)))
(rule (length (ok X)) (ok (length X)))
(rule (cons (ok X1) (ok X2)) (ok (cons X1 X2)))
(rule (take (ok X1) (ok X2)) (ok (take X1 X2)))
(rule (uTake1 (ok X)) (ok (uTake1 X)))
(rule (uTake2 (ok X1) (ok X2) (ok X3) (ok X4)) (ok (uTake2 X1 X2 X3 X4)))
(rule (uLength (ok X1) (ok X2)) (ok (uLength X1 X2)))
(rule (top (mark X)) (top (proper X)))
(rule (top (ok X)) (top (active X)))