OAI/Computability/Superstring/PrefixMatching.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Superstring.PrefixGreedy.poly_prefer line 9
  2. theorem OAI.Superstring.PrefixGreedy.poly_largest line 14
  3. theorem OAI.Superstring.PrefixGreedy.poly_prefixB line 25
  4. theorem OAI.Superstring.PrefixGreedy.poly_remove line 32
  5. theorem OAI.Superstring.PrefixGreedy.poly_extension line 39
  6. theorem OAI.Superstring.PrefixGreedy.poly_step line 45
  7. theorem OAI.Superstring.PrefixGreedy.largest_size line 50
  8. theorem OAI.Superstring.PrefixGreedy.extension_size line 53
  9. theorem OAI.Superstring.PrefixGreedy.step_bounds line 64
  10. theorem OAI.Superstring.PrefixGreedy.iterate_size line 78
  11. theorem OAI.Superstring.PrefixGreedy.poly_iterate line 91
  12. def OAI.Superstring.PrefixGreedy.compute line 109
  13. theorem OAI.Superstring.PrefixGreedy.poly_compute line 112
  14. theorem OAI.Superstring.PrefixGreedy.compute_correct line 119