OAI/Computability/Interspersed/Rules.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Reversible interspersed-history instruction cylinders.

  1. inductive OAI.PrefixFlows.Interspersed.Control line 13
  2. abbrev OAI.PrefixFlows.Interspersed.Record line 21
  3. abbrev OAI.PrefixFlows.Interspersed.Symbol line 22
  4. abbrev OAI.PrefixFlows.Interspersed.Config line 23
  5. inductive OAI.PrefixFlows.Interspersed.Branch line 28
  6. def OAI.PrefixFlows.Interspersed.source line 38
  7. def OAI.PrefixFlows.Interspersed.target line 48
  8. theorem OAI.PrefixFlows.Interspersed.source_unique line 65
  9. theorem OAI.PrefixFlows.Interspersed.target_unique line 71
  10. def OAI.PrefixFlows.Interspersed.sourceCylinder line 78
  11. def OAI.PrefixFlows.Interspersed.imageCylinder line 82
  12. theorem OAI.PrefixFlows.Interspersed.source_cylinders_disjoint line 86
  13. theorem OAI.PrefixFlows.Interspersed.image_cylinders_disjoint line 92
  14. def OAI.PrefixFlows.Interspersed.Step line 100
  15. theorem OAI.PrefixFlows.Interspersed.Step.of_branch line 103
  16. theorem OAI.PrefixFlows.Interspersed.Step.deterministic line 107
  17. theorem OAI.PrefixFlows.Interspersed.Step.injective line 114
  18. theorem OAI.PrefixFlows.Interspersed.no_step_from_halt line 121