OAI/Computability/PerfectCompleteness/Machines/SourceClauseCountMachine.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.SourceClauseCountMachine.Alphabet line 17
  2. abbrev OAI.PerfectCompleteness.SourceClauseCountMachine.State line 18
  3. def OAI.PerfectCompleteness.SourceClauseCountMachine.clean line 19
  4. inductive OAI.PerfectCompleteness.SourceClauseCountMachine.Label line 21
  5. def OAI.PerfectCompleteness.SourceClauseCountMachine.main line 27
  6. def OAI.PerfectCompleteness.SourceClauseCountMachine.steps line 29
  7. theorem OAI.PerfectCompleteness.SourceClauseCountMachine.steps_eq line 34
  8. def OAI.PerfectCompleteness.SourceClauseCountMachine.instruction line 47
  9. def OAI.PerfectCompleteness.SourceClauseCountMachine.workTapes line 60
  10. theorem OAI.PerfectCompleteness.SourceClauseCountMachine.workTapes_input line 64
  11. theorem OAI.PerfectCompleteness.SourceClauseCountMachine.workTapes_output line 70
  12. theorem OAI.PerfectCompleteness.SourceClauseCountMachine.update_input line 74
  13. theorem OAI.PerfectCompleteness.SourceClauseCountMachine.workTapes_empty line 84
  14. theorem OAI.PerfectCompleteness.SourceClauseCountMachine.joinTrace line 91
  15. theorem OAI.PerfectCompleteness.SourceClauseCountMachine.copyTrace line 103
  16. theorem OAI.PerfectCompleteness.SourceClauseCountMachine.skipTrace line 121
  17. theorem OAI.PerfectCompleteness.SourceClauseCountMachine.readTrace line 142
  18. theorem OAI.PerfectCompleteness.SourceClauseCountMachine.drainTrace line 153
  19. theorem OAI.PerfectCompleteness.SourceClauseCountMachine.countTrace line 162
  20. def OAI.PerfectCompleteness.SourceClauseCountMachine.countInTime line 184
  21. theorem OAI.PerfectCompleteness.SourceClauseCountMachine.label_finite line 198