OAI/Combinatorics/MatchingCount/Machines/TreeList.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatchingFPRAS.TreeTyped.Realizer.congr line 11
  2. def OAI.MatchingFPRAS.TreeTyped.listCons line 14
  3. def OAI.MatchingFPRAS.TreeTyped.reverse line 17
  4. def OAI.MatchingFPRAS.TreeTyped.toBits line 23
  5. def OAI.MatchingFPRAS.TreeTyped.double line 26
  6. def OAI.MatchingFPRAS.TreeTyped.mulStep line 31
  7. def OAI.MatchingFPRAS.TreeTyped.mulStepRealizer line 34
  8. lemma OAI.MatchingFPRAS.TreeTyped.mulStep_fold line 42
  9. def OAI.MatchingFPRAS.TreeTyped.multiply line 52
  10. lemma OAI.MatchingFPRAS.TreeTyped.size_encode_list line 62
  11. lemma OAI.MatchingFPRAS.TreeTyped.size_encode_mem line 68
  12. lemma OAI.MatchingFPRAS.TreeTyped.size_encode_tail line 79
  13. lemma OAI.MatchingFPRAS.TreeTyped.Fold.cost_bound line 84