OAI/MathematicalPhysics/NavierStokes/ForcedComputation/Programs/GappedInstructions.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Closed radix rectangles for Section 4 of Finite Instructions and Solenoidal Shear Flows. These statements concern whole intervals and rectangles, not merely the subset consisting of encoded tapes.

  1. def OAI.ForcedComputation.Radix.push line 17
  2. def OAI.ForcedComputation.Radix.pop line 19
  3. def OAI.ForcedComputation.Radix.cylinder line 21
  4. theorem OAI.ForcedComputation.Radix.pop_push line 23
  5. theorem OAI.ForcedComputation.Radix.push_pop line 29
  6. theorem OAI.ForcedComputation.Radix.push_mem_cylinder line 35
  7. theorem OAI.ForcedComputation.Radix.pop_mem_unit line 45
  8. theorem OAI.ForcedComputation.Radix.push_image_unit line 49
  9. theorem OAI.ForcedComputation.Radix.pop_image_cylinder line 58
  10. theorem OAI.ForcedComputation.Radix.cylinder_gap line 63
  11. theorem OAI.ForcedComputation.Radix.nested_cylinder_gap line 72
  12. def OAI.ForcedComputation.Radix.rectangle line 86
  13. def OAI.ForcedComputation.Radix.rightMove line 88
  14. def OAI.ForcedComputation.Radix.stayMove line 91
  15. def OAI.ForcedComputation.Radix.leftMove line 94
  16. theorem OAI.ForcedComputation.Radix.rightMove_image line 97
  17. theorem OAI.ForcedComputation.Radix.stayMove_image line 108
  18. theorem OAI.ForcedComputation.Radix.leftMove_image line 122