OAI/Combinatorics/MatchingCount/Machines/TableLookup.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatchingFPRAS.TreeData.bit line 10
  2. def OAI.MatchingFPRAS.TreeData.nat line 11
  3. def OAI.MatchingFPRAS.TreeData.row line 12
  4. def OAI.MatchingFPRAS.TreeData.table line 13
  5. lemma OAI.MatchingFPRAS.TreeData.nat_zero line 14
  6. lemma OAI.MatchingFPRAS.TreeData.row_nil line 15
  7. lemma OAI.MatchingFPRAS.TreeData.map_getD line 16
  8. lemma OAI.MatchingFPRAS.TreeData.row_getD line 24
  9. lemma OAI.MatchingFPRAS.TreeData.table_getD line 27
  10. lemma OAI.MatchingFPRAS.TreeLookup.result_frame line 35
  11. abbrev OAI.MatchingFPRAS.TableLookup.R line 46
  12. abbrev OAI.MatchingFPRAS.TableLookup.first line 47
  13. def OAI.MatchingFPRAS.TableLookup.middle line 49
  14. def OAI.MatchingFPRAS.TableLookup.result line 53
  15. def OAI.MatchingFPRAS.TableLookup.program line 56
  16. lemma OAI.MatchingFPRAS.TableLookup.output line 61
  17. lemma OAI.MatchingFPRAS.TableLookup.middle_zero line 65
  18. lemma OAI.MatchingFPRAS.TableLookup.middle_one line 67
  19. theorem OAI.MatchingFPRAS.TableLookup.stack_exec line 76