OAI/Computability/PerfectCompleteness/Decoding/CleanDecoderOddLists.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.CleanDecoderOddLists.F2 line 20
  2. def OAI.PerfectCompleteness.CleanDecoderOddLists.nativeLeaf line 26
  3. theorem OAI.PerfectCompleteness.CleanDecoderOddLists.slotEmbedding_cast_target line 30
  4. theorem OAI.PerfectCompleteness.CleanDecoderOddLists.nativeLeaf_embedding line 37
  5. theorem OAI.PerfectCompleteness.CleanDecoderOddLists.nativeLeaf_slots line 44
  6. abbrev OAI.PerfectCompleteness.CleanDecoderOddLists.leftNative line 53
  7. abbrev OAI.PerfectCompleteness.CleanDecoderOddLists.rightNative line 54
  8. def OAI.PerfectCompleteness.CleanDecoderOddLists.designatedLeaf line 56
  9. theorem OAI.PerfectCompleteness.CleanDecoderOddLists.leftNative_designated line 58
  10. theorem OAI.PerfectCompleteness.CleanDecoderOddLists.rightNative_designated line 66
  11. def OAI.PerfectCompleteness.CleanDecoderOddLists.leftEncoding line 74
  12. def OAI.PerfectCompleteness.CleanDecoderOddLists.rightEncoding line 78
  13. abbrev OAI.PerfectCompleteness.CleanDecoderOddLists.Occurrences line 82
  14. def OAI.PerfectCompleteness.CleanDecoderOddLists.leftQuestions line 84
  15. def OAI.PerfectCompleteness.CleanDecoderOddLists.rightQuestions line 85
  16. def OAI.PerfectCompleteness.CleanDecoderOddLists.fullProjection line 88
  17. theorem OAI.PerfectCompleteness.CleanDecoderOddLists.nativeProjection_designated line 98
  18. theorem OAI.PerfectCompleteness.CleanDecoderOddLists.projection_encode line 114
  19. def OAI.PerfectCompleteness.CleanDecoderOddLists.target line 128
  20. def OAI.PerfectCompleteness.CleanDecoderOddLists.leftResponse line 131
  21. def OAI.PerfectCompleteness.CleanDecoderOddLists.rightResponse line 137
  22. def OAI.PerfectCompleteness.CleanDecoderOddLists.strategy line 143
  23. theorem OAI.PerfectCompleteness.CleanDecoderOddLists.forms_agree line 149
  24. theorem OAI.PerfectCompleteness.CleanDecoderOddLists.responses_accept line 167
  25. theorem OAI.PerfectCompleteness.CleanDecoderOddLists.strategy_wins line 195