; @origtpdbfilename ./TRS/TRCSR/LengthOfFiniteLists_complete_L.trs
; @xtcfilename "./TRS_Standard/Transformed_CSR_04/LengthOfFiniteLists_complete_L.xml"
(format TRS)
(fun U61 1)
(fun tt 0)
(fun s 1)
(fun length 1)
(fun and 1)
(fun zeros 0)
(fun cons 1)
(fun |0| 0)
(fun U11 1)
(fun U12 1)
(fun isNatList 0)
(fun U21 1)
(fun U22 1)
(fun isNat 0)
(fun U31 1)
(fun U32 1)
(fun U41 1)
(fun U42 1)
(fun U43 1)
(fun isNatIList 0)
(fun U51 1)
(fun U52 1)
(fun U53 1)
(fun isNatIListKind 0)
(fun isNatKind 0)
(fun nil 0)
(rule (U61 tt) (s (length L)))
(rule (and tt) X)
(rule zeros (cons |0|))
(rule (U11 tt) (U12 isNatList))
(rule (U12 tt) tt)
(rule (U21 tt) (U22 isNat))
(rule (U22 tt) tt)
(rule (U31 tt) (U32 isNatList))
(rule (U32 tt) tt)
(rule (U41 tt) (U42 isNat))
(rule (U42 tt) (U43 isNatIList))
(rule (U43 tt) tt)
(rule (U51 tt) (U52 isNat))
(rule (U52 tt) (U53 isNatList))
(rule (U53 tt) tt)
(rule isNat tt)
(rule isNat (U11 isNatIListKind))
(rule isNat (U21 isNatKind))
(rule isNatIList (U31 isNatIListKind))
(rule isNatIList tt)
(rule isNatIList (U41 (and isNatKind)))
(rule isNatIListKind tt)
(rule isNatIListKind (and isNatKind))
(rule isNatKind tt)
(rule isNatKind isNatIListKind)
(rule isNatKind isNatKind)
(rule isNatList tt)
(rule isNatList (U51 (and isNatKind)))
(rule (length nil) |0|)
(rule (length (cons N)) (U61 (and (and isNatList))))