OAI/Combinatorics/MatchingCount/Tapes/TreeSparseStage.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MatchingFPRAS.ExecutableSource.StageControls line 15
  2. abbrev OAI.MatchingFPRAS.ExecutableSource.SparseStageData line 16
  3. abbrev OAI.MatchingFPRAS.ExecutableSource.SparseStageInput line 17
  4. def OAI.MatchingFPRAS.ExecutableSource.currentActivityArg line 19
  5. def OAI.MatchingFPRAS.ExecutableSource.currentActivityArgRealizer line 20
  6. lemma OAI.MatchingFPRAS.ExecutableSource.polynomial_currentActivityArg line 22
  7. def OAI.MatchingFPRAS.ExecutableSource.sparseCurrentMatrix line 24
  8. def OAI.MatchingFPRAS.ExecutableSource.sparseCurrentMatrixRealizer line 25
  9. lemma OAI.MatchingFPRAS.ExecutableSource.polynomial_sparseCurrentMatrix line 27
  10. def OAI.MatchingFPRAS.ExecutableSource.nextActivityArg line 30
  11. def OAI.MatchingFPRAS.ExecutableSource.nextActivityArgRealizer line 31
  12. lemma OAI.MatchingFPRAS.ExecutableSource.polynomial_nextActivityArg line 33
  13. def OAI.MatchingFPRAS.ExecutableSource.sparseNextMatrix line 39
  14. def OAI.MatchingFPRAS.ExecutableSource.sparseNextMatrixRealizer line 40
  15. lemma OAI.MatchingFPRAS.ExecutableSource.polynomial_sparseNextMatrix line 42
  16. def OAI.MatchingFPRAS.ExecutableSource.sparseBagInput line 45
  17. def OAI.MatchingFPRAS.ExecutableSource.sparseBagInputRealizer line 47
  18. lemma OAI.MatchingFPRAS.ExecutableSource.polynomial_sparseBagInput line 50
  19. def OAI.MatchingFPRAS.ExecutableSource.sparseGeneratedInput line 57
  20. def OAI.MatchingFPRAS.ExecutableSource.sparseGeneratedInputRealizer line 59
  21. lemma OAI.MatchingFPRAS.ExecutableSource.polynomial_sparseGeneratedInput line 61
  22. def OAI.MatchingFPRAS.ExecutableSource.sparseUpdateData line 68
  23. def OAI.MatchingFPRAS.ExecutableSource.sparseUpdateDataRealizer line 70
  24. lemma OAI.MatchingFPRAS.ExecutableSource.polynomial_sparseUpdateData line 72
  25. def OAI.MatchingFPRAS.ExecutableSource.sparseStage line 76
  26. def OAI.MatchingFPRAS.ExecutableSource.sparseStageRealizer line 77
  27. lemma OAI.MatchingFPRAS.ExecutableSource.polynomial_sparseStage line 80
  28. lemma OAI.MatchingFPRAS.ExecutableSource.sparseUpdateData_source line 84
  29. lemma OAI.MatchingFPRAS.ExecutableSource.sparseStage_source line 96
  30. theorem OAI.MatchingFPRAS.ExecutableSource.sparseStage_post line 119