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