OAI/Computability/SolenoidalRecorder/Halting.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Terminal recorder checkpoints and initialized halting equivalence.

  1. def OAI.Solenoidal.Recorder.Terminal line 11
  2. theorem OAI.Solenoidal.Recorder.rule_nonterminal line 13
  3. theorem OAI.Solenoidal.Recorder.terminal_no_step line 24
  4. theorem OAI.Solenoidal.Recorder.Steps.head line 31
  5. theorem OAI.Solenoidal.Recorder.Steps.terminal_length_bound line 47
  6. theorem OAI.Solenoidal.Recorder.nonhalting_arbitrarily_long line 69
  7. theorem OAI.Solenoidal.Recorder.halting_iff line 82
  8. theorem OAI.Solenoidal.Recorder.Steps.prefix line 102
  9. theorem OAI.Solenoidal.Recorder.Steps.endpoint_unique line 115
  10. theorem OAI.Solenoidal.Recorder.nonhalting_every_microstep line 127
  11. theorem OAI.Solenoidal.Recorder.nonhalting_execution line 135