OAI/Computability/PerfectCompleteness/Machines/EncodingLemmas.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PerfectCompleteness.Encoding.parseLabel line 13
  2. theorem OAI.PerfectCompleteness.Encoding.parseLabel_value line 16
  3. theorem OAI.PerfectCompleteness.Encoding.parseLabels_values line 20
  4. def OAI.PerfectCompleteness.Encoding.parseImages line 26
  5. theorem OAI.PerfectCompleteness.Encoding.parseImages_values line 33
  6. def OAI.PerfectCompleteness.Encoding.parseProjection line 41
  7. theorem OAI.PerfectCompleteness.Encoding.parseProjection_encoded line 50
  8. theorem OAI.PerfectCompleteness.Encoding.tableWords_length line 56
  9. def OAI.PerfectCompleteness.Encoding.parseEdge line 60
  10. theorem OAI.PerfectCompleteness.Encoding.parseEdge_encoded line 69
  11. def OAI.PerfectCompleteness.Encoding.parseEdges line 78
  12. theorem OAI.PerfectCompleteness.Encoding.parseEdges_encoded line 86
  13. def OAI.PerfectCompleteness.Encoding.decodeGameWords line 94
  14. theorem OAI.PerfectCompleteness.Encoding.decodeGameWords_encoded line 106
  15. def OAI.PerfectCompleteness.Encoding.decodeGameBits line 114
  16. theorem OAI.PerfectCompleteness.Encoding.decodeGameBits_encoded line 117
  17. theorem OAI.PerfectCompleteness.Encoding.gameBits_injective line 121
  18. theorem OAI.PerfectCompleteness.Encoding.edgeWords_length line 126
  19. theorem OAI.PerfectCompleteness.Encoding.edgesWords_length line 130
  20. theorem OAI.PerfectCompleteness.Encoding.gameWords_length line 139
  21. theorem OAI.PerfectCompleteness.Encoding.gameBits_length line 144
  22. theorem OAI.PerfectCompleteness.Encoding.tableWords_sum_le line 155
  23. theorem OAI.PerfectCompleteness.Encoding.edgeWords_sum_le line 170
  24. theorem OAI.PerfectCompleteness.Encoding.edgesWords_sum_le line 180
  25. theorem OAI.PerfectCompleteness.Encoding.gameWords_sum_le line 194
  26. theorem OAI.PerfectCompleteness.Encoding.gameBits_length_le line 204
  27. theorem OAI.PerfectCompleteness.Encoding.gameBits_length_le_of_edge_count line 217