; @origtpdbfilename ./TRS/TRCSR/Ex4_DLMMU04_L.trs
; @xtcfilename "./TRS_Standard/Transformed_CSR_04/Ex4_DLMMU04_L.xml"
(format TRS)
(fun uTake2 1)
(fun tt 0)
(fun cons 1)
(fun uLength 1)
(fun s 1)
(fun length 1)
(fun and 2)
(fun isNatIList 0)
(fun isNatList 0)
(fun isNat 0)
(fun zeros 0)
(fun |0| 0)
(fun take 2)
(fun uTake1 1)
(fun nil 0)
(rule (uTake2 tt) (cons N))
(rule (uLength tt) (s (length L)))
(rule (and tt T) T)
(rule isNatIList isNatList)
(rule isNat tt)
(rule isNat isNat)
(rule isNat isNatList)
(rule isNatIList tt)
(rule isNatIList (and isNat isNatIList))
(rule isNatList tt)
(rule isNatList (and isNat isNatList))
(rule isNatList (and isNat isNatIList))
(rule zeros (cons |0|))
(rule (take |0| IL) (uTake1 isNatIList))
(rule (uTake1 tt) nil)
(rule (take (s M) (cons N)) (uTake2 (and isNat (and isNat isNatIList))))
(rule (length (cons N)) (uLength (and isNat isNatList)))