OAI/Probability/CriticalPercolation/Exploration/State.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.CriticalPercolation.ExactExposure.State line 25
  2. def OAI.CriticalPercolation.ExactExposure.eligible line 29
  3. def OAI.CriticalPercolation.ExactExposure.closed line 32
  4. def OAI.CriticalPercolation.ExactExposure.opened line 35
  5. def OAI.CriticalPercolation.ExactExposure.compile line 38
  6. lemma OAI.CriticalPercolation.ExactExposure.eligible_succ line 46
  7. lemma OAI.CriticalPercolation.ExactExposure.compile_valid line 49
  8. lemma OAI.CriticalPercolation.ExactExposure.edge_reachable line 60
  9. def OAI.CriticalPercolation.ExactExposure.Consistent line 68
  10. def OAI.CriticalPercolation.ExactExposure.Sound line 71
  11. lemma OAI.CriticalPercolation.ExactExposure.consistent_closed line 75
  12. lemma OAI.CriticalPercolation.ExactExposure.consistent_opened line 82
  13. lemma OAI.CriticalPercolation.ExactExposure.sound_opened line 89
  14. lemma OAI.CriticalPercolation.ExactExposure.compile_invariants line 99
  15. lemma OAI.CriticalPercolation.ExactExposure.compile_read line 119
  16. lemma OAI.CriticalPercolation.ExactExposure.compile_exhausted line 139
  17. lemma OAI.CriticalPercolation.ExactExposure.compile_reads_incident line 163