A generic position of the play in tree form.

Drawing a position in tree form. For each position we draw the current node and all previous nodes, numbered as they are in the play. The usual moves of Tarski plays are denoted by edges. Each node and each move has the color of the player it belongs to. The positions Eloise can reach with intuitionistic backtracking (all negative judgement, and the last positive judgement, which are not retracted by a non-intuitionistic backtracking) are dotted by a big dot. The positions Eloise cannot reach with an intuitionistic backtracking are dotted with a small dot. If the position can be recovered by an irreversible backtracking, the edges of its branch are thick. If the position cannot be recovered by an irreversible backtracking, the edges of its branch are thin.The golden ball marks the current position of the play. We call this picture, including all backtracking by Eloise: Eloise's view-tree. The background of the picture is a pale pink, Eloise's color. Here is Eloise's view-tree at step 14 of a play of this subsection.
With respect to a Tarski play, a BCK-play is a tree, not a single branch. A forking in the tree correspond to a move changed by Eloise. The branch leading to the current position of the play (to the golden ball) forms a Tarski play, which we call the current Tarski play.

Recovering a retracted node. When Eloise recovers a retracted node j, we do not just recover a node, the whole play comes back to the state it was in position j. We mark this fact by drawing any edge leading to some position in 1, ..., j thin if it were thin in position j, and thick if it were thick in position j. All edges leading to a position >j, instead, are drawn thinner (they are leading to a retracted node). A single move can change the look of the view-tree deeply, because we can recover an older state of the tree. A single move in these games always adds one node.

The current Tarski play is the only part of the play which matters to Abelard, who cannot backtrack to any previous node. We call the tree form of the current Tarski play Abelard's view-tree. This is a picture of it, at step 14 of the same play. The background is a pale blue, Abelard's color.

View-trees for Eloise and Abelard are asymmetric. The reason is that the notion itself of backtracking game is asymmetric, biased in favor of Eloise.

Created by Mathematica  (November 11, 2006)