NO 0.07/0.18 NO 0.07/0.18 0.07/0.18 Problem: 0.07/0.18 U62(tt()) -> s(length(L)) 0.07/0.18 zeros() -> cons(0()) 0.07/0.18 U11(tt()) -> tt() 0.07/0.18 U21(tt()) -> tt() 0.07/0.18 U31(tt()) -> tt() 0.07/0.18 U41(tt()) -> U42(isNatIList()) 0.07/0.18 U42(tt()) -> tt() 0.07/0.18 U51(tt()) -> U52(isNatList()) 0.07/0.18 U52(tt()) -> tt() 0.07/0.18 U61(tt()) -> U62(isNat()) 0.07/0.18 isNat() -> tt() 0.07/0.18 isNat() -> U11(isNatList()) 0.07/0.18 isNat() -> U21(isNat()) 0.07/0.18 isNatIList() -> U31(isNatList()) 0.07/0.18 isNatIList() -> tt() 0.07/0.18 isNatIList() -> U41(isNat()) 0.07/0.18 isNatList() -> tt() 0.07/0.18 isNatList() -> U51(isNat()) 0.07/0.18 length(nil()) -> 0() 0.07/0.18 length(cons(N)) -> U61(isNatList()) 0.07/0.18 0.07/0.18 Proof: 0.07/0.18 Fresh Variable Processor: 0.07/0.18 loop length: 1 0.07/0.18 terms: 0.07/0.18 U62(tt()) 0.07/0.18 context: s(length([])) 0.07/0.18 substitution: 0.07/0.18 L -> U62(tt()) 0.07/0.18 Qed 0.07/0.19 EOF