OAI/Computability/DirectedFeedback/Main.lean

GitHub source file

122 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.DirectedFeedback.CookLevin.LocalCSP.queryCount line 19
  2. def OAI.DirectedFeedback.CookLevin.LocalCSP.asVerifier line 21
  3. def OAI.DirectedFeedback.CookLevin.LocalCSP.asFormula line 26
  4. theorem OAI.DirectedFeedback.CookLevin.LocalCSP.convert_satisfiable_iff line 28
  5. theorem OAI.DirectedFeedback.CookLevin.LocalCSP.asFormula_satisfiable_iff line 52
  6. def OAI.DirectedFeedback.CookLevin.NPTableau.alphabetCodec line 64
  7. instance OAI.DirectedFeedback.CookLevin.NPTableau.codec_width_nonempty line 71
  8. def OAI.DirectedFeedback.CookLevin.NPTableau.formula line 78
  9. theorem OAI.DirectedFeedback.CookLevin.NPTableau.formula_satisfiable_iff line 81
  10. def OAI.DirectedFeedback.CookLevin.LocalCSP.padAt line 98
  11. theorem OAI.DirectedFeedback.CookLevin.LocalCSP.padAt_satisfiable_iff line 103
  12. def OAI.DirectedFeedback.CookLevin.NPTableau.eventCount line 110
  13. def OAI.DirectedFeedback.CookLevin.NPTableau.decodeEvent line 112
  14. theorem OAI.DirectedFeedback.CookLevin.NPTableau.decodeEvent_surjective line 118
  15. abbrev OAI.DirectedFeedback.CookLevin.NPTableau.FixedSlot line 132
  16. def OAI.DirectedFeedback.CookLevin.NPTableau.queryNumber line 135
  17. def OAI.DirectedFeedback.CookLevin.NPTableau.slotIndex line 137
  18. def OAI.DirectedFeedback.CookLevin.NPTableau.variableIndex line 139
  19. theorem OAI.DirectedFeedback.CookLevin.NPTableau.variableIndex_val line 142
  20. def OAI.DirectedFeedback.CookLevin.NPTableau.canonicalVerifier line 146
  21. theorem OAI.DirectedFeedback.CookLevin.NPTableau.canonicalVerifier_satisfiable_iff line 156
  22. theorem OAI.DirectedFeedback.CookLevin.NPTableau.queryNumber_ge line 193
  23. def OAI.DirectedFeedback.CookLevin.NPTableau.canonicalFormula line 196
  24. theorem OAI.DirectedFeedback.CookLevin.NPTableau.canonicalFormula_correct line 199
  25. def OAI.DirectedFeedback.CookLevin.WDef line 218
  26. theorem OAI.DirectedFeedback.CookLevin.WDef.congr line 225
  27. theorem OAI.DirectedFeedback.CookLevin.WDef.ite line 229
  28. theorem OAI.DirectedFeedback.CookLevin.WDef.update line 235
  29. theorem OAI.DirectedFeedback.CookLevin.WDef.push line 245
  30. theorem OAI.DirectedFeedback.CookLevin.WDef.pop line 255
  31. structure OAI.DirectedFeedback.CookLevin.CDef line 260
  32. theorem OAI.DirectedFeedback.CookLevin.CDef.congr line 269
  33. theorem OAI.DirectedFeedback.CookLevin.CDef.ite line 274
  34. theorem OAI.DirectedFeedback.CookLevin.CDef.bind line 282
  35. theorem OAI.DirectedFeedback.CookLevin.wordStepAux_def line 293
  36. theorem OAI.DirectedFeedback.CookLevin.wordNext_def line 309
  37. theorem OAI.DirectedFeedback.CookLevin.localWord_def line 336
  38. def OAI.DirectedFeedback.CookLevin.rawData line 362
  39. def OAI.DirectedFeedback.CookLevin.rawStepAccepts line 367
  40. theorem OAI.DirectedFeedback.CookLevin.rawStepAccepts_eq line 374
  41. theorem OAI.DirectedFeedback.CookLevin.rawStepAccepts_def line 384
  42. instance OAI.DirectedFeedback.CookLevin.NPTableau.verifierAlphabet line 413
  43. theorem OAI.DirectedFeedback.CookLevin.NPTableau.certBound_def line 416
  44. theorem OAI.DirectedFeedback.CookLevin.NPTableau.inputBound_def line 419
  45. theorem OAI.DirectedFeedback.CookLevin.NPTableau.horizon_def line 422
  46. theorem OAI.DirectedFeedback.CookLevin.NPTableau.capacity_def line 425
  47. theorem OAI.DirectedFeedback.CookLevin.NPTableau.fixedPrefix_def line 428
  48. def OAI.DirectedFeedback.CookLevin.NPTableau.rawInitialAccepts line 433
  49. theorem OAI.DirectedFeedback.CookLevin.NPTableau.rawInitialAccepts_eq line 439
  50. theorem OAI.DirectedFeedback.CookLevin.NPTableau.rawInitialAccepts_def line 445
  51. def OAI.DirectedFeedback.CookLevin.rawCell line 483
  52. theorem OAI.DirectedFeedback.CookLevin.rawCell_eq line 485
  53. theorem OAI.DirectedFeedback.CookLevin.rawCell_def line 489
  54. def OAI.DirectedFeedback.CookLevin.rawInitialQuery line 496
  55. def OAI.DirectedFeedback.CookLevin.rawStepQuery line 499
  56. theorem OAI.DirectedFeedback.CookLevin.rawInitialQuery_eq line 504
  57. theorem OAI.DirectedFeedback.CookLevin.rawStepQuery_eq line 509
  58. def OAI.DirectedFeedback.CookLevin.AddrDef line 516
  59. theorem OAI.DirectedFeedback.CookLevin.AddrDef.const line 521
  60. theorem OAI.DirectedFeedback.CookLevin.AddrDef.ite line 522
  61. theorem OAI.DirectedFeedback.CookLevin.AddrDef.congr line 527
  62. theorem OAI.DirectedFeedback.CookLevin.rawInitialQuery_def line 532
  63. theorem OAI.DirectedFeedback.CookLevin.rawStepQuery_def line 541
  64. def OAI.DirectedFeedback.CookLevin.NPTableau.rawTableauQuery line 556
  65. theorem OAI.DirectedFeedback.CookLevin.NPTableau.rawTableauQuery_def line 567
  66. theorem OAI.DirectedFeedback.CookLevin.NPTableau.rawTableauQuery_correct line 599
  67. def OAI.DirectedFeedback.CookLevin.NPTableau.rawQuery line 620
  68. theorem OAI.DirectedFeedback.CookLevin.NPTableau.rawQuery_def line 628
  69. theorem OAI.DirectedFeedback.CookLevin.NPTableau.rawQuery_correct line 636
  70. def OAI.DirectedFeedback.CookLevin.NPTableau.decodedPattern line 662
  71. def OAI.DirectedFeedback.CookLevin.NPTableau.rawAccepts line 666
  72. theorem OAI.DirectedFeedback.CookLevin.NPTableau.rawAccepts_def line 675
  73. theorem OAI.DirectedFeedback.CookLevin.NPTableau.rawAccepts_correct line 691
  74. def OAI.DirectedFeedback.CookLevin.NPTableau.family line 709
  75. def OAI.DirectedFeedback.CookLevin.NPTableau.computation line 722
  76. theorem OAI.DirectedFeedback.CookLevin.NPTableau.computation_finite line 726
  77. def OAI.DirectedFeedback.BinaryEmbed.name line 741
  78. theorem OAI.DirectedFeedback.BinaryEmbed.name_bits line 745
  79. theorem OAI.DirectedFeedback.BinaryEmbed.name_injective line 751
  80. def OAI.DirectedFeedback.BinaryEmbed.literal line 756
  81. def OAI.DirectedFeedback.BinaryEmbed.clause line 757
  82. def OAI.DirectedFeedback.BinaryEmbed.formula line 758
  83. theorem OAI.DirectedFeedback.BinaryEmbed.literal_eval line 760
  84. theorem OAI.DirectedFeedback.BinaryEmbed.clause_eval line 763
  85. theorem OAI.DirectedFeedback.BinaryEmbed.satisfiable_iff line 767
  86. theorem OAI.DirectedFeedback.BinaryEmbed.frame_replicate line 785
  87. theorem OAI.DirectedFeedback.BinaryEmbed.literal_bits line 794
  88. def OAI.DirectedFeedback.BinaryEmbed.clauseBody line 798
  89. theorem OAI.DirectedFeedback.BinaryEmbed.formula_bits line 800
  90. abbrev OAI.DirectedFeedback.BoundedExpr.BinaryCNFPrinter.Lit line 821
  91. def OAI.DirectedFeedback.BoundedExpr.BinaryCNFPrinter.literalBits line 823
  92. def OAI.DirectedFeedback.BoundedExpr.BinaryCNFPrinter.clauseBits line 824
  93. def OAI.DirectedFeedback.BoundedExpr.BinaryCNFPrinter.rawSplit line 826
  94. theorem OAI.DirectedFeedback.BoundedExpr.BinaryCNFPrinter.clauseBits_eq line 831
  95. theorem OAI.DirectedFeedback.BoundedExpr.BinaryCNFPrinter.rawSplit_eq line 837
  96. theorem OAI.DirectedFeedback.BoundedExpr.BinaryCNFPrinter.literalBits_def line 859
  97. theorem OAI.DirectedFeedback.BoundedExpr.BinaryCNFPrinter.clauseBits_def line 864
  98. theorem OAI.DirectedFeedback.BoundedExpr.BinaryCNFPrinter.rawSplit_def line 871
  99. abbrev OAI.DirectedFeedback.BoundedExpr.BinaryCNFPrinter.Family line 898
  100. def OAI.DirectedFeedback.BoundedExpr.BinaryCNFPrinter.Family.blockBits line 903
  101. def OAI.DirectedFeedback.BoundedExpr.BinaryCNFPrinter.Family.eventBits line 913
  102. def OAI.DirectedFeedback.BoundedExpr.BinaryCNFPrinter.Family.bits line 916
  103. theorem OAI.DirectedFeedback.BoundedExpr.BinaryCNFPrinter.Family.blockBits_def line 919
  104. theorem OAI.DirectedFeedback.BoundedExpr.BinaryCNFPrinter.Family.eventBits_def line 940
  105. theorem OAI.DirectedFeedback.BoundedExpr.BinaryCNFPrinter.Family.bits_def line 943
  106. theorem OAI.DirectedFeedback.BoundedExpr.BinaryCNFPrinter.Family.blockBits_correct line 965
  107. theorem OAI.DirectedFeedback.BoundedExpr.BinaryCNFPrinter.Family.eventBits_correct line 990
  108. theorem OAI.DirectedFeedback.BoundedExpr.BinaryCNFPrinter.Family.bits_correct line 997
  109. def OAI.DirectedFeedback.BoundedExpr.BinaryCNFPrinter.Family.computation line 1010
  110. theorem OAI.DirectedFeedback.BoundedExpr.BinaryCNFPrinter.Family.computation_finite line 1020
  111. def OAI.DirectedFeedback.CookLevin.NPTableau.binaryFormula line 1037
  112. def OAI.DirectedFeedback.CookLevin.NPTableau.binaryInput line 1040
  113. theorem OAI.DirectedFeedback.CookLevin.NPTableau.binaryInput_correct line 1043
  114. def OAI.DirectedFeedback.CookLevin.NPTableau.binaryComputation line 1048
  115. theorem OAI.DirectedFeedback.CookLevin.NPTableau.binaryComputation_finite line 1058
  116. def OAI.DirectedFeedback.CookLevin.NPTableau.sourceComputation line 1061
  117. theorem OAI.DirectedFeedback.CookLevin.NPTableau.sourceComputation_finite line 1066
  118. def OAI.DirectedFeedback.RawFamily.gameComputation line 1093
  119. theorem OAI.DirectedFeedback.RawFamily.gameComputation_finite line 1103
  120. def OAI.DirectedFeedback.RawFamily.reduction line 1109
  121. theorem OAI.DirectedFeedback.rankSize_pos line 1126
  122. theorem OAI.DirectedFeedback.main line 1132

    Distinct definitions of this name: ComparatorChallenges/DirectedFeedback.lean:98 (different declaration text). Qualify references as OAI.DirectedFeedback.main@path.