Lets assume there is pure_2 Prolog with dif/2 and pure_1 Prolog without dif/2. Can we realize Peano apartness for values, i.e. Peano numbers, without using dif/2? Thus lets assume we have Peano apartness like this in pure_2 Prolog:
/* pure_2 Prolog */
neq(X, Y) :- dif(X, Y).
Can we replace neq(X,Y) by a more pure definition, namely from pure_1 Prolog that doesn't use dif/2? So that we have a terminating neq/2 predicate that can decide inequality for Peano numbers? So what would be its definition?
/* pure_1 Prolog */
neq(X, Y) :- ??
Using less from this comment:
less(0, s(_)).
less(s(X), s(Y)) :- less(X, Y).
neq(X, Y) :- less(X, Y); less(Y, X).