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