OAI/Computability/PerfectCompleteness/Machines/BinaryTokenMachine.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.BinaryTokenMachine.Tape line 18
  2. abbrev OAI.PerfectCompleteness.BinaryTokenMachine.Alphabet line 19
  3. abbrev OAI.PerfectCompleteness.BinaryTokenMachine.State line 20
  4. inductive OAI.PerfectCompleteness.BinaryTokenMachine.Label line 22
  5. def OAI.PerfectCompleteness.BinaryTokenMachine.afterName line 31
  6. theorem OAI.PerfectCompleteness.BinaryTokenMachine.afterName_zero line 34
  7. theorem OAI.PerfectCompleteness.BinaryTokenMachine.afterName_one line 35
  8. theorem OAI.PerfectCompleteness.BinaryTokenMachine.afterName_two line 36
  9. def OAI.PerfectCompleteness.BinaryTokenMachine.jump line 38
  10. def OAI.PerfectCompleteness.BinaryTokenMachine.clauseInstruction line 41
  11. def OAI.PerfectCompleteness.BinaryTokenMachine.signInstruction line 48
  12. def OAI.PerfectCompleteness.BinaryTokenMachine.nameInstruction line 54
  13. def OAI.PerfectCompleteness.BinaryTokenMachine.program line 66
  14. abbrev OAI.PerfectCompleteness.BinaryTokenMachine.machine line 74
  15. def OAI.PerfectCompleteness.BinaryTokenMachine.tapes line 85
  16. def OAI.PerfectCompleteness.BinaryTokenMachine.cfg line 88
  17. theorem OAI.PerfectCompleteness.BinaryTokenMachine.tapes_zero line 92
  18. theorem OAI.PerfectCompleteness.BinaryTokenMachine.tapes_one line 95
  19. theorem OAI.PerfectCompleteness.BinaryTokenMachine.tapes_two line 98
  20. theorem OAI.PerfectCompleteness.BinaryTokenMachine.update_zero line 101
  21. theorem OAI.PerfectCompleteness.BinaryTokenMachine.update_one line 107
  22. theorem OAI.PerfectCompleteness.BinaryTokenMachine.clauseStep line 113
  23. theorem OAI.PerfectCompleteness.BinaryTokenMachine.finalStep line 120
  24. theorem OAI.PerfectCompleteness.BinaryTokenMachine.signStep line 127
  25. theorem OAI.PerfectCompleteness.BinaryTokenMachine.nameEndStep line 135
  26. theorem OAI.PerfectCompleteness.BinaryTokenMachine.nameDigitStep line 143
  27. theorem OAI.PerfectCompleteness.BinaryTokenMachine.nameTrace line 152
  28. theorem OAI.PerfectCompleteness.BinaryTokenMachine.literalTrace line 169
  29. theorem OAI.PerfectCompleteness.BinaryTokenMachine.joinTrace line 186
  30. theorem OAI.PerfectCompleteness.BinaryTokenMachine.clauseTrace line 190
  31. def OAI.PerfectCompleteness.BinaryTokenMachine.tokens line 211
  32. theorem OAI.PerfectCompleteness.BinaryTokenMachine.tokens_nil line 213
  33. theorem OAI.PerfectCompleteness.BinaryTokenMachine.tokens_cons line 215
  34. theorem OAI.PerfectCompleteness.BinaryTokenMachine.tokens_length line 219
  35. theorem OAI.PerfectCompleteness.BinaryTokenMachine.stripTrace line 228
  36. theorem OAI.PerfectCompleteness.BinaryTokenMachine.restoreTrace line 260
  37. theorem OAI.PerfectCompleteness.BinaryTokenMachine.initList_eq line 276
  38. theorem OAI.PerfectCompleteness.BinaryTokenMachine.haltList_eq line 283
  39. theorem OAI.PerfectCompleteness.BinaryTokenMachine.acceptTrace line 290
  40. theorem OAI.PerfectCompleteness.BinaryTokenMachine.haltStep line 308
  41. theorem OAI.PerfectCompleteness.BinaryTokenMachine.tokenTrace line 313
  42. theorem OAI.PerfectCompleteness.BinaryTokenMachine.tokenSteps_le line 322
  43. def OAI.PerfectCompleteness.BinaryTokenMachine.outputsInTime line 328
  44. def OAI.PerfectCompleteness.BinaryTokenMachine.computableInPolyTime line 336
  45. theorem OAI.PerfectCompleteness.BinaryTokenMachine.machine_finiteAlphabet line 351