NO 0.08/0.18 NO 0.08/0.18 0.08/0.18 Problem: 0.08/0.18 U12(tt()) -> s(length(L)) 0.08/0.18 U23(tt()) -> cons(N) 0.08/0.18 zeros() -> cons(0()) 0.08/0.18 U11(tt()) -> U12(tt()) 0.08/0.18 U21(tt()) -> U22(tt()) 0.08/0.18 U22(tt()) -> U23(tt()) 0.08/0.18 length(nil()) -> 0() 0.08/0.18 length(cons(N)) -> U11(tt()) 0.08/0.18 take(0(),IL) -> nil() 0.08/0.18 take(s(M),cons(N)) -> U21(tt()) 0.08/0.18 0.08/0.18 Proof: 0.08/0.18 Fresh Variable Processor: 0.08/0.18 loop length: 1 0.08/0.18 terms: 0.08/0.18 U12(tt()) 0.08/0.18 context: s(length([])) 0.08/0.18 substitution: 0.08/0.18 L -> U12(tt()) 0.08/0.18 Qed 0.08/0.18 EOF