OAI/Computability/PerfectCompleteness/Machines/SourceClauseSelectMachine.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PerfectCompleteness.SourceClauseSelectMachine.steps line 17
  2. theorem OAI.PerfectCompleteness.SourceClauseSelectMachine.steps_le line 23
  3. abbrev OAI.PerfectCompleteness.SourceClauseSelectMachine.Alphabet line 47
  4. abbrev OAI.PerfectCompleteness.SourceClauseSelectMachine.State line 48
  5. def OAI.PerfectCompleteness.SourceClauseSelectMachine.clean line 49
  6. inductive OAI.PerfectCompleteness.SourceClauseSelectMachine.Label line 51
  7. def OAI.PerfectCompleteness.SourceClauseSelectMachine.finish line 58
  8. def OAI.PerfectCompleteness.SourceClauseSelectMachine.instruction line 64
  9. def OAI.PerfectCompleteness.SourceClauseSelectMachine.selectTapes line 81
  10. theorem OAI.PerfectCompleteness.SourceClauseSelectMachine.selectTapes_input line 86
  11. theorem OAI.PerfectCompleteness.SourceClauseSelectMachine.selectTapes_offset line 92
  12. theorem OAI.PerfectCompleteness.SourceClauseSelectMachine.selectTapes_output line 98
  13. theorem OAI.PerfectCompleteness.SourceClauseSelectMachine.update_input line 103
  14. theorem OAI.PerfectCompleteness.SourceClauseSelectMachine.update_offset line 113
  15. theorem OAI.PerfectCompleteness.SourceClauseSelectMachine.update_output line 124
  16. theorem OAI.PerfectCompleteness.SourceClauseSelectMachine.tapesAt_select line 130
  17. theorem OAI.PerfectCompleteness.SourceClauseSelectMachine.stepAux_finish line 138
  18. theorem OAI.PerfectCompleteness.SourceClauseSelectMachine.joinTrace line 142
  19. theorem OAI.PerfectCompleteness.SourceClauseSelectMachine.guardStep line 154
  20. theorem OAI.PerfectCompleteness.SourceClauseSelectMachine.zeroStep line 163
  21. theorem OAI.PerfectCompleteness.SourceClauseSelectMachine.skipTrace line 174
  22. theorem OAI.PerfectCompleteness.SourceClauseSelectMachine.zeroTrace line 194
  23. theorem OAI.PerfectCompleteness.SourceClauseSelectMachine.selectTrace line 231
  24. def OAI.PerfectCompleteness.SourceClauseSelectMachine.selectInTime line 264