OAI/MathematicalPhysics/NavierStokes/ForcedComputation/Programs/TapeCoordinates.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Symbolic tape updates give the closed-rectangle affine maps

The first stream lists cells to the left of the head, nearest first; the second starts at the current cell. The three formulas include writing the new symbol before moving the head.

  1. abbrev OAI.ForcedComputation.Radix.Tape line 20
  2. def OAI.ForcedComputation.Radix.coordinates line 22
  3. def OAI.ForcedComputation.Radix.writeRight line 25
  4. def OAI.ForcedComputation.Radix.writeStay line 28
  5. def OAI.ForcedComputation.Radix.writeLeft line 31
  6. theorem OAI.ForcedComputation.Radix.encode_pop line 34
  7. theorem OAI.ForcedComputation.Radix.coordinates_right line 40
  8. theorem OAI.ForcedComputation.Radix.coordinates_stay line 48
  9. theorem OAI.ForcedComputation.Radix.coordinates_left line 60
  10. theorem OAI.ForcedComputation.Radix.coordinates_mem_rectangle line 74