; @origtpdbfilename ./TRS/TRCSR/Ex4_DLMMU04_FR.trs
; @xtcfilename "./TRS_Standard/Transformed_CSR_04/Ex4_DLMMU04_FR.xml"
(format TRS)
(fun and 2)
(fun tt 0)
(fun isNatIList 1)
(fun isNatList 1)
(fun activate 1)
(fun isNat 1)
(fun n__0 0)
(fun n__s 1)
(fun n__length 1)
(fun n__zeros 0)
(fun n__cons 2)
(fun n__nil 0)
(fun n__take 2)
(fun zeros 0)
(fun cons 2)
(fun |0| 0)
(fun take 2)
(fun uTake1 1)
(fun nil 0)
(fun s 1)
(fun uTake2 4)
(fun length 1)
(fun uLength 2)
(rule (and tt T) T)
(rule (isNatIList IL) (isNatList (activate IL)))
(rule (isNat n__0) tt)
(rule (isNat (n__s N)) (isNat (activate N)))
(rule (isNat (n__length L)) (isNatList (activate L)))
(rule (isNatIList n__zeros) tt)
(rule (isNatIList (n__cons N IL)) (and (isNat (activate N)) (isNatIList (activate IL))))
(rule (isNatList n__nil) tt)
(rule (isNatList (n__cons N L)) (and (isNat (activate N)) (isNatList (activate L))))
(rule (isNatList (n__take N IL)) (and (isNat (activate N)) (isNatIList (activate IL))))
(rule zeros (cons |0| n__zeros))
(rule (take |0| IL) (uTake1 (isNatIList IL)))
(rule (uTake1 tt) nil)
(rule (take (s M) (cons N IL)) (uTake2 (and (isNat M) (and (isNat N) (isNatIList (activate IL)))) M N (activate IL)))
(rule (uTake2 tt M N IL) (cons (activate N) (n__take (activate M) (activate IL))))
(rule (length (cons N L)) (uLength (and (isNat N) (isNatList (activate L))) (activate L)))
(rule (uLength tt L) (s (length (activate L))))
(rule |0| n__0)
(rule (s X) (n__s X))
(rule (length X) (n__length X))
(rule zeros n__zeros)
(rule (cons X1 X2) (n__cons X1 X2))
(rule nil n__nil)
(rule (take X1 X2) (n__take X1 X2))
(rule (activate n__0) |0|)
(rule (activate (n__s X)) (s (activate X)))
(rule (activate (n__length X)) (length (activate X)))
(rule (activate n__zeros) zeros)
(rule (activate (n__cons X1 X2)) (cons (activate X1) X2))
(rule (activate n__nil) nil)
(rule (activate (n__take X1 X2)) (take (activate X1) (activate X2)))
(rule (activate X) X)