OAI/Computability/MinUncut/Machines/MachineBinaryRenameMachine.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MinUncutGames.BinaryRenameMachine.Tape line 15
  2. abbrev OAI.MinUncutGames.BinaryRenameMachine.Alphabet line 16
  3. abbrev OAI.MinUncutGames.BinaryRenameMachine.State line 17
  4. inductive OAI.MinUncutGames.BinaryRenameMachine.Label line 19
  5. def OAI.MinUncutGames.BinaryRenameMachine.loopTapes line 26
  6. theorem OAI.MinUncutGames.BinaryRenameMachine.loopTapes_injective line 28
  7. def OAI.MinUncutGames.BinaryRenameMachine.program line 33
  8. abbrev OAI.MinUncutGames.BinaryRenameMachine.machine line 46
  9. def OAI.MinUncutGames.BinaryRenameMachine.tapes line 57
  10. def OAI.MinUncutGames.BinaryRenameMachine.cfg line 67
  11. theorem OAI.MinUncutGames.BinaryRenameMachine.initList_eq line 72
  12. theorem OAI.MinUncutGames.BinaryRenameMachine.haltList_eq line 79
  13. theorem OAI.MinUncutGames.BinaryRenameMachine.copyTrace line 86
  14. theorem OAI.MinUncutGames.BinaryRenameMachine.restoreTrace line 103
  15. theorem OAI.MinUncutGames.BinaryRenameMachine.headerTrace line 124
  16. theorem OAI.MinUncutGames.BinaryRenameMachine.cleanupTrace line 148
  17. theorem OAI.MinUncutGames.BinaryRenameMachine.outputBody_eq line 166
  18. theorem OAI.MinUncutGames.BinaryRenameMachine.loopTrace line 181
  19. theorem OAI.MinUncutGames.BinaryRenameMachine.joinTrace line 224
  20. def OAI.MinUncutGames.BinaryRenameMachine.steps line 228
  21. theorem OAI.MinUncutGames.BinaryRenameMachine.renameTrace line 235
  22. theorem OAI.MinUncutGames.BinaryRenameMachine.clause_count_le_stream line 254
  23. theorem OAI.MinUncutGames.BinaryRenameMachine.body_length_le line 259
  24. def OAI.MinUncutGames.BinaryRenameMachine.timePolynomial line 270
  25. theorem OAI.MinUncutGames.BinaryRenameMachine.steps_le line 274
  26. def OAI.MinUncutGames.BinaryRenameMachine.outputsInTime line 294
  27. def OAI.MinUncutGames.BinaryRenameMachine.tokenComputation line 302
  28. def OAI.MinUncutGames.BinaryRenameMachine.preprocessing line 315
  29. def OAI.MinUncutGames.BinaryRenameMachine.computableInPolyTime line 325
  30. theorem OAI.MinUncutGames.BinaryRenameMachine.machine_finiteAlphabet line 330
  31. theorem OAI.MinUncutGames.BinaryRenameMachine.computation_finiteAlphabet line 334