OAI/MathematicalPhysics/NavierStokes/BalancedTransport/MachineHalting.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BalancedTransport.Recorder.Checkpoint.coded_halting_iff line 8
  2. def OAI.BalancedTransport.FiniteMachine.normalized line 25
  3. abbrev OAI.BalancedTransport.FiniteMachine.WorkConfiguration line 35
  4. def OAI.BalancedTransport.FiniteMachine.initialWork line 38
  5. def OAI.BalancedTransport.TapeConfiguration.advance line 47
  6. structure OAI.BalancedTransport.FiniteMachine.Represents line 61
  7. theorem OAI.BalancedTransport.FiniteMachine.initialWork_represents line 67
  8. theorem OAI.BalancedTransport.FiniteMachine.Represents.advance line 91
  9. theorem OAI.BalancedTransport.FiniteMachine.Represents.stop line 185
  10. theorem OAI.BalancedTransport.Recorder.Checkpoint.next_state line 197
  11. theorem OAI.BalancedTransport.FiniteMachine.lift_step line 211
  12. theorem OAI.BalancedTransport.FiniteMachine.lift_execution line 233
  13. theorem OAI.BalancedTransport.FiniteMachine.lift_halt line 245
  14. def OAI.BalancedTransport.FiniteMachine.Corresponds line 259
  15. theorem OAI.BalancedTransport.FiniteMachine.reflect_step line 264
  16. theorem OAI.BalancedTransport.FiniteMachine.reflect_execution line 285
  17. theorem OAI.BalancedTransport.FiniteMachine.normalized_halting_iff line 297
  18. theorem OAI.BalancedTransport.FiniteMachine.discrete_compiled_halting_iff line 315