OAI/Combinatorics/MatchingCount/Machines/TreeRepeat.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatchingFPRAS.TreeTyped.predecessor line 12
  2. def OAI.MatchingFPRAS.TreeTyped.countDown line 14
  3. inductive OAI.MatchingFPRAS.TreeTyped.Repeat.Point line 21
  4. instance OAI.MatchingFPRAS.TreeTyped.Repeat.(instance at line 23) line 23
  5. def OAI.MatchingFPRAS.TreeTyped.Repeat.next line 24
  6. def OAI.MatchingFPRAS.TreeTyped.Repeat.nextRealizer line 25
  7. def OAI.MatchingFPRAS.TreeTyped.Repeat.code line 28
  8. def OAI.MatchingFPRAS.TreeTyped.Repeat.cost line 35
  9. lemma OAI.MatchingFPRAS.TreeTyped.Repeat.runs line 39
  10. def OAI.MatchingFPRAS.TreeTyped.iterateDown line 89
  11. def OAI.MatchingFPRAS.TreeTyped.rangeStep line 94
  12. def OAI.MatchingFPRAS.TreeTyped.rangeStepRealizer line 95
  13. lemma OAI.MatchingFPRAS.TreeTyped.countDown_range line 96
  14. def OAI.MatchingFPRAS.TreeTyped.range line 100
  15. lemma OAI.MatchingFPRAS.TreeTyped.Repeat.cost_bound line 105