OAI/Probability/CriticalZ3/ExplorationInvariant.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CriticalZ3.Coarse.Exploration.after_determined line 14
  2. theorem OAI.CriticalZ3.Coarse.Exploration.markedBad_determined line 24
  3. theorem OAI.CriticalZ3.Coarse.Exploration.advance_determined line 31
  4. theorem OAI.CriticalZ3.Coarse.Exploration.badMass_eq line 38
  5. def OAI.CriticalZ3.Coarse.Exploration.frozenEvent line 47
  6. theorem OAI.CriticalZ3.Coarse.Exploration.frozenEvent_determined line 50
  7. theorem OAI.CriticalZ3.Coarse.Exploration.frozenEvent_probability line 56
  8. theorem OAI.CriticalZ3.Coarse.Exploration.accept_current_iff line 61
  9. theorem OAI.CriticalZ3.Coarse.Exploration.relay_failure line 67
  10. theorem OAI.CriticalZ3.Coarse.Exploration.badMass_bound line 106
  11. theorem OAI.CriticalZ3.Coarse.Exploration.everHit_bound line 172
  12. theorem OAI.CriticalZ3.Coarse.Exploration.advance_processed line 188
  13. theorem OAI.CriticalZ3.Coarse.Exploration.advance_queue line 192
  14. theorem OAI.CriticalZ3.Coarse.Exploration.mem_advance_queue line 197
  15. theorem OAI.CriticalZ3.Coarse.Exploration.processed_advance_mono line 203
  16. theorem OAI.CriticalZ3.Coarse.Exploration.good_advance_mono line 209
  17. theorem OAI.CriticalZ3.Coarse.Exploration.bad_advance_mono line 218
  18. theorem OAI.CriticalZ3.Coarse.Exploration.visited_advance_mono line 227
  19. theorem OAI.CriticalZ3.Coarse.Exploration.new_visited line 244
  20. theorem OAI.CriticalZ3.Coarse.Exploration.accepted_neighbors line 259
  21. structure OAI.CriticalZ3.Coarse.Exploration.Colored line 269
  22. def OAI.CriticalZ3.Coarse.Exploration.Closed line 273
  23. def OAI.CriticalZ3.Coarse.Exploration.Covered line 276
  24. theorem OAI.CriticalZ3.Coarse.Exploration.Colored.good_processed line 279
  25. theorem OAI.CriticalZ3.Coarse.Exploration.Colored.bad_processed line 282
  26. theorem OAI.CriticalZ3.Coarse.Exploration.colored_advance line 285
  27. theorem OAI.CriticalZ3.Coarse.Exploration.closed_advance line 301
  28. theorem OAI.CriticalZ3.Coarse.Exploration.covered_advance line 314
  29. def OAI.CriticalZ3.Coarse.Exploration.run line 329
  30. theorem OAI.CriticalZ3.Coarse.Exploration.run_zero line 333
  31. theorem OAI.CriticalZ3.Coarse.Exploration.run_succ line 336
  32. theorem OAI.CriticalZ3.Coarse.Exploration.run_succ_right line 339
  33. theorem OAI.CriticalZ3.Coarse.Exploration.run_valid line 345
  34. theorem OAI.CriticalZ3.Coarse.Exploration.run_colored line 351
  35. theorem OAI.CriticalZ3.Coarse.Exploration.run_closed line 357
  36. theorem OAI.CriticalZ3.Coarse.Exploration.run_covered line 363
  37. theorem OAI.CriticalZ3.Coarse.Exploration.run_good_mono line 369
  38. theorem OAI.CriticalZ3.Coarse.Exploration.run_bad_mono line 376
  39. theorem OAI.CriticalZ3.Coarse.Exploration.run_empty line 383
  40. def OAI.CriticalZ3.Coarse.Exploration.Good line 389
  41. def OAI.CriticalZ3.Coarse.Exploration.Bad line 391
  42. theorem OAI.CriticalZ3.Coarse.Exploration.initial_good_subset line 394