x = h(h(x)+1) is an identity for no h:N→N.
∃x.x≠h(h(x)+1)

In[516]:=

In[517]:=

Out[517]=

This is a simple, non-essential way of using backtracking, just a preliminary example. No matter what h is, the predicate x≠h(h(x)+1) is true either for some x in {h(0), 0, h(h(0)+1)} (we skip the proof). The winning strategy of Eloise consists in selecting the 3 values x=h(0), 0, h(h(0)+1), one after the other. The first time x≠h(h(x)+1) is true, Eloise wins. There are no moves of Abelard in this game. Backtracking allows Eloise to change her move of x. Eloise could by-pass, in this case, the use of backtracking, by computing first what is the right x, then selecting x just once.

Now we choose the parameters of the game and we play. During the play, whenever Eloise backtracks, say, from position 3 to position 1, we draw edges leading to positions 2, 3 thinner. This marks the fact that these position cannot any more be used in the play. Thick edges form the current Tarski play, which, for irreversible backtracking, is always the rightmost branch in the view-tree. In this section, backtracking is irreversible and whenever we backtrack to a position of index i we retract all positions of index >i. In this example, h(x) is the polynomial x*(x-1)

In[518]:=

In[519]:=

Created by Mathematica  (October 20, 2006)