OAI/Computability/PerfectCompleteness/Construction/SourceLocalOddLists.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.SourceLocalOddLists.F2 line 15
  2. abbrev OAI.PerfectCompleteness.SourceLocalOddLists.Form line 21
  3. def OAI.PerfectCompleteness.SourceLocalOddLists.leafSupport line 24
  4. def OAI.PerfectCompleteness.SourceLocalOddLists.extract line 32
  5. theorem OAI.PerfectCompleteness.SourceLocalOddLists.extract_accepts line 38
  6. theorem OAI.PerfectCompleteness.SourceLocalOddLists.map_eq_of_map_eq line 74
  7. abbrev OAI.PerfectCompleteness.SourceLocalOddLists.LeftQuestions line 87
  8. abbrev OAI.PerfectCompleteness.SourceLocalOddLists.RightQuestions line 88
  9. abbrev OAI.PerfectCompleteness.SourceLocalOddLists.Occurrences line 89
  10. abbrev OAI.PerfectCompleteness.SourceLocalOddLists.LeftForms line 91
  11. abbrev OAI.PerfectCompleteness.SourceLocalOddLists.RightForms line 94
  12. def OAI.PerfectCompleteness.SourceLocalOddLists.leftResponse line 97
  13. def OAI.PerfectCompleteness.SourceLocalOddLists.rightResponse line 104
  14. def OAI.PerfectCompleteness.SourceLocalOddLists.treeProjection line 109
  15. abbrev OAI.PerfectCompleteness.SourceLocalOddLists.CleanLeaves line 119
  16. def OAI.PerfectCompleteness.SourceLocalOddLists.fill line 121
  17. theorem OAI.PerfectCompleteness.SourceLocalOddLists.fill_clean line 125
  18. theorem OAI.PerfectCompleteness.SourceLocalOddLists.fill_comp line 130
  19. def OAI.PerfectCompleteness.SourceLocalOddLists.strategy line 141
  20. theorem OAI.PerfectCompleteness.SourceLocalOddLists.strategy_wins line 150