OAI/Computability/MinUncut/Machines/MachineBinaryLiteralMachine.lean

GitHub source file

66 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MinUncutGames.BinaryLiteralMachine.Alphabet line 15
  2. abbrev OAI.MinUncutGames.BinaryLiteralMachine.State line 16
  3. abbrev OAI.MinUncutGames.BinaryLiteralMachine.clean line 17
  4. inductive OAI.MinUncutGames.BinaryLiteralMachine.Label line 20
  5. def OAI.MinUncutGames.BinaryLiteralMachine.searchTapes line 26
  6. theorem OAI.MinUncutGames.BinaryLiteralMachine.searchTapes_injective line 35
  7. def OAI.MinUncutGames.BinaryLiteralMachine.finish line 41
  8. def OAI.MinUncutGames.BinaryLiteralMachine.readSign line 47
  9. def OAI.MinUncutGames.BinaryLiteralMachine.emitSign line 55
  10. def OAI.MinUncutGames.BinaryLiteralMachine.instruction line 61
  11. def OAI.MinUncutGames.BinaryLiteralMachine.signWord line 81
  12. def OAI.MinUncutGames.BinaryLiteralMachine.index line 83
  13. def OAI.MinUncutGames.BinaryLiteralMachine.outputWord line 86
  14. def OAI.MinUncutGames.BinaryLiteralMachine.steps line 89
  15. theorem OAI.MinUncutGames.BinaryLiteralMachine.afterMatch_length_le line 95
  16. theorem OAI.MinUncutGames.BinaryLiteralMachine.steps_le line 104
  17. theorem OAI.MinUncutGames.BinaryLiteralMachine.stepAux_finish line 120
  18. theorem OAI.MinUncutGames.BinaryLiteralMachine.joinTrace line 124
  19. theorem OAI.MinUncutGames.BinaryLiteralMachine.literalTrace line 128
  20. def OAI.MinUncutGames.BinaryLiteralMachine.literalInTime line 298
  21. abbrev OAI.MinUncutGames.BinaryRenameLoop.Token line 331
  22. def OAI.MinUncutGames.BinaryRenameLoop.nextSlot line 333
  23. def OAI.MinUncutGames.BinaryRenameLoop.clauseIncrement line 335
  24. def OAI.MinUncutGames.BinaryRenameLoop.finalSlot line 337
  25. def OAI.MinUncutGames.BinaryRenameLoop.completedClauses line 341
  26. theorem OAI.MinUncutGames.BinaryRenameLoop.finalSlot_three line 345
  27. theorem OAI.MinUncutGames.BinaryRenameLoop.completedClauses_three line 348
  28. theorem OAI.MinUncutGames.BinaryRenameLoop.finalSlot_triples line 352
  29. theorem OAI.MinUncutGames.BinaryRenameLoop.completedClauses_triples line 357
  30. def OAI.MinUncutGames.BinaryRenameLoop.outputBody line 362
  31. theorem OAI.MinUncutGames.BinaryRenameLoop.outputBody_nil line 365
  32. theorem OAI.MinUncutGames.BinaryRenameLoop.outputBody_cons line 367
  33. def OAI.MinUncutGames.BinaryRenameLoop.steps line 371
  34. theorem OAI.MinUncutGames.BinaryRenameLoop.payload_length_le_stream line 375
  35. def OAI.MinUncutGames.BinaryRenameLoop.perLiteralBound line 390
  36. theorem OAI.MinUncutGames.BinaryRenameLoop.literal_steps_le line 393
  37. theorem OAI.MinUncutGames.BinaryRenameLoop.steps_le line 405
  38. theorem OAI.MinUncutGames.BinaryRenameLoop.steps_le_cubic line 418
  39. abbrev OAI.MinUncutGames.BinaryRenameLoop.Alphabet line 436
  40. abbrev OAI.MinUncutGames.BinaryRenameLoop.State line 437
  41. abbrev OAI.MinUncutGames.BinaryRenameLoop.clean line 438
  42. inductive OAI.MinUncutGames.BinaryRenameLoop.Label line 441
  43. def OAI.MinUncutGames.BinaryRenameLoop.literalTapes line 447
  44. theorem OAI.MinUncutGames.BinaryRenameLoop.literalTapes_injective line 450
  45. def OAI.MinUncutGames.BinaryRenameLoop.finish line 456
  46. def OAI.MinUncutGames.BinaryRenameLoop.next line 462
  47. def OAI.MinUncutGames.BinaryRenameLoop.instruction line 466
  48. def OAI.MinUncutGames.BinaryRenameLoop.loopTapes line 482
  49. theorem OAI.MinUncutGames.BinaryRenameLoop.loopTapes_cursor line 487
  50. theorem OAI.MinUncutGames.BinaryRenameLoop.loopTapes_output line 493
  51. theorem OAI.MinUncutGames.BinaryRenameLoop.loopTapes_variables line 499
  52. theorem OAI.MinUncutGames.BinaryRenameLoop.loopTapes_clauses line 505
  53. theorem OAI.MinUncutGames.BinaryRenameLoop.update_cursor line 510
  54. theorem OAI.MinUncutGames.BinaryRenameLoop.update_output line 520
  55. theorem OAI.MinUncutGames.BinaryRenameLoop.update_variables line 530
  56. theorem OAI.MinUncutGames.BinaryRenameLoop.update_clauses line 540
  57. theorem OAI.MinUncutGames.BinaryRenameLoop.loopTapes_other line 546
  58. theorem OAI.MinUncutGames.BinaryRenameLoop.stepAux_finish line 552
  59. theorem OAI.MinUncutGames.BinaryRenameLoop.joinTrace line 557
  60. theorem OAI.MinUncutGames.BinaryRenameLoop.peekStep line 569
  61. theorem OAI.MinUncutGames.BinaryRenameLoop.emptyStep line 581
  62. theorem OAI.MinUncutGames.BinaryRenameLoop.tallyStep line 592
  63. theorem OAI.MinUncutGames.BinaryRenameLoop.bodyTrace line 607
  64. theorem OAI.MinUncutGames.BinaryRenameLoop.loopTrace line 679
  65. theorem OAI.MinUncutGames.BinaryRenameLoop.triplesTrace line 723
  66. def OAI.MinUncutGames.BinaryRenameLoop.triplesInTime line 740