OAI/Combinatorics/MatchingCount/Sampling/TreeDPProgram.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MatchingFPRAS.ExecutableDP.Params line 9
  2. abbrev OAI.MatchingFPRAS.ExecutableDP.State line 10
  3. def OAI.MatchingFPRAS.ExecutableDP.update line 12
  4. def OAI.MatchingFPRAS.ExecutableDP.updateProgram line 14
  5. def OAI.MatchingFPRAS.ExecutableDP.step line 17
  6. def OAI.MatchingFPRAS.ExecutableDP.stepRealizer line 25
  7. def OAI.MatchingFPRAS.ExecutableDP.runState line 36
  8. def OAI.MatchingFPRAS.ExecutableDP.run line 41
  9. lemma OAI.MatchingFPRAS.ExecutableDP.step_fold line 43
  10. def OAI.MatchingFPRAS.ExecutableDP.runRealizer line 52
  11. lemma OAI.MatchingFPRAS.ExecutableDP.tabulate_materialized line 62
  12. lemma OAI.MatchingFPRAS.ExecutableDP.update_eq line 66
  13. lemma OAI.MatchingFPRAS.ExecutableDP.privateNumber_perm line 80
  14. lemma OAI.MatchingFPRAS.ExecutableDP.sharedNumber_perm line 82
  15. lemma OAI.MatchingFPRAS.ExecutableDP.totalNumber_perm line 84
  16. lemma OAI.MatchingFPRAS.ExecutableDP.context_perm line 86
  17. lemma OAI.MatchingFPRAS.ExecutableDP.update_perm line 89
  18. def OAI.MatchingFPRAS.ExecutableDP.parentTag line 93
  19. def OAI.MatchingFPRAS.ExecutableDP.parentRep line 96
  20. lemma OAI.MatchingFPRAS.ExecutableDP.parentRep_length line 97
  21. lemma OAI.MatchingFPRAS.ExecutableDP.parentRep_getD line 99
  22. lemma OAI.MatchingFPRAS.ExecutableDP.run_eq line 103