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

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Finite little-endian stack codes and the effective support bound for the actual machine's marked tape. The width grows twice as fast as the head.

  1. def OAI.ForcedComputation.Lattice.stackValue line 10
  2. theorem OAI.ForcedComputation.Lattice.stackValue_ext line 14
  3. theorem OAI.ForcedComputation.Lattice.stackValue_zero line 22
  4. theorem OAI.ForcedComputation.Lattice.stackValue_lt line 27
  5. theorem OAI.ForcedComputation.Lattice.stackValue_head line 35
  6. theorem OAI.ForcedComputation.Lattice.stackValue_tail line 39
  7. theorem OAI.ForcedComputation.Lattice.stackValue_add line 43
  8. theorem OAI.ForcedComputation.Lattice.stackValue_extend line 56
  9. def OAI.ForcedComputation.Lattice.configurationWidth line 64
  10. def OAI.ForcedComputation.Lattice.leftDigits line 66
  11. def OAI.ForcedComputation.Lattice.rightDigits line 69
  12. theorem OAI.ForcedComputation.Lattice.configurationWidth_pos line 72
  13. theorem OAI.ForcedComputation.Lattice.configurationWidth_succ line 75
  14. theorem OAI.ForcedComputation.Lattice.marked_tape_outside line 80
  15. theorem OAI.ForcedComputation.Lattice.leftDigits_zero line 86
  16. theorem OAI.ForcedComputation.Lattice.rightDigits_zero line 95
  17. def OAI.ForcedComputation.Lattice.configurationCode line 104
  18. theorem OAI.ForcedComputation.Lattice.configurationCode_lt line 111