OAI/Probability/CriticalPercolation/Exploration/SearchTree.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.CriticalPercolation.SearchTree line 15
  2. def OAI.CriticalPercolation.SearchTree.run line 21
  3. def OAI.CriticalPercolation.SearchTree.reads line 25
  4. def OAI.CriticalPercolation.SearchTree.Valid line 29
  5. lemma OAI.CriticalPercolation.SearchTree.reads_disjoint line 33
  6. lemma OAI.CriticalPercolation.SearchTree.reads_nodup line 47
  7. abbrev OAI.CriticalPercolation.LazyDFS.Dart line 63
  8. structure OAI.CriticalPercolation.LazyDFS.State line 65
  9. def OAI.CriticalPercolation.LazyDFS.State.closed line 69
  10. def OAI.CriticalPercolation.LazyDFS.State.opened line 70
  11. def OAI.CriticalPercolation.LazyDFS.push line 73
  12. lemma OAI.CriticalPercolation.LazyDFS.push_length line 77
  13. def OAI.CriticalPercolation.LazyDFS.compile line 80
  14. lemma OAI.CriticalPercolation.LazyDFS.compile_valid line 93
  15. def OAI.CriticalPercolation.LazyDFS.rank line 113
  16. lemma OAI.CriticalPercolation.LazyDFS.rank_pop line 117
  17. lemma OAI.CriticalPercolation.LazyDFS.rank_closed line 121
  18. lemma OAI.CriticalPercolation.LazyDFS.rank_opened line 124
  19. lemma OAI.CriticalPercolation.LazyDFS.compile_mono line 141