OAI/Combinatorics/MatchingCount/Tapes/Input.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MatchingFPRAS.LiteralInput.PairState line 10
  2. def OAI.MatchingFPRAS.LiteralInput.pairStep line 11
  3. def OAI.MatchingFPRAS.LiteralInput.pairStepRealizer line 13
  4. lemma OAI.MatchingFPRAS.LiteralInput.polynomial_pairStep line 18
  5. lemma OAI.MatchingFPRAS.LiteralInput.pairStep_weight line 23
  6. lemma OAI.MatchingFPRAS.LiteralInput.pairFold_weight line 35
  7. lemma OAI.MatchingFPRAS.LiteralInput.polynomial_pairFold line 44
  8. def OAI.MatchingFPRAS.LiteralInput.pairs line 56
  9. def OAI.MatchingFPRAS.LiteralInput.pairsRealizer line 57
  10. lemma OAI.MatchingFPRAS.LiteralInput.polynomial_pairs line 60
  11. lemma OAI.MatchingFPRAS.LiteralInput.pair_pair line 63
  12. lemma OAI.MatchingFPRAS.LiteralInput.pairs_reverse line 65
  13. abbrev OAI.MatchingFPRAS.LiteralInput.Parsed line 75
  14. def OAI.MatchingFPRAS.LiteralInput.ratTail line 76
  15. def OAI.MatchingFPRAS.LiteralInput.ratTailRealizer line 78
  16. lemma OAI.MatchingFPRAS.LiteralInput.polynomial_ratTail line 82
  17. def OAI.MatchingFPRAS.LiteralInput.fromNumbers line 91
  18. def OAI.MatchingFPRAS.LiteralInput.reversedTailRealizer line 93
  19. def OAI.MatchingFPRAS.LiteralInput.fromNumbersRealizer line 95
  20. lemma OAI.MatchingFPRAS.LiteralInput.polynomial_reversedTail line 99
  21. lemma OAI.MatchingFPRAS.LiteralInput.polynomial_fromNumbers line 101
  22. def OAI.MatchingFPRAS.LiteralInput.parseInput line 111
  23. def OAI.MatchingFPRAS.LiteralInput.parseInputRealizer line 112
  24. lemma OAI.MatchingFPRAS.LiteralInput.polynomial_parseInput line 113
  25. def OAI.MatchingFPRAS.LiteralInput.edgeNumbers line 116
  26. lemma OAI.MatchingFPRAS.LiteralInput.edges_fold line 118
  27. lemma OAI.MatchingFPRAS.LiteralInput.parse_source line 126
  28. lemma OAI.MatchingFPRAS.LiteralInput.parseInput_source line 134