OAI/Computability/DirectedFeedback/Machines/MachineBinaryLiteralMachine.lean

GitHub source file

66 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.DFVSGames.BinaryLiteralMachine.Alphabet line 60
  2. abbrev OAI.DFVSGames.BinaryLiteralMachine.State line 61
  3. abbrev OAI.DFVSGames.BinaryLiteralMachine.clean line 62
  4. inductive OAI.DFVSGames.BinaryLiteralMachine.Label line 65
  5. def OAI.DFVSGames.BinaryLiteralMachine.searchTapes line 71
  6. theorem OAI.DFVSGames.BinaryLiteralMachine.searchTapes_injective line 80
  7. def OAI.DFVSGames.BinaryLiteralMachine.finish line 86
  8. def OAI.DFVSGames.BinaryLiteralMachine.readSign line 92
  9. def OAI.DFVSGames.BinaryLiteralMachine.emitSign line 100
  10. def OAI.DFVSGames.BinaryLiteralMachine.instruction line 106
  11. def OAI.DFVSGames.BinaryLiteralMachine.signWord line 126
  12. def OAI.DFVSGames.BinaryLiteralMachine.index line 128
  13. def OAI.DFVSGames.BinaryLiteralMachine.outputWord line 131
  14. def OAI.DFVSGames.BinaryLiteralMachine.steps line 134
  15. theorem OAI.DFVSGames.BinaryLiteralMachine.afterMatch_length_le line 140
  16. theorem OAI.DFVSGames.BinaryLiteralMachine.steps_le line 149
  17. theorem OAI.DFVSGames.BinaryLiteralMachine.stepAux_finish line 165
  18. theorem OAI.DFVSGames.BinaryLiteralMachine.joinTrace_inline_MachineBinaryLiteralMachine line 169
  19. theorem OAI.DFVSGames.BinaryLiteralMachine.literalTrace line 173
  20. def OAI.DFVSGames.BinaryLiteralMachine.literalInTime line 343
  21. abbrev OAI.DFVSGames.BinaryRenameLoop.Token line 380
  22. def OAI.DFVSGames.BinaryRenameLoop.nextSlot line 382
  23. def OAI.DFVSGames.BinaryRenameLoop.clauseIncrement line 384
  24. def OAI.DFVSGames.BinaryRenameLoop.finalSlot line 386
  25. def OAI.DFVSGames.BinaryRenameLoop.completedClauses line 390
  26. theorem OAI.DFVSGames.BinaryRenameLoop.finalSlot_three line 394
  27. theorem OAI.DFVSGames.BinaryRenameLoop.completedClauses_three line 397
  28. theorem OAI.DFVSGames.BinaryRenameLoop.finalSlot_triples line 401
  29. theorem OAI.DFVSGames.BinaryRenameLoop.completedClauses_triples line 406
  30. def OAI.DFVSGames.BinaryRenameLoop.outputBody line 411
  31. theorem OAI.DFVSGames.BinaryRenameLoop.outputBody_nil line 414
  32. theorem OAI.DFVSGames.BinaryRenameLoop.outputBody_cons line 416
  33. def OAI.DFVSGames.BinaryRenameLoop.steps line 420
  34. theorem OAI.DFVSGames.BinaryRenameLoop.payload_length_le_stream line 424
  35. def OAI.DFVSGames.BinaryRenameLoop.perLiteralBound line 439
  36. theorem OAI.DFVSGames.BinaryRenameLoop.literal_steps_le line 442
  37. theorem OAI.DFVSGames.BinaryRenameLoop.steps_le line 454
  38. theorem OAI.DFVSGames.BinaryRenameLoop.steps_le_cubic line 467
  39. abbrev OAI.DFVSGames.BinaryRenameLoop.Alphabet line 487
  40. abbrev OAI.DFVSGames.BinaryRenameLoop.State line 488
  41. abbrev OAI.DFVSGames.BinaryRenameLoop.clean line 489
  42. inductive OAI.DFVSGames.BinaryRenameLoop.Label line 492
  43. def OAI.DFVSGames.BinaryRenameLoop.literalTapes line 498
  44. theorem OAI.DFVSGames.BinaryRenameLoop.literalTapes_injective line 501
  45. def OAI.DFVSGames.BinaryRenameLoop.finish line 507
  46. def OAI.DFVSGames.BinaryRenameLoop.next line 513
  47. def OAI.DFVSGames.BinaryRenameLoop.instruction line 517
  48. def OAI.DFVSGames.BinaryRenameLoop.loopTapes line 533
  49. theorem OAI.DFVSGames.BinaryRenameLoop.loopTapes_cursor line 538
  50. theorem OAI.DFVSGames.BinaryRenameLoop.loopTapes_output line 544
  51. theorem OAI.DFVSGames.BinaryRenameLoop.loopTapes_variables line 550
  52. theorem OAI.DFVSGames.BinaryRenameLoop.loopTapes_clauses line 556
  53. theorem OAI.DFVSGames.BinaryRenameLoop.update_cursor_inline_MachineBinaryRenameLoop line 561
  54. theorem OAI.DFVSGames.BinaryRenameLoop.update_output_inline_MachineBinaryRenameLoop line 571
  55. theorem OAI.DFVSGames.BinaryRenameLoop.update_variables_inline_MachineBinaryRenameLoop line 581
  56. theorem OAI.DFVSGames.BinaryRenameLoop.update_clauses_inline_MachineBinaryRenameLoop line 591
  57. theorem OAI.DFVSGames.BinaryRenameLoop.loopTapes_other line 597
  58. theorem OAI.DFVSGames.BinaryRenameLoop.stepAux_finish line 603
  59. theorem OAI.DFVSGames.BinaryRenameLoop.joinTrace_inline_MachineBinaryRenameLoop line 608
  60. theorem OAI.DFVSGames.BinaryRenameLoop.peekStep line 620
  61. theorem OAI.DFVSGames.BinaryRenameLoop.emptyStep line 632
  62. theorem OAI.DFVSGames.BinaryRenameLoop.tallyStep line 643
  63. theorem OAI.DFVSGames.BinaryRenameLoop.bodyTrace line 658
  64. theorem OAI.DFVSGames.BinaryRenameLoop.loopTrace line 730
  65. theorem OAI.DFVSGames.BinaryRenameLoop.triplesTrace line 774
  66. def OAI.DFVSGames.BinaryRenameLoop.triplesInTime line 791