NO 0.08/0.17 NO 0.08/0.18 0.08/0.18 Problem: 0.08/0.18 and(tt()) -> X 0.08/0.18 __(__(X,Y),Z) -> __(X,__(Y,Z)) 0.08/0.18 __(X,nil()) -> X 0.08/0.18 __(nil(),X) -> X 0.08/0.18 isNePal(__(I,__(P,I))) -> tt() 0.08/0.18 0.08/0.18 Proof: 0.08/0.18 Fresh Variable Processor: loop length: 1 0.08/0.18 terms: 0.08/0.18 and(tt()) 0.08/0.18 context: [] 0.08/0.18 substitution: 0.08/0.18 X -> and(tt()) 0.08/0.18 Qed 0.08/0.18 EOF