OAI/Computability/MinUncut/Machines/MachineBinaryParsing.lean

GitHub source file

105 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MinUncutGames.BinaryParsing.frame_eq line 11
  2. theorem OAI.MinUncutGames.BinaryParsing.canonical_cons_cons line 16
  3. theorem OAI.MinUncutGames.BinaryParsing.canonical_iff line 19
  4. theorem OAI.MinUncutGames.BinaryParsing.canonical_nat_bits line 44
  5. theorem OAI.MinUncutGames.BinaryParsing.parseFrame_sound line 49
  6. theorem OAI.MinUncutGames.BinaryParsing.parseName_sound line 73
  7. theorem OAI.MinUncutGames.BinaryParsing.parseLiteral_sound line 89
  8. theorem OAI.MinUncutGames.BinaryParsing.parseClause_sound line 104
  9. theorem OAI.MinUncutGames.BinaryParsing.parseClauses_sound line 128
  10. theorem OAI.MinUncutGames.BinaryParsing.decodeFormula_sound line 156
  11. theorem OAI.MinUncutGames.BinaryParsing.decodeFormula_eq_some_iff line 170
  12. theorem OAI.MinUncutGames.BinaryParsing.scanSpec_nameBits line 174
  13. abbrev OAI.MinUncutGames.BinaryTokenMachine.Tape line 194
  14. abbrev OAI.MinUncutGames.BinaryTokenMachine.Alphabet line 195
  15. abbrev OAI.MinUncutGames.BinaryTokenMachine.State line 196
  16. inductive OAI.MinUncutGames.BinaryTokenMachine.Label line 198
  17. def OAI.MinUncutGames.BinaryTokenMachine.afterName line 207
  18. theorem OAI.MinUncutGames.BinaryTokenMachine.afterName_zero line 210
  19. theorem OAI.MinUncutGames.BinaryTokenMachine.afterName_one line 211
  20. theorem OAI.MinUncutGames.BinaryTokenMachine.afterName_two line 212
  21. def OAI.MinUncutGames.BinaryTokenMachine.jump line 214
  22. def OAI.MinUncutGames.BinaryTokenMachine.clauseInstruction line 217
  23. def OAI.MinUncutGames.BinaryTokenMachine.signInstruction line 224
  24. def OAI.MinUncutGames.BinaryTokenMachine.nameInstruction line 230
  25. def OAI.MinUncutGames.BinaryTokenMachine.program line 242
  26. abbrev OAI.MinUncutGames.BinaryTokenMachine.machine line 250
  27. def OAI.MinUncutGames.BinaryTokenMachine.tapes line 261
  28. def OAI.MinUncutGames.BinaryTokenMachine.cfg line 264
  29. theorem OAI.MinUncutGames.BinaryTokenMachine.tapes_zero line 268
  30. theorem OAI.MinUncutGames.BinaryTokenMachine.tapes_one line 271
  31. theorem OAI.MinUncutGames.BinaryTokenMachine.tapes_two line 274
  32. theorem OAI.MinUncutGames.BinaryTokenMachine.update_zero line 277
  33. theorem OAI.MinUncutGames.BinaryTokenMachine.update_one line 283
  34. theorem OAI.MinUncutGames.BinaryTokenMachine.clauseStep line 289
  35. theorem OAI.MinUncutGames.BinaryTokenMachine.finalStep line 295
  36. theorem OAI.MinUncutGames.BinaryTokenMachine.signStep line 301
  37. theorem OAI.MinUncutGames.BinaryTokenMachine.nameEndStep line 308
  38. theorem OAI.MinUncutGames.BinaryTokenMachine.nameDigitStep line 315
  39. theorem OAI.MinUncutGames.BinaryTokenMachine.nameTrace line 323
  40. theorem OAI.MinUncutGames.BinaryTokenMachine.literalTrace line 340
  41. theorem OAI.MinUncutGames.BinaryTokenMachine.joinTrace line 357
  42. theorem OAI.MinUncutGames.BinaryTokenMachine.clauseTrace line 361
  43. def OAI.MinUncutGames.BinaryTokenMachine.tokens line 382
  44. theorem OAI.MinUncutGames.BinaryTokenMachine.tokens_nil line 384
  45. theorem OAI.MinUncutGames.BinaryTokenMachine.tokens_cons line 386
  46. theorem OAI.MinUncutGames.BinaryTokenMachine.tokens_length line 390
  47. theorem OAI.MinUncutGames.BinaryTokenMachine.stripTrace line 399
  48. theorem OAI.MinUncutGames.BinaryTokenMachine.restoreTrace line 431
  49. theorem OAI.MinUncutGames.BinaryTokenMachine.initList_eq line 447
  50. theorem OAI.MinUncutGames.BinaryTokenMachine.haltList_eq line 454
  51. theorem OAI.MinUncutGames.BinaryTokenMachine.acceptTrace line 461
  52. theorem OAI.MinUncutGames.BinaryTokenMachine.haltStep line 479
  53. theorem OAI.MinUncutGames.BinaryTokenMachine.tokenTrace line 484
  54. theorem OAI.MinUncutGames.BinaryTokenMachine.tokenSteps_le line 493
  55. def OAI.MinUncutGames.BinaryTokenMachine.outputsInTime line 499
  56. def OAI.MinUncutGames.BinaryTokenMachine.computableInPolyTime line 506
  57. theorem OAI.MinUncutGames.BinaryTokenMachine.machine_finiteAlphabet line 521
  58. def OAI.MinUncutGames.BinaryRenameWords.clauseLiterals line 531
  59. def OAI.MinUncutGames.BinaryRenameWords.literals line 533
  60. def OAI.MinUncutGames.BinaryRenameWords.token line 535
  61. def OAI.MinUncutGames.BinaryRenameWords.tokens line 538
  62. theorem OAI.MinUncutGames.BinaryRenameWords.literals_nil line 541
  63. theorem OAI.MinUncutGames.BinaryRenameWords.literals_cons line 543
  64. theorem OAI.MinUncutGames.BinaryRenameWords.literals_length line 546
  65. theorem OAI.MinUncutGames.BinaryRenameWords.tokens_length line 552
  66. theorem OAI.MinUncutGames.BinaryRenameWords.literals_names line 555
  67. theorem OAI.MinUncutGames.BinaryRenameWords.tokens_payloads line 560
  68. theorem OAI.MinUncutGames.BinaryRenameWords.token_bits line 565
  69. theorem OAI.MinUncutGames.BinaryRenameWords.tokens_stream line 570
  70. theorem OAI.MinUncutGames.BinaryRenameWords.tokens_canonical line 581
  71. theorem OAI.MinUncutGames.BinaryRenameWords.payload_index line 587
  72. theorem OAI.MinUncutGames.BinaryRenameWords.token_payload_mem line 592
  73. theorem OAI.MinUncutGames.BinaryRenameWords.payloadSize_tokens line 599
  74. def OAI.MinUncutGames.BinaryRenameWords.outputLiteral line 612
  75. def OAI.MinUncutGames.BinaryRenameWords.body line 616
  76. theorem OAI.MinUncutGames.BinaryRenameWords.encoded_clause line 619
  77. theorem OAI.MinUncutGames.BinaryRenameWords.encodeWords_flatMap line 627
  78. theorem OAI.MinUncutGames.BinaryRenameWords.encoded_body line 634
  79. theorem OAI.MinUncutGames.BinaryRenameWords.encoded_renamed line 647
  80. abbrev OAI.MinUncutGames.BinaryHeaderMachine.Alphabet line 665
  81. abbrev OAI.MinUncutGames.BinaryHeaderMachine.State line 666
  82. def OAI.MinUncutGames.BinaryHeaderMachine.delimiter line 672
  83. def OAI.MinUncutGames.BinaryHeaderMachine.tapes line 676
  84. theorem OAI.MinUncutGames.BinaryHeaderMachine.tapes_variables line 681
  85. theorem OAI.MinUncutGames.BinaryHeaderMachine.tapes_clauses line 688
  86. theorem OAI.MinUncutGames.BinaryHeaderMachine.tapes_destination line 695
  87. theorem OAI.MinUncutGames.BinaryHeaderMachine.tapes_other line 701
  88. theorem OAI.MinUncutGames.BinaryHeaderMachine.update_variables line 707
  89. theorem OAI.MinUncutGames.BinaryHeaderMachine.update_clauses line 724
  90. theorem OAI.MinUncutGames.BinaryHeaderMachine.update_destination line 738
  91. theorem OAI.MinUncutGames.BinaryHeaderMachine.clauseDelimiterStep line 757
  92. theorem OAI.MinUncutGames.BinaryHeaderMachine.variableDelimiterStep line 769
  93. theorem OAI.MinUncutGames.BinaryHeaderMachine.clauseCounterTrace line 781
  94. theorem OAI.MinUncutGames.BinaryHeaderMachine.variableCounterTrace line 801
  95. theorem OAI.MinUncutGames.BinaryHeaderMachine.joinTrace line 820
  96. theorem OAI.MinUncutGames.BinaryHeaderMachine.headerTrace line 826
  97. def OAI.MinUncutGames.BinaryHeaderMachine.headerInTime line 855
  98. abbrev OAI.MinUncutGames.BinaryHeaderMachine.ConcreteTape line 870
  99. abbrev OAI.MinUncutGames.BinaryHeaderMachine.ConcreteLabel line 871
  100. def OAI.MinUncutGames.BinaryHeaderMachine.concreteProgram line 873
  101. abbrev OAI.MinUncutGames.BinaryHeaderMachine.machine line 880
  102. def OAI.MinUncutGames.BinaryHeaderMachine.start line 891
  103. theorem OAI.MinUncutGames.BinaryHeaderMachine.haltList_eq line 895
  104. def OAI.MinUncutGames.BinaryHeaderMachine.machineInTime line 903
  105. theorem OAI.MinUncutGames.BinaryHeaderMachine.machine_finiteAlphabet line 913