OAI/MathematicalPhysics/NavierStokes/ForcedComputation/Detector/ExpandingRecorderAlphabet.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

A finite executable alphabet for the reversible recorder. The blank is assigned digit zero, so finite integer stacks represent infinite blank tails. All seven guarded instruction rows are retained, including unreachable rows.

  1. def OAI.ForcedComputation.ExpandingDetector.controlCode line 12
  2. theorem OAI.ForcedComputation.ExpandingDetector.controlCode_lt line 15
  3. theorem OAI.ForcedComputation.ExpandingDetector.controlCode_injective line 19
  4. def OAI.ForcedComputation.ExpandingDetector.symbolList line 24
  5. theorem OAI.ForcedComputation.ExpandingDetector.mem_symbolList line 28
  6. def OAI.ForcedComputation.ExpandingDetector.symbolCode line 34
  7. theorem OAI.ForcedComputation.ExpandingDetector.symbolCode_lt line 37
  8. theorem OAI.ForcedComputation.ExpandingDetector.symbolCode_blank line 42
  9. theorem OAI.ForcedComputation.ExpandingDetector.symbolCode_injective line 46
  10. theorem OAI.ForcedComputation.ExpandingDetector.symbolCode_eq_zero line 51
  11. def OAI.ForcedComputation.ExpandingDetector.alphabetBase line 56
  12. theorem OAI.ForcedComputation.ExpandingDetector.alphabetBase_two_le line 59
  13. theorem OAI.ForcedComputation.ExpandingDetector.symbolCode_lt_base line 62
  14. def OAI.ForcedComputation.ExpandingDetector.encodedLocal line 66
  15. theorem OAI.ForcedComputation.ExpandingDetector.encodedLocal_complete line 73
  16. theorem OAI.ForcedComputation.ExpandingDetector.encodedLocal_predecessor_unique line 85