OAI/Computability/PerfectCompleteness/Machines/CanonicalKeyMachine.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PerfectCompleteness.CanonicalKeyMachine.actualSlots line 20
  2. def OAI.PerfectCompleteness.CanonicalKeyMachine.recoveredKey line 24
  3. def OAI.PerfectCompleteness.CanonicalKeyMachine.prefixBits line 31
  4. def OAI.PerfectCompleteness.CanonicalKeyMachine.payload line 34
  5. theorem OAI.PerfectCompleteness.CanonicalKeyMachine.metadata_words line 39
  6. theorem OAI.PerfectCompleteness.CanonicalKeyMachine.encodeWords_flatMap line 56
  7. theorem OAI.PerfectCompleteness.CanonicalKeyMachine.payload_eq line 62
  8. inductive OAI.PerfectCompleteness.CanonicalKeyMachine.Command line 79
  9. def OAI.PerfectCompleteness.CanonicalKeyMachine.LocalLabel line 85
  10. instance OAI.PerfectCompleteness.CanonicalKeyMachine.localLabelFintype line 90
  11. instance OAI.PerfectCompleteness.CanonicalKeyMachine.localLabelDecidableEq line 93
  12. def OAI.PerfectCompleteness.CanonicalKeyMachine.main line 96
  13. def OAI.PerfectCompleteness.CanonicalKeyMachine.commands line 101
  14. abbrev OAI.PerfectCompleteness.CanonicalKeyMachine.Label line 104
  15. abbrev OAI.PerfectCompleteness.CanonicalKeyMachine.Alphabet line 108
  16. abbrev OAI.PerfectCompleteness.CanonicalKeyMachine.State line 109
  17. def OAI.PerfectCompleteness.CanonicalKeyMachine.localInstruction line 111
  18. def OAI.PerfectCompleteness.CanonicalKeyMachine.entry line 120
  19. def OAI.PerfectCompleteness.CanonicalKeyMachine.instruction line 123
  20. def OAI.PerfectCompleteness.CanonicalKeyMachine.commandBits line 130
  21. def OAI.PerfectCompleteness.CanonicalKeyMachine.commandCost line 138
  22. def OAI.PerfectCompleteness.CanonicalKeyMachine.sourceLength line 146
  23. theorem OAI.PerfectCompleteness.CanonicalKeyMachine.resultOf_prepend line 149
  24. theorem OAI.PerfectCompleteness.CanonicalKeyMachine.steps_constant line 160
  25. theorem OAI.PerfectCompleteness.CanonicalKeyMachine.commands_bits line 167
  26. theorem OAI.PerfectCompleteness.CanonicalKeyMachine.commandCost_metadata_le line 178
  27. theorem OAI.PerfectCompleteness.CanonicalKeyMachine.commands_cost line 189
  28. theorem OAI.PerfectCompleteness.CanonicalKeyMachine.commands_cost_le line 197
  29. theorem OAI.PerfectCompleteness.CanonicalKeyMachine.source_ne_output line 215
  30. def OAI.PerfectCompleteness.CanonicalKeyMachine.keyInTime line 227
  31. theorem OAI.PerfectCompleteness.CanonicalKeyMachine.output_frame line 321
  32. theorem OAI.PerfectCompleteness.CanonicalKeyMachine.output_sources line 326
  33. theorem OAI.PerfectCompleteness.CanonicalKeyMachine.output_scratch line 334
  34. theorem OAI.PerfectCompleteness.CanonicalKeyMachine.label_finite line 339
  35. theorem OAI.PerfectCompleteness.CanonicalKeyMachine.state_finite line 341