NO 0.08/0.17 NO 0.08/0.17 0.08/0.17 Problem: 0.08/0.17 U11(tt()) -> s(length(L)) 0.08/0.17 and(tt()) -> X 0.08/0.17 zeros() -> cons(0()) 0.08/0.17 isNat() -> tt() 0.08/0.17 isNat() -> isNatList() 0.08/0.17 isNat() -> isNat() 0.08/0.17 isNatIList() -> isNatList() 0.08/0.17 isNatIList() -> tt() 0.08/0.17 isNatIList() -> and(isNat()) 0.08/0.17 isNatList() -> tt() 0.08/0.17 isNatList() -> and(isNat()) 0.08/0.17 length(nil()) -> 0() 0.08/0.17 length(cons(N)) -> U11(and(isNatList())) 0.08/0.17 0.08/0.17 Proof: 0.08/0.17 Fresh Variable Processor: 0.08/0.17 loop length: 1 0.08/0.17 terms: 0.08/0.17 U11(tt()) 0.08/0.17 context: s(length([])) 0.08/0.17 substitution: 0.08/0.17 L -> U11(tt()) 0.08/0.17 Qed 0.08/0.17 EOF