OAI/Computability/MatchingCount/RawSearchCompiler.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.BinaryMatching.Raw.SearchContext line 9
  2. abbrev OAI.BinaryMatching.Raw.SearchState line 10
  3. def OAI.BinaryMatching.Raw.searchStep line 12
  4. def OAI.BinaryMatching.Raw.searchInitial line 14
  5. lemma OAI.BinaryMatching.Raw.searchStep_iterate line 17
  6. theorem OAI.BinaryMatching.Raw.Compiler.residual_poly line 26
  7. theorem OAI.BinaryMatching.Raw.Compiler.initial_poly line 31
  8. theorem OAI.BinaryMatching.Raw.Compiler.predecessor_poly line 38
  9. def OAI.BinaryMatching.Raw.Compiler.pathEntry line 52
  10. theorem OAI.BinaryMatching.Raw.Compiler.pathEntry_poly line 59
  11. theorem OAI.BinaryMatching.Raw.Compiler.pathStep_poly line 79
  12. theorem OAI.BinaryMatching.Raw.Compiler.searchStep_poly line 83
  13. theorem OAI.BinaryMatching.Raw.Compiler.searchInitial_poly line 90
  14. theorem OAI.BinaryMatching.Raw.Compiler.search_poly line 96