OAI/MathematicalPhysics/AlternatingFlow/Detector.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.AlternatingNS.Detector.increment line 12
  2. def OAI.AlternatingNS.Detector.signal line 15
  3. def OAI.AlternatingNS.Detector.during line 19
  4. def OAI.AlternatingNS.Detector.loading line 22
  5. lemma OAI.AlternatingNS.Detector.signal_formula line 24
  6. lemma OAI.AlternatingNS.Detector.signal_before_halt line 33
  7. lemma OAI.AlternatingNS.Detector.signal_first_halt line 43
  8. lemma OAI.AlternatingNS.Detector.increment_nonneg line 50
  9. lemma OAI.AlternatingNS.Detector.increment_le line 58
  10. lemma OAI.AlternatingNS.Detector.signal_monotone line 64
  11. lemma OAI.AlternatingNS.Detector.during_zero line 70
  12. lemma OAI.AlternatingNS.Detector.during_one line 73
  13. lemma OAI.AlternatingNS.Detector.during_before_halt line 76
  14. lemma OAI.AlternatingNS.Detector.loading_negative line 87
  15. lemma OAI.AlternatingNS.Detector.scalar_reachability line 96
  16. lemma OAI.AlternatingNS.Detector.signal_upper_bound line 115
  17. lemma OAI.AlternatingNS.Detector.signal_in_plateau line 129
  18. lemma OAI.AlternatingNS.Detector.during_in_plateau line 138
  19. lemma OAI.AlternatingNS.Detector.machine_scalar_reachability line 150