; @origtpdbfilename ./TRS/TRCSR/LengthOfFiniteLists_nokinds-noand_L.trs
; @xtcfilename "./TRS_Standard/Transformed_CSR_04/LengthOfFiniteLists_nokinds-noand_L.xml"
(format TRS)
(fun U62 1)
(fun tt 0)
(fun s 1)
(fun length 1)
(fun zeros 0)
(fun cons 1)
(fun |0| 0)
(fun U11 1)
(fun U21 1)
(fun U31 1)
(fun U41 1)
(fun U42 1)
(fun isNatIList 0)
(fun U51 1)
(fun U52 1)
(fun isNatList 0)
(fun U61 1)
(fun isNat 0)
(fun nil 0)
(rule (U62 tt) (s (length L)))
(rule zeros (cons |0|))
(rule (U11 tt) tt)
(rule (U21 tt) tt)
(rule (U31 tt) tt)
(rule (U41 tt) (U42 isNatIList))
(rule (U42 tt) tt)
(rule (U51 tt) (U52 isNatList))
(rule (U52 tt) tt)
(rule (U61 tt) (U62 isNat))
(rule isNat tt)
(rule isNat (U11 isNatList))
(rule isNat (U21 isNat))
(rule isNatIList (U31 isNatList))
(rule isNatIList tt)
(rule isNatIList (U41 isNat))
(rule isNatList tt)
(rule isNatList (U51 isNat))
(rule (length nil) |0|)
(rule (length (cons N)) (U61 isNatList))