OAI/Computability/PerfectCompleteness/Machines/SourceOccurrenceLoopMachine.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PerfectCompleteness.SourceOccurrenceLoopMachine.bodySteps line 17
  2. def OAI.PerfectCompleteness.SourceOccurrenceLoopMachine.steps line 20
  3. theorem OAI.PerfectCompleteness.SourceOccurrenceLoopMachine.bodySteps_le line 24
  4. theorem OAI.PerfectCompleteness.SourceOccurrenceLoopMachine.steps_le line 31
  5. abbrev OAI.PerfectCompleteness.SourceOccurrenceLoopMachine.Alphabet line 50
  6. abbrev OAI.PerfectCompleteness.SourceOccurrenceLoopMachine.State line 51
  7. abbrev OAI.PerfectCompleteness.SourceOccurrenceLoopMachine.clean line 52
  8. def OAI.PerfectCompleteness.SourceOccurrenceLoopMachine.indexMap line 54
  9. def OAI.PerfectCompleteness.SourceOccurrenceLoopMachine.indexTapes line 59
  10. theorem OAI.PerfectCompleteness.SourceOccurrenceLoopMachine.indexTapes_injective line 62
  11. inductive OAI.PerfectCompleteness.SourceOccurrenceLoopMachine.Label line 66
  12. def OAI.PerfectCompleteness.SourceOccurrenceLoopMachine.finish line 73
  13. def OAI.PerfectCompleteness.SourceOccurrenceLoopMachine.instruction line 79
  14. def OAI.PerfectCompleteness.SourceOccurrenceLoopMachine.loopTapes line 93
  15. theorem OAI.PerfectCompleteness.SourceOccurrenceLoopMachine.loopTapes_input line 99
  16. theorem OAI.PerfectCompleteness.SourceOccurrenceLoopMachine.loopTapes_remaining line 105
  17. theorem OAI.PerfectCompleteness.SourceOccurrenceLoopMachine.loopTapes_index line 111
  18. theorem OAI.PerfectCompleteness.SourceOccurrenceLoopMachine.loopTapes_scratch line 117
  19. theorem OAI.PerfectCompleteness.SourceOccurrenceLoopMachine.loopTapes_output line 123
  20. theorem OAI.PerfectCompleteness.SourceOccurrenceLoopMachine.update_input line 128
  21. theorem OAI.PerfectCompleteness.SourceOccurrenceLoopMachine.update_remaining line 139
  22. theorem OAI.PerfectCompleteness.SourceOccurrenceLoopMachine.update_index line 151
  23. theorem OAI.PerfectCompleteness.SourceOccurrenceLoopMachine.update_output line 163
  24. theorem OAI.PerfectCompleteness.SourceOccurrenceLoopMachine.tapesAt_loop line 169
  25. theorem OAI.PerfectCompleteness.SourceOccurrenceLoopMachine.stepAux_finish line 177
  26. theorem OAI.PerfectCompleteness.SourceOccurrenceLoopMachine.joinTrace line 181
  27. theorem OAI.PerfectCompleteness.SourceOccurrenceLoopMachine.guardStep line 193
  28. theorem OAI.PerfectCompleteness.SourceOccurrenceLoopMachine.emptyStep line 204
  29. theorem OAI.PerfectCompleteness.SourceOccurrenceLoopMachine.tallyStep line 217
  30. theorem OAI.PerfectCompleteness.SourceOccurrenceLoopMachine.bodyTrace line 226
  31. theorem OAI.PerfectCompleteness.SourceOccurrenceLoopMachine.loopTrace line 278
  32. def OAI.PerfectCompleteness.SourceOccurrenceLoopMachine.loopInTime line 303