; @origtpdbfilename ./TRS/TRCSR/LengthOfFiniteLists_nokinds_FR.trs
; @xtcfilename "./TRS_Standard/Transformed_CSR_04/LengthOfFiniteLists_nokinds_FR.xml"
(format TRS)
(fun zeros 0)
(fun cons 2)
(fun |0| 0)
(fun n__zeros 0)
(fun U11 2)
(fun tt 0)
(fun s 1)
(fun length 1)
(fun activate 1)
(fun and 2)
(fun isNat 1)
(fun n__0 0)
(fun n__length 1)
(fun isNatList 1)
(fun n__s 1)
(fun isNatIList 1)
(fun n__cons 2)
(fun n__isNatIList 1)
(fun n__nil 0)
(fun n__isNatList 1)
(fun nil 0)
(fun n__isNat 1)
(rule zeros (cons |0| n__zeros))
(rule (U11 tt L) (s (length (activate L))))
(rule (and tt X) (activate X))
(rule (isNat n__0) tt)
(rule (isNat (n__length V1)) (isNatList (activate V1)))
(rule (isNat (n__s V1)) (isNat (activate V1)))
(rule (isNatIList V) (isNatList (activate V)))
(rule (isNatIList n__zeros) tt)
(rule (isNatIList (n__cons V1 V2)) (and (isNat (activate V1)) (n__isNatIList (activate V2))))
(rule (isNatList n__nil) tt)
(rule (isNatList (n__cons V1 V2)) (and (isNat (activate V1)) (n__isNatList (activate V2))))
(rule (length nil) |0|)
(rule (length (cons N L)) (U11 (and (isNatList (activate L)) (n__isNat N)) (activate L)))
(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 (isNatIList X) (n__isNatIList X))
(rule nil n__nil)
(rule (isNatList X) (n__isNatList X))
(rule (isNat X) (n__isNat X))
(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__isNatIList X)) (isNatIList X))
(rule (activate n__nil) nil)
(rule (activate (n__isNatList X)) (isNatList X))
(rule (activate (n__isNat X)) (isNat X))
(rule (activate X) X)