OAI/Probability/CriticalZ3/ExplorationConnectivity.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CriticalZ3.LatticeGraph.Subgraph.containsBox line 13
  2. theorem OAI.CriticalZ3.LatticeGraph.seedReaches_witness line 17
  3. def OAI.CriticalZ3.Coarse.facingFace line 41
  4. theorem OAI.CriticalZ3.Coarse.facing_neighbor line 44
  5. def OAI.CriticalZ3.Coarse.rootPacket line 79
  6. def OAI.CriticalZ3.Coarse.initial line 86
  7. theorem OAI.CriticalZ3.Coarse.root_internal_disjoint line 93
  8. theorem OAI.CriticalZ3.Coarse.initial_seed_event line 104
  9. theorem OAI.CriticalZ3.Coarse.initial_promise line 139
  10. theorem OAI.CriticalZ3.Coarse.mem_initial_queue line 160
  11. theorem OAI.CriticalZ3.Coarse.initial_valid line 164
  12. theorem OAI.CriticalZ3.Coarse.initial_colored line 190
  13. theorem OAI.CriticalZ3.Coarse.initial_closed line 195
  14. theorem OAI.CriticalZ3.Coarse.initial_covered line 203