/**
 * A computational strategy for determining whether two values in
 * pred/succ notation are equal.  Based on a solution by Wyatt
 * Gaswick, modified by Sam Rebelsky.
 *
 * Strategy:
 *   (1) "Move" all the modifiers from the first to the second argument.
 *   (2) Treat the two arguments as stacks.
 *     (a) If the top of both stacks is the same, pop 'em.
 *     (b) Otherwise, move values back from right to left.
 */
equals(zero,Y) :- balance(zero,Y).
equals(pred(X),Y) :- equals(X,succ(Y)).
equals(succ(X),Y) :- equals(X,pred(Y)).

/* 0 == 0 */
balance(zero,zero).
/* X-1 == Y-1 iff X = Y */
balance(pred(X),pred(Y)) :- balance(X,Y).
/* X+1 == Y+1 iff X = Y */
balance(succ(X),succ(Y)) :- balance(X,Y).
/* X+1 == Y-1 iff X+2 = Y */
balance(succ(X),pred(Y)) :- balance(succ(succ(X)), Y).
/* X-1 == Y+1 iff X-2 = Y */
balance(pred(X),succ(Y)) :- balance(pred(pred(X)), Y).
/* 0 == Y-1 iff Y == - */
balance(zero,pred(Y)) :- balance(succ(zero), Y).
/* 0 == Y+1 iff Y == -1 */
balance(zero,succ(Y)) :- balance(pred(zero), Y).