OAI/Computability/PerfectCompleteness/Machines/BinaryTotalInputMachine.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.PerfectCompleteness.BinaryTotalInputMachine.Label line 20
  2. abbrev OAI.PerfectCompleteness.BinaryTotalInputMachine.Label.enumList line 27
  3. theorem OAI.PerfectCompleteness.BinaryTotalInputMachine.Label.enumList_getElem?_ctorIdx_eq line 29
  4. theorem OAI.PerfectCompleteness.BinaryTotalInputMachine.Label.enumList_nodup line 33
  5. instance OAI.PerfectCompleteness.BinaryTotalInputMachine.(instance at line 35) line 35
  6. abbrev OAI.PerfectCompleteness.BinaryTotalInputMachine.Alphabet line 39
  7. abbrev OAI.PerfectCompleteness.BinaryTotalInputMachine.State line 40
  8. def OAI.PerfectCompleteness.BinaryTotalInputMachine.rejectedWord line 42
  9. def OAI.PerfectCompleteness.BinaryTotalInputMachine.instruction line 44
  10. abbrev OAI.PerfectCompleteness.BinaryTotalInputMachine.machine line 58
  11. def OAI.PerfectCompleteness.BinaryTotalInputMachine.tapes line 69
  12. def OAI.PerfectCompleteness.BinaryTotalInputMachine.cfg line 74
  13. theorem OAI.PerfectCompleteness.BinaryTotalInputMachine.tapes_input line 78
  14. theorem OAI.PerfectCompleteness.BinaryTotalInputMachine.tapes_output line 81
  15. theorem OAI.PerfectCompleteness.BinaryTotalInputMachine.tapes_saved line 84
  16. theorem OAI.PerfectCompleteness.BinaryTotalInputMachine.update_input line 87
  17. theorem OAI.PerfectCompleteness.BinaryTotalInputMachine.update_output line 93
  18. theorem OAI.PerfectCompleteness.BinaryTotalInputMachine.update_saved line 99
  19. def OAI.PerfectCompleteness.BinaryTotalInputMachine.afterScan line 105
  20. theorem OAI.PerfectCompleteness.BinaryTotalInputMachine.step_scan_empty line 107
  21. theorem OAI.PerfectCompleteness.BinaryTotalInputMachine.step_scan_cons line 114
  22. theorem OAI.PerfectCompleteness.BinaryTotalInputMachine.scanTrace line 122
  23. theorem OAI.PerfectCompleteness.BinaryTotalInputMachine.restoreTrace line 138
  24. theorem OAI.PerfectCompleteness.BinaryTotalInputMachine.drainTrace line 150
  25. theorem OAI.PerfectCompleteness.BinaryTotalInputMachine.step_rejectOutput line 161
  26. theorem OAI.PerfectCompleteness.BinaryTotalInputMachine.joinTrace line 171
  27. theorem OAI.PerfectCompleteness.BinaryTotalInputMachine.acceptedTrace line 175
  28. theorem OAI.PerfectCompleteness.BinaryTotalInputMachine.rejectedTrace line 186
  29. theorem OAI.PerfectCompleteness.BinaryTotalInputMachine.initList_eq line 201
  30. theorem OAI.PerfectCompleteness.BinaryTotalInputMachine.haltList_eq line 208
  31. def OAI.PerfectCompleteness.BinaryTotalInputMachine.steps line 215
  32. theorem OAI.PerfectCompleteness.BinaryTotalInputMachine.steps_le line 218
  33. theorem OAI.PerfectCompleteness.BinaryTotalInputMachine.totalTrace line 222
  34. def OAI.PerfectCompleteness.BinaryTotalInputMachine.outputsInTime line 244
  35. def OAI.PerfectCompleteness.BinaryTotalInputMachine.computableInPolyTime line 252
  36. theorem OAI.PerfectCompleteness.BinaryTotalInputMachine.machine_finiteAlphabet line 266
  37. theorem OAI.PerfectCompleteness.BinaryTotalInputMachine.computation_finiteAlphabet line 270