OAI/Computability/DirectedFeedback/Machines/MachineBinaryTokenMachine.lean

GitHub source file

93 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.DFVSGames.BinaryTokenMachine.Tape line 59
  2. abbrev OAI.DFVSGames.BinaryTokenMachine.Alphabet line 60
  3. abbrev OAI.DFVSGames.BinaryTokenMachine.State line 61
  4. inductive OAI.DFVSGames.BinaryTokenMachine.Label line 63
  5. def OAI.DFVSGames.BinaryTokenMachine.afterName line 72
  6. theorem OAI.DFVSGames.BinaryTokenMachine.afterName_zero line 75
  7. theorem OAI.DFVSGames.BinaryTokenMachine.afterName_one line 76
  8. theorem OAI.DFVSGames.BinaryTokenMachine.afterName_two line 77
  9. def OAI.DFVSGames.BinaryTokenMachine.jump line 79
  10. def OAI.DFVSGames.BinaryTokenMachine.clauseInstruction line 82
  11. def OAI.DFVSGames.BinaryTokenMachine.signInstruction line 89
  12. def OAI.DFVSGames.BinaryTokenMachine.nameInstruction line 95
  13. def OAI.DFVSGames.BinaryTokenMachine.program line 107
  14. abbrev OAI.DFVSGames.BinaryTokenMachine.machine line 115
  15. def OAI.DFVSGames.BinaryTokenMachine.tapes line 126
  16. def OAI.DFVSGames.BinaryTokenMachine.cfg line 129
  17. theorem OAI.DFVSGames.BinaryTokenMachine.tapes_zero line 133
  18. theorem OAI.DFVSGames.BinaryTokenMachine.tapes_one line 136
  19. theorem OAI.DFVSGames.BinaryTokenMachine.tapes_two line 139
  20. theorem OAI.DFVSGames.BinaryTokenMachine.update_zero_inline_MachineBinaryTokenMachine line 142
  21. theorem OAI.DFVSGames.BinaryTokenMachine.update_one_inline_MachineBinaryTokenMachine line 148
  22. theorem OAI.DFVSGames.BinaryTokenMachine.clauseStep line 154
  23. theorem OAI.DFVSGames.BinaryTokenMachine.finalStep line 161
  24. theorem OAI.DFVSGames.BinaryTokenMachine.signStep line 168
  25. theorem OAI.DFVSGames.BinaryTokenMachine.nameEndStep line 176
  26. theorem OAI.DFVSGames.BinaryTokenMachine.nameDigitStep line 184
  27. theorem OAI.DFVSGames.BinaryTokenMachine.nameTrace line 193
  28. theorem OAI.DFVSGames.BinaryTokenMachine.literalTrace line 210
  29. theorem OAI.DFVSGames.BinaryTokenMachine.joinTrace_inline_MachineBinaryTokenMachine line 227
  30. theorem OAI.DFVSGames.BinaryTokenMachine.clauseTrace line 231
  31. def OAI.DFVSGames.BinaryTokenMachine.tokens line 252
  32. theorem OAI.DFVSGames.BinaryTokenMachine.tokens_nil line 254
  33. theorem OAI.DFVSGames.BinaryTokenMachine.tokens_cons line 256
  34. theorem OAI.DFVSGames.BinaryTokenMachine.tokens_length line 260
  35. theorem OAI.DFVSGames.BinaryTokenMachine.stripTrace line 269
  36. theorem OAI.DFVSGames.BinaryTokenMachine.restoreTrace line 301
  37. theorem OAI.DFVSGames.BinaryTokenMachine.initList_eq line 318
  38. theorem OAI.DFVSGames.BinaryTokenMachine.haltList_eq line 325
  39. theorem OAI.DFVSGames.BinaryTokenMachine.acceptTrace line 332
  40. theorem OAI.DFVSGames.BinaryTokenMachine.haltStep line 350
  41. theorem OAI.DFVSGames.BinaryTokenMachine.tokenTrace line 355
  42. theorem OAI.DFVSGames.BinaryTokenMachine.tokenSteps_le line 364
  43. def OAI.DFVSGames.BinaryTokenMachine.outputsInTime line 370
  44. def OAI.DFVSGames.BinaryTokenMachine.computableInPolyTime line 377
  45. theorem OAI.DFVSGames.BinaryTokenMachine.machine_finiteAlphabet line 392
  46. def OAI.DFVSGames.BinaryRenameWords.clauseLiterals line 406
  47. def OAI.DFVSGames.BinaryRenameWords.literals line 408
  48. def OAI.DFVSGames.BinaryRenameWords.token line 410
  49. def OAI.DFVSGames.BinaryRenameWords.tokens line 413
  50. theorem OAI.DFVSGames.BinaryRenameWords.literals_nil line 416
  51. theorem OAI.DFVSGames.BinaryRenameWords.literals_cons line 418
  52. theorem OAI.DFVSGames.BinaryRenameWords.literals_length line 421
  53. theorem OAI.DFVSGames.BinaryRenameWords.tokens_length line 427
  54. theorem OAI.DFVSGames.BinaryRenameWords.literals_names line 430
  55. theorem OAI.DFVSGames.BinaryRenameWords.tokens_payloads line 435
  56. theorem OAI.DFVSGames.BinaryRenameWords.token_bits line 440
  57. theorem OAI.DFVSGames.BinaryRenameWords.tokens_stream line 445
  58. theorem OAI.DFVSGames.BinaryRenameWords.tokens_canonical line 456
  59. theorem OAI.DFVSGames.BinaryRenameWords.payload_index line 462
  60. theorem OAI.DFVSGames.BinaryRenameWords.token_payload_mem line 467
  61. theorem OAI.DFVSGames.BinaryRenameWords.payloadSize_tokens line 474
  62. def OAI.DFVSGames.BinaryRenameWords.outputLiteral line 487
  63. def OAI.DFVSGames.BinaryRenameWords.body line 491
  64. theorem OAI.DFVSGames.BinaryRenameWords.encoded_clause line 494
  65. theorem OAI.DFVSGames.BinaryRenameWords.encodeWords_flatMap_inline_MachineBinaryRenameWords line 502
  66. theorem OAI.DFVSGames.BinaryRenameWords.encoded_body line 509
  67. theorem OAI.DFVSGames.BinaryRenameWords.encoded_renamed line 522
  68. abbrev OAI.DFVSGames.BinaryHeaderMachine.Alphabet line 544
  69. abbrev OAI.DFVSGames.BinaryHeaderMachine.State line 545
  70. def OAI.DFVSGames.BinaryHeaderMachine.delimiter line 551
  71. def OAI.DFVSGames.BinaryHeaderMachine.tapes line 555
  72. theorem OAI.DFVSGames.BinaryHeaderMachine.tapes_variables line 560
  73. theorem OAI.DFVSGames.BinaryHeaderMachine.tapes_clauses line 567
  74. theorem OAI.DFVSGames.BinaryHeaderMachine.tapes_destination line 574
  75. theorem OAI.DFVSGames.BinaryHeaderMachine.tapes_other line 580
  76. theorem OAI.DFVSGames.BinaryHeaderMachine.update_variables_inline_MachineBinaryHeaderMachine line 586
  77. theorem OAI.DFVSGames.BinaryHeaderMachine.update_clauses_inline_MachineBinaryHeaderMachine line 603
  78. theorem OAI.DFVSGames.BinaryHeaderMachine.update_destination_inline_MachineBinaryHeaderMachine line 617
  79. theorem OAI.DFVSGames.BinaryHeaderMachine.clauseDelimiterStep line 636
  80. theorem OAI.DFVSGames.BinaryHeaderMachine.variableDelimiterStep line 648
  81. theorem OAI.DFVSGames.BinaryHeaderMachine.clauseCounterTrace line 660
  82. theorem OAI.DFVSGames.BinaryHeaderMachine.variableCounterTrace line 680
  83. theorem OAI.DFVSGames.BinaryHeaderMachine.joinTrace_inline_MachineBinaryHeaderMachine line 699
  84. theorem OAI.DFVSGames.BinaryHeaderMachine.headerTrace line 705
  85. def OAI.DFVSGames.BinaryHeaderMachine.headerInTime line 734
  86. abbrev OAI.DFVSGames.BinaryHeaderMachine.ConcreteTape line 749
  87. abbrev OAI.DFVSGames.BinaryHeaderMachine.ConcreteLabel line 750
  88. def OAI.DFVSGames.BinaryHeaderMachine.concreteProgram line 752
  89. abbrev OAI.DFVSGames.BinaryHeaderMachine.machine line 759
  90. def OAI.DFVSGames.BinaryHeaderMachine.start line 770
  91. theorem OAI.DFVSGames.BinaryHeaderMachine.haltList_eq line 774
  92. def OAI.DFVSGames.BinaryHeaderMachine.machineInTime line 782
  93. theorem OAI.DFVSGames.BinaryHeaderMachine.machine_finiteAlphabet line 792