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

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

A terminating finite compiler for every prefix of the full address array. It enumerates all guarded wires, independently of the chosen run.

  1. theorem OAI.ForcedComputation.ExpandingDetector.list_sum_range_eq line 14
  2. def OAI.ForcedComputation.ExpandingDetector.rationalRadius line 20
  3. def OAI.ForcedComputation.ExpandingDetector.rationalDuration line 23
  4. def OAI.ForcedComputation.ExpandingDetector.rationalStageStart line 26
  5. theorem OAI.ForcedComputation.ExpandingDetector.rationalRadius_val line 29
  6. theorem OAI.ForcedComputation.ExpandingDetector.rationalDuration_val line 33
  7. theorem OAI.ForcedComputation.ExpandingDetector.rationalStageStart_val line 37
  8. def OAI.ForcedComputation.ExpandingDetector.stageWireOrder line 49
  9. def OAI.ForcedComputation.ExpandingDetector.orderedStageWires line 57
  10. theorem OAI.ForcedComputation.ExpandingDetector.sum_orderedStageWires line 62
  11. def OAI.ForcedComputation.ExpandingDetector.stageCode line 71
  12. theorem OAI.ForcedComputation.ExpandingDetector.stageCode_val line 80
  13. def OAI.ForcedComputation.ExpandingDetector.prefixCode line 96
  14. theorem OAI.ForcedComputation.ExpandingDetector.prefixCode_val line 101