Below is an informal and formal description of three axioms, a theorem, and a graphical representation of these.
Axiom 1. 4 turns leave the robot in the same position facing the same direction. Formally, $\forall x~turn(turn(turn(turn(x))))= x$.
Axiom 2. 4 moves interleaved with 4 turns leave the robot in the same position. Goes around a block in a counter clockwise direction. Formally, $\forall x~ turn(move(turn(move(turn(move(turn(move(x)))))))) = x$
Axiom 3. A move followed by two turns, then a move and two turns. Goes to next intersection turns around come back and turn twice to face in the original direction. Formally, $\forall x~ turn(turn(move(turn(turn(move(x)))))) = x$.
Theorem. Going clockwise half way around the block will leave the robot in the same position and orientation as going anticlockwise and then making three turns. Note turns are anti-clockwise only. Formally, $\forall x ~ move(turn(turn(turn(move(turn(x)))))) = turn(turn(turn(move(turn(move(x))))))$
The diagrams represent concrete examples with most of the turns omitted. The outer square represents a part of a grid on which the robot can move. The inner lines represent actual turns and moves, they could be have been drawn with any start/finish positions.
Below is a Fitch Style Proof of the theorem based on that from a previous post. Lines 1,2, and 3 are the assumptions or axioms, same as the Prover9 assumptions from previous post. The goal or theorem to be proved is: $\forall x~ move(turn(turn(turn(move (turn(x)))))) = turn (turn (turn (move (turn (move(x))))))$. The axioms and goal were written in Prover9 as:
all p turn(turn( turn( turn(p)))) = p .
all p (turn( move( turn( move( turn( move( turn( move(p)))))))) = p) .
all p (turn( turn( move( turn( turn( move( p)))))) = p) .
Goal
all p (turn(turn(turn(move(turn(move(p)))))) = move(turn(turn(turn(move(turn(p))))))) .
I used the Fitch proof checker to write a first order proof below, I abbreviated $turn$ to $t$ and $move$ to $m$.
Fitch Style Proof
The Fitch Style Proof represents my effort to translated the output of the Prover9 proof from a previous post. The theorem appears intuitively obvious from the diagram, where one has a global view, but I found it very difficult to derive the formal proof from the axioms. Using equational reasoning, it seems to me at least the following tactics could be used:
1) If $a=b$ then we can deduce $f(a)=f(b)$, where $f,a,b$ are legal combinations of $turn$ and $move$.
2) If we have $f(x)$, where $f$ is a legal combination of $turn$ and $move$, we can substitute any of the axioms for $x$
My questions are:
Could human intuition be used in the proof to help make it easier to understand?
Can other proof tactics be applied?
What heuristics can be used?
Can this proof be simplified to make it more understandable?
What seems intuitively obvious seems to require a very complex and verbose proof. Is this just the way it is or can one do better?
This may not be at all what you are looking for, but it's equivalent to showing that $MT^3MT=T^3MTM$ for a (nonabelian) group for which all you know is that $T^4=(TM)^4=(T^2M)^2=I$ (the identity element). The essential steps, as they'd be written in a standard group-theory proof, are
$$\begin{align} MT^3MT &=MT^3MT(TM)^4&\text{(since }(TM)^4=I)\\ &=MT(T^2M)^2(TM)^3&\text{(rearranging parentheses)}\\ &=MT(TM)^3&\text{(since }(T^2M)^2=I)\\ &=(T^4)MT(TM)^3&\text{(since }T^4=I)\\ &=T^2(T^2M)^2(TM)^2&\text{(rearranging parentheses)}\\ &=T^2(TM)^2&\text{(since }(T^2M)^2=I)\\ &=T^3MTM&\text{(rearranging parentheses)} \end{align}$$