OAI/Computability/MatchingCount/DenseOracle.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.BinaryMatching.DenseOracle.Matrix line 11
  2. def OAI.BinaryMatching.DenseOracle.make line 13
  3. def OAI.BinaryMatching.DenseOracle.view line 16
  4. lemma OAI.BinaryMatching.DenseOracle.view_make line 18
  5. abbrev OAI.BinaryMatching.DenseOracle.Paths line 21
  6. def OAI.BinaryMatching.DenseOracle.pathView line 23
  7. def OAI.BinaryMatching.DenseOracle.pathInitial line 25
  8. def OAI.BinaryMatching.DenseOracle.pathStep line 27
  9. def OAI.BinaryMatching.DenseOracle.search line 30
  10. lemma OAI.BinaryMatching.DenseOracle.pathView_ofFn line 34
  11. lemma OAI.BinaryMatching.DenseOracle.search_view line 37
  12. def OAI.BinaryMatching.DenseOracle.augment line 43
  13. def OAI.BinaryMatching.DenseOracle.iterate line 48
  14. lemma OAI.BinaryMatching.DenseOracle.augment_view line 52
  15. lemma OAI.BinaryMatching.DenseOracle.iterate_view line 60
  16. def OAI.BinaryMatching.DenseOracle.mincut line 66
  17. lemma OAI.BinaryMatching.DenseOracle.mincut_eq line 70
  18. def OAI.BinaryMatching.DenseOracle.terminalCut line 77
  19. lemma OAI.BinaryMatching.DenseOracle.terminalCut_eq line 83
  20. def OAI.BinaryMatching.DenseOracle.contract line 87
  21. lemma OAI.BinaryMatching.DenseOracle.contract_view line 89
  22. def OAI.BinaryMatching.DenseOracle.recurse line 92
  23. lemma OAI.BinaryMatching.DenseOracle.recurse_eq line 106
  24. def OAI.BinaryMatching.DenseOracle.oddCut line 118
  25. lemma OAI.BinaryMatching.DenseOracle.oddCut_eq line 120
  26. theorem OAI.BinaryMatching.DenseOracle.oddCut_correct line 123