; @origtpdbfilename ./TRS/TRCSR/LengthOfFiniteLists_complete-noand_L.trs
; @xtcfilename "./TRS_Standard/Transformed_CSR_04/LengthOfFiniteLists_complete-noand_L.xml"
(format TRS)
(fun U94 1)
(fun tt 0)
(fun s 1)
(fun length 1)
(fun zeros 0)
(fun cons 1)
(fun |0| 0)
(fun U11 1)
(fun U12 1)
(fun isNatIListKind 0)
(fun U13 1)
(fun isNatList 0)
(fun U21 1)
(fun U22 1)
(fun isNatKind 0)
(fun U23 1)
(fun isNat 0)
(fun U31 1)
(fun U32 1)
(fun U33 1)
(fun U41 1)
(fun U42 1)
(fun U43 1)
(fun U44 1)
(fun U45 1)
(fun U46 1)
(fun isNatIList 0)
(fun U51 1)
(fun U52 1)
(fun U61 1)
(fun U71 1)
(fun U81 1)
(fun U82 1)
(fun U83 1)
(fun U84 1)
(fun U85 1)
(fun U86 1)
(fun U91 1)
(fun U92 1)
(fun U93 1)
(fun nil 0)
(rule (U94 tt) (s (length L)))
(rule zeros (cons |0|))
(rule (U11 tt) (U12 isNatIListKind))
(rule (U12 tt) (U13 isNatList))
(rule (U13 tt) tt)
(rule (U21 tt) (U22 isNatKind))
(rule (U22 tt) (U23 isNat))
(rule (U23 tt) tt)
(rule (U31 tt) (U32 isNatIListKind))
(rule (U32 tt) (U33 isNatList))
(rule (U33 tt) tt)
(rule (U41 tt) (U42 isNatKind))
(rule (U42 tt) (U43 isNatIListKind))
(rule (U43 tt) (U44 isNatIListKind))
(rule (U44 tt) (U45 isNat))
(rule (U45 tt) (U46 isNatIList))
(rule (U46 tt) tt)
(rule (U51 tt) (U52 isNatIListKind))
(rule (U52 tt) tt)
(rule (U61 tt) tt)
(rule (U71 tt) tt)
(rule (U81 tt) (U82 isNatKind))
(rule (U82 tt) (U83 isNatIListKind))
(rule (U83 tt) (U84 isNatIListKind))
(rule (U84 tt) (U85 isNat))
(rule (U85 tt) (U86 isNatList))
(rule (U86 tt) tt)
(rule (U91 tt) (U92 isNatIListKind))
(rule (U92 tt) (U93 isNat))
(rule (U93 tt) (U94 isNatKind))
(rule isNat tt)
(rule isNat (U11 isNatIListKind))
(rule isNat (U21 isNatKind))
(rule isNatIList (U31 isNatIListKind))
(rule isNatIList tt)
(rule isNatIList (U41 isNatKind))
(rule isNatIListKind tt)
(rule isNatIListKind (U51 isNatKind))
(rule isNatKind tt)
(rule isNatKind (U61 isNatIListKind))
(rule isNatKind (U71 isNatKind))
(rule isNatList tt)
(rule isNatList (U81 isNatKind))
(rule (length nil) |0|)
(rule (length (cons N)) (U91 isNatList))