OAI/Computability/PerfectCompleteness/Machines/CanonicalKeyShapeMachineLemmas.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PerfectCompleteness.CanonicalKeyShapeMachine.inputEnum line 17
  2. def OAI.PerfectCompleteness.CanonicalKeyShapeMachine.inputBits line 20
  3. def OAI.PerfectCompleteness.CanonicalKeyShapeMachine.defaultInput line 23
  4. def OAI.PerfectCompleteness.CanonicalKeyShapeMachine.modeEnum line 26
  5. def OAI.PerfectCompleteness.CanonicalKeyShapeMachine.modeWords line 28
  6. theorem OAI.PerfectCompleteness.CanonicalKeyShapeMachine.modeWords_length line 31
  7. theorem OAI.PerfectCompleteness.CanonicalKeyShapeMachine.modeWords_injective line 34
  8. def OAI.PerfectCompleteness.CanonicalKeyShapeMachine.outputWords line 41
  9. def OAI.PerfectCompleteness.CanonicalKeyShapeMachine.outputBits line 44
  10. theorem OAI.PerfectCompleteness.CanonicalKeyShapeMachine.outputWords_length line 46
  11. theorem OAI.PerfectCompleteness.CanonicalKeyShapeMachine.outputWords_eq_iff line 50
  12. theorem OAI.PerfectCompleteness.CanonicalKeyShapeMachine.outputBits_eq_iff line 62
  13. def OAI.PerfectCompleteness.CanonicalKeyShapeMachine.computation line 71
  14. def OAI.PerfectCompleteness.CanonicalKeyShapeMachine.machine_output line 75
  15. def OAI.PerfectCompleteness.CanonicalKeyShapeMachine.recoverKey line 85
  16. theorem OAI.PerfectCompleteness.CanonicalKeyShapeMachine.recoverKey_input line 89
  17. theorem OAI.PerfectCompleteness.CanonicalKeyShapeMachine.recoverKey_of_same_output line 94
  18. theorem OAI.PerfectCompleteness.CanonicalKeyShapeMachine.workAlphabet_finite line 100
  19. theorem OAI.PerfectCompleteness.CanonicalOnlineNames.firstIndex_append_current line 117
  20. theorem OAI.PerfectCompleteness.CanonicalOnlineNames.firstIndex_le_prefix line 123
  21. theorem OAI.PerfectCompleteness.CanonicalOnlineNames.firstIndex_eq_prefix line 129
  22. def OAI.PerfectCompleteness.CanonicalOnlineNames.onlineID line 143
  23. theorem OAI.PerfectCompleteness.CanonicalOnlineNames.tokens_append_current line 147
  24. theorem OAI.PerfectCompleteness.CanonicalOnlineNames.current_payload_mem line 152
  25. theorem OAI.PerfectCompleteness.CanonicalOnlineNames.dictionary_canonical line 157
  26. theorem OAI.PerfectCompleteness.CanonicalOnlineNames.onlineID_le_prefix line 162
  27. theorem OAI.PerfectCompleteness.CanonicalOnlineNames.onlineID_eq_global line 169
  28. theorem OAI.PerfectCompleteness.CanonicalOnlineNames.onlineID_eq_name_val line 179
  29. theorem OAI.PerfectCompleteness.CanonicalOnlineNames.onlineID_eq_prefix_index line 184
  30. theorem OAI.PerfectCompleteness.CanonicalOnlineNames.onlineID_repeat line 193
  31. theorem OAI.PerfectCompleteness.CanonicalOnlineNames.onlineID_eq_iff_same_final line 201
  32. def OAI.PerfectCompleteness.CanonicalOnlineNames.onlineName line 217
  33. theorem OAI.PerfectCompleteness.CanonicalOnlineNames.onlineName_val line 220
  34. def OAI.PerfectCompleteness.CanonicalOnlineNames.paddedName line 223
  35. theorem OAI.PerfectCompleteness.CanonicalOnlineNames.paddedName_val line 228
  36. theorem OAI.PerfectCompleteness.CanonicalOnlineNames.paddedName_eq_iff line 233
  37. def OAI.PerfectCompleteness.CanonicalOnlineNames.paddedEmbedding line 245
  38. def OAI.PerfectCompleteness.CanonicalOnlineNames.onlinePaddedName line 253
  39. theorem OAI.PerfectCompleteness.CanonicalOnlineNames.onlinePaddedName_eq_final line 257