OAI/Computability/BinPacking/Search/SearchInitializeEncoding.lean

GitHub source file

136 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BinPackingGap.ExtensionQuery.Agrees line 12
  2. def OAI.BinPackingGap.ExtensionQuery.Ext line 16
  3. theorem OAI.BinPackingGap.ExtensionQuery.agrees_nil_left line 20
  4. theorem OAI.BinPackingGap.ExtensionQuery.agrees_nil_right line 26
  5. theorem OAI.BinPackingGap.ExtensionQuery.agrees_cons line 32
  6. theorem OAI.BinPackingGap.ExtensionQuery.agrees_replicate_none line 61
  7. theorem OAI.BinPackingGap.ExtensionQuery.agrees_map_some line 71
  8. theorem OAI.BinPackingGap.ExtensionQuery.ext_none_iff line 81
  9. theorem OAI.BinPackingGap.ExtensionQuery.ext_full_iff line 92
  10. theorem OAI.BinPackingGap.ExtensionQuery.ext_fixed_length line 104
  11. theorem OAI.BinPackingGap.ExtensionQuery.ext_iff_exists_packing line 110
  12. theorem OAI.BinPackingGap.ExtensionQuery.ext_none_iff_hasPacking line 128
  13. theorem OAI.BinPackingGap.SearchSemantics.get_some_of_lt line 140
  14. theorem OAI.BinPackingGap.SearchSemantics.mem_of_get_some line 149
  15. theorem OAI.BinPackingGap.SearchSemantics.get_set_same line 161
  16. theorem OAI.BinPackingGap.SearchSemantics.get_set_other line 170
  17. def OAI.BinPackingGap.SearchSemantics.Prefix line 177
  18. theorem OAI.BinPackingGap.SearchSemantics.prefix_none line 181
  19. theorem OAI.BinPackingGap.SearchSemantics.prefix_set line 189
  20. theorem OAI.BinPackingGap.SearchSemantics.agrees_set line 203
  21. theorem OAI.BinPackingGap.SearchSemantics.ext_next_exists line 215
  22. def OAI.BinPackingGap.SearchSemantics.labels line 224
  23. theorem OAI.BinPackingGap.SearchSemantics.labels_eq_of_complete line 227
  24. theorem OAI.BinPackingGap.SearchSemantics.ext_complete line 241
  25. inductive OAI.BinPackingGap.SearchSemantics.Phase line 247
  26. structure OAI.BinPackingGap.SearchSemantics.State line 251
  27. def OAI.BinPackingGap.SearchSemantics.initial line 260
  28. def OAI.BinPackingGap.SearchSemantics.query line 266
  29. def OAI.BinPackingGap.SearchSemantics.update line 273
  30. def OAI.BinPackingGap.SearchSemantics.step line 286
  31. def OAI.BinPackingGap.SearchSemantics.run line 288
  32. theorem OAI.BinPackingGap.SearchSemantics.run_eq_iterate line 292
  33. def OAI.BinPackingGap.SearchSemantics.queryTrace line 299
  34. theorem OAI.BinPackingGap.SearchSemantics.queryTrace_length line 303
  35. def OAI.BinPackingGap.SearchSemantics.fuel line 309
  36. def OAI.BinPackingGap.SearchSemantics.output line 311
  37. def OAI.BinPackingGap.SearchSemantics.search line 316
  38. def OAI.BinPackingGap.SearchSemantics.DecidesExtension line 319
  39. theorem OAI.BinPackingGap.SearchSemantics.update_items line 322
  40. theorem OAI.BinPackingGap.SearchSemantics.step_done line 326
  41. theorem OAI.BinPackingGap.SearchSemantics.step_invalid line 329
  42. theorem OAI.BinPackingGap.SearchSemantics.run_done line 332
  43. theorem OAI.BinPackingGap.SearchSemantics.run_invalid line 338
  44. theorem OAI.BinPackingGap.SearchSemantics.ext_none_opt_iff line 344
  45. theorem OAI.BinPackingGap.SearchSemantics.opt_pos line 355
  46. structure OAI.BinPackingGap.SearchSemantics.FindInvariant line 361
  47. structure OAI.BinPackingGap.SearchSemantics.FillInvariant line 368
  48. structure OAI.BinPackingGap.SearchSemantics.DoneInvariant line 378
  49. def OAI.BinPackingGap.SearchSemantics.Invariant line 386
  50. theorem OAI.BinPackingGap.SearchSemantics.find_smaller_infeasible line 393
  51. theorem OAI.BinPackingGap.SearchSemantics.initial_invariant line 401
  52. theorem OAI.BinPackingGap.SearchSemantics.step_invariant line 421
  53. theorem OAI.BinPackingGap.SearchSemantics.index_of_mem line 506
  54. theorem OAI.BinPackingGap.SearchSemantics.ext_label_lt line 517
  55. theorem OAI.BinPackingGap.SearchSemantics.invariant_bounds line 523
  56. def OAI.BinPackingGap.SearchSemantics.rank line 562
  57. theorem OAI.BinPackingGap.SearchSemantics.rank_pos line 568
  58. theorem OAI.BinPackingGap.SearchSemantics.rank_step_lt line 589
  59. theorem OAI.BinPackingGap.SearchSemantics.rank_initial_le line 629
  60. theorem OAI.BinPackingGap.SearchSemantics.run_finishes line 634
  61. theorem OAI.BinPackingGap.SearchSemantics.run_invariant line 653
  62. theorem OAI.BinPackingGap.SearchSemantics.search_optimal line 660
  63. theorem OAI.BinPackingGap.SearchSemantics.search_empty line 675
  64. theorem OAI.BinPackingGap.SearchSemantics.search_invalid line 679
  65. theorem OAI.BinPackingGap.SearchSemantics.fuel_eq_query_bound line 683
  66. theorem OAI.BinPackingGap.SearchSemantics.fuel_empty line 687
  67. theorem OAI.BinPackingGap.SearchSemantics.search_query_count line 689
  68. def OAI.BinPackingGap.ExtensionCertificate.validItems line 700
  69. def OAI.BinPackingGap.ExtensionCertificate.agreesBool line 703
  70. def OAI.BinPackingGap.ExtensionCertificate.capacityCheck line 710
  71. def OAI.BinPackingGap.ExtensionCertificate.check line 714
  72. def OAI.BinPackingGap.ExtensionCertificate.verify line 722
  73. def OAI.BinPackingGap.ExtensionCertificate.language line 728
  74. theorem OAI.BinPackingGap.ExtensionCertificate.validItems_eq_true_iff line 733
  75. theorem OAI.BinPackingGap.ExtensionCertificate.agreesBool_eq_true_iff line 737
  76. theorem OAI.BinPackingGap.ExtensionCertificate.capacityCheck_eq_true_iff line 747
  77. theorem OAI.BinPackingGap.ExtensionCertificate.capacityCheck_eq_true_iff_load line 754
  78. theorem OAI.BinPackingGap.ExtensionCertificate.check_eq_true_iff line 761
  79. theorem OAI.BinPackingGap.ExtensionCertificate.verify_encoded line 785
  80. theorem OAI.BinPackingGap.ExtensionCertificate.language_extensionBits line 791
  81. theorem OAI.BinPackingGap.ExtensionCertificate.verify_sound line 796
  82. theorem OAI.BinPackingGap.ExtensionCertificate.verify_complete line 815
  83. def OAI.BinPackingGap.SearchEncoding.phaseBits line 834
  84. def OAI.BinPackingGap.SearchEncoding.parsePhase line 840
  85. theorem OAI.BinPackingGap.SearchEncoding.phaseBits_length line 847
  86. theorem OAI.BinPackingGap.SearchEncoding.parsePhase_phaseBits line 850
  87. def OAI.BinPackingGap.SearchEncoding.parseUnary line 854
  88. theorem OAI.BinPackingGap.SearchEncoding.parseUnary_encodeWord line 861
  89. def OAI.BinPackingGap.SearchEncoding.fixedBits line 871
  90. def OAI.BinPackingGap.SearchEncoding.parseFixed line 874
  91. theorem OAI.BinPackingGap.SearchEncoding.parseFixed_fixedBits line 876
  92. def OAI.BinPackingGap.SearchEncoding.stateBits line 881
  93. def OAI.BinPackingGap.SearchEncoding.parseState line 885
  94. def OAI.BinPackingGap.SearchEncoding.decodeState line 894
  95. theorem OAI.BinPackingGap.SearchEncoding.parseState_stateBits line 896
  96. theorem OAI.BinPackingGap.SearchEncoding.decodeState_stateBits line 901
  97. theorem OAI.BinPackingGap.SearchEncoding.stateBits_injective line 904
  98. theorem OAI.BinPackingGap.SearchEncoding.stateBits_length line 907
  99. theorem OAI.BinPackingGap.SearchEncoding.label_le_stateBits_length line 913
  100. theorem OAI.BinPackingGap.SearchEncoding.size_le_self line 917
  101. theorem OAI.BinPackingGap.SearchEncoding.listBits_set_length_le line 923
  102. theorem OAI.BinPackingGap.SearchEncoding.fixedBits_set_length_le line 937
  103. theorem OAI.BinPackingGap.SearchEncoding.update_label_le line 947
  104. theorem OAI.BinPackingGap.SearchEncoding.update_length_le line 951
  105. theorem OAI.BinPackingGap.SearchEncoding.step_label_le line 957
  106. theorem OAI.BinPackingGap.SearchEncoding.step_length_le line 960
  107. theorem OAI.BinPackingGap.SearchEncoding.iterate_label_le line 964
  108. theorem OAI.BinPackingGap.SearchEncoding.iterate_length_le line 973
  109. def OAI.BinPackingGap.SearchEncoding.growthPolynomial line 984
  110. theorem OAI.BinPackingGap.SearchEncoding.growthBound line 987
  111. def OAI.BinPackingGap.SearchMachineComposition.prepare line 1016
  112. def OAI.BinPackingGap.SearchMachineComposition.applyAnswer line 1018
  113. def OAI.BinPackingGap.SearchMachineComposition.«initialize» line 1020
  114. def OAI.BinPackingGap.SearchMachineComposition.algorithm line 1027
  115. theorem OAI.BinPackingGap.SearchMachineComposition.algorithm_eq_search line 1030
  116. theorem OAI.BinPackingGap.SearchMachineComposition.algorithm_encoded line 1042
  117. theorem OAI.BinPackingGap.SearchMachineComposition.algorithm_malformed line 1047
  118. theorem OAI.BinPackingGap.SearchMachineComposition.algorithm_invalid line 1052
  119. theorem OAI.BinPackingGap.SearchMachineComposition.algorithm_empty line 1062
  120. theorem OAI.BinPackingGap.SearchMachineComposition.algorithm_optimal line 1066
  121. structure OAI.BinPackingGap.SearchMachineComposition.Stages line 1075
  122. def OAI.BinPackingGap.SearchMachineComposition.bodyComputation line 1089
  123. theorem OAI.BinPackingGap.SearchMachineComposition.bodyComputation_finiteAlphabet line 1100
  124. def OAI.BinPackingGap.SearchMachineComposition.loopComputation line 1110
  125. theorem OAI.BinPackingGap.SearchMachineComposition.loopComputation_finiteAlphabet line 1118
  126. def OAI.BinPackingGap.SearchMachineComposition.computation line 1127
  127. theorem OAI.BinPackingGap.SearchMachineComposition.computation_finiteAlphabet line 1138
  128. theorem OAI.BinPackingGap.SearchOptimalConstruction.decidesExtension_of_language line 1153
  129. def OAI.BinPackingGap.SearchOptimalConstruction.ofDecision line 1160
  130. theorem OAI.BinPackingGap.SearchOptimalConstruction.exists_of_stages_and_membership line 1175
  131. abbrev OAI.BinPackingGap.SearchInitializeEncoding.Data line 1187
  132. def OAI.BinPackingGap.SearchInitializeEncoding.shapeBits line 1189
  133. def OAI.BinPackingGap.SearchInitializeEncoding.classify line 1192
  134. def OAI.BinPackingGap.SearchInitializeEncoding.dataBits line 1197
  135. def OAI.BinPackingGap.SearchInitializeEncoding.emit line 1200
  136. theorem OAI.BinPackingGap.SearchInitializeEncoding.emit_classify line 1204