; @origtpdbfilename ./TRS/TRCSR/Ex4_DLMMU04_iGM.trs
; @xtcfilename "./TRS_Standard/Transformed_CSR_04/Ex4_DLMMU04_iGM.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)
(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 (mark (and X1 X2)) (active (and (mark X1) (mark X2))))
(rule (mark tt) (active tt))
(rule (mark (isNatIList X)) (active (isNatIList X)))
(rule (mark (isNatList X)) (active (isNatList X)))
(rule (mark (isNat X)) (active (isNat X)))
(rule (mark |0|) (active |0|))
(rule (mark (s X)) (active (s (mark X))))
(rule (mark (length X)) (active (length (mark X))))
(rule (mark zeros) (active zeros))
(rule (mark (cons X1 X2)) (active (cons (mark X1) X2)))
(rule (mark nil) (active nil))
(rule (mark (take X1 X2)) (active (take (mark X1) (mark X2))))
(rule (mark (uTake1 X)) (active (uTake1 (mark X))))
(rule (mark (uTake2 X1 X2 X3 X4)) (active (uTake2 (mark X1) X2 X3 X4)))
(rule (mark (uLength X1 X2)) (active (uLength (mark X1) X2)))
(rule (and (mark X1) X2) (and X1 X2))
(rule (and X1 (mark X2)) (and X1 X2))
(rule (and (active X1) X2) (and X1 X2))
(rule (and X1 (active X2)) (and X1 X2))
(rule (isNatIList (mark X)) (isNatIList X))
(rule (isNatIList (active X)) (isNatIList X))
(rule (isNatList (mark X)) (isNatList X))
(rule (isNatList (active X)) (isNatList X))
(rule (isNat (mark X)) (isNat X))
(rule (isNat (active X)) (isNat X))
(rule (s (mark X)) (s X))
(rule (s (active X)) (s X))
(rule (length (mark X)) (length X))
(rule (length (active X)) (length X))
(rule (cons (mark X1) X2) (cons X1 X2))
(rule (cons X1 (mark X2)) (cons X1 X2))
(rule (cons (active X1) X2) (cons X1 X2))
(rule (cons X1 (active X2)) (cons X1 X2))
(rule (take (mark X1) X2) (take X1 X2))
(rule (take X1 (mark X2)) (take X1 X2))
(rule (take (active X1) X2) (take X1 X2))
(rule (take X1 (active X2)) (take X1 X2))
(rule (uTake1 (mark X)) (uTake1 X))
(rule (uTake1 (active X)) (uTake1 X))
(rule (uTake2 (mark X1) X2 X3 X4) (uTake2 X1 X2 X3 X4))
(rule (uTake2 X1 (mark X2) X3 X4) (uTake2 X1 X2 X3 X4))
(rule (uTake2 X1 X2 (mark X3) X4) (uTake2 X1 X2 X3 X4))
(rule (uTake2 X1 X2 X3 (mark X4)) (uTake2 X1 X2 X3 X4))
(rule (uTake2 (active X1) X2 X3 X4) (uTake2 X1 X2 X3 X4))
(rule (uTake2 X1 (active X2) X3 X4) (uTake2 X1 X2 X3 X4))
(rule (uTake2 X1 X2 (active X3) X4) (uTake2 X1 X2 X3 X4))
(rule (uTake2 X1 X2 X3 (active X4)) (uTake2 X1 X2 X3 X4))
(rule (uLength (mark X1) X2) (uLength X1 X2))
(rule (uLength X1 (mark X2)) (uLength X1 X2))
(rule (uLength (active X1) X2) (uLength X1 X2))
(rule (uLength X1 (active X2)) (uLength X1 X2))