OAI/Combinatorics/MatchingCount/Arithmetic/TreeMultiply.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MatchingFPRAS.TreeMultiply.R line 12
  2. inductive OAI.MatchingFPRAS.TreeMultiply.Point line 13
  3. instance OAI.MatchingFPRAS.TreeMultiply.(instance at line 16) line 16
  4. def OAI.MatchingFPRAS.TreeMultiply.program line 17
  5. def OAI.MatchingFPRAS.TreeMultiply.prep line 26
  6. def OAI.MatchingFPRAS.TreeMultiply.summed line 27
  7. def OAI.MatchingFPRAS.TreeMultiply.next line 29
  8. def OAI.MatchingFPRAS.TreeMultiply.accum line 31
  9. def OAI.MatchingFPRAS.TreeMultiply.result line 32
  10. lemma OAI.MatchingFPRAS.TreeMultiply.bits_add_length line 36
  11. lemma OAI.MatchingFPRAS.TreeMultiply.bit_length line 41
  12. lemma OAI.MatchingFPRAS.TreeMultiply.next_zero line 42
  13. lemma OAI.MatchingFPRAS.TreeMultiply.next_one line 44
  14. lemma OAI.MatchingFPRAS.TreeMultiply.next_two line 46
  15. lemma OAI.MatchingFPRAS.TreeMultiply.next_three line 49
  16. lemma OAI.MatchingFPRAS.TreeMultiply.next_four line 51
  17. lemma OAI.MatchingFPRAS.TreeMultiply.next_five line 53
  18. lemma OAI.MatchingFPRAS.TreeMultiply.accum_bound line 55
  19. lemma OAI.MatchingFPRAS.TreeMultiply.output line 70
  20. lemma OAI.MatchingFPRAS.TreeMultiply.frame line 79
  21. lemma OAI.MatchingFPRAS.TreeMultiply.halt_runs line 84
  22. lemma OAI.MatchingFPRAS.TreeMultiply.cycle_runs line 87
  23. lemma OAI.MatchingFPRAS.TreeMultiply.runs line 143
  24. def OAI.MatchingFPRAS.TreeMultiply.multiply line 164
  25. theorem OAI.MatchingFPRAS.TreeMultiply.exec line 166