OAI/Computability/BinPacking/Search/ExtensionCapacityBounds.lean

GitHub source file

118 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BinPackingGap.ExtensionWitness.bound line 15
  2. def OAI.BinPackingGap.ExtensionWitness.witnessPolynomial line 17
  3. theorem OAI.BinPackingGap.ExtensionWitness.witnessPolynomial_eval line 20
  4. theorem OAI.BinPackingGap.ExtensionWitness.bins_size_le_input line 24
  5. theorem OAI.BinPackingGap.ExtensionWitness.items_length_le_input line 30
  6. theorem OAI.BinPackingGap.ExtensionWitness.denominatorBits_le_rawInstanceBits line 38
  7. theorem OAI.BinPackingGap.ExtensionWitness.denominatorBits_le_input line 47
  8. theorem OAI.BinPackingGap.ExtensionWitness.denominatorBits_append line 54
  9. theorem OAI.BinPackingGap.ExtensionWitness.assignmentBits_length_le line 59
  10. theorem OAI.BinPackingGap.ExtensionWitness.assignmentBits_length_le_bound line 77
  11. theorem OAI.BinPackingGap.ExtensionWitness.load_den_width_le_input line 92
  12. theorem OAI.BinPackingGap.ExtensionWitness.load_num_width_le_input line 100
  13. theorem OAI.BinPackingGap.ExtensionWitness.scan_operands_width_le_input line 109
  14. theorem OAI.BinPackingGap.ExtensionWitness.scan_step_width_le_input line 128
  15. theorem OAI.BinPackingGap.ExtensionWitness.exists_bounded_witness line 149
  16. theorem OAI.BinPackingGap.ExtensionWitness.language_iff_bounded_witness line 170
  17. inductive OAI.BinPackingGap.ExtensionFractionMachine.Product line 187
  18. abbrev OAI.BinPackingGap.ExtensionFractionMachine.Product.enumList line 191
  19. theorem OAI.BinPackingGap.ExtensionFractionMachine.Product.enumList_getElem?_ctorIdx_eq line 194
  20. theorem OAI.BinPackingGap.ExtensionFractionMachine.Product.enumList_nodup line 198
  21. instance OAI.BinPackingGap.ExtensionFractionMachine.(instance at line 200) line 200
  22. inductive OAI.BinPackingGap.ExtensionFractionMachine.Label line 204
  23. abbrev OAI.BinPackingGap.ExtensionFractionMachine.State line 210
  24. abbrev OAI.BinPackingGap.ExtensionFractionMachine.Alphabet line 211
  25. abbrev OAI.BinPackingGap.ExtensionFractionMachine.Tape line 213
  26. def OAI.BinPackingGap.ExtensionFractionMachine.productTapes line 215
  27. def OAI.BinPackingGap.ExtensionFractionMachine.productExit line 223
  28. def OAI.BinPackingGap.ExtensionFractionMachine.statement line 230
  29. def OAI.BinPackingGap.ExtensionFractionMachine.program line 242
  30. def OAI.BinPackingGap.ExtensionFractionMachine.machine line 245
  31. def OAI.BinPackingGap.ExtensionFractionMachine.leftProduct line 256
  32. def OAI.BinPackingGap.ExtensionFractionMachine.rightProduct line 259
  33. def OAI.BinPackingGap.ExtensionFractionMachine.nextNumerator line 262
  34. def OAI.BinPackingGap.ExtensionFractionMachine.nextDenominator line 266
  35. def OAI.BinPackingGap.ExtensionFractionMachine.steps line 269
  36. theorem OAI.BinPackingGap.ExtensionFractionMachine.nextNumerator_bits line 277
  37. theorem OAI.BinPackingGap.ExtensionFractionMachine.nextDenominator_bits line 282
  38. theorem OAI.BinPackingGap.ExtensionFractionMachine.machine_finiteAlphabet line 286
  39. theorem OAI.BinPackingGap.ExtensionFractionMachine.workspace_multiply line 291
  40. theorem OAI.BinPackingGap.ExtensionFractionMachine.workspace_update line 304
  41. def OAI.BinPackingGap.ExtensionFractionMachine.resultTapes line 312
  42. def OAI.BinPackingGap.ExtensionFractionMachine.arithmeticBudget line 317
  43. def OAI.BinPackingGap.ExtensionFractionMachine.arithmeticInTime line 324
  44. def OAI.BinPackingGap.ExtensionFractionMachine.timePolynomial line 487
  45. theorem OAI.BinPackingGap.ExtensionFractionMachine.arithmeticBudget_le line 490
  46. def OAI.BinPackingGap.ExtensionFractionMachine.arithmeticInPolynomialTime line 517
  47. inductive OAI.BinPackingGap.ExtensionCapacityMachine.Field line 543
  48. abbrev OAI.BinPackingGap.ExtensionCapacityMachine.Field.enumList line 547
  49. theorem OAI.BinPackingGap.ExtensionCapacityMachine.Field.enumList_getElem?_ctorIdx_eq line 549
  50. theorem OAI.BinPackingGap.ExtensionCapacityMachine.Field.enumList_nodup line 553
  51. instance OAI.BinPackingGap.ExtensionCapacityMachine.(instance at line 555) line 555
  52. inductive OAI.BinPackingGap.ExtensionCapacityMachine.Compare line 559
  53. abbrev OAI.BinPackingGap.ExtensionCapacityMachine.Compare.enumList line 563
  54. theorem OAI.BinPackingGap.ExtensionCapacityMachine.Compare.enumList_getElem?_ctorIdx_eq line 565
  55. theorem OAI.BinPackingGap.ExtensionCapacityMachine.Compare.enumList_nodup line 569
  56. instance OAI.BinPackingGap.ExtensionCapacityMachine.(instance at line 571) line 571
  57. inductive OAI.BinPackingGap.ExtensionCapacityMachine.Label line 575
  58. abbrev OAI.BinPackingGap.ExtensionCapacityMachine.Tape line 585
  59. abbrev OAI.BinPackingGap.ExtensionCapacityMachine.Alphabet line 586
  60. abbrev OAI.BinPackingGap.ExtensionCapacityMachine.State line 587
  61. def OAI.BinPackingGap.ExtensionCapacityMachine.numberTapes line 589
  62. def OAI.BinPackingGap.ExtensionCapacityMachine.compareTapes line 594
  63. def OAI.BinPackingGap.ExtensionCapacityMachine.fractionTapes line 598
  64. def OAI.BinPackingGap.ExtensionCapacityMachine.afterNumber line 601
  65. def OAI.BinPackingGap.ExtensionCapacityMachine.comparisonExits line 606
  66. def OAI.BinPackingGap.ExtensionCapacityMachine.finish line 615
  67. def OAI.BinPackingGap.ExtensionCapacityMachine.statement line 619
  68. def OAI.BinPackingGap.ExtensionCapacityMachine.allTapes line 666
  69. inductive OAI.BinPackingGap.ExtensionCapacityMachine.FullLabel line 668
  70. def OAI.BinPackingGap.ExtensionCapacityMachine.cleanupEntry line 675
  71. def OAI.BinPackingGap.ExtensionCapacityMachine.program line 678
  72. def OAI.BinPackingGap.ExtensionCapacityMachine.machine line 688
  73. theorem OAI.BinPackingGap.ExtensionCapacityMachine.machine_finiteAlphabet line 699
  74. def OAI.BinPackingGap.ExtensionCapacityMachine.inputTapes line 703
  75. def OAI.BinPackingGap.ExtensionCapacityMachine.initialTapes line 712
  76. def OAI.BinPackingGap.ExtensionCapacityMachine.initialCfg line 719
  77. def OAI.BinPackingGap.ExtensionCapacityMachine.finalTapes line 722
  78. def OAI.BinPackingGap.ExtensionCapacityMachine.finalCfg line 724
  79. def OAI.BinPackingGap.ExtensionCapacityMachine.inputLength line 727
  80. def OAI.BinPackingGap.ExtensionCapacityMachine.timePolynomial line 731
  81. theorem OAI.BinPackingGap.ExtensionCapacityMachine.initializeStep line 734
  82. theorem OAI.BinPackingGap.ExtensionCapacityMachine.cleanup_tapes line 745
  83. def OAI.BinPackingGap.ExtensionCapacityMachine.cleanupInTime line 751
  84. def OAI.BinPackingGap.ExtensionArithmeticBounds.timePolynomial line 799
  85. theorem OAI.BinPackingGap.ExtensionArithmeticBounds.timePolynomial_eval line 802
  86. theorem OAI.BinPackingGap.ExtensionArithmeticBounds.fractionTime_le line 806
  87. theorem OAI.BinPackingGap.ExtensionArithmeticBounds.scan_arithmeticBudget_le_input line 817
  88. theorem OAI.BinPackingGap.ExtensionArithmeticBounds.visit_budget_le line 833
  89. def OAI.BinPackingGap.ExtensionCapacityMachine.clean line 854
  90. def OAI.BinPackingGap.ExtensionCapacityMachine.cfg line 856
  91. def OAI.BinPackingGap.ExtensionCapacityMachine.work line 859
  92. def OAI.BinPackingGap.ExtensionCapacityMachine.ready line 874
  93. theorem OAI.BinPackingGap.ExtensionCapacityMachine.update0 line 879
  94. theorem OAI.BinPackingGap.ExtensionCapacityMachine.update1 line 882
  95. theorem OAI.BinPackingGap.ExtensionCapacityMachine.update2 line 885
  96. theorem OAI.BinPackingGap.ExtensionCapacityMachine.update3 line 888
  97. theorem OAI.BinPackingGap.ExtensionCapacityMachine.update5 line 891
  98. theorem OAI.BinPackingGap.ExtensionCapacityMachine.update6 line 894
  99. theorem OAI.BinPackingGap.ExtensionCapacityMachine.update7 line 897
  100. theorem OAI.BinPackingGap.ExtensionCapacityMachine.update10 line 900
  101. theorem OAI.BinPackingGap.ExtensionCapacityMachine.update11 line 903
  102. theorem OAI.BinPackingGap.ExtensionCapacityMachine.update12 line 906
  103. def OAI.BinPackingGap.ExtensionCapacityMachine.oneStep line 910
  104. def OAI.BinPackingGap.ExtensionCapacityMachine.join line 916
  105. def OAI.BinPackingGap.ExtensionCapacityMachine.enlarge line 924
  106. theorem OAI.BinPackingGap.ExtensionCapacityMachine.guard_cons_step line 931
  107. theorem OAI.BinPackingGap.ExtensionCapacityMachine.guard_nil_step line 940
  108. def OAI.BinPackingGap.ExtensionCapacityMachine.numberInTime line 949
  109. def OAI.BinPackingGap.ExtensionCapacityMachine.parseRowInTime line 966
  110. def OAI.BinPackingGap.ExtensionCapacityMachine.compareInTime line 989
  111. theorem OAI.BinPackingGap.ExtensionCapacityMachine.labelComparisonExit line 1009
  112. theorem OAI.BinPackingGap.ExtensionCapacityMachine.capacityComparisonExit line 1018
  113. def OAI.BinPackingGap.ExtensionCapacityMachine.fractionInTime line 1025
  114. def OAI.BinPackingGap.ExtensionCapacityMachine.clearRowInTime line 1056
  115. def OAI.BinPackingGap.ExtensionCapacityMachine.installInTime line 1075
  116. def OAI.BinPackingGap.ExtensionCapacityMachine.rowCost line 1118
  117. theorem OAI.BinPackingGap.ExtensionCapacityMachine.rowCost_le line 1128
  118. theorem OAI.BinPackingGap.ExtensionCapacityMachine.next_denominator_budget line 1154