NO 0.08/0.17 NO 0.08/0.17 0.08/0.17 Problem: 0.08/0.17 and(tt()) -> X 0.08/0.17 plus(N,0()) -> N 0.08/0.17 plus(N,s(M)) -> s(plus(N,M)) 0.08/0.17 0.08/0.17 Proof: 0.08/0.17 Fresh Variable Processor: loop length: 1 0.08/0.17 terms: 0.08/0.17 and(tt()) 0.08/0.17 context: [] 0.08/0.17 substitution: 0.08/0.17 X -> and(tt()) 0.08/0.17 Qed 0.08/0.18 EOF