OAI/Computability/PerfectCompleteness/Machines/LocalCompletionMachineLemmas.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PerfectCompleteness.LocalCompletionMachine.inputEnum line 18
  2. def OAI.PerfectCompleteness.LocalCompletionMachine.resultEnum line 21
  3. def OAI.PerfectCompleteness.LocalCompletionMachine.inputBits line 24
  4. def OAI.PerfectCompleteness.LocalCompletionMachine.resultBits line 27
  5. theorem OAI.PerfectCompleteness.LocalCompletionMachine.inputBits_length line 30
  6. theorem OAI.PerfectCompleteness.LocalCompletionMachine.resultBits_length line 34
  7. theorem OAI.PerfectCompleteness.LocalCompletionMachine.resultBits_injective line 38
  8. def OAI.PerfectCompleteness.LocalCompletionMachine.defaultInput line 42
  9. def OAI.PerfectCompleteness.LocalCompletionMachine.computation line 45
  10. theorem OAI.PerfectCompleteness.LocalCompletionMachine.workAlphabet_finite line 49
  11. theorem OAI.PerfectCompleteness.LocalCompletionMachine.exact_pushBound line 54
  12. theorem OAI.PerfectCompleteness.LocalCompletionMachine.produces_correct_result line 58
  13. theorem OAI.PerfectCompleteness.LocalCompletionMachine.statement_trace line 73
  14. def OAI.PerfectCompleteness.LocalCompletionSerialization.rawTableWords line 99
  15. theorem OAI.PerfectCompleteness.LocalCompletionSerialization.rawTableWords_length line 102
  16. def OAI.PerfectCompleteness.LocalCompletionSerialization.payloadWords line 106
  17. def OAI.PerfectCompleteness.LocalCompletionSerialization.payloadBits line 109
  18. theorem OAI.PerfectCompleteness.LocalCompletionSerialization.payloadWords_length line 112
  19. theorem OAI.PerfectCompleteness.LocalCompletionSerialization.payloadBits_length_le line 125
  20. theorem OAI.PerfectCompleteness.LocalCompletionSerialization.decode_payloadBits line 141
  21. def OAI.PerfectCompleteness.LocalCompletionSerialization.projection line 145
  22. theorem OAI.PerfectCompleteness.LocalCompletionSerialization.projection_apply line 151
  23. theorem OAI.PerfectCompleteness.LocalCompletionSerialization.rawTableWords_eq line 156
  24. theorem OAI.PerfectCompleteness.LocalCompletionSerialization.parse_rawTableWords line 164
  25. def OAI.PerfectCompleteness.LocalCompletionSerialization.parseTables line 170
  26. theorem OAI.PerfectCompleteness.LocalCompletionSerialization.parseTables_encoded line 177
  27. def OAI.PerfectCompleteness.LocalCompletionSerialization.parsePayload line 192
  28. theorem OAI.PerfectCompleteness.LocalCompletionSerialization.parse_payload line 198
  29. def OAI.PerfectCompleteness.LocalCompletionSerialization.emit line 219
  30. def OAI.PerfectCompleteness.LocalCompletionSerialization.computation line 222
  31. def OAI.PerfectCompleteness.LocalCompletionSerialization.machine_output line 226
  32. theorem OAI.PerfectCompleteness.LocalCompletionSerialization.machine_output_parses line 237
  33. theorem OAI.PerfectCompleteness.LocalCompletionSerialization.workAlphabet_finite line 249