OAI/MathematicalPhysics/NavierStokes/Material/Machines.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Alternating.configurationAt_zero line 7
  2. theorem OAI.Alternating.configurationAt_succ line 10
  3. theorem OAI.Alternating.Machine.instruction_bounds line 14
  4. def OAI.Alternating.Configuration.ValidFor line 20
  5. theorem OAI.Alternating.initialConfiguration_valid line 23
  6. theorem OAI.Alternating.Machine.step_valid line 34
  7. theorem OAI.Alternating.configurationAt_valid line 49
  8. theorem OAI.Alternating.Machine.step_head_bounds line 55
  9. theorem OAI.Alternating.configurationAt_head_bounds line 68
  10. theorem OAI.Alternating.Machine.step_tape_unchanged line 77
  11. theorem OAI.Alternating.initialConfiguration_tape_outside line 86
  12. theorem OAI.Alternating.configurationAt_tape_outside line 93
  13. theorem OAI.Alternating.Machine.step_of_halted line 105
  14. theorem OAI.Alternating.configurationAt_freezes line 108
  15. theorem OAI.Alternating.neZeroThree line 117
  16. def OAI.Alternating.Machine.normalizedInstruction line 119
  17. def OAI.Alternating.applyInstruction line 124
  18. theorem OAI.Alternating.Machine.step_eq_normalized line 129
  19. theorem OAI.Alternating.Machine.normalizedInstruction_bounds line 138