OAI/Computability/MatchingCount/RawSearch.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BinaryMatching.Raw.residual line 10
  2. def OAI.BinaryMatching.Raw.initial line 12
  3. def OAI.BinaryMatching.Raw.predecessor line 13
  4. def OAI.BinaryMatching.Raw.pathStep line 15
  5. def OAI.BinaryMatching.Raw.search line 21
  6. def OAI.BinaryMatching.Raw.reached line 23
  7. lemma OAI.BinaryMatching.Raw.nth_pathRep line 25
  8. lemma OAI.BinaryMatching.Raw.residual_rep line 28
  9. lemma OAI.BinaryMatching.Raw.initial_rep line 33
  10. lemma OAI.BinaryMatching.Raw.predecessor_rep line 42
  11. lemma OAI.BinaryMatching.Raw.pathStep_rep line 53
  12. lemma OAI.BinaryMatching.Raw.search_rep line 71
  13. lemma OAI.BinaryMatching.Raw.reached_rep line 81
  14. def OAI.BinaryMatching.Raw.pathFlow line 88
  15. lemma OAI.BinaryMatching.Raw.pathFlow_rep line 92