As I wrote in Local FAN-IN eliminates global FAN-OUT (I) , the introduction of the three moves (FAN-IN and the two DIST moves) eliminates global FAN-OUT from the lambda calculus sector of the graphic lambda calculus. In this post we shall see that we can safely eliminate other two moves, namely R1a, R1b, as well as improving the behaviour of the crossings from the -TANGLE sector.
The equilibrium is thus established: three new moves instead of the three old moves. And there are some unexpected advantages.
- (a) The moves local pruning, DIST, graphic beta move, CO-COMM imply the move R1a.
- (b) Conversely, the moves R1a and FAN-IN imply CO-COMM.
- (c) The move FAN-IN and the elimination of loops implies R1b.
Proof. (a) Done in the following picture.
The proof of (b) is here:
Finally, here is the proof of (c):
The -TANGLE sector of the graphic lambda calculus is obtained by using the lambda-crossing macros
In Theorem 6.3 arXiv:1305.5786 [cs.LO] I proved that all the oriented Reidemeister moves (with the crossings replaced by the respective macros), with the exception of the moves R2c, R2d, R3a and R3h, can be proved by using the graphic beta move and elimination of loops. We can improve the theorem in the following way.
Theorem. By using the graphic beta move, elimination of loops, FAN-IN and CO-COMM, we can prove all the 16 oriented Reidemeister moves.
Proof. The missing moves R2c, R2d, R3a and R3h are all equivalent (by using the graphic beta move and elimination of loops, see this question/answer at mathoverflow) with the following switching move, which we can prove with FAN-IN and CO-COMM:
The proof is done.