OAI/Combinatorics/MatchingCount/Machines/TreeTransfer.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.MatchingFPRAS.TreeData.Data line 7
  2. def OAI.MatchingFPRAS.TreeData.encode line 13
  3. lemma OAI.MatchingFPRAS.TreeData.encode_nonempty line 16
  4. lemma OAI.MatchingFPRAS.TreeData.encode_length_pos line 17
  5. def OAI.MatchingFPRAS.TreeData.size line 18
  6. lemma OAI.MatchingFPRAS.TreeData.encode_length line 21
  7. abbrev OAI.MatchingFPRAS.TreeTransfer.Store line 32
  8. abbrev OAI.MatchingFPRAS.TreeTransfer.Stacks line 33
  9. def OAI.MatchingFPRAS.TreeTransfer.program line 34
  10. def OAI.MatchingFPRAS.TreeTransfer.stackData line 40
  11. def OAI.MatchingFPRAS.TreeTransfer.cfg line 41
  12. lemma OAI.MatchingFPRAS.TreeTransfer.stacks_zero line 43
  13. lemma OAI.MatchingFPRAS.TreeTransfer.stacks_one line 44
  14. lemma OAI.MatchingFPRAS.TreeTransfer.stacks_two line 45
  15. lemma OAI.MatchingFPRAS.TreeTransfer.update_zero line 46
  16. lemma OAI.MatchingFPRAS.TreeTransfer.update_one line 48
  17. lemma OAI.MatchingFPRAS.TreeTransfer.update_two line 50
  18. lemma OAI.MatchingFPRAS.TreeTransfer.step_nil line 52
  19. lemma OAI.MatchingFPRAS.TreeTransfer.step_cons line 56
  20. lemma OAI.MatchingFPRAS.TreeTransfer.step_stop line 60
  21. theorem OAI.MatchingFPRAS.TreeTransfer.run_tree line 64
  22. theorem OAI.MatchingFPRAS.TreeTransfer.run_transfer line 77
  23. lemma OAI.MatchingFPRAS.TreeTransfer.accesses_bound line 83