OAI/Computability/DirectedFeedback/Machines/MachineSubdivisionLoop.lean

GitHub source file

100 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.DFVSGames.Explicit.MachineSubdivisionLoop.rowPayload_eq line 15
  2. theorem OAI.DFVSGames.Explicit.MachineSubdivisionLoop.bodyResult_eq_frame line 24
  3. def OAI.DFVSGames.Explicit.MachineSubdivisionLoop.bodyBound line 47
  4. def OAI.DFVSGames.Explicit.MachineSubdivisionLoop.bodyInTime line 49
  5. def OAI.DFVSGames.Explicit.MachineSubdivisionLoop.loopInTime line 63
  6. def OAI.DFVSGames.Explicit.MachineSubdivisionFinish.timePolynomial line 117
  7. theorem OAI.DFVSGames.Explicit.MachineSubdivisionFinish.haltList_eq line 120
  8. def OAI.DFVSGames.Explicit.MachineSubdivisionFinish.finishStartInTime line 129
  9. theorem OAI.DFVSGames.Explicit.MachineSubdivisionFinish.covers line 141
  10. def OAI.DFVSGames.Explicit.MachineSubdivisionFinish.completePrefix line 148
  11. structure OAI.DFVSGames.Explicit.OccurrenceGame line 184
  12. structure OAI.DFVSGames.Explicit.BipartiteGame line 189
  13. def OAI.DFVSGames.Explicit.OccurrenceGame.Satisfied line 197
  14. instance OAI.DFVSGames.Explicit.OccurrenceGame.satisfiedDecidable line 201
  15. def OAI.DFVSGames.Explicit.OccurrenceGame.IsTranslation line 205
  16. def OAI.DFVSGames.Explicit.BipartiteGame.Satisfied line 212
  17. instance OAI.DFVSGames.Explicit.BipartiteGame.satisfiedDecidable line 216
  18. def OAI.DFVSGames.Explicit.BipartiteGame.IsTranslation line 220
  19. def OAI.DFVSGames.Explicit.OccurrenceGame.satisfiedCount line 232
  20. theorem OAI.DFVSGames.Explicit.OccurrenceGame.satisfiedCount_eq_sum_satisfied line 235
  21. def OAI.DFVSGames.Explicit.OccurrenceGame.maxSatisfied line 250
  22. def OAI.DFVSGames.Explicit.OccurrenceGame.value line 254
  23. theorem OAI.DFVSGames.Explicit.OccurrenceGame.satisfiedCount_le_maxSatisfied line 257
  24. theorem OAI.DFVSGames.Explicit.OccurrenceGame.maxSatisfied_attained line 262
  25. def OAI.DFVSGames.Explicit.BipartiteGame.satisfiedCount line 275
  26. theorem OAI.DFVSGames.Explicit.BipartiteGame.satisfiedCount_eq_sum_satisfied line 278
  27. def OAI.DFVSGames.Explicit.BipartiteGame.maxSatisfied line 294
  28. def OAI.DFVSGames.Explicit.BipartiteGame.value line 298
  29. theorem OAI.DFVSGames.Explicit.BipartiteGame.satisfiedCount_le_maxSatisfied line 301
  30. theorem OAI.DFVSGames.Explicit.BipartiteGame.maxSatisfied_attained line 307
  31. abbrev OAI.DFVSGames.Explicit.Subdivision.Left line 321
  32. abbrev OAI.DFVSGames.Explicit.Subdivision.Right line 323
  33. abbrev OAI.DFVSGames.Explicit.Subdivision.Edge line 325
  34. def OAI.DFVSGames.Explicit.Subdivision.left line 327
  35. def OAI.DFVSGames.Explicit.Subdivision.right line 332
  36. def OAI.DFVSGames.Explicit.Subdivision.permutation line 334
  37. theorem OAI.DFVSGames.Explicit.Subdivision.endpoints_injective line 337
  38. def OAI.DFVSGames.Explicit.Subdivision.game line 344
  39. theorem OAI.DFVSGames.Explicit.Subdivision.isTranslation line 351
  40. theorem OAI.DFVSGames.Explicit.Subdivision.binary_translation_offsets line 363
  41. def OAI.DFVSGames.Explicit.Subdivision.restrict line 375
  42. def OAI.DFVSGames.Explicit.Subdivision.extendLeft line 377
  43. def OAI.DFVSGames.Explicit.Subdivision.extendRight line 380
  44. theorem OAI.DFVSGames.Explicit.Subdivision.restrict_extendLeft line 383
  45. theorem OAI.DFVSGames.Explicit.Subdivision.four_satisfied_implies_original line 386
  46. theorem OAI.DFVSGames.Explicit.Subdivision.local_count_le line 394
  47. theorem OAI.DFVSGames.Explicit.Subdivision.local_count_extend line 402
  48. theorem OAI.DFVSGames.Explicit.Subdivision.count_on_occurrence_le line 415
  49. theorem OAI.DFVSGames.Explicit.Subdivision.count_on_occurrence_extend line 426
  50. theorem OAI.DFVSGames.Explicit.Subdivision.satisfiedCount_le line 437
  51. theorem OAI.DFVSGames.Explicit.Subdivision.satisfiedCount_extend line 449
  52. theorem OAI.DFVSGames.Explicit.Subdivision.edge_count line 457
  53. theorem OAI.DFVSGames.Explicit.Subdivision.left_count line 460
  54. theorem OAI.DFVSGames.Explicit.Subdivision.right_count line 464
  55. theorem OAI.DFVSGames.Explicit.Subdivision.maxSatisfied_eq line 469
  56. theorem OAI.DFVSGames.Explicit.Subdivision.value_eq line 481
  57. structure OAI.DFVSGames.Foundations.PCP.ClauseAnswer line 499
  58. inductive OAI.DFVSGames.Foundations.PCP.Slot line 505
  59. def OAI.DFVSGames.Foundations.PCP.answerAt line 511
  60. def OAI.DFVSGames.Foundations.PCP.nameAt line 516
  61. def OAI.DFVSGames.Foundations.PCP.literalValue line 521
  62. def OAI.DFVSGames.Foundations.PCP.localSatisfies line 524
  63. def OAI.DFVSGames.Foundations.PCP.honestAnswer line 529
  64. theorem OAI.DFVSGames.Foundations.PCP.honest_satisfies line 533
  65. theorem OAI.DFVSGames.Foundations.PCP.honest_answerAt line 536
  66. def OAI.DFVSGames.Foundations.PCP.matchingSlots line 541
  67. theorem OAI.DFVSGames.Foundations.PCP.matchingSlots_le line 546
  68. theorem OAI.DFVSGames.Foundations.PCP.matchingSlots_eq_three line 551
  69. def OAI.DFVSGames.Foundations.PCP.acceptedSlots line 556
  70. def OAI.DFVSGames.Foundations.PCP.clauseFailure line 559
  71. theorem OAI.DFVSGames.Foundations.PCP.local_rejection_bound line 562
  72. def OAI.DFVSGames.Foundations.PCP.clauseAt line 584
  73. abbrev OAI.DFVSGames.Foundations.PCP.RandomEvent line 587
  74. abbrev OAI.DFVSGames.Foundations.PCP.AliceStrategy line 588
  75. abbrev OAI.DFVSGames.Foundations.PCP.BobStrategy line 589
  76. def OAI.DFVSGames.Foundations.PCP.accepts line 591
  77. def OAI.DFVSGames.Foundations.PCP.acceptedCount line 596
  78. def OAI.DFVSGames.Foundations.PCP.failureCount line 602
  79. theorem OAI.DFVSGames.Foundations.PCP.total_rejection_bound line 607
  80. def OAI.DFVSGames.Foundations.PCP.allIndices line 618
  81. theorem OAI.DFVSGames.Foundations.PCP.hastad_basic_verifier_soundness line 621
  82. theorem OAI.DFVSGames.Foundations.PCP.honest_accepts line 632
  83. theorem OAI.DFVSGames.Foundations.PCP.verifier_completeness line 640
  84. abbrev OAI.DFVSGames.Foundations.PCP.LeftLabel line 647
  85. def OAI.DFVSGames.Foundations.PCP.edgeProjection line 650
  86. theorem OAI.DFVSGames.Foundations.PCP.verifier_eq_projection line 653
  87. def OAI.DFVSGames.Foundations.PCP.eventsAt line 660
  88. def OAI.DFVSGames.Foundations.PCP.enumerateEvents line 663
  89. theorem OAI.DFVSGames.Foundations.PCP.length_enumerateEvents line 668
  90. theorem OAI.DFVSGames.Foundations.PCP.accepted_eventsAt line 677
  91. theorem OAI.DFVSGames.Foundations.PCP.accepted_enumerateEvents line 689
  92. def OAI.DFVSGames.Foundations.PCP.allEvents line 699
  93. theorem OAI.DFVSGames.Foundations.PCP.length_allEvents line 702
  94. theorem OAI.DFVSGames.Foundations.PCP.allEvents_nonempty line 706
  95. theorem OAI.DFVSGames.Foundations.PCP.verifier_event_soundness line 715
  96. def OAI.DFVSGames.Foundations.PCP.occurrencesAt line 725
  97. def OAI.DFVSGames.Foundations.PCP.occurrenceCount line 730
  98. theorem OAI.DFVSGames.Foundations.PCP.variable_eventsAt line 735
  99. theorem OAI.DFVSGames.Foundations.PCP.variable_enumerateEvents line 745
  100. theorem OAI.DFVSGames.Foundations.PCP.regular_bob_marginal line 756