OAI/Computability/SolenoidalRecorder/Rules.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Full-domain reversible recorder instructions and unique predecessors.

  1. inductive OAI.Solenoidal.Recorder.History line 13
  2. inductive OAI.Solenoidal.Recorder.Control line 17
  3. structure OAI.Solenoidal.Recorder.Letter line 22
  4. inductive OAI.Solenoidal.Recorder.Rule line 30
  5. def OAI.Solenoidal.Recorder.incoming line 48
  6. def OAI.Solenoidal.Recorder.undo line 57
  7. theorem OAI.Solenoidal.Recorder.fixed_incoming line 71
  8. theorem OAI.Solenoidal.Recorder.undo_rule line 75
  9. theorem OAI.Solenoidal.Recorder.local_predecessor_unique line 79
  10. theorem OAI.Solenoidal.Recorder.rule_deterministic line 87
  11. structure OAI.Solenoidal.Recorder.Config line 97
  12. def OAI.Solenoidal.Recorder.successor line 103
  13. def OAI.Solenoidal.Recorder.Step line 106
  14. theorem OAI.Solenoidal.Recorder.step_deterministic line 110
  15. theorem OAI.Solenoidal.Recorder.predecessor_unique line 118