OAI/Combinatorics/MatchingCount/Arithmetic/TreeDivision.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MatchingFPRAS.TreeDivision.Reg line 15
  2. inductive OAI.MatchingFPRAS.TreeDivision.Point line 16
  3. instance OAI.MatchingFPRAS.TreeDivision.(instance at line 19) line 19
  4. def OAI.MatchingFPRAS.TreeDivision.program line 21
  5. def OAI.MatchingFPRAS.TreeDivision.splitState line 36
  6. def OAI.MatchingFPRAS.TreeDivision.shiftState line 37
  7. def OAI.MatchingFPRAS.TreeDivision.copyState line 39
  8. def OAI.MatchingFPRAS.TreeDivision.tested line 41
  9. def OAI.MatchingFPRAS.TreeDivision.reduced line 43
  10. def OAI.MatchingFPRAS.TreeDivision.digitState line 46
  11. def OAI.MatchingFPRAS.TreeDivision.next line 49
  12. def OAI.MatchingFPRAS.TreeDivision.result line 51
  13. lemma OAI.MatchingFPRAS.TreeDivision.next_zero line 55
  14. lemma OAI.MatchingFPRAS.TreeDivision.next_one line 58
  15. lemma OAI.MatchingFPRAS.TreeDivision.next_two line 61
  16. lemma OAI.MatchingFPRAS.TreeDivision.next_three line 65
  17. lemma OAI.MatchingFPRAS.TreeDivision.next_four line 67
  18. lemma OAI.MatchingFPRAS.TreeDivision.next_five line 69
  19. lemma OAI.MatchingFPRAS.TreeDivision.next_six line 72
  20. lemma OAI.MatchingFPRAS.TreeDivision.outputs line 76
  21. lemma OAI.MatchingFPRAS.TreeDivision.cycle_runs line 85
  22. lemma OAI.MatchingFPRAS.TreeDivision.runs line 202
  23. def OAI.MatchingFPRAS.TreeDivision.divide line 223
  24. theorem OAI.MatchingFPRAS.TreeDivision.exec line 225