OAI/Computability/BinPacking/Hardness/LiteralSlotGraphEnumeration.lean

GitHub source file

113 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BinPackingGap.LiteralSlotGraphMachine.twoTapes line 13
  2. theorem OAI.BinPackingGap.LiteralSlotGraphMachine.twoTapes_source line 17
  3. theorem OAI.BinPackingGap.LiteralSlotGraphMachine.twoTapes_destination line 22
  4. theorem OAI.BinPackingGap.LiteralSlotGraphMachine.twoTapes_update_source line 27
  5. theorem OAI.BinPackingGap.LiteralSlotGraphMachine.twoTapes_update_destination line 38
  6. theorem OAI.BinPackingGap.LiteralSlotGraphMachine.readVariable_loop_exec line 44
  7. theorem OAI.BinPackingGap.LiteralSlotGraphMachine.readVariable_exec line 83
  8. theorem OAI.BinPackingGap.LiteralSlotGraphMachine.readSign_exec line 93
  9. abbrev OAI.BinPackingGap.LiteralSlotGraphMachine.RawLiteral line 108
  10. def OAI.BinPackingGap.LiteralSlotGraphMachine.counterHead line 110
  11. def OAI.BinPackingGap.LiteralSlotGraphMachine.comparedControl line 112
  12. def OAI.BinPackingGap.LiteralSlotGraphMachine.comparisonResult line 115
  13. theorem OAI.BinPackingGap.LiteralSlotGraphMachine.counter_head_tail_eq line 118
  14. theorem OAI.BinPackingGap.LiteralSlotGraphMachine.compareGuard_eval line 122
  15. theorem OAI.BinPackingGap.LiteralSlotGraphMachine.comparisonResult_step line 135
  16. theorem OAI.BinPackingGap.LiteralSlotGraphMachine.compareLoop_exec line 140
  17. theorem OAI.BinPackingGap.LiteralSlotGraphMachine.compareVariables_exec line 183
  18. def OAI.BinPackingGap.LiteralSlotGraphMachine.vertexBodyCost line 199
  19. def OAI.BinPackingGap.LiteralSlotGraphMachine.vertexRecord line 202
  20. theorem OAI.BinPackingGap.LiteralSlotGraphMachine.vertexBody_exec line 204
  21. def OAI.BinPackingGap.LiteralSlotGraphMachine.vertexRecords line 233
  22. def OAI.BinPackingGap.LiteralSlotGraphMachine.vertexLoopCost line 237
  23. def OAI.BinPackingGap.LiteralSlotGraphMachine.vertexResult line 241
  24. theorem OAI.BinPackingGap.LiteralSlotGraphMachine.vertices_exec line 246
  25. theorem OAI.BinPackingGap.LiteralSlotGraphMachine.bits_length_le line 285
  26. theorem OAI.BinPackingGap.LiteralSlotGraphMachine.vertexBodyCost_le line 289
  27. theorem OAI.BinPackingGap.LiteralSlotGraphMachine.vertexLoopCost_le line 295
  28. theorem OAI.BinPackingGap.LiteralSlotGraphMachine.vertexRecords_range line 305
  29. theorem OAI.BinPackingGap.LiteralSlotGraphMachine.vertexRecords_listBits line 311
  30. def OAI.BinPackingGap.LiteralSlotGraphMachine.pairRecord line 320
  31. def OAI.BinPackingGap.LiteralSlotGraphMachine.pairCost line 323
  32. theorem OAI.BinPackingGap.LiteralSlotGraphMachine.emitPair_exec line 325
  33. def OAI.BinPackingGap.LiteralSlotGraphMachine.literalBits line 355
  34. def OAI.BinPackingGap.LiteralSlotGraphMachine.literalsBits line 358
  35. def OAI.BinPackingGap.LiteralSlotGraphMachine.bodyEdge line 360
  36. instance OAI.BinPackingGap.LiteralSlotGraphMachine.(instance at line 363) line 363
  37. def OAI.BinPackingGap.LiteralSlotGraphMachine.bodyControl line 367
  38. def OAI.BinPackingGap.LiteralSlotGraphMachine.branchCost line 370
  39. def OAI.BinPackingGap.LiteralSlotGraphMachine.innerBodyCost line 373
  40. def OAI.BinPackingGap.LiteralSlotGraphMachine.bodyAccumulator line 377
  41. def OAI.BinPackingGap.LiteralSlotGraphMachine.innerBodyResult line 382
  42. theorem OAI.BinPackingGap.LiteralSlotGraphMachine.innerBody_exec line 387
  43. theorem OAI.BinPackingGap.LiteralSlotGraphMachine.pairCost_le line 474
  44. theorem OAI.BinPackingGap.LiteralSlotGraphMachine.innerBodyCost_le line 480
  45. def OAI.BinPackingGap.LiteralSlotGraphMachine.rowEdges line 492
  46. def OAI.BinPackingGap.LiteralSlotGraphMachine.suffixEdges line 499
  47. theorem OAI.BinPackingGap.LiteralSlotGraphMachine.literalsBits_cons line 503
  48. theorem OAI.BinPackingGap.LiteralSlotGraphMachine.literalsBits_ne_nil line 506
  49. theorem OAI.BinPackingGap.LiteralSlotGraphMachine.remaining_same_clause line 512
  50. def OAI.BinPackingGap.LiteralSlotGraphMachine.edgeRecords line 516
  51. def OAI.BinPackingGap.LiteralSlotGraphMachine.rowControl line 519
  52. def OAI.BinPackingGap.LiteralSlotGraphMachine.innerLoopCost line 523
  53. def OAI.BinPackingGap.LiteralSlotGraphMachine.innerLoopResult line 528
  54. theorem OAI.BinPackingGap.LiteralSlotGraphMachine.bodyControl_remaining line 534
  55. theorem OAI.BinPackingGap.LiteralSlotGraphMachine.bodyControl_slot line 537
  56. theorem OAI.BinPackingGap.LiteralSlotGraphMachine.bodyControl_outerSign line 540
  57. theorem OAI.BinPackingGap.LiteralSlotGraphMachine.rowControl_slot line 543
  58. theorem OAI.BinPackingGap.LiteralSlotGraphMachine.rowControl_outerSign line 549
  59. theorem OAI.BinPackingGap.LiteralSlotGraphMachine.innerLoop_exec line 555
  60. theorem OAI.BinPackingGap.LiteralSlotGraphMachine.innerLoopCost_le line 628
  61. def OAI.BinPackingGap.LiteralSlotGraphMachine.rowStartControl line 641
  62. def OAI.BinPackingGap.LiteralSlotGraphMachine.outerBodyControl line 644
  63. def OAI.BinPackingGap.LiteralSlotGraphMachine.outerBodyCost line 647
  64. def OAI.BinPackingGap.LiteralSlotGraphMachine.outerBodyResult line 654
  65. theorem OAI.BinPackingGap.LiteralSlotGraphMachine.outerBody_exec line 660
  66. theorem OAI.BinPackingGap.LiteralSlotGraphMachine.outerBodyControl_slot line 754
  67. theorem OAI.BinPackingGap.LiteralSlotGraphMachine.outerBodyCost_le line 758
  68. def OAI.BinPackingGap.LiteralSlotGraphMachine.outerControl line 772
  69. def OAI.BinPackingGap.LiteralSlotGraphMachine.outerLoopCost line 776
  70. def OAI.BinPackingGap.LiteralSlotGraphMachine.outerLoopResult line 781
  71. theorem OAI.BinPackingGap.LiteralSlotGraphMachine.outerLoop_exec line 786
  72. theorem OAI.BinPackingGap.LiteralSlotGraphMachine.outerLoopCost_le line 839
  73. theorem OAI.BinPackingGap.LiteralSlotGraphMachine.skipField_exec line 858
  74. def OAI.BinPackingGap.LiteralSlotGraphMachine.countHeaderResult line 880
  75. theorem OAI.BinPackingGap.LiteralSlotGraphMachine.countHeader_exec line 885
  76. def OAI.BinPackingGap.LiteralSlotGraphMachine.mainTapes line 936
  77. theorem OAI.BinPackingGap.LiteralSlotGraphMachine.mainTapes_input line 945
  78. theorem OAI.BinPackingGap.LiteralSlotGraphMachine.mainTapes_accumulator line 949
  79. theorem OAI.BinPackingGap.LiteralSlotGraphMachine.mainTapes_outerIndex line 953
  80. theorem OAI.BinPackingGap.LiteralSlotGraphMachine.mainTapes_vertexCount line 957
  81. theorem OAI.BinPackingGap.LiteralSlotGraphMachine.mainTapes_unary line 961
  82. theorem OAI.BinPackingGap.LiteralSlotGraphMachine.mainTapes_output line 965
  83. theorem OAI.BinPackingGap.LiteralSlotGraphMachine.mainTapes_scratch line 969
  84. def OAI.BinPackingGap.LiteralSlotGraphMachine.rawInput line 973
  85. def OAI.BinPackingGap.LiteralSlotGraphMachine.rawGraphWord line 976
  86. def OAI.BinPackingGap.LiteralSlotGraphMachine.phaseCosts line 980
  87. def OAI.BinPackingGap.LiteralSlotGraphMachine.rawCost line 988
  88. theorem OAI.BinPackingGap.LiteralSlotGraphMachine.raw_program_exec line 991
  89. def OAI.BinPackingGap.LiteralSlotGraphMachine.rawLiteral line 1110
  90. def OAI.BinPackingGap.LiteralSlotGraphMachine.clauseLiterals line 1113
  91. def OAI.BinPackingGap.LiteralSlotGraphMachine.formulaLiterals line 1116
  92. theorem OAI.BinPackingGap.LiteralSlotGraphMachine.clauseLiterals_length line 1119
  93. theorem OAI.BinPackingGap.LiteralSlotGraphMachine.formulaLiterals_length line 1122
  94. theorem OAI.BinPackingGap.LiteralSlotGraphMachine.clauseLiterals_bits line 1132
  95. theorem OAI.BinPackingGap.LiteralSlotGraphMachine.clausesLiterals_bits line 1137
  96. theorem OAI.BinPackingGap.LiteralSlotGraphMachine.formulaBits_eq_formulaLiterals line 1148
  97. theorem OAI.BinPackingGap.LiteralSlotGraphMachine.literalSlots_le_formulaBits_length line 1154
  98. theorem OAI.BinPackingGap.LiteralSlotGraphMachine.formulaLiterals_eq_ofFn line 1161
  99. abbrev OAI.BinPackingGap.LiteralSlotGraphMachine.TaggedLiteral line 1186
  100. def OAI.BinPackingGap.LiteralSlotGraphMachine.indexFrom line 1188
  101. def OAI.BinPackingGap.LiteralSlotGraphMachine.taggedConflict line 1192
  102. instance OAI.BinPackingGap.LiteralSlotGraphMachine.(instance at line 1195) line 1195
  103. def OAI.BinPackingGap.LiteralSlotGraphMachine.pairEntry line 1199
  104. def OAI.BinPackingGap.LiteralSlotGraphMachine.rowEntry line 1202
  105. def OAI.BinPackingGap.LiteralSlotGraphMachine.forwardRows line 1205
  106. theorem OAI.BinPackingGap.LiteralSlotGraphMachine.rowEdges_eq_filterMap line 1209
  107. theorem OAI.BinPackingGap.LiteralSlotGraphMachine.suffixEdges_eq_forwardRows line 1218
  108. theorem OAI.BinPackingGap.LiteralSlotGraphMachine.indexFrom_ofFn line 1225
  109. theorem OAI.BinPackingGap.LiteralSlotGraphMachine.forwardRows_eq_allPairs line 1236
  110. theorem OAI.BinPackingGap.LiteralSlotGraphMachine.filtered_product line 1256
  111. def OAI.BinPackingGap.LiteralSlotGraphMachine.tagVertex line 1280
  112. theorem OAI.BinPackingGap.LiteralSlotGraphMachine.tagVertex_conflict line 1283
  113. theorem OAI.BinPackingGap.LiteralSlotGraphMachine.suffixEdges_formulaLiterals line 1288