OAI/Computability/BinPacking/Reductions/BinaryTokenMachine.lean

GitHub source file

90 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BinPackingCompleteness.BinaryEncoding.bitsValue_bits line 12
  2. theorem OAI.BinPackingCompleteness.BinaryEncoding.parseFrame_encoded line 19
  3. theorem OAI.BinPackingCompleteness.BinaryEncoding.frame_length line 25
  4. theorem OAI.BinPackingCompleteness.BinaryEncoding.parseName_encoded line 31
  5. theorem OAI.BinPackingCompleteness.BinaryEncoding.nameBits_length line 35
  6. theorem OAI.BinPackingCompleteness.BinaryEncoding.nameBits_length_le_of_lt_pow line 39
  7. def OAI.BinPackingCompleteness.BinaryEncoding.literalBits line 45
  8. def OAI.BinPackingCompleteness.BinaryEncoding.parseLiteral line 48
  9. theorem OAI.BinPackingCompleteness.BinaryEncoding.parseLiteral_encoded line 54
  10. theorem OAI.BinPackingCompleteness.BinaryEncoding.literalBits_length line 59
  11. def OAI.BinPackingCompleteness.BinaryEncoding.clauseBits line 63
  12. def OAI.BinPackingCompleteness.BinaryEncoding.parseClause line 66
  13. theorem OAI.BinPackingCompleteness.BinaryEncoding.clause_three_entries line 72
  14. theorem OAI.BinPackingCompleteness.BinaryEncoding.parseClause_encoded line 78
  15. def OAI.BinPackingCompleteness.BinaryEncoding.clauseNameSize line 82
  16. theorem OAI.BinPackingCompleteness.BinaryEncoding.clauseBits_length line 85
  17. def OAI.BinPackingCompleteness.BinaryEncoding.clausesBits line 90
  18. def OAI.BinPackingCompleteness.BinaryEncoding.formulaBits line 94
  19. def OAI.BinPackingCompleteness.BinaryEncoding.namesBitSize line 96
  20. theorem OAI.BinPackingCompleteness.BinaryEncoding.namesBitSize_nil line 99
  21. theorem OAI.BinPackingCompleteness.BinaryEncoding.namesBitSize_cons line 101
  22. theorem OAI.BinPackingCompleteness.BinaryEncoding.clausesBits_length line 105
  23. theorem OAI.BinPackingCompleteness.BinaryEncoding.formulaBits_length line 114
  24. theorem OAI.BinPackingCompleteness.BinaryEncoding.clauses_length_lt_bits line 119
  25. def OAI.BinPackingCompleteness.BinaryEncoding.ordinarySize line 124
  26. theorem OAI.BinPackingCompleteness.BinaryEncoding.ordinarySize_le_bits line 127
  27. theorem OAI.BinPackingCompleteness.BinaryEncoding.bits_le_three_ordinarySize line 133
  28. def OAI.BinPackingCompleteness.BinaryEncoding.parseClauses line 139
  29. theorem OAI.BinPackingCompleteness.BinaryEncoding.parseClauses_encoded line 148
  30. def OAI.BinPackingCompleteness.BinaryEncoding.decodeFormula line 163
  31. theorem OAI.BinPackingCompleteness.BinaryEncoding.decodeFormula_encoded line 167
  32. theorem OAI.BinPackingCompleteness.BinaryEncoding.formulaBits_injective line 176
  33. theorem OAI.BinPackingCompleteness.BinaryEncoding.dense_encoding_bound line 181
  34. theorem OAI.BinPackingCompleteness.BinaryParsing.frame_eq line 197
  35. theorem OAI.BinPackingCompleteness.BinaryParsing.canonical_cons_cons line 202
  36. theorem OAI.BinPackingCompleteness.BinaryParsing.canonical_iff line 205
  37. theorem OAI.BinPackingCompleteness.BinaryParsing.canonical_nat_bits line 230
  38. theorem OAI.BinPackingCompleteness.BinaryParsing.parseFrame_sound line 235
  39. theorem OAI.BinPackingCompleteness.BinaryParsing.parseName_sound line 259
  40. theorem OAI.BinPackingCompleteness.BinaryParsing.parseLiteral_sound line 275
  41. theorem OAI.BinPackingCompleteness.BinaryParsing.parseClause_sound line 290
  42. theorem OAI.BinPackingCompleteness.BinaryParsing.parseClauses_sound line 314
  43. theorem OAI.BinPackingCompleteness.BinaryParsing.decodeFormula_sound line 342
  44. theorem OAI.BinPackingCompleteness.BinaryParsing.decodeFormula_eq_some_iff line 356
  45. theorem OAI.BinPackingCompleteness.BinaryParsing.scanSpec_nameBits line 360
  46. abbrev OAI.BinPackingCompleteness.BinaryTokenMachine.Tape line 380
  47. abbrev OAI.BinPackingCompleteness.BinaryTokenMachine.Alphabet line 381
  48. abbrev OAI.BinPackingCompleteness.BinaryTokenMachine.State line 382
  49. inductive OAI.BinPackingCompleteness.BinaryTokenMachine.Label line 384
  50. def OAI.BinPackingCompleteness.BinaryTokenMachine.afterName line 393
  51. theorem OAI.BinPackingCompleteness.BinaryTokenMachine.afterName_zero line 396
  52. theorem OAI.BinPackingCompleteness.BinaryTokenMachine.afterName_one line 397
  53. theorem OAI.BinPackingCompleteness.BinaryTokenMachine.afterName_two line 398
  54. def OAI.BinPackingCompleteness.BinaryTokenMachine.jump line 400
  55. def OAI.BinPackingCompleteness.BinaryTokenMachine.clauseInstruction line 403
  56. def OAI.BinPackingCompleteness.BinaryTokenMachine.signInstruction line 410
  57. def OAI.BinPackingCompleteness.BinaryTokenMachine.nameInstruction line 416
  58. def OAI.BinPackingCompleteness.BinaryTokenMachine.program line 428
  59. abbrev OAI.BinPackingCompleteness.BinaryTokenMachine.machine line 436
  60. def OAI.BinPackingCompleteness.BinaryTokenMachine.tapes line 447
  61. def OAI.BinPackingCompleteness.BinaryTokenMachine.cfg line 450
  62. theorem OAI.BinPackingCompleteness.BinaryTokenMachine.tapes_zero line 454
  63. theorem OAI.BinPackingCompleteness.BinaryTokenMachine.tapes_one line 457
  64. theorem OAI.BinPackingCompleteness.BinaryTokenMachine.tapes_two line 460
  65. theorem OAI.BinPackingCompleteness.BinaryTokenMachine.update_zero line 463
  66. theorem OAI.BinPackingCompleteness.BinaryTokenMachine.update_one line 469
  67. theorem OAI.BinPackingCompleteness.BinaryTokenMachine.clauseStep line 475
  68. theorem OAI.BinPackingCompleteness.BinaryTokenMachine.finalStep line 482
  69. theorem OAI.BinPackingCompleteness.BinaryTokenMachine.signStep line 489
  70. theorem OAI.BinPackingCompleteness.BinaryTokenMachine.nameEndStep line 497
  71. theorem OAI.BinPackingCompleteness.BinaryTokenMachine.nameDigitStep line 505
  72. theorem OAI.BinPackingCompleteness.BinaryTokenMachine.nameTrace line 514
  73. theorem OAI.BinPackingCompleteness.BinaryTokenMachine.literalTrace line 531
  74. theorem OAI.BinPackingCompleteness.BinaryTokenMachine.joinTrace line 548
  75. theorem OAI.BinPackingCompleteness.BinaryTokenMachine.clauseTrace line 552
  76. def OAI.BinPackingCompleteness.BinaryTokenMachine.tokens line 573
  77. theorem OAI.BinPackingCompleteness.BinaryTokenMachine.tokens_nil line 575
  78. theorem OAI.BinPackingCompleteness.BinaryTokenMachine.tokens_cons line 577
  79. theorem OAI.BinPackingCompleteness.BinaryTokenMachine.tokens_length line 581
  80. theorem OAI.BinPackingCompleteness.BinaryTokenMachine.stripTrace line 590
  81. theorem OAI.BinPackingCompleteness.BinaryTokenMachine.restoreTrace line 622
  82. theorem OAI.BinPackingCompleteness.BinaryTokenMachine.initList_eq line 638
  83. theorem OAI.BinPackingCompleteness.BinaryTokenMachine.haltList_eq line 645
  84. theorem OAI.BinPackingCompleteness.BinaryTokenMachine.acceptTrace line 652
  85. theorem OAI.BinPackingCompleteness.BinaryTokenMachine.haltStep line 670
  86. theorem OAI.BinPackingCompleteness.BinaryTokenMachine.tokenTrace line 675
  87. theorem OAI.BinPackingCompleteness.BinaryTokenMachine.tokenSteps_le line 684
  88. def OAI.BinPackingCompleteness.BinaryTokenMachine.outputsInTime line 690
  89. def OAI.BinPackingCompleteness.BinaryTokenMachine.computableInPolyTime line 697
  90. theorem OAI.BinPackingCompleteness.BinaryTokenMachine.machine_finiteAlphabet line 712