OAI/Combinatorics/MatchingCount/Machines/TreeFold.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.MatchingFPRAS.TreeTyped.Fold.Point line 14
  2. instance OAI.MatchingFPRAS.TreeTyped.Fold.(instance at line 16) line 16
  3. def OAI.MatchingFPRAS.TreeTyped.Fold.code line 18
  4. def OAI.MatchingFPRAS.TreeTyped.Fold.heads line 29
  5. lemma OAI.MatchingFPRAS.TreeTyped.Fold.splitHeads line 30
  6. lemma OAI.MatchingFPRAS.TreeTyped.Fold.pushTail line 41
  7. lemma OAI.MatchingFPRAS.TreeTyped.Fold.pushArgs line 50
  8. def OAI.MatchingFPRAS.TreeTyped.Fold.cost line 61
  9. lemma OAI.MatchingFPRAS.TreeTyped.Fold.runs line 65
  10. def OAI.MatchingFPRAS.TreeTyped.fold line 127