OAI/Computability/PerfectCompleteness/Machines/BinaryPairMachine.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.BinaryPairMachine.Tape line 15
  2. abbrev OAI.PerfectCompleteness.BinaryPairMachine.Label line 16
  3. abbrev OAI.PerfectCompleteness.BinaryPairMachine.State line 17
  4. abbrev OAI.PerfectCompleteness.BinaryPairMachine.Alphabet line 18
  5. def OAI.PerfectCompleteness.BinaryPairMachine.stop line 20
  6. def OAI.PerfectCompleteness.BinaryPairMachine.count line 23
  7. def OAI.PerfectCompleteness.BinaryPairMachine.copy line 31
  8. def OAI.PerfectCompleteness.BinaryPairMachine.program line 40
  9. abbrev OAI.PerfectCompleteness.BinaryPairMachine.machine line 46
  10. def OAI.PerfectCompleteness.BinaryPairMachine.tapes line 57
  11. def OAI.PerfectCompleteness.BinaryPairMachine.cfg line 60
  12. theorem OAI.PerfectCompleteness.BinaryPairMachine.tapes_zero line 64
  13. theorem OAI.PerfectCompleteness.BinaryPairMachine.tapes_one line 67
  14. theorem OAI.PerfectCompleteness.BinaryPairMachine.tapes_two line 70
  15. theorem OAI.PerfectCompleteness.BinaryPairMachine.update_zero line 73
  16. theorem OAI.PerfectCompleteness.BinaryPairMachine.update_one line 79
  17. theorem OAI.PerfectCompleteness.BinaryPairMachine.update_two line 85
  18. theorem OAI.PerfectCompleteness.BinaryPairMachine.countStep_true line 91
  19. theorem OAI.PerfectCompleteness.BinaryPairMachine.countStep_false line 98
  20. theorem OAI.PerfectCompleteness.BinaryPairMachine.countTrace line 105
  21. theorem OAI.PerfectCompleteness.BinaryPairMachine.copyStep_empty line 124
  22. theorem OAI.PerfectCompleteness.BinaryPairMachine.copyStep_cons line 131
  23. theorem OAI.PerfectCompleteness.BinaryPairMachine.copyTrace line 139
  24. theorem OAI.PerfectCompleteness.BinaryPairMachine.restoreTrace line 154
  25. theorem OAI.PerfectCompleteness.BinaryPairMachine.initList_eq line 167
  26. theorem OAI.PerfectCompleteness.BinaryPairMachine.joinTrace line 174
  27. theorem OAI.PerfectCompleteness.BinaryPairMachine.pairTrace line 178
  28. def OAI.PerfectCompleteness.BinaryPairMachine.pairInTime line 193
  29. theorem OAI.PerfectCompleteness.BinaryPairMachine.haltStep line 201
  30. def OAI.PerfectCompleteness.BinaryPairMachine.pairHaltInTime line 207
  31. theorem OAI.PerfectCompleteness.BinaryPairMachine.pairSteps_le_pairedLength line 219
  32. theorem OAI.PerfectCompleteness.BinaryPairMachine.machine_finiteAlphabet line 225