OAI/Computability/PerfectCompleteness/Machines/BinaryRenameMachine.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.BinaryRenameMachine.Tape line 18
  2. abbrev OAI.PerfectCompleteness.BinaryRenameMachine.Alphabet line 19
  3. abbrev OAI.PerfectCompleteness.BinaryRenameMachine.State line 20
  4. inductive OAI.PerfectCompleteness.BinaryRenameMachine.Label line 22
  5. def OAI.PerfectCompleteness.BinaryRenameMachine.loopTapes line 29
  6. theorem OAI.PerfectCompleteness.BinaryRenameMachine.loopTapes_injective line 31
  7. def OAI.PerfectCompleteness.BinaryRenameMachine.program line 36
  8. abbrev OAI.PerfectCompleteness.BinaryRenameMachine.machine line 49
  9. def OAI.PerfectCompleteness.BinaryRenameMachine.tapes line 60
  10. def OAI.PerfectCompleteness.BinaryRenameMachine.cfg line 70
  11. theorem OAI.PerfectCompleteness.BinaryRenameMachine.initList_eq line 75
  12. theorem OAI.PerfectCompleteness.BinaryRenameMachine.haltList_eq line 82
  13. theorem OAI.PerfectCompleteness.BinaryRenameMachine.copyTrace line 89
  14. theorem OAI.PerfectCompleteness.BinaryRenameMachine.restoreTrace line 106
  15. theorem OAI.PerfectCompleteness.BinaryRenameMachine.headerTrace line 127
  16. theorem OAI.PerfectCompleteness.BinaryRenameMachine.cleanupTrace line 151
  17. theorem OAI.PerfectCompleteness.BinaryRenameMachine.outputBody_eq line 169
  18. theorem OAI.PerfectCompleteness.BinaryRenameMachine.loopTrace line 184
  19. theorem OAI.PerfectCompleteness.BinaryRenameMachine.joinTrace line 227
  20. def OAI.PerfectCompleteness.BinaryRenameMachine.steps line 231
  21. theorem OAI.PerfectCompleteness.BinaryRenameMachine.renameTrace line 238
  22. theorem OAI.PerfectCompleteness.BinaryRenameMachine.clause_count_le_stream line 257
  23. theorem OAI.PerfectCompleteness.BinaryRenameMachine.body_length_le line 262
  24. def OAI.PerfectCompleteness.BinaryRenameMachine.timePolynomial line 273
  25. theorem OAI.PerfectCompleteness.BinaryRenameMachine.steps_le line 277
  26. def OAI.PerfectCompleteness.BinaryRenameMachine.outputsInTime line 297
  27. def OAI.PerfectCompleteness.BinaryRenameMachine.tokenComputation line 305
  28. def OAI.PerfectCompleteness.BinaryRenameMachine.preprocessing line 318
  29. def OAI.PerfectCompleteness.BinaryRenameMachine.computableInPolyTime line 328
  30. theorem OAI.PerfectCompleteness.BinaryRenameMachine.machine_finiteAlphabet line 333
  31. theorem OAI.PerfectCompleteness.BinaryRenameMachine.computation_finiteAlphabet line 337