(VAR I P X Y Z ) (RULES and(tt) -> X __(__(X, Y), Z) -> __(X, __(Y, Z)) __(X, nil) -> X __(nil, X) -> X isNePal(__(I, __(P, I))) -> tt )