OAI/Computability/DirectedFeedback/Encoding/FormulaEncoding.lean

GitHub source file

121 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DFVSGames.Foundations.Complexity.parseLiteral line 11
  2. theorem OAI.DFVSGames.Foundations.Complexity.parseLiteral_encoded line 20
  3. def OAI.DFVSGames.Foundations.Complexity.parseClause line 26
  4. theorem OAI.DFVSGames.Foundations.Complexity.clause_three_entries line 32
  5. theorem OAI.DFVSGames.Foundations.Complexity.parseClause_encoded line 39
  6. def OAI.DFVSGames.Foundations.Complexity.parseClauses line 44
  7. theorem OAI.DFVSGames.Foundations.Complexity.parseClauses_encoded line 51
  8. def OAI.DFVSGames.Foundations.Complexity.decodeFormulaWords line 58
  9. theorem OAI.DFVSGames.Foundations.Complexity.decodeFormulaWords_encoded line 64
  10. def OAI.DFVSGames.Foundations.Complexity.decodeFormulaBits line 72
  11. theorem OAI.DFVSGames.Foundations.Complexity.decodeFormulaBits_encoded line 75
  12. theorem OAI.DFVSGames.Foundations.Complexity.formulaBits_injective line 79
  13. def OAI.DFVSGames.Foundations.Complexity.parseLabel line 91
  14. theorem OAI.DFVSGames.Foundations.Complexity.parseLabel_value line 94
  15. theorem OAI.DFVSGames.Foundations.Complexity.parseLabels_values line 97
  16. def OAI.DFVSGames.Foundations.Complexity.parseImages line 103
  17. theorem OAI.DFVSGames.Foundations.Complexity.parseImages_values line 109
  18. def OAI.DFVSGames.Foundations.Complexity.findPreimage line 116
  19. theorem OAI.DFVSGames.Foundations.Complexity.findPreimage_permutation line 119
  20. def OAI.DFVSGames.Foundations.Complexity.searchedInverse line 138
  21. theorem OAI.DFVSGames.Foundations.Complexity.searchedInverse_permutation line 141
  22. def OAI.DFVSGames.Foundations.Complexity.tableWords line 147
  23. def OAI.DFVSGames.Foundations.Complexity.parsePermutation line 150
  24. theorem OAI.DFVSGames.Foundations.Complexity.parsePermutation_encoded line 159
  25. theorem OAI.DFVSGames.Foundations.Complexity.tableWords_length line 166
  26. def OAI.DFVSGames.Foundations.Complexity.constraintWords line 169
  27. def OAI.DFVSGames.Foundations.Complexity.parseConstraint line 172
  28. theorem OAI.DFVSGames.Foundations.Complexity.parseConstraint_encoded line 181
  29. def OAI.DFVSGames.Foundations.Complexity.parseConstraints line 190
  30. theorem OAI.DFVSGames.Foundations.Complexity.parseConstraints_encoded line 198
  31. def OAI.DFVSGames.Foundations.Complexity.gameWords line 207
  32. def OAI.DFVSGames.Foundations.Complexity.gameBits line 210
  33. def OAI.DFVSGames.Foundations.Complexity.decodeGameWords line 212
  34. theorem OAI.DFVSGames.Foundations.Complexity.decodeGameWords_encoded line 222
  35. def OAI.DFVSGames.Foundations.Complexity.decodeGameBits line 230
  36. theorem OAI.DFVSGames.Foundations.Complexity.decodeGameBits_encoded line 233
  37. theorem OAI.DFVSGames.Foundations.Complexity.gameBits_injective line 237
  38. theorem OAI.DFVSGames.Foundations.Complexity.constraintWords_length line 242
  39. theorem OAI.DFVSGames.Foundations.Complexity.constraintsWords_length line 245
  40. theorem OAI.DFVSGames.Foundations.Complexity.gameWords_length line 254
  41. def OAI.DFVSGames.Foundations.Complexity.naturalWordsEncoding line 264
  42. def OAI.DFVSGames.Foundations.Complexity.formulaEncoding line 269
  43. def OAI.DFVSGames.Foundations.Complexity.gameEncoding line 274
  44. def OAI.DFVSGames.Foundations.Complexity.prefixBitMachine line 279
  45. def OAI.DFVSGames.Foundations.Complexity.prefixBitPolyTime line 290
  46. def OAI.DFVSGames.Foundations.Complexity.enlargePolynomialBound line 309
  47. def OAI.DFVSGames.Foundations.Complexity.composeMachinePhases line 322
  48. structure OAI.DFVSGames.Foundations.Complexity.PolynomialGapReduction line 334
  49. structure OAI.DFVSGames.Integration.RealTarget.PolynomialGapReduction line 348
  50. def OAI.DFVSGames.Integration.RealTarget.ofRational line 362
  51. theorem OAI.DFVSGames.Integration.RealTarget.for_all_real_of_dyadic line 379
  52. def OAI.DFVSGames.Integration.InstanceValue.maxSatisfied line 398
  53. def OAI.DFVSGames.Integration.InstanceValue.value line 402
  54. theorem OAI.DFVSGames.Integration.InstanceValue.countSatisfied_le_maxSatisfied line 405
  55. theorem OAI.DFVSGames.Integration.InstanceValue.maxSatisfied_le_length line 413
  56. theorem OAI.DFVSGames.Integration.InstanceValue.maxSatisfied_attained line 419
  57. theorem OAI.DFVSGames.Integration.InstanceValue.value_attained line 428
  58. theorem OAI.DFVSGames.Integration.InstanceValue.labeling_rate_le_value line 434
  59. theorem OAI.DFVSGames.Integration.InstanceValue.satisfactionRate_le_value line 441
  60. theorem OAI.DFVSGames.Integration.InstanceValue.value_nonneg line 446
  61. theorem OAI.DFVSGames.Integration.InstanceValue.value_le_one line 449
  62. theorem OAI.DFVSGames.Integration.InstanceValue.value_mem_unitInterval line 455
  63. theorem OAI.DFVSGames.Integration.InstanceValue.exists_rate_ge_iff line 458
  64. theorem OAI.DFVSGames.Integration.InstanceValue.forall_rate_le_iff line 469
  65. theorem OAI.DFVSGames.Integration.InstanceValue.completeAt_iff_value line 480
  66. theorem OAI.DFVSGames.Integration.InstanceValue.soundAt_iff_value line 485
  67. theorem OAI.DFVSGames.Integration.InstanceValue.realTarget_completeness line 490
  68. theorem OAI.DFVSGames.Integration.InstanceValue.realTarget_soundness line 498
  69. theorem OAI.DFVSGames.Integration.InstanceValue.realTarget_value_guarantees line 506
  70. abbrev OAI.DFVSGames.Integration.BinaryCoordinates.Coordinates line 519
  71. def OAI.DFVSGames.Integration.BinaryCoordinates.pack line 521
  72. def OAI.DFVSGames.Integration.BinaryCoordinates.unpack line 525
  73. theorem OAI.DFVSGames.Integration.BinaryCoordinates.pack_get line 528
  74. theorem OAI.DFVSGames.Integration.BinaryCoordinates.unpack_pack line 537
  75. theorem OAI.DFVSGames.Integration.BinaryCoordinates.pack_unpack line 541
  76. theorem OAI.DFVSGames.Integration.BinaryCoordinates.unpack_injective line 546
  77. theorem OAI.DFVSGames.Integration.BinaryCoordinates.pack_injective line 551
  78. theorem OAI.DFVSGames.Integration.BinaryCoordinates.unpack_xor line 556
  79. theorem OAI.DFVSGames.Integration.BinaryCoordinates.pack_xor line 561
  80. theorem OAI.DFVSGames.Integration.BinaryCoordinates.unpack_zero line 566
  81. theorem OAI.DFVSGames.Integration.BinaryCoordinates.pack_zero line 570
  82. abbrev OAI.DFVSGames.Integration.BinaryLinear.F2 line 581
  83. abbrev OAI.DFVSGames.Integration.BinaryLinear.Vector line 582
  84. def OAI.DFVSGames.Integration.BinaryLinear.ofBit line 584
  85. def OAI.DFVSGames.Integration.BinaryLinear.toBit line 585
  86. theorem OAI.DFVSGames.Integration.BinaryLinear.scalar_cases line 587
  87. theorem OAI.DFVSGames.Integration.BinaryLinear.ofBit_toBit line 588
  88. theorem OAI.DFVSGames.Integration.BinaryLinear.toBit_ofBit line 589
  89. theorem OAI.DFVSGames.Integration.BinaryLinear.ofBit_xor line 590
  90. theorem OAI.DFVSGames.Integration.BinaryLinear.toBit_add line 591
  91. def OAI.DFVSGames.Integration.BinaryLinear.toVector line 593
  92. def OAI.DFVSGames.Integration.BinaryLinear.fromVector line 594
  93. theorem OAI.DFVSGames.Integration.BinaryLinear.toVector_fromVector line 596
  94. theorem OAI.DFVSGames.Integration.BinaryLinear.fromVector_toVector line 600
  95. def OAI.DFVSGames.Integration.BinaryLinear.coordinatesEquiv line 604
  96. theorem OAI.DFVSGames.Integration.BinaryLinear.toVector_xor line 610
  97. theorem OAI.DFVSGames.Integration.BinaryLinear.fromVector_add line 615
  98. theorem OAI.DFVSGames.Integration.BinaryLinear.toVector_zero line 619
  99. theorem OAI.DFVSGames.Integration.BinaryLinear.fromVector_zero line 624
  100. def OAI.DFVSGames.Integration.BinaryLinear.liftLinear line 627
  101. theorem OAI.DFVSGames.Integration.BinaryLinear.liftLinear_apply line 638
  102. theorem OAI.DFVSGames.Integration.BinaryLinear.finrank_vector line 643
  103. def OAI.DFVSGames.Integration.TranslationTarget.IsTranslationInstance line 654
  104. structure OAI.DFVSGames.Integration.TranslationTarget.PolynomialGapReduction line 660
  105. def OAI.DFVSGames.Integration.TranslationTarget.ofRational line 666
  106. theorem OAI.DFVSGames.Integration.TranslationTarget.for_all_real_of_dyadic line 677
  107. theorem OAI.DFVSGames.Explicit.UniformTarget.copy_length line 699
  108. def OAI.DFVSGames.Explicit.UniformTarget.construct line 707
  109. theorem OAI.DFVSGames.Explicit.UniformTarget.vertices line 715
  110. theorem OAI.DFVSGames.Explicit.UniformTarget.edge_count line 718
  111. theorem OAI.DFVSGames.Explicit.UniformTarget.count_append_inline_UniformTarget line 722
  112. theorem OAI.DFVSGames.Explicit.UniformTarget.count_copies line 727
  113. theorem OAI.DFVSGames.Explicit.UniformTarget.count line 737
  114. theorem OAI.DFVSGames.Explicit.UniformTarget.maxSatisfied line 742
  115. theorem OAI.DFVSGames.Explicit.UniformTarget.value line 757
  116. theorem OAI.DFVSGames.Explicit.UniformTarget.mem_original line 767
  117. theorem OAI.DFVSGames.Explicit.UniformTarget.translations line 774
  118. theorem OAI.DFVSGames.Explicit.UniformTarget.flatMap_copies line 781
  119. theorem OAI.DFVSGames.Explicit.UniformTarget.encode_copies line 789
  120. theorem OAI.DFVSGames.Explicit.UniformTarget.gameWords_construct line 797
  121. theorem OAI.DFVSGames.Explicit.UniformTarget.gameBits_construct line 805