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

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

One complete period of the actual planar processor implements every filled instruction rectangle and, consequently, each encoded machine step.

  1. theorem OAI.ForcedComputation.Recorder.Planar.normalized_branch_planar_in line 14
  2. theorem OAI.ForcedComputation.Recorder.Planar.normalized_branch_planar line 35
  3. theorem OAI.ForcedComputation.Recorder.Planar.normalized_branch_planar_safe line 47
  4. theorem OAI.ForcedComputation.Recorder.Planar.normalized_planar_step line 61