OAI/Computability/PerfectCompleteness/Construction/MixedSourceLocalOddLists.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.MixedSourceLocalOddLists.F2 line 13
  2. theorem OAI.PerfectCompleteness.MixedSourceLocalOddLists.parity_comp line 22
  3. theorem OAI.PerfectCompleteness.MixedSourceLocalOddLists.oddList_map_comp line 51
  4. theorem OAI.PerfectCompleteness.MixedSourceLocalOddLists.map_eq_of_map_eq line 60
  5. theorem OAI.PerfectCompleteness.MixedSourceLocalOddLists.encoded_accepts line 74
  6. abbrev OAI.PerfectCompleteness.MixedSourceLocalOddLists.Endpoints line 99
  7. def OAI.PerfectCompleteness.MixedSourceLocalOddLists.slotsOf line 101
  8. abbrev OAI.PerfectCompleteness.MixedSourceLocalOddLists.RightForms line 105
  9. def OAI.PerfectCompleteness.MixedSourceLocalOddLists.defaultValue line 109
  10. def OAI.PerfectCompleteness.MixedSourceLocalOddLists.readBit line 113
  11. def OAI.PerfectCompleteness.MixedSourceLocalOddLists.leafToBits line 117
  12. def OAI.PerfectCompleteness.MixedSourceLocalOddLists.rightResponse line 122
  13. def OAI.PerfectCompleteness.MixedSourceLocalOddLists.target line 129
  14. def OAI.PerfectCompleteness.MixedSourceLocalOddLists.step line 133
  15. def OAI.PerfectCompleteness.MixedSourceLocalOddLists.rightEndpoints line 138
  16. def OAI.PerfectCompleteness.MixedSourceLocalOddLists.treeProjection line 143
  17. theorem OAI.PerfectCompleteness.MixedSourceLocalOddLists.clean_leaf_projection line 150
  18. def OAI.PerfectCompleteness.MixedSourceLocalOddLists.strategy line 171
  19. theorem OAI.PerfectCompleteness.MixedSourceLocalOddLists.fill_rightEndpoints line 182
  20. theorem OAI.PerfectCompleteness.MixedSourceLocalOddLists.strategy_wins line 193