To begin with an obvious remark: at every vertex, entries and exits must alternate. The difference between the initial vertex and the rest is that at the initial vertex an exit occurs first, whereas at every other vertex an entry occurs first. Hence the following simple but important result, which is essentially due to Tarry:

Theorem 1 Suppose a maze-walking algorithm is such that

(a) No edge is traversed more than once in the same direction.

(b) If on entry to a vertex there are one or more edges that have not yet been used as an exit,
then at least one of them can be used as an exit now.

Then the walk can be forced to stop only at the initial vertex.

Proof Let *V* be a vertex other than the initial vertex and consider entering *V*
for the *n*th time (*n*≥1).
Since *V* is not the initial vertex, *V* has been exited exactly *n*−1 times.
By (a) there are at least *n* edges at *V*. Hence *V* has at least one edge that has not been used as an exit,
and by (b) the walk can continue along one of these. ■

Note that Tarry’s method of marking gives us more information than is actually needed to carry out his algorithm. When we arrive at a vertex, Tarry’s method allows us to distinguish edges that have not been used at all from edges that have been used only to enter that vertex; but we are allowed to exit by an edge of either kind, and therefore do not need to make this distinction. If desired, a simpler method can be used, as follows.

On exit from any vertex, mark the exit edge with a red mark at that vertex only (not at both ends). On arriving at any vertex for the first time, as shown by the absence of any marks, mark the entry edge with a green mark. Now the rule on arriving at any vertex is: exit by an unmarked edge, if there is one; failing that, exit by the edge with the green mark, if there is one; failing that, the walk is over (and you are back at the initial vertex).

On exit from a vertex by the green-marked edge, every edge at that vertex has been traversed twice and the vertex will not be visited again. Thus, if applying the algorithm in a real-life maze, you can now remove all the marks from that vertex. If this is done throughout the walk, then at the end there will be no marks left littering the maze.

Theorem 2 Tarry’s algorithm solves the maze, i.e. at the end of the walk every edge has been walked exactly once in each direction.

Proof By Theorem 1, the walk must end at the initial vertex. Suppose this happens on entering the initial vertex for
the *n*th time. Since this is the initial vertex, we must have exited from it exactly *n* times. Since there are no
more exits, the initial vertex has exactly *n* edges. Hence each edge has been traversed exactly once in each direction.

We now argue as in König, except that his use of contradiction is unnecessary.
Denote by *A*_{1},*A*_{2},…,*A _{k}* the vertices that have been visited when the walk is over, and suppose these are
labelled in the order in which they were first visited,

To show that all vertices of the maze have been visited, let *B* be any vertex.
Since the maze is connected, *B* is joined to the initial vertex by a path *B*_{1}*B*_{2}…*B _{m}*, where

Very little has been written about Trémaux himself, who is remembered only for his maze algorithm. The French Wikipedia has identified him as Charles Pierre Trémaux from Charrecey in Burgundy.

A number of websites have cut-and-pasted a statement that Trémaux’s algorithm uses a line drawn along the floor of the maze. It may be that, under certain conditions, such a procedure is equivalent to Trémaux’s algorithm, but it is not what Trémaux said.

To prove that Trémaux’s algorithm leads to a solution of the maze (i.e. every edge is walked exactly once in each direction), the complicated argument of König seems unnecessary. Since Tarry’s algorithm is easily proved to lead to a solution (see above), it is enough to show that every Trémaux walk is also a Tarry walk. However, Tarry’s Remarque to that effect does not establish this. Tarry makes it an explicit rule that the edge of first entry to a vertex is not used as an exit unless there is no alternative. Trémaux does not make this a rule; it turns out to be true for his algorithm, but it needs to be proved.

Theorem 3 Every walk that follows Trémaux’s rules also follows Tarry’s rules (and therefore solves the maze).

Proof For the most part this is easy to check. If you arrive by a new edge at a vertex that has already been visited,
Trémaux says you must turn back; Tarry does not force this, but it is allowed by his rules since the
edge you are walking is not the edge of *first* entry.
The only tricky part is proving that Trémaux’s algorithm conforms to Tarry’s fundamental rule,
that on arriving at a vertex other than the initial vertex, you do not exit by the edge of first entry unless
there is no alternative. This can be done by proving that certain conditions remain invariant throughout any
Trémaux walk. Namely, we prove that when you are between vertices, i.e. walking some edge of the graph,
the following hold:

(a) If the edge you are now walking has been walked before, then the previous walk was in the opposite direction.

(b) At any vertex except the initial vertex the number of edges with a single mark is either zero or two. If there are two such edges then one was used for the first entry to the vertex, and the other as an exit.

(c) At the initial vertex there is exactly one edge with a single mark, and that edge was used as an exit.

Clearly (a)–(c) are true at the beginning of the walk, i.e. after you have left the initial vertex for the first time and have not yet arrived at any vertex. We need to show that, if (a)–(c) are true, then they remain true after arriving at a vertex and continuing the walk. There are several cases, corresponding to Trémaux’s rules.

Rule 1.1: You arrive by a new edge at a dead end. Then you retreat. Clearly (a) is still true. Also the edge by which you arrived and left has changed from no marks to two, so statements (b) and (c), about edges with a single mark, are not affected. You are leaving by the edge of first entry, but there is no alternative.

Rule 1.2: You arrive by a new edge at a new vertex, which is not a dead end. Since this vertex is not the initial vertex, (c) is not affected. You leave by any edge except the edge by which you entered. This edge has not been walked before, so (a) holds. The entry edge and the exit edge each get a single mark, so (b) holds.

Rule 2: You arrive by a new edge at a vertex that you have previously visited. Then you retreat. (a)–(c) remain true as in Rule 1.1.

Rule 3: You arrive by a previously walked edge at some vertex *V*, which has necessarily been visited before. On
arrival, the edge by which you enter has a single mark (you will add another) and by (a) was previously used to exit
from *V*.

First suppose *V* is not the initial vertex. On arrival you mark the entry edge as always, so it now has two marks.
By (b) *V* also has an edge with a single mark that was used for the first entry to *V*.
If there are unused edges at *V* then you leave *V* by one of these, which gets a single mark, so (b) remains true.
Otherwise you take the edge with a single mark, which now gets a second mark, so that *V* now has no edge with a single
mark and again (b) remains true.
In the second case you are leaving by the edge of first entry, but there is no alternative.
In either case you can continue the walk, and (a)–(c) remain true.

Now suppose *V* is the initial vertex. By (c) the edge by which you arrive is the unique edge at *V* with a single mark,
and it now gets an extra mark. If *V* has unused edges then you exit by one of these and mark it, so that (c) remains
true. Otherwise every edge at *V* now has two marks; there is no exit and the walk is finished.

Thus with Trémaux, as with Tarry, you do not leave a vertex by the edge of first entry unless there is no alternative. ■