OAI/Computability/BinPacking/PCP/NormalizationEmitMachine.lean

GitHub source file

167 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.BinPackingCompleteness.SourceClause.Triple line 19
  2. def OAI.BinPackingCompleteness.SourceClause.Triple.at line 21
  3. def OAI.BinPackingCompleteness.SourceClause.literalTruth line 27
  4. def OAI.BinPackingCompleteness.SourceClause.localEval line 30
  5. def OAI.BinPackingCompleteness.SourceClause.allTriples line 34
  6. def OAI.BinPackingCompleteness.SourceClause.satisfyingTriples line 40
  7. theorem OAI.BinPackingCompleteness.SourceClause.mem_allTriples line 43
  8. theorem OAI.BinPackingCompleteness.SourceClause.mem_satisfyingTriples line 47
  9. theorem OAI.BinPackingCompleteness.SourceClause.satisfyingTriples_nodup line 51
  10. theorem OAI.BinPackingCompleteness.SourceClause.satisfyingTriples_length line 56
  11. theorem OAI.BinPackingCompleteness.SourceClause.coordinate_truth_table line 61
  12. theorem OAI.BinPackingCompleteness.SourceClause.coordinate_surjective line 68
  13. theorem OAI.BinPackingCompleteness.SourceClause.pair_truth_table line 74
  14. theorem OAI.BinPackingCompleteness.SourceClause.pair_surjective line 81
  15. structure OAI.BinPackingCompleteness.SourceClause.NormalizedClause line 88
  16. def OAI.BinPackingCompleteness.SourceClause.NormalizedClause.variable line 93
  17. def OAI.BinPackingCompleteness.SourceClause.NormalizedClause.signs line 96
  18. def OAI.BinPackingCompleteness.SourceClause.NormalizedClause.restrict line 99
  19. theorem OAI.BinPackingCompleteness.SourceClause.localEval_restrict line 103
  20. theorem OAI.BinPackingCompleteness.SourceClause.variable_ne line 108
  21. def OAI.BinPackingCompleteness.SourceClause.NormalizedClause.extend line 112
  22. theorem OAI.BinPackingCompleteness.SourceClause.restrict_extend line 116
  23. theorem OAI.BinPackingCompleteness.SourceClause.satisfying_label_realized line 123
  24. abbrev OAI.BinPackingCompleteness.SourceClause.Occurrence line 131
  25. def OAI.BinPackingCompleteness.SourceClause.occurrenceVariable line 133
  26. theorem OAI.BinPackingCompleteness.SourceClause.occurrence_determined_by_endpoints line 137
  27. theorem OAI.BinPackingCompleteness.SourceClause.projection_determined_by_endpoints line 150
  28. def OAI.BinPackingCompleteness.SourceClause.agreementCount line 157
  29. theorem OAI.BinPackingCompleteness.SourceClause.agreementCount_le_three line 163
  30. theorem OAI.BinPackingCompleteness.SourceClause.agreementCount_le_two_of_unsatisfied line 168
  31. theorem OAI.BinPackingCompleteness.SourceClause.agreementCount_le_two_add_satisfied line 188
  32. theorem OAI.BinPackingCompleteness.SourceClause.totalAgreement_le line 197
  33. def OAI.BinPackingCompleteness.Normalization.tripleClause line 219
  34. def OAI.BinPackingCompleteness.Normalization.normalizedTriple line 222
  35. def OAI.BinPackingCompleteness.Normalization.outputVariables line 233
  36. def OAI.BinPackingCompleteness.Normalization.oldVariable line 235
  37. def OAI.BinPackingCompleteness.Normalization.freshVariable line 238
  38. def OAI.BinPackingCompleteness.Normalization.copyVariable line 246
  39. def OAI.BinPackingCompleteness.Normalization.paddingVariable line 250
  40. theorem OAI.BinPackingCompleteness.Normalization.freshVariable_injective line 253
  41. theorem OAI.BinPackingCompleteness.Normalization.copy_ne_copy line 264
  42. theorem OAI.BinPackingCompleteness.Normalization.copy_ne_old line 273
  43. theorem OAI.BinPackingCompleteness.Normalization.copy_ne_padding line 281
  44. theorem OAI.BinPackingCompleteness.Normalization.old_ne_padding line 289
  45. def OAI.BinPackingCompleteness.Normalization.mainClause line 297
  46. def OAI.BinPackingCompleteness.Normalization.equalityClauses line 305
  47. def OAI.BinPackingCompleteness.Normalization.gadget line 318
  48. def OAI.BinPackingCompleteness.Normalization.gadgetClauses line 323
  49. theorem OAI.BinPackingCompleteness.Normalization.equalityClauses_length line 327
  50. theorem OAI.BinPackingCompleteness.Normalization.gadget_length line 330
  51. theorem OAI.BinPackingCompleteness.Normalization.gadgetClauses_length line 333
  52. def OAI.BinPackingCompleteness.Normalization.restrictAssignment line 336
  53. def OAI.BinPackingCompleteness.Normalization.extendAssignment line 339
  54. theorem OAI.BinPackingCompleteness.Normalization.extend_oldVariable line 351
  55. theorem OAI.BinPackingCompleteness.Normalization.extend_copyVariable line 355
  56. theorem OAI.BinPackingCompleteness.Normalization.restrict_extend line 364
  57. theorem OAI.BinPackingCompleteness.Normalization.main_eval_of_copies_match line 369
  58. theorem OAI.BinPackingCompleteness.Normalization.equalityClauses_failures line 377
  59. theorem OAI.BinPackingCompleteness.Normalization.gadget_failures line 390
  60. theorem OAI.BinPackingCompleteness.Normalization.clauseFailures_zero_iff line 405
  61. theorem OAI.BinPackingCompleteness.Normalization.gadget_complete_of_copies_match line 410
  62. theorem OAI.BinPackingCompleteness.Normalization.gadget_failure_domination line 420
  63. theorem OAI.BinPackingCompleteness.Normalization.gadget_failed line 451
  64. def OAI.BinPackingCompleteness.Normalization.normalizedClauses line 457
  65. def OAI.BinPackingCompleteness.Normalization.normalize line 460
  66. theorem OAI.BinPackingCompleteness.Normalization.normalize_clauses_eq_map line 464
  67. theorem OAI.BinPackingCompleteness.Normalization.normalize_distinct line 469
  68. theorem OAI.BinPackingCompleteness.Normalization.normalize_variables line 477
  69. theorem OAI.BinPackingCompleteness.Normalization.normalize_clause_count line 480
  70. theorem OAI.BinPackingCompleteness.Normalization.normalize_nonempty line 487
  71. theorem OAI.BinPackingCompleteness.Normalization.normalize_completeness line 495
  72. theorem OAI.BinPackingCompleteness.Normalization.failedCount_domination line 507
  73. theorem OAI.BinPackingCompleteness.Normalization.normalize_reflects line 518
  74. theorem OAI.BinPackingCompleteness.Normalization.normalize_satisfiable_iff line 529
  75. theorem OAI.BinPackingCompleteness.Normalization.normalize_gap line 533
  76. abbrev OAI.BinPackingCompleteness.NormalizationWords.Signs line 554
  77. abbrev OAI.BinPackingCompleteness.NormalizationWords.Names line 555
  78. inductive OAI.BinPackingCompleteness.NormalizationWords.NameRef line 557
  79. inductive OAI.BinPackingCompleteness.NormalizationWords.SignRef line 562
  80. structure OAI.BinPackingCompleteness.NormalizationWords.LiteralRecipe line 567
  81. def OAI.BinPackingCompleteness.NormalizationWords.sourceValue line 572
  82. def OAI.BinPackingCompleteness.NormalizationWords.offset line 576
  83. def OAI.BinPackingCompleteness.NormalizationWords.nameValue line 580
  84. def OAI.BinPackingCompleteness.NormalizationWords.signValue line 583
  85. def OAI.BinPackingCompleteness.NormalizationWords.literalWords line 587
  86. def OAI.BinPackingCompleteness.NormalizationWords.literalBits line 591
  87. def OAI.BinPackingCompleteness.NormalizationWords.mainRecipe line 595
  88. def OAI.BinPackingCompleteness.NormalizationWords.equalityRecipe line 598
  89. def OAI.BinPackingCompleteness.NormalizationWords.recipe line 604
  90. theorem OAI.BinPackingCompleteness.NormalizationWords.recipe_length line 607
  91. def OAI.BinPackingCompleteness.NormalizationWords.words line 609
  92. def OAI.BinPackingCompleteness.NormalizationWords.bits line 612
  93. def OAI.BinPackingCompleteness.NormalizationWords.clauseSigns line 615
  94. def OAI.BinPackingCompleteness.NormalizationWords.clauseNames line 617
  95. theorem OAI.BinPackingCompleteness.NormalizationWords.encodeWords_flatMap line 619
  96. theorem OAI.BinPackingCompleteness.NormalizationWords.bits_eq_flatMap line 625
  97. theorem OAI.BinPackingCompleteness.NormalizationWords.gadget_words line 629
  98. theorem OAI.BinPackingCompleteness.NormalizationWords.gadget_bits line 641
  99. def OAI.BinPackingCompleteness.NormalizationWords.body line 648
  100. theorem OAI.BinPackingCompleteness.NormalizationWords.encoded_body line 653
  101. theorem OAI.BinPackingCompleteness.NormalizationWords.encoded_normalize line 661
  102. def OAI.BinPackingCompleteness.SourceGame.decodeLabel line 678
  103. theorem OAI.BinPackingCompleteness.SourceGame.decodeLabel_mem line 683
  104. theorem OAI.BinPackingCompleteness.SourceGame.decodeLabel_legal line 687
  105. theorem OAI.BinPackingCompleteness.SourceGame.decodeLabel_injective line 691
  106. def OAI.BinPackingCompleteness.SourceGame.encodeLabel line 696
  107. theorem OAI.BinPackingCompleteness.SourceGame.decodeLabel_encodeLabel line 701
  108. def OAI.BinPackingCompleteness.SourceGame.projection line 706
  109. theorem OAI.BinPackingCompleteness.SourceGame.projection_surjective line 710
  110. theorem OAI.BinPackingCompleteness.SourceGame.projection_pair_surjective line 718
  111. theorem OAI.BinPackingCompleteness.SourceGame.leftAlphabet_card line 726
  112. theorem OAI.BinPackingCompleteness.SourceGame.rightAlphabet_card line 727
  113. def OAI.BinPackingCompleteness.SourceGame.game line 731
  114. theorem OAI.BinPackingCompleteness.SourceGame.endpointDetermined line 736
  115. def OAI.BinPackingCompleteness.SourceGame.endpointPredicate line 743
  116. theorem OAI.BinPackingCompleteness.SourceGame.endpointPredicate_eq_true line 748
  117. def OAI.BinPackingCompleteness.SourceGame.presentation line 755
  118. def OAI.BinPackingCompleteness.SourceGame.questionGame line 769
  119. theorem OAI.BinPackingCompleteness.SourceGame.questionGame_success line 773
  120. theorem OAI.BinPackingCompleteness.SourceGame.restrict_at line 778
  121. def OAI.BinPackingCompleteness.SourceGame.completenessStrategy line 784
  122. theorem OAI.BinPackingCompleteness.SourceGame.completeness_wins line 790
  123. theorem OAI.BinPackingCompleteness.SourceGame.completeness_success line 798
  124. theorem OAI.BinPackingCompleteness.SourceGame.completeness_value line 807
  125. def OAI.BinPackingCompleteness.SourceGame.winCount line 815
  126. def OAI.BinPackingCompleteness.SourceGame.violatedCount line 819
  127. theorem OAI.BinPackingCompleteness.SourceGame.winCount_add_violated_le line 823
  128. theorem OAI.BinPackingCompleteness.SourceGame.probability_uniform line 839
  129. theorem OAI.BinPackingCompleteness.SourceGame.success_eq_winCount_div line 849
  130. theorem OAI.BinPackingCompleteness.SourceGame.success_le_one_sub_third_violations line 869
  131. abbrev OAI.BinPackingCompleteness.NormalizationEmitMachine.Alphabet line 902
  132. abbrev OAI.BinPackingCompleteness.NormalizationEmitMachine.State line 903
  133. def OAI.BinPackingCompleteness.NormalizationEmitMachine.clean line 905
  134. def OAI.BinPackingCompleteness.NormalizationEmitMachine.sourceIndex line 907
  135. theorem OAI.BinPackingCompleteness.NormalizationEmitMachine.sourceIndex_ne_scratch line 911
  136. theorem OAI.BinPackingCompleteness.NormalizationEmitMachine.sourceIndex_ne_output line 921
  137. inductive OAI.BinPackingCompleteness.NormalizationEmitMachine.LocalLabel line 931
  138. abbrev OAI.BinPackingCompleteness.NormalizationEmitMachine.LocalLabel.enumList line 937
  139. theorem OAI.BinPackingCompleteness.NormalizationEmitMachine.LocalLabel.enumList_getElem?_ctorIdx_eq line 939
  140. theorem OAI.BinPackingCompleteness.NormalizationEmitMachine.LocalLabel.enumList_nodup line 943
  141. instance OAI.BinPackingCompleteness.NormalizationEmitMachine.(instance at line 945) line 945
  142. def OAI.BinPackingCompleteness.NormalizationEmitMachine.emitSign line 949
  143. def OAI.BinPackingCompleteness.NormalizationEmitMachine.emit line 956
  144. def OAI.BinPackingCompleteness.NormalizationEmitMachine.localInstruction line 961
  145. theorem OAI.BinPackingCompleteness.NormalizationEmitMachine.joinTrace line 970
  146. theorem OAI.BinPackingCompleteness.NormalizationEmitMachine.stepAux_emit line 974
  147. theorem OAI.BinPackingCompleteness.NormalizationEmitMachine.literalTrace line 1005
  148. def OAI.BinPackingCompleteness.NormalizationEmitMachine.result line 1035
  149. def OAI.BinPackingCompleteness.NormalizationEmitMachine.cost line 1039
  150. def OAI.BinPackingCompleteness.NormalizationEmitMachine.commandSteps line 1042
  151. theorem OAI.BinPackingCompleteness.NormalizationEmitMachine.resultOf_eq line 1045
  152. theorem OAI.BinPackingCompleteness.NormalizationEmitMachine.sequenceSteps_eq line 1055
  153. theorem OAI.BinPackingCompleteness.NormalizationEmitMachine.sourceValue_le line 1065
  154. theorem OAI.BinPackingCompleteness.NormalizationEmitMachine.commandSteps_le line 1072
  155. abbrev OAI.BinPackingCompleteness.NormalizationEmitMachine.Labels line 1084
  156. def OAI.BinPackingCompleteness.NormalizationEmitMachine.sequenceInstruction line 1087
  157. def OAI.BinPackingCompleteness.NormalizationEmitMachine.sequenceEntry line 1093
  158. theorem OAI.BinPackingCompleteness.NormalizationEmitMachine.sequenceTrace line 1098
  159. abbrev OAI.BinPackingCompleteness.NormalizationEmitMachine.Label line 1127
  160. def OAI.BinPackingCompleteness.NormalizationEmitMachine.main line 1129
  161. def OAI.BinPackingCompleteness.NormalizationEmitMachine.instruction line 1131
  162. def OAI.BinPackingCompleteness.NormalizationEmitMachine.steps line 1135
  163. theorem OAI.BinPackingCompleteness.NormalizationEmitMachine.steps_le line 1137
  164. theorem OAI.BinPackingCompleteness.NormalizationEmitMachine.gadgetTrace line 1143
  165. def OAI.BinPackingCompleteness.NormalizationEmitMachine.gadgetInTime line 1167
  166. theorem OAI.BinPackingCompleteness.NormalizationEmitMachine.label_finite line 1187
  167. theorem OAI.BinPackingCompleteness.NormalizationEmitMachine.state_finite line 1189