OAI/Computability/DirectedFeedback/Games/AlphabetReduction.lean

GitHub source file

131 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.DFVSGames.Foundations.PCP.AlphabetReduction.LegalPair line 16
2. abbrev OAI.DFVSGames.Foundations.PCP.AlphabetReduction.InputCoordinate line 19
3. def OAI.DFVSGames.Foundations.PCP.AlphabetReduction.pairEncoding line 21
4. def OAI.DFVSGames.Foundations.PCP.AlphabetReduction.edgeTesterReject line 25
5. theorem OAI.DFVSGames.Foundations.PCP.AlphabetReduction.rejected_edge_tester_bound line 29
6. theorem OAI.DFVSGames.Foundations.PCP.AlphabetReduction.honest_edge_tester line 45
7. def OAI.DFVSGames.Foundations.PCP.UniformRestriction.restrict line 64
8. def OAI.DFVSGames.Foundations.PCP.UniformRestriction.extend line 68
9. def OAI.DFVSGames.Foundations.PCP.UniformRestriction.canonicalize line 71
10. theorem OAI.DFVSGames.Foundations.PCP.UniformRestriction.restrict_apply line 74
11. theorem OAI.DFVSGames.Foundations.PCP.UniformRestriction.extend_apply_of_mem line 77
12. theorem OAI.DFVSGames.Foundations.PCP.UniformRestriction.extend_apply_of_not_mem line 81
13. theorem OAI.DFVSGames.Foundations.PCP.UniformRestriction.restrict_extend line 85
14. theorem OAI.DFVSGames.Foundations.PCP.UniformRestriction.canonicalize_apply_of_mem line 90
15. theorem OAI.DFVSGames.Foundations.PCP.UniformRestriction.canonicalize_apply_of_not_mem line 94
16. theorem OAI.DFVSGames.Foundations.PCP.UniformRestriction.restrict_canonicalize line 98
17. theorem OAI.DFVSGames.Foundations.PCP.UniformRestriction.canonicalize_idempotent line 102
18. theorem OAI.DFVSGames.Foundations.PCP.UniformRestriction.canonicalize_eq_iff line 106
19. theorem OAI.DFVSGames.Foundations.PCP.UniformRestriction.expect_restrict line 117
20. theorem OAI.DFVSGames.Foundations.PCP.UniformRestriction.expect_canonicalize line 133
21. theorem OAI.DFVSGames.Foundations.PCP.UniformRestriction.expect_restrict_pair line 138
22. abbrev OAI.DFVSGames.Foundations.PCP.AlphabetGraph.Address line 159
23. abbrev OAI.DFVSGames.Foundations.PCP.AlphabetGraph.LocalEvent line 161
24. abbrev OAI.DFVSGames.Foundations.PCP.AlphabetGraph.Event line 164
25. abbrev OAI.DFVSGames.Foundations.PCP.AlphabetGraph.legal line 168
26. instance OAI.DFVSGames.Foundations.PCP.AlphabetGraph.legalDecidable line 171
27. def OAI.DFVSGames.Foundations.PCP.AlphabetGraph.restrictTape line 175
28. def OAI.DFVSGames.Foundations.PCP.AlphabetGraph.extendTape line 178
29. def OAI.DFVSGames.Foundations.PCP.AlphabetGraph.globalizeQuery line 182
30. def OAI.DFVSGames.Foundations.PCP.AlphabetGraph.verifier line 187
31. def OAI.DFVSGames.Foundations.PCP.AlphabetGraph.vertexBlock line 194
32. def OAI.DFVSGames.Foundations.PCP.AlphabetGraph.edgeOracle line 197
33. theorem OAI.DFVSGames.Foundations.PCP.AlphabetGraph.oracleAnswer_globalize line 202
34. theorem OAI.DFVSGames.Foundations.PCP.AlphabetGraph.response_eq_local line 214
35. def OAI.DFVSGames.Foundations.PCP.AlphabetGraph.eventReject line 227
36. theorem OAI.DFVSGames.Foundations.PCP.AlphabetGraph.eventReject_eq_local line 232
37. theorem OAI.DFVSGames.Foundations.PCP.AlphabetGraph.expect_prod line 245
38. def OAI.DFVSGames.Foundations.PCP.AlphabetGraph.localAverage line 250
39. theorem OAI.DFVSGames.Foundations.PCP.AlphabetGraph.expect_restrict_five line 253
40. theorem OAI.DFVSGames.Foundations.PCP.AlphabetGraph.localAverage_eq_tester line 290
41. def OAI.DFVSGames.Foundations.PCP.AlphabetGraph.average line 308
42. theorem OAI.DFVSGames.Foundations.PCP.AlphabetGraph.average_eq_testers line 313
43. def OAI.DFVSGames.Foundations.PCP.AlphabetGraph.decodedLabeling line 322
44. theorem OAI.DFVSGames.Foundations.PCP.AlphabetGraph.local_gap line 325
45. theorem OAI.DFVSGames.Foundations.PCP.AlphabetGraph.average_gap line 342
46. theorem OAI.DFVSGames.Foundations.PCP.AlphabetGraph.expect_rejection_eq_count line 350
47. theorem OAI.DFVSGames.Foundations.PCP.AlphabetGraph.average_eq_count line 363
48. theorem OAI.DFVSGames.Foundations.PCP.AlphabetGraph.card_event line 370
49. theorem OAI.DFVSGames.Foundations.PCP.AlphabetGraph.card_localEvent line 376
50. theorem OAI.DFVSGames.Foundations.PCP.AlphabetGraph.card_address line 383
51. theorem OAI.DFVSGames.Foundations.PCP.AlphabetGraph.rejection_count_bound line 389
52. def OAI.DFVSGames.Foundations.PCP.AlphabetGraph.honestAssignment line 416
53. theorem OAI.DFVSGames.Foundations.PCP.AlphabetGraph.honest_vertexBlock line 421
54. theorem OAI.DFVSGames.Foundations.PCP.AlphabetGraph.honest_edgeOracle line 425
55. theorem OAI.DFVSGames.Foundations.PCP.AlphabetGraph.honest_event line 434
56. def OAI.DFVSGames.Foundations.PCP.AlphabetGraph.graph line 446
57. theorem OAI.DFVSGames.Foundations.PCP.AlphabetGraph.perfect_completeness line 451
58. theorem OAI.DFVSGames.Foundations.PCP.AlphabetGraph.gap_transfer line 457
59. theorem OAI.DFVSGames.Foundations.PCP.AlphabetGraph.alphabet_card line 483
60. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Enumeration.bitValue line 495
61. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Enumeration.boolEquiv line 497
62. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Enumeration.boolEquiv_val line 499
63. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Enumeration.productEquiv line 502
64. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Enumeration.productEquiv_val line 506
65. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Enumeration.sumEquiv line 512
66. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Enumeration.sumEquiv_inl_val line 516
67. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Enumeration.sumEquiv_inr_val line 520
68. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Enumeration.tapeCount line 524
69. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Enumeration.pairTapeCount line 525
70. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Enumeration.fiveTapeCount line 526
71. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Enumeration.localCount line 527
72. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Enumeration.eventCount line 528
73. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Enumeration.addressCount line 529
74. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Enumeration.vertexCount line 530
75. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Enumeration.dartCount line 531
76. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Enumeration.cubeEquiv line 533
77. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Enumeration.cubeRank line 536
78. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Enumeration.cubeUnrank line 537
79. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Enumeration.cubeUnrank_cubeRank line 540
80. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Enumeration.cubeRank_cubeUnrank line 543
81. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Enumeration.cubeUnrank_digit line 546
82. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Enumeration.cubeEquiv_val line 554
83. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Enumeration.pairIndex line 560
84. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Enumeration.pairIndex_val line 562
85. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Enumeration.pairCubeEquiv line 567
86. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Enumeration.pairCubeRank line 570
87. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Enumeration.pairCubeUnrank line 573
88. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Enumeration.pairCubeUnrank_pairCubeRank line 576
89. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Enumeration.pairCubeRank_pairCubeUnrank line 579
90. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Enumeration.pairCubeEquiv_val line 582
91. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Enumeration.inputCoordinateEquiv line 587
92. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Enumeration.fivePairTapesEquiv line 591
93. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Enumeration.localEventEquiv line 600
94. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Enumeration.eventEquiv line 605
95. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Enumeration.addressEquiv line 609
96. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Enumeration.vertexEquiv line 614
97. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Enumeration.dartEquiv line 619
98. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Enumeration.labelEquiv line 624
99. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Enumeration.labelEquiv_val line 626
100. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Enumeration.inputCoordinateEquiv_val line 630
101. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Enumeration.fivePairTapesEquiv_val line 635
102. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Enumeration.localEventEquiv_val line 643
103. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Enumeration.eventEquiv_val line 652
104. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Enumeration.addressEquiv_inl_val line 659
105. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Enumeration.addressEquiv_inr_val line 666
106. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Enumeration.vertexEquiv_event_val line 673
107. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Enumeration.vertexEquiv_vertexAddress_val line 677
108. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Enumeration.vertexEquiv_edgeAddress_val line 684
109. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Enumeration.dartEquiv_val line 692
110. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Enumeration.dartEquiv_reverse_val line 700
111. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Enumeration.ordered line 706
112. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Enumeration.ordered_length line 709
113. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Enumeration.mem_ordered line 712
114. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Enumeration.ordered_nodup line 717
115. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Enumeration.ordered_refl line 722
116. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Enumeration.ordered_bool line 724
117. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Enumeration.ordered_trans_finCongr line 726
118. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Enumeration.ordered_product line 732
119. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Enumeration.ordered_sum line 748
120. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Enumeration.localEvents line 768
121. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Enumeration.localEvents_length line 771
122. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Enumeration.ordered_event line 774
123. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Enumeration.ordered_dart line 781
124. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Enumeration.card_cube line 792
125. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Enumeration.card_pairCube line 795
126. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Enumeration.card_localEvent line 799
127. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Enumeration.card_event line 803
128. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Enumeration.card_address line 807
129. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Enumeration.card_vertex line 811
130. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Enumeration.card_dart line 816
131. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Enumeration.localCount_formula line 821