; @origtpdbfilename ./TRS/TRCSR/LengthOfFiniteLists_nokinds-noand_FR.trs
; @xtcfilename "./TRS_Standard/Transformed_CSR_04/LengthOfFiniteLists_nokinds-noand_FR.xml"
(format TRS)
(fun zeros 0)
(fun cons 2)
(fun |0| 0)
(fun n__zeros 0)
(fun U11 1)
(fun tt 0)
(fun U21 1)
(fun U31 1)
(fun U41 2)
(fun U42 1)
(fun isNatIList 1)
(fun activate 1)
(fun U51 2)
(fun U52 1)
(fun isNatList 1)
(fun U61 3)
(fun U62 2)
(fun isNat 1)
(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) tt)
(rule (U21 tt) tt)
(rule (U31 tt) tt)
(rule (U41 tt V2) (U42 (isNatIList (activate V2))))
(rule (U42 tt) tt)
(rule (U51 tt V2) (U52 (isNatList (activate V2))))
(rule (U52 tt) tt)
(rule (U61 tt L N) (U62 (isNat (activate N)) (activate L)))
(rule (U62 tt L) (s (length (activate L))))
(rule (isNat n__0) tt)
(rule (isNat (n__length V1)) (U11 (isNatList (activate V1))))
(rule (isNat (n__s V1)) (U21 (isNat (activate V1))))
(rule (isNatIList V) (U31 (isNatList (activate V))))
(rule (isNatIList n__zeros) tt)
(rule (isNatIList (n__cons V1 V2)) (U41 (isNat (activate V1)) (activate V2)))
(rule (isNatList n__nil) tt)
(rule (isNatList (n__cons V1 V2)) (U51 (isNat (activate V1)) (activate V2)))
(rule (length nil) |0|)
(rule (length (cons N L)) (U61 (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)