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

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

The finite lattice lookup table obtained from an actual machine. The least significant bit of every symbol is a read-only origin marker. Missing instructions use the existing normalized extra halting state.

  1. def OAI.ForcedComputation.Lattice.machineBase line 11
  2. theorem OAI.ForcedComputation.Lattice.machineBase_two_le line 14
  3. theorem OAI.ForcedComputation.Lattice.machineBase_symbols line 16
  4. theorem OAI.ForcedComputation.Lattice.machineBase_states line 19
  5. def OAI.ForcedComputation.Lattice.markedDigit line 22
  6. theorem OAI.ForcedComputation.Lattice.markedDigit_symbol line 24
  7. theorem OAI.ForcedComputation.Lattice.markedDigit_bit line 29
  8. theorem OAI.ForcedComputation.Lattice.markedDigit_lt line 32
  9. def OAI.ForcedComputation.Lattice.markedTape line 37
  10. theorem OAI.ForcedComputation.Lattice.markedTape_symbol line 40
  11. theorem OAI.ForcedComputation.Lattice.markedTape_origin line 43
  12. theorem OAI.ForcedComputation.Lattice.markedTape_lt line 48
  13. def OAI.ForcedComputation.Lattice.machineRule line 52
  14. def OAI.ForcedComputation.Lattice.machineTable line 74
  15. theorem OAI.ForcedComputation.Lattice.machineTable_lookup line 79
  16. theorem OAI.ForcedComputation.Lattice.machineTable_halting line 84
  17. theorem OAI.ForcedComputation.Lattice.machineRule_halted line 90
  18. theorem OAI.ForcedComputation.Lattice.machineRule_spec line 99
  19. theorem OAI.ForcedComputation.Lattice.machineRule_preserves_origin line 109