Merging intuitionistic and irreversible backtracking.

Defining backtracking for Classical and constructive implication. The rules are the same for LCM and constructive implication, with one exception. There is one more kind of move for Eloise, reversible backtracking. Eloise can use reversible backtracking to recover a move retracted by irreversible backtracking (which, strictly speaking, is not ``irreversible'' any more).
To make it short, Eloise can backtrack to any position in the play, but using different kind of backtracking, according to the node. In each case we precise the backtracking used by Eloise, and we distinguish: an intuitionistic backtracking, an irreversible backtracking (a move of LCM games), a reversible backtracking (a move of games with Classical Logic).

View-Trees and Sequent-view are defined as for LCM with constructive implication. In particular:
- nodes available with intuitionistic backtracking have a big dot;
- nodes available with ``irreversible'' backtracking have a branch with thick edges;
- node not available by irreversible backtracking have a branch with thinner edges.
Nodes not available by irreversible backtracking can be recovered by Eloise, using a move with reversible backtracking.

Recovering a retracted node. When Eloise recovers a retracted node i, we also recover, in the view-tree, the assignment of thin/thick branches for nodes <i we had at step i. All nodes >i, instead, are temporarily retracted.

Created by Mathematica  (November 11, 2006)