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

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

A fresh initial state, with no incoming machine transition. It performs one stationary step before simulating the supplied machine. This lets a periodically repeated loader occupy an otherwise unused incoming branch.

  1. def OAI.ForcedComputation.shiftInstruction line 12
  2. def OAI.ForcedComputation.freshMachine line 15
  3. abbrev OAI.ForcedComputation.freshInput line 21
  4. theorem OAI.ForcedComputation.freshMachine_stateCount line 23
  5. theorem OAI.ForcedComputation.freshMachine_symbolCount line 26
  6. theorem OAI.ForcedComputation.freshMachine_wellFormed line 29
  7. theorem OAI.ForcedComputation.freshInput_valid line 58
  8. theorem OAI.ForcedComputation.freshInput_wellFormed line 62
  9. theorem OAI.ForcedComputation.freshMachine_not_halting_zero line 66
  10. theorem OAI.ForcedComputation.freshMachine_halting_succ line 70
  11. theorem OAI.ForcedComputation.freshMachine_instruction_zero line 76
  12. theorem OAI.ForcedComputation.freshMachine_instruction_succ line 81
  13. def OAI.ForcedComputation.liftConfiguration line 93
  14. theorem OAI.ForcedComputation.freshMachine_step_lift line 96
  15. theorem OAI.ForcedComputation.freshMachine_initial_step line 107
  16. theorem OAI.ForcedComputation.freshInput_configuration line 118
  17. theorem OAI.ForcedComputation.freshInput_halts_iff line 126
  18. theorem OAI.ForcedComputation.freshMachine_no_incoming line 140