OAI/Computability/DirectedFeedback/Games/UniformReduction.lean

GitHub source file

120 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DFVSGames.Reduction.UniformReduction.rawSource line 59
  2. def OAI.DFVSGames.Reduction.UniformReduction.source line 62
  3. def OAI.DFVSGames.Reduction.UniformReduction.output line 65
  4. def OAI.DFVSGames.Reduction.UniformReduction.satisfaction line 69
  5. theorem OAI.DFVSGames.Reduction.UniformReduction.source_variables line 72
  6. theorem OAI.DFVSGames.Reduction.UniformReduction.source_occurrences line 75
  7. theorem OAI.DFVSGames.Reduction.UniformReduction.source_occurrences_le line 79
  8. theorem OAI.DFVSGames.Reduction.UniformReduction.source_distinct line 87
  9. theorem OAI.DFVSGames.Reduction.UniformReduction.output_constraint_count line 90
  10. theorem OAI.DFVSGames.Reduction.UniformReduction.output_vertex_count line 100
  11. def OAI.DFVSGames.Reduction.UniformReduction.liftAssignment line 105
  12. theorem OAI.DFVSGames.Reduction.UniformReduction.source_failure_preserved line 109
  13. theorem OAI.DFVSGames.Reduction.UniformReduction.raw_failure_add_satisfaction line 114
  14. theorem OAI.DFVSGames.Reduction.UniformReduction.source_complete line 123
  15. theorem OAI.DFVSGames.Reduction.UniformReduction.raw_quarter_count_gap line 132
  16. theorem OAI.DFVSGames.Reduction.UniformReduction.source_sound line 144
  17. theorem OAI.DFVSGames.Reduction.UniformReduction.sourceGame_sound line 164
  18. theorem OAI.DFVSGames.Reduction.UniformReduction.completeAt_of_parameters line 179
  19. theorem OAI.DFVSGames.Reduction.OutputTranslations.translationTable_vector line 211
  20. theorem OAI.DFVSGames.Reduction.OutputTranslations.translationTable_coordinates line 216
  21. theorem OAI.DFVSGames.Reduction.OutputTranslations.explicitEdge_vector line 224
  22. theorem OAI.DFVSGames.Reduction.OutputTranslations.explicitEdge_coordinates line 234
  23. theorem OAI.DFVSGames.Reduction.OutputTranslations.outputInstanceWithEnumeration_vector line 245
  24. theorem OAI.DFVSGames.Reduction.OutputTranslations.outputInstanceWithEnumeration_coordinates line 255
  25. theorem OAI.DFVSGames.Reduction.OutputTranslations.tableOutput_vector line 265
  26. theorem OAI.DFVSGames.Reduction.OutputTranslations.tableOutput_coordinates line 274
  27. theorem OAI.DFVSGames.Reduction.OutputTranslations.uniformOutput_vector line 283
  28. theorem OAI.DFVSGames.Reduction.OutputTranslations.uniformOutput_coordinates line 292
  29. abbrev OAI.DFVSGames.Reduction.AddressGame.bodyCapacity line 312
  30. def OAI.DFVSGames.Reduction.AddressGame.vertexCount line 315
  31. def OAI.DFVSGames.Reduction.AddressGame.vertexAddress line 317
  32. theorem OAI.DFVSGames.Reduction.AddressGame.vertexAddress_injective line 321
  33. def OAI.DFVSGames.Reduction.AddressGame.queryAddress line 331
  34. theorem OAI.DFVSGames.Reduction.AddressGame.vertexAddress_query line 336
  35. def OAI.DFVSGames.Reduction.AddressGame.explicitToAddress line 341
  36. theorem OAI.DFVSGames.Reduction.AddressGame.explicitToAddress_injective line 345
  37. theorem OAI.DFVSGames.Reduction.AddressGame.explicitToAddress_apply line 349
  38. def OAI.DFVSGames.Reduction.AddressGame.semanticToAddress line 355
  39. theorem OAI.DFVSGames.Reduction.AddressGame.semanticToAddress_injective line 359
  40. theorem OAI.DFVSGames.Reduction.AddressGame.semanticToAddress_apply line 363
  41. def OAI.DFVSGames.Reduction.AddressGame.addressEdge line 369
  42. theorem OAI.DFVSGames.Reduction.AddressGame.addressEdge_eq_embed line 377
  43. theorem OAI.DFVSGames.Reduction.AddressGame.addressEdge_eq_semantic_embed line 384
  44. theorem OAI.DFVSGames.Reduction.AddressGame.addressEdge_permutation line 391
  45. def OAI.DFVSGames.Reduction.AddressGame.outputInstance line 395
  46. theorem OAI.DFVSGames.Reduction.AddressGame.outputInstance_eq_embed line 406
  47. theorem OAI.DFVSGames.Reduction.AddressGame.outputInstance_length line 415
  48. theorem OAI.DFVSGames.Reduction.AddressGame.outputInstance_count line 422
  49. theorem OAI.DFVSGames.Reduction.AddressGame.completeAt_outputInstance_iff_explicit line 433
  50. theorem OAI.DFVSGames.Reduction.AddressGame.soundAt_outputInstance_iff_explicit line 440
  51. theorem OAI.DFVSGames.Reduction.AddressGame.completeAt_outputInstance_iff line 447
  52. theorem OAI.DFVSGames.Reduction.AddressGame.soundAt_outputInstance_iff line 453
  53. theorem OAI.DFVSGames.Reduction.AddressGame.outputInstance_translations line 459
  54. def OAI.DFVSGames.Reduction.AddressGame.tableOutput line 469
  55. theorem OAI.DFVSGames.Reduction.AddressGame.completeAt_tableOutput_iff line 474
  56. theorem OAI.DFVSGames.Reduction.AddressGame.soundAt_tableOutput_iff line 479
  57. theorem OAI.DFVSGames.Reduction.AddressGame.tableOutput_translations line 484
  58. theorem OAI.DFVSGames.Reduction.AddressGame.vertexCount_eq_polynomial line 489
  59. abbrev OAI.DFVSGames.Reduction.FixedOutcomes.Parameter line 507
  60. def OAI.DFVSGames.Reduction.FixedOutcomes.occurrenceTuples line 510
  61. def OAI.DFVSGames.Reduction.FixedOutcomes.fixedParams line 513
  62. def OAI.DFVSGames.Reduction.FixedOutcomes.assemble line 517
  63. def OAI.DFVSGames.Reduction.FixedOutcomes.outcomeEquiv line 521
  64. theorem OAI.DFVSGames.Reduction.FixedOutcomes.pairs_associate_inline_FixedOutcomes line 526
  65. theorem OAI.DFVSGames.Reduction.FixedOutcomes.indexedOutcomes_factor line 533
  66. theorem OAI.DFVSGames.Reduction.FixedOutcomes.indexedOutcomes_reassociate line 540
  67. theorem OAI.DFVSGames.Reduction.FixedOutcomes.occurrenceTuples_length line 547
  68. theorem OAI.DFVSGames.Reduction.FixedOutcomes.fixedParams_length line 550
  69. theorem OAI.DFVSGames.Reduction.FixedOutcomes.fixedParams_nonempty line 559
  70. abbrev OAI.DFVSGames.Reduction.FixedOutcomes.CoefficientParameter line 565
  71. def OAI.DFVSGames.Reduction.FixedOutcomes.coefficientValues line 568
  72. def OAI.DFVSGames.Reduction.FixedOutcomes.fixedCoefficientParams line 571
  73. def OAI.DFVSGames.Reduction.FixedOutcomes.fromCoefficientParameter line 576
  74. theorem OAI.DFVSGames.Reduction.FixedOutcomes.fixedCoefficientParams_map line 580
  75. theorem OAI.DFVSGames.Reduction.FixedOutcomes.fixedCoefficientParams_length line 587
  76. def OAI.DFVSGames.Reduction.FixedOutcomes.tableParams line 592
  77. theorem OAI.DFVSGames.Reduction.FixedOutcomes.tableParams_length line 596
  78. theorem OAI.DFVSGames.Reduction.FixedOutcomes.outputInstance_constraints line 600
  79. theorem OAI.DFVSGames.Reduction.FixedOutcomes.tableOutput_constraints line 611
  80. def OAI.DFVSGames.Reduction.AddressByteSemantics.queryWords line 629
  81. def OAI.DFVSGames.Reduction.AddressByteSemantics.queryRank line 635
  82. def OAI.DFVSGames.Reduction.AddressByteSemantics.permutationWords line 639
  83. def OAI.DFVSGames.Reduction.AddressByteSemantics.edgeWords line 647
  84. def OAI.DFVSGames.Reduction.AddressByteSemantics.edgeBits line 652
  85. theorem OAI.DFVSGames.Reduction.AddressByteSemantics.queryWords_length line 656
  86. theorem OAI.DFVSGames.Reduction.AddressByteSemantics.permutationWords_length line 662
  87. theorem OAI.DFVSGames.Reduction.AddressByteSemantics.queryWords_actual line 666
  88. theorem OAI.DFVSGames.Reduction.AddressByteSemantics.queryAddress_false line 673
  89. theorem OAI.DFVSGames.Reduction.AddressByteSemantics.queryAddress_true line 682
  90. theorem OAI.DFVSGames.Reduction.AddressByteSemantics.addressEdge_words line 692
  91. theorem OAI.DFVSGames.Reduction.AddressByteSemantics.addressEdge_bits line 706
  92. theorem OAI.DFVSGames.Reduction.AddressByteSemantics.edgeBits_split line 717
  93. abbrev OAI.DFVSGames.Reduction.AddressOutcomeSpecs.Spec line 734
  94. abbrev OAI.DFVSGames.Reduction.AddressOutcomeSpecs.Values line 735
  95. abbrev OAI.DFVSGames.Reduction.AddressOutcomeSpecs.Parameter line 736
  96. def OAI.DFVSGames.Reduction.AddressOutcomeSpecs.bitVector line 739
  97. def OAI.DFVSGames.Reduction.AddressOutcomeSpecs.rightMap line 741
  98. def OAI.DFVSGames.Reduction.AddressOutcomeSpecs.row line 744
  99. def OAI.DFVSGames.Reduction.AddressOutcomeSpecs.rows line 752
  100. theorem OAI.DFVSGames.Reduction.AddressOutcomeSpecs.row_left_length line 756
  101. theorem OAI.DFVSGames.Reduction.AddressOutcomeSpecs.row_right_length line 760
  102. theorem OAI.DFVSGames.Reduction.AddressOutcomeSpecs.rows_length line 764
  103. theorem OAI.DFVSGames.Reduction.AddressOutcomeSpecs.selected_rows line 768
  104. def OAI.DFVSGames.Reduction.AddressOutcomeSpecs.interpreted line 774
  105. theorem OAI.DFVSGames.Reduction.AddressOutcomeSpecs.interpreted_encoded line 779
  106. def OAI.DFVSGames.Reduction.AddressOutcomeSpecs.values line 783
  107. theorem OAI.DFVSGames.Reduction.AddressOutcomeSpecs.row_left_output line 793
  108. theorem OAI.DFVSGames.Reduction.AddressOutcomeSpecs.row_right_output line 799
  109. theorem OAI.DFVSGames.Reduction.AddressOutcomeSpecs.values_row_left line 805
  110. theorem OAI.DFVSGames.Reduction.AddressOutcomeSpecs.values_row_right line 813
  111. theorem OAI.DFVSGames.Reduction.AddressOutcomeSpecs.correct_rows line 821
  112. theorem OAI.DFVSGames.Reduction.AddressOutcomeSpecs.payload_row line 837
  113. def OAI.DFVSGames.Reduction.AddressOutcomeSpecs.rhsBits line 846
  114. theorem OAI.DFVSGames.Reduction.AddressOutcomeSpecs.bitVector_rhsBits line 849
  115. theorem OAI.DFVSGames.Reduction.AddressOutcomeSpecs.rightMap_actual line 852
  116. theorem OAI.DFVSGames.Reduction.AddressOutcomeSpecs.payload_row_actual line 857
  117. def OAI.DFVSGames.Reduction.AddressOutcomeSpecs.tupleBits line 869
  118. theorem OAI.DFVSGames.Reduction.AddressOutcomeSpecs.tuplePayload_actual line 875
  119. theorem OAI.DFVSGames.Reduction.AddressOutcomeSpecs.encodeWords_flatMap_inline_AddressOutcomeSpecs line 886
  120. theorem OAI.DFVSGames.Reduction.AddressOutcomeSpecs.gameBits_factor line 893