OAI/Combinatorics/MatchingCount/Machines/TreeLookup.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatchingFPRAS.TreeData.ofList line 9
  2. def OAI.MatchingFPRAS.TreeData.unary line 12
  3. lemma OAI.MatchingFPRAS.TreeData.ofList_nil line 15
  4. lemma OAI.MatchingFPRAS.TreeData.ofList_cons line 16
  5. lemma OAI.MatchingFPRAS.TreeData.unary_encode_length line 17
  6. lemma OAI.MatchingFPRAS.TreeData.encode_head_le line 19
  7. lemma OAI.MatchingFPRAS.TreeData.encode_tail_le line 21
  8. lemma OAI.MatchingFPRAS.TreeMachine.SizeBound.update line 28
  9. lemma OAI.MatchingFPRAS.TreeMachine.SizeBound.putPair line 34
  10. lemma OAI.MatchingFPRAS.TreeMachine.SizeBound.split line 37
  11. inductive OAI.MatchingFPRAS.TreeLookup.Point line 47
  12. instance OAI.MatchingFPRAS.TreeLookup.(instance at line 50) line 50
  13. abbrev OAI.MatchingFPRAS.TreeLookup.R line 51
  14. def OAI.MatchingFPRAS.TreeLookup.program line 53
  15. def OAI.MatchingFPRAS.TreeLookup.result line 63
  16. def OAI.MatchingFPRAS.TreeLookup.steps line 69
  17. lemma OAI.MatchingFPRAS.TreeLookup.steps_le line 73
  18. lemma OAI.MatchingFPRAS.TreeLookup.output line 81
  19. lemma OAI.MatchingFPRAS.TreeLookup.nil_bound line 88
  20. lemma OAI.MatchingFPRAS.TreeLookup.halt_runs line 93
  21. lemma OAI.MatchingFPRAS.TreeLookup.missing_runs line 95
  22. lemma OAI.MatchingFPRAS.TreeLookup.found_runs line 99
  23. theorem OAI.MatchingFPRAS.TreeLookup.runs line 104
  24. theorem OAI.MatchingFPRAS.TreeLookup.stack_exec line 155