OAI/Combinatorics/MatchingCount/Machines/TreeFunction.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MatchingFPRAS.TreeFunction.Reg line 9
  2. def OAI.MatchingFPRAS.TreeFunction.env line 10
  3. lemma OAI.MatchingFPRAS.TreeFunction.env0 line 11
  4. lemma OAI.MatchingFPRAS.TreeFunction.env1 line 12
  5. lemma OAI.MatchingFPRAS.TreeFunction.env2 line 13
  6. def OAI.MatchingFPRAS.TreeFunction.size line 14
  7. lemma OAI.MatchingFPRAS.TreeFunction.size_nil line 15
  8. lemma OAI.MatchingFPRAS.TreeFunction.size_cons line 16
  9. def OAI.MatchingFPRAS.TreeFunction.Realizes line 19
  10. lemma OAI.MatchingFPRAS.TreeFunction.env_ext line 22
  11. lemma OAI.MatchingFPRAS.TreeFunction.env_update0 line 24
  12. lemma OAI.MatchingFPRAS.TreeFunction.env_update1 line 26
  13. lemma OAI.MatchingFPRAS.TreeFunction.env_update2 line 28
  14. def OAI.MatchingFPRAS.TreeFunction.clear line 32
  15. def OAI.MatchingFPRAS.TreeFunction.copy line 33
  16. def OAI.MatchingFPRAS.TreeFunction.cons line 34
  17. def OAI.MatchingFPRAS.TreeFunction.split line 35
  18. lemma OAI.MatchingFPRAS.TreeFunction.copy01 line 37
  19. lemma OAI.MatchingFPRAS.TreeFunction.copy10 line 40
  20. lemma OAI.MatchingFPRAS.TreeFunction.cons12 line 43
  21. lemma OAI.MatchingFPRAS.TreeFunction.cons02 line 46
  22. lemma OAI.MatchingFPRAS.TreeFunction.cons10 line 49
  23. lemma OAI.MatchingFPRAS.TreeFunction.split12 line 52
  24. lemma OAI.MatchingFPRAS.TreeFunction.split10 line 55
  25. lemma OAI.MatchingFPRAS.TreeFunction.clear0 line 58
  26. lemma OAI.MatchingFPRAS.TreeFunction.clear1 line 61
  27. lemma OAI.MatchingFPRAS.TreeFunction.realizes_seq line 65
  28. def OAI.MatchingFPRAS.TreeFunction.pair line 69
  29. lemma OAI.MatchingFPRAS.TreeFunction.realizes_pair line 75