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

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

Explicit indices of each extraction, scaling, and insertion pulse. These are arithmetic indices into the actual compiled list, not choice functions.

  1. def OAI.ForcedComputation.PlanarRouting.blocks line 12
  2. theorem OAI.ForcedComputation.PlanarRouting.blocks_length line 15
  3. theorem OAI.ForcedComputation.PlanarRouting.block_index_lt line 24
  4. theorem OAI.ForcedComputation.PlanarRouting.blocks_get line 30
  5. theorem OAI.ForcedComputation.PlanarRouting.append_three_left line 49
  6. theorem OAI.ForcedComputation.PlanarRouting.append_three_middle line 54
  7. theorem OAI.ForcedComputation.PlanarRouting.append_three_right line 60
  8. instance OAI.ForcedComputation.Recorder.Planar.(instance at line 72) line 72
  9. def OAI.ForcedComputation.Recorder.Planar.extractionBlock line 83
  10. def OAI.ForcedComputation.Recorder.Planar.scalingBlock line 87
  11. def OAI.ForcedComputation.Recorder.Planar.insertionBlock line 90
  12. theorem OAI.ForcedComputation.Recorder.Planar.actions_eq_blocks line 94
  13. theorem OAI.ForcedComputation.Recorder.Planar.actions_length line 98
  14. def OAI.ForcedComputation.Recorder.Planar.sourceRank line 105
  15. def OAI.ForcedComputation.Recorder.Planar.targetRank line 109
  16. theorem OAI.ForcedComputation.Recorder.Planar.sourceRank_get line 113
  17. theorem OAI.ForcedComputation.Recorder.Planar.targetRank_get line 117
  18. def OAI.ForcedComputation.Recorder.Planar.Action.index line 121
  19. theorem OAI.ForcedComputation.Recorder.Planar.Action.index_lt line 130
  20. def OAI.ForcedComputation.Recorder.Planar.extractionIndex line 142
  21. def OAI.ForcedComputation.Recorder.Planar.scalingIndex line 151
  22. def OAI.ForcedComputation.Recorder.Planar.insertionIndex line 159
  23. theorem OAI.ForcedComputation.Recorder.Planar.extractionIndex_get line 168
  24. theorem OAI.ForcedComputation.Recorder.Planar.scalingIndex_get line 181
  25. theorem OAI.ForcedComputation.Recorder.Planar.insertionIndex_get line 195