OAI/Computability/PerfectCompleteness/Machines/SourceClauseLookupMachine.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.SourceClauseLookupMachine.Alphabet line 15
  2. abbrev OAI.PerfectCompleteness.SourceClauseLookupMachine.State line 16
  3. def OAI.PerfectCompleteness.SourceClauseLookupMachine.clean line 17
  4. inductive OAI.PerfectCompleteness.SourceClauseLookupMachine.Label line 19
  5. def OAI.PerfectCompleteness.SourceClauseLookupMachine.main line 26
  6. def OAI.PerfectCompleteness.SourceClauseLookupMachine.selectMap line 28
  7. theorem OAI.PerfectCompleteness.SourceClauseLookupMachine.body_drop_length_le line 33
  8. def OAI.PerfectCompleteness.SourceClauseLookupMachine.suffix line 48
  9. def OAI.PerfectCompleteness.SourceClauseLookupMachine.steps line 51
  10. theorem OAI.PerfectCompleteness.SourceClauseLookupMachine.steps_le line 56
  11. def OAI.PerfectCompleteness.SourceClauseLookupMachine.selectTapes line 73
  12. theorem OAI.PerfectCompleteness.SourceClauseLookupMachine.selectTapes_injective line 76
  13. def OAI.PerfectCompleteness.SourceClauseLookupMachine.instruction line 80
  14. def OAI.PerfectCompleteness.SourceClauseLookupMachine.workTapes line 97
  15. theorem OAI.PerfectCompleteness.SourceClauseLookupMachine.workTapes_output line 102
  16. theorem OAI.PerfectCompleteness.SourceClauseLookupMachine.workTapes_input line 107
  17. theorem OAI.PerfectCompleteness.SourceClauseLookupMachine.workTapes_counter line 113
  18. theorem OAI.PerfectCompleteness.SourceClauseLookupMachine.update_input line 119
  19. theorem OAI.PerfectCompleteness.SourceClauseLookupMachine.update_counter line 129
  20. theorem OAI.PerfectCompleteness.SourceClauseLookupMachine.workTapes_empty line 139
  21. theorem OAI.PerfectCompleteness.SourceClauseLookupMachine.joinTrace line 148
  22. theorem OAI.PerfectCompleteness.SourceClauseLookupMachine.copyTableTrace line 160
  23. theorem OAI.PerfectCompleteness.SourceClauseLookupMachine.copyIndexTrace line 178
  24. theorem OAI.PerfectCompleteness.SourceClauseLookupMachine.headerTrace line 198
  25. theorem OAI.PerfectCompleteness.SourceClauseLookupMachine.drainTrace line 220
  26. theorem OAI.PerfectCompleteness.SourceClauseLookupMachine.selectTrace line 229
  27. theorem OAI.PerfectCompleteness.SourceClauseLookupMachine.lookupTrace line 248
  28. def OAI.PerfectCompleteness.SourceClauseLookupMachine.lookupInTime line 280
  29. theorem OAI.PerfectCompleteness.SourceClauseLookupMachine.label_finite line 296