; @origtpdbfilename ./TRS/TRCSR/LengthOfFiniteLists_complete-noand_FR.trs
; @xtcfilename "./TRS_Standard/Transformed_CSR_04/LengthOfFiniteLists_complete-noand_FR.xml"
(format TRS)
(fun zeros 0)
(fun cons 2)
(fun |0| 0)
(fun n__zeros 0)
(fun U11 2)
(fun tt 0)
(fun U12 2)
(fun isNatIListKind 1)
(fun activate 1)
(fun U13 1)
(fun isNatList 1)
(fun U21 2)
(fun U22 2)
(fun isNatKind 1)
(fun U23 1)
(fun isNat 1)
(fun U31 2)
(fun U32 2)
(fun U33 1)
(fun U41 3)
(fun U42 3)
(fun U43 3)
(fun U44 3)
(fun U45 2)
(fun U46 1)
(fun isNatIList 1)
(fun U51 2)
(fun U52 1)
(fun U61 1)
(fun U71 1)
(fun U81 3)
(fun U82 3)
(fun U83 3)
(fun U84 3)
(fun U85 2)
(fun U86 1)
(fun U91 3)
(fun U92 3)
(fun U93 3)
(fun U94 2)
(fun s 1)
(fun length 1)
(fun n__0 0)
(fun n__length 1)
(fun n__s 1)
(fun n__cons 2)
(fun n__nil 0)
(fun nil 0)
(rule zeros (cons |0| n__zeros))
(rule (U11 tt V1) (U12 (isNatIListKind (activate V1)) (activate V1)))
(rule (U12 tt V1) (U13 (isNatList (activate V1))))
(rule (U13 tt) tt)
(rule (U21 tt V1) (U22 (isNatKind (activate V1)) (activate V1)))
(rule (U22 tt V1) (U23 (isNat (activate V1))))
(rule (U23 tt) tt)
(rule (U31 tt V) (U32 (isNatIListKind (activate V)) (activate V)))
(rule (U32 tt V) (U33 (isNatList (activate V))))
(rule (U33 tt) tt)
(rule (U41 tt V1 V2) (U42 (isNatKind (activate V1)) (activate V1) (activate V2)))
(rule (U42 tt V1 V2) (U43 (isNatIListKind (activate V2)) (activate V1) (activate V2)))
(rule (U43 tt V1 V2) (U44 (isNatIListKind (activate V2)) (activate V1) (activate V2)))
(rule (U44 tt V1 V2) (U45 (isNat (activate V1)) (activate V2)))
(rule (U45 tt V2) (U46 (isNatIList (activate V2))))
(rule (U46 tt) tt)
(rule (U51 tt V2) (U52 (isNatIListKind (activate V2))))
(rule (U52 tt) tt)
(rule (U61 tt) tt)
(rule (U71 tt) tt)
(rule (U81 tt V1 V2) (U82 (isNatKind (activate V1)) (activate V1) (activate V2)))
(rule (U82 tt V1 V2) (U83 (isNatIListKind (activate V2)) (activate V1) (activate V2)))
(rule (U83 tt V1 V2) (U84 (isNatIListKind (activate V2)) (activate V1) (activate V2)))
(rule (U84 tt V1 V2) (U85 (isNat (activate V1)) (activate V2)))
(rule (U85 tt V2) (U86 (isNatList (activate V2))))
(rule (U86 tt) tt)
(rule (U91 tt L N) (U92 (isNatIListKind (activate L)) (activate L) (activate N)))
(rule (U92 tt L N) (U93 (isNat (activate N)) (activate L) (activate N)))
(rule (U93 tt L N) (U94 (isNatKind (activate N)) (activate L)))
(rule (U94 tt L) (s (length (activate L))))
(rule (isNat n__0) tt)
(rule (isNat (n__length V1)) (U11 (isNatIListKind (activate V1)) (activate V1)))
(rule (isNat (n__s V1)) (U21 (isNatKind (activate V1)) (activate V1)))
(rule (isNatIList V) (U31 (isNatIListKind (activate V)) (activate V)))
(rule (isNatIList n__zeros) tt)
(rule (isNatIList (n__cons V1 V2)) (U41 (isNatKind (activate V1)) (activate V1) (activate V2)))
(rule (isNatIListKind n__nil) tt)
(rule (isNatIListKind n__zeros) tt)
(rule (isNatIListKind (n__cons V1 V2)) (U51 (isNatKind (activate V1)) (activate V2)))
(rule (isNatKind n__0) tt)
(rule (isNatKind (n__length V1)) (U61 (isNatIListKind (activate V1))))
(rule (isNatKind (n__s V1)) (U71 (isNatKind (activate V1))))
(rule (isNatList n__nil) tt)
(rule (isNatList (n__cons V1 V2)) (U81 (isNatKind (activate V1)) (activate V1) (activate V2)))
(rule (length nil) |0|)
(rule (length (cons N L)) (U91 (isNatList (activate L)) (activate L) N))
(rule zeros n__zeros)
(rule |0| n__0)
(rule (length X) (n__length X))
(rule (s X) (n__s X))
(rule (cons X1 X2) (n__cons X1 X2))
(rule nil n__nil)
(rule (activate n__zeros) zeros)
(rule (activate n__0) |0|)
(rule (activate (n__length X)) (length (activate X)))
(rule (activate (n__s X)) (s (activate X)))
(rule (activate (n__cons X1 X2)) (cons (activate X1) X2))
(rule (activate n__nil) nil)
(rule (activate X) X)