OAI/MathematicalPhysics/NavierStokes/ForcedComputation/Flow/PlanarProcessorData.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

The explicitly translated finite rational rectangle table used by the normalized planar processor.

  1. def OAI.ForcedComputation.PlanarRouting.translatedInstruction line 14
  2. theorem OAI.ForcedComputation.PlanarRouting.translatedBox_image line 17
  3. theorem OAI.ForcedComputation.PlanarRouting.translatedInstruction_affine line 29
  4. theorem OAI.ForcedComputation.PlanarRouting.translatedInstruction_image line 37
  5. theorem OAI.ForcedComputation.PlanarRouting.translatedBox_separation line 55
  6. def OAI.ForcedComputation.Recorder.Planar.normalizedInstruction line 73
  7. def OAI.ForcedComputation.Recorder.Planar.normalizedProgram line 78
  8. def OAI.ForcedComputation.Recorder.Planar.normalizedNeighborhood line 81
  9. theorem OAI.ForcedComputation.Recorder.Planar.normalizedInstruction_mem line 86
  10. theorem OAI.ForcedComputation.Recorder.Planar.normalizedInstruction_properties line 93
  11. theorem OAI.ForcedComputation.Recorder.Planar.normalizedInstruction_separation line 105
  12. theorem OAI.ForcedComputation.Recorder.Planar.normalizedInstruction_neighborhood line 115
  13. theorem OAI.ForcedComputation.Recorder.Planar.normalizedInstruction_period line 130
  14. theorem OAI.ForcedComputation.Recorder.Planar.normalizedInstruction_encodes line 141