OAI/Computability/MatchingCount/ResidualSearch.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.BinaryMatching.ResidualSearch.Table line 10
  2. def OAI.BinaryMatching.ResidualSearch.initial line 12
  3. def OAI.BinaryMatching.ResidualSearch.predecessor line 14
  4. def OAI.BinaryMatching.ResidualSearch.step line 18
  5. def OAI.BinaryMatching.ResidualSearch.search line 25
  6. def OAI.BinaryMatching.ResidualSearch.reached line 29
  7. def OAI.BinaryMatching.ResidualSearch.Closed line 31
  8. structure OAI.BinaryMatching.ResidualSearch.Good line 34
  9. lemma OAI.BinaryMatching.ResidualSearch.mem_reached line 41
  10. lemma OAI.BinaryMatching.ResidualSearch.predecessor_some line 44
  11. lemma OAI.BinaryMatching.ResidualSearch.predecessor_exists line 50
  12. lemma OAI.BinaryMatching.ResidualSearch.step_old line 55
  13. lemma OAI.BinaryMatching.ResidualSearch.step_some line 59
  14. lemma OAI.BinaryMatching.ResidualSearch.step_reached line 75
  15. lemma OAI.BinaryMatching.ResidualSearch.reached_mono line 96
  16. lemma OAI.BinaryMatching.ResidualSearch.good_initial line 99
  17. lemma OAI.BinaryMatching.ResidualSearch.good_step line 110
  18. lemma OAI.BinaryMatching.ResidualSearch.good_search line 148
  19. lemma OAI.BinaryMatching.ResidualSearch.closed_step_eq line 154
  20. lemma OAI.BinaryMatching.ResidualSearch.closed_step line 164
  21. lemma OAI.BinaryMatching.ResidualSearch.card_increases line 169
  22. lemma OAI.BinaryMatching.ResidualSearch.closed_or_card line 180
  23. lemma OAI.BinaryMatching.ResidualSearch.search_closed line 198
  24. lemma OAI.BinaryMatching.ResidualSearch.source_reached line 206
  25. lemma OAI.BinaryMatching.ResidualSearch.search_path line 212
  26. lemma OAI.BinaryMatching.ResidualSearch.search_no_path line 219