OAI/Computability/PerfectCompleteness/Machines/CanonicalDictionaryAppendMachine.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.CanonicalDictionaryAppendMachine.Alphabet line 16
  2. abbrev OAI.PerfectCompleteness.CanonicalDictionaryAppendMachine.State line 17
  3. abbrev OAI.PerfectCompleteness.CanonicalDictionaryAppendMachine.clean line 18
  4. def OAI.PerfectCompleteness.CanonicalDictionaryAppendMachine.payload line 20
  5. theorem OAI.PerfectCompleteness.CanonicalDictionaryAppendMachine.payload_frame line 22
  6. def OAI.PerfectCompleteness.CanonicalDictionaryAppendMachine.finish line 29
  7. def OAI.PerfectCompleteness.CanonicalDictionaryAppendMachine.emitLoop line 33
  8. theorem OAI.PerfectCompleteness.CanonicalDictionaryAppendMachine.update_source line 41
  9. theorem OAI.PerfectCompleteness.CanonicalDictionaryAppendMachine.update_destination line 52
  10. theorem OAI.PerfectCompleteness.CanonicalDictionaryAppendMachine.emitStep_empty line 58
  11. theorem OAI.PerfectCompleteness.CanonicalDictionaryAppendMachine.emitStep_cons line 72
  12. theorem OAI.PerfectCompleteness.CanonicalDictionaryAppendMachine.emitTrace line 86
  13. inductive OAI.PerfectCompleteness.CanonicalDictionaryAppendMachine.Label line 108
  14. abbrev OAI.PerfectCompleteness.CanonicalDictionaryAppendMachine.Label.enumList line 112
  15. theorem OAI.PerfectCompleteness.CanonicalDictionaryAppendMachine.Label.enumList_getElem?_ctorIdx_eq line 115
  16. theorem OAI.PerfectCompleteness.CanonicalDictionaryAppendMachine.Label.enumList_nodup line 119
  17. instance OAI.PerfectCompleteness.CanonicalDictionaryAppendMachine.(instance at line 121) line 121
  18. def OAI.PerfectCompleteness.CanonicalDictionaryAppendMachine.instruction line 125
  19. def OAI.PerfectCompleteness.CanonicalDictionaryAppendMachine.steps line 137
  20. theorem OAI.PerfectCompleteness.CanonicalDictionaryAppendMachine.joinTrace line 140
  21. theorem OAI.PerfectCompleteness.CanonicalDictionaryAppendMachine.appendTrace line 144
  22. def OAI.PerfectCompleteness.CanonicalDictionaryAppendMachine.appendInTime line 247
  23. def OAI.PerfectCompleteness.CanonicalDictionaryAppendMachine.machine line 266
  24. theorem OAI.PerfectCompleteness.CanonicalDictionaryAppendMachine.machine_finiteAlphabet line 277