OAI/Combinatorics/MatchingCount/Machines/RegisterTree.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MatchingFPRAS.RegisterProc.exec_perm line 9
  2. def OAI.MatchingFPRAS.RegisterProc.p02 line 28
  3. def OAI.MatchingFPRAS.RegisterProc.p01 line 29
  4. def OAI.MatchingFPRAS.RegisterProc.p12 line 30
  5. def OAI.MatchingFPRAS.RegisterProc.p201 line 31
  6. def OAI.MatchingFPRAS.RegisterProc.p120 line 33
  7. lemma OAI.MatchingFPRAS.RegisterProc.vector_p01 line 34
  8. lemma OAI.MatchingFPRAS.RegisterProc.vector_p02 line 36
  9. lemma OAI.MatchingFPRAS.RegisterProc.vector_p12 line 38
  10. lemma OAI.MatchingFPRAS.RegisterProc.vector_p201 line 40
  11. lemma OAI.MatchingFPRAS.RegisterProc.vector_p120 line 42
  12. def OAI.MatchingFPRAS.RegisterProc.reverse02 line 45
  13. def OAI.MatchingFPRAS.RegisterProc.reverse10 line 46
  14. def OAI.MatchingFPRAS.RegisterProc.reverse20 line 47
  15. def OAI.MatchingFPRAS.RegisterProc.reverse21 line 48
  16. lemma OAI.MatchingFPRAS.RegisterProc.reverse02_exec line 49
  17. lemma OAI.MatchingFPRAS.RegisterProc.reverse10_exec line 53
  18. lemma OAI.MatchingFPRAS.RegisterProc.reverse20_exec line 57
  19. lemma OAI.MatchingFPRAS.RegisterProc.reverse21_exec line 61
  20. def OAI.MatchingFPRAS.RegisterProc.finishCons line 66
  21. lemma OAI.MatchingFPRAS.RegisterProc.finishCons_exec line 67
  22. def OAI.MatchingFPRAS.RegisterProc.cons line 73
  23. lemma OAI.MatchingFPRAS.RegisterProc.cons_exec line 74
  24. def OAI.MatchingFPRAS.RegisterProc.clear1 line 83
  25. lemma OAI.MatchingFPRAS.RegisterProc.clear1_exec line 84
  26. def OAI.MatchingFPRAS.RegisterProc.copy line 88
  27. lemma OAI.MatchingFPRAS.RegisterProc.copy_exec line 89
  28. def OAI.MatchingFPRAS.RegisterProc.startSplit line 99
  29. lemma OAI.MatchingFPRAS.RegisterProc.startSplit_exec line 100
  30. def OAI.MatchingFPRAS.RegisterProc.transfer12 line 105
  31. lemma OAI.MatchingFPRAS.RegisterProc.transfer12_exec line 106
  32. def OAI.MatchingFPRAS.RegisterProc.split line 112
  33. lemma OAI.MatchingFPRAS.RegisterProc.split_exec line 113