OAI/Combinatorics/MatchingCount/Sampling/TreeUnitBranch.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MatchingFPRAS.UnitRefresh.gapEquiv_val line 8
  2. lemma OAI.MatchingFPRAS.UnitRefresh.removePair_last_val line 10
  3. def OAI.MatchingFPRAS.ExecutableUnit.skip line 29
  4. def OAI.MatchingFPRAS.ExecutableUnit.skipRealizer line 30
  5. def OAI.MatchingFPRAS.ExecutableUnit.residual line 32
  6. def OAI.MatchingFPRAS.ExecutableUnit.residualRealizer line 34
  7. lemma OAI.MatchingFPRAS.ExecutableUnit.residual_ordered line 41
  8. abbrev OAI.MatchingFPRAS.ExecutableUnit.Context line 57
  9. def OAI.MatchingFPRAS.ExecutableUnit.valid line 59
  10. def OAI.MatchingFPRAS.ExecutableUnit.validRealizer line 65
  11. def OAI.MatchingFPRAS.ExecutableUnit.branch line 77
  12. def OAI.MatchingFPRAS.ExecutableUnit.branchRealizer line 79
  13. def OAI.MatchingFPRAS.ExecutableUnit.edgeCount line 83
  14. def OAI.MatchingFPRAS.ExecutableUnit.edgeCountRealizer line 84
  15. lemma OAI.MatchingFPRAS.ExecutableUnit.branch_eq line 87
  16. lemma OAI.MatchingFPRAS.ExecutableUnit.valid_eq line 100
  17. lemma OAI.MatchingFPRAS.ExecutableUnit.edgeCount_eq line 120