OAI/Computability/PerfectCompleteness/Machines/NormalizationLoopMachine.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PerfectCompleteness.NormalizationLoopMachine.nameSum line 18
  2. def OAI.PerfectCompleteness.NormalizationLoopMachine.bodySteps line 21
  3. def OAI.PerfectCompleteness.NormalizationLoopMachine.steps line 26
  4. theorem OAI.PerfectCompleteness.NormalizationLoopMachine.bodySteps_le line 30
  5. theorem OAI.PerfectCompleteness.NormalizationLoopMachine.steps_le line 44
  6. abbrev OAI.PerfectCompleteness.NormalizationLoopMachine.Alphabet line 63
  7. abbrev OAI.PerfectCompleteness.NormalizationLoopMachine.State line 64
  8. abbrev OAI.PerfectCompleteness.NormalizationLoopMachine.clean line 65
  9. def OAI.PerfectCompleteness.NormalizationLoopMachine.reset line 66
  10. def OAI.PerfectCompleteness.NormalizationLoopMachine.readerIndex line 68
  11. def OAI.PerfectCompleteness.NormalizationLoopMachine.emitterIndex line 74
  12. def OAI.PerfectCompleteness.NormalizationLoopMachine.oldIndex line 82
  13. def OAI.PerfectCompleteness.NormalizationLoopMachine.readerTapes line 84
  14. def OAI.PerfectCompleteness.NormalizationLoopMachine.emitterTapes line 85
  15. theorem OAI.PerfectCompleteness.NormalizationLoopMachine.readerTapes_injective line 88
  16. theorem OAI.PerfectCompleteness.NormalizationLoopMachine.emitterTapes_injective line 93
  17. inductive OAI.PerfectCompleteness.NormalizationLoopMachine.Label line 97
  18. def OAI.PerfectCompleteness.NormalizationLoopMachine.afterDrain line 105
  19. def OAI.PerfectCompleteness.NormalizationLoopMachine.finish line 108
  20. def OAI.PerfectCompleteness.NormalizationLoopMachine.instruction line 114
  21. def OAI.PerfectCompleteness.NormalizationLoopMachine.loopTapes line 131
  22. theorem OAI.PerfectCompleteness.NormalizationLoopMachine.loopTapes_input line 137
  23. theorem OAI.PerfectCompleteness.NormalizationLoopMachine.loopTapes_fresh line 144
  24. theorem OAI.PerfectCompleteness.NormalizationLoopMachine.loopTapes_remaining line 152
  25. theorem OAI.PerfectCompleteness.NormalizationLoopMachine.loopTapes_count line 160
  26. theorem OAI.PerfectCompleteness.NormalizationLoopMachine.loopTapes_output line 168
  27. theorem OAI.PerfectCompleteness.NormalizationLoopMachine.update_remaining line 173
  28. theorem OAI.PerfectCompleteness.NormalizationLoopMachine.update_fresh line 185
  29. theorem OAI.PerfectCompleteness.NormalizationLoopMachine.update_count line 197
  30. theorem OAI.PerfectCompleteness.NormalizationLoopMachine.stepAux_finish line 209
  31. theorem OAI.PerfectCompleteness.NormalizationLoopMachine.joinTrace line 213
  32. theorem OAI.PerfectCompleteness.NormalizationLoopMachine.guardStep line 225
  33. theorem OAI.PerfectCompleteness.NormalizationLoopMachine.emptyStep line 237
  34. theorem OAI.PerfectCompleteness.NormalizationLoopMachine.tallyStep line 247
  35. theorem OAI.PerfectCompleteness.NormalizationLoopMachine.bodyTrace line 265
  36. theorem OAI.PerfectCompleteness.NormalizationLoopMachine.loopTrace line 410
  37. def OAI.PerfectCompleteness.NormalizationLoopMachine.loopInTime line 445