OAI/Computability/MinUncut/Machines/AlphabetGraph.lean

GitHub source file

125 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.MinUncutGames.Foundations.PCP.AlphabetGraph.Address line 14
2. abbrev OAI.MinUncutGames.Foundations.PCP.AlphabetGraph.LocalEvent line 16
3. abbrev OAI.MinUncutGames.Foundations.PCP.AlphabetGraph.Event line 19
4. abbrev OAI.MinUncutGames.Foundations.PCP.AlphabetGraph.legal line 23
5. instance OAI.MinUncutGames.Foundations.PCP.AlphabetGraph.legalDecidable line 26
6. def OAI.MinUncutGames.Foundations.PCP.AlphabetGraph.restrictTape line 30
7. def OAI.MinUncutGames.Foundations.PCP.AlphabetGraph.extendTape line 33
8. def OAI.MinUncutGames.Foundations.PCP.AlphabetGraph.globalizeQuery line 37
9. def OAI.MinUncutGames.Foundations.PCP.AlphabetGraph.verifier line 42
10. def OAI.MinUncutGames.Foundations.PCP.AlphabetGraph.vertexBlock line 49
11. def OAI.MinUncutGames.Foundations.PCP.AlphabetGraph.edgeOracle line 52
12. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetGraph.oracleAnswer_globalize line 57
13. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetGraph.response_eq_local line 69
14. def OAI.MinUncutGames.Foundations.PCP.AlphabetGraph.eventReject line 82
15. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetGraph.eventReject_eq_local line 87
16. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetGraph.expect_prod line 100
17. def OAI.MinUncutGames.Foundations.PCP.AlphabetGraph.localAverage line 105
18. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetGraph.expect_restrict_five line 108
19. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetGraph.localAverage_eq_tester line 145
20. def OAI.MinUncutGames.Foundations.PCP.AlphabetGraph.average line 163
21. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetGraph.average_eq_testers line 168
22. def OAI.MinUncutGames.Foundations.PCP.AlphabetGraph.decodedLabeling line 177
23. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetGraph.local_gap line 180
24. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetGraph.average_gap line 197
25. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetGraph.expect_rejection_eq_count line 205
26. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetGraph.average_eq_count line 218
27. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetGraph.card_event line 225
28. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetGraph.card_localEvent line 230
29. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetGraph.card_address line 237
30. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetGraph.rejection_count_bound line 243
31. def OAI.MinUncutGames.Foundations.PCP.AlphabetGraph.honestAssignment line 270
32. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetGraph.honest_vertexBlock line 275
33. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetGraph.honest_edgeOracle line 279
34. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetGraph.honest_event line 288
35. def OAI.MinUncutGames.Foundations.PCP.AlphabetGraph.graph line 300
36. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetGraph.perfect_completeness line 305
37. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetGraph.gap_transfer line 311
38. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetGraph.alphabet_card line 337
39. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Enumeration.bitValue line 347
40. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Enumeration.boolEquiv line 349
41. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Enumeration.boolEquiv_val line 351
42. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Enumeration.productEquiv line 354
43. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Enumeration.productEquiv_val line 358
44. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Enumeration.sumEquiv line 364
45. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Enumeration.sumEquiv_inl_val line 368
46. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Enumeration.sumEquiv_inr_val line 372
47. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Enumeration.tapeCount line 376
48. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Enumeration.pairTapeCount line 377
49. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Enumeration.fiveTapeCount line 378
50. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Enumeration.localCount line 379
51. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Enumeration.eventCount line 380
52. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Enumeration.addressCount line 381
53. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Enumeration.vertexCount line 382
54. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Enumeration.dartCount line 383
55. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Enumeration.cubeEquiv line 385
56. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Enumeration.cubeRank line 388
57. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Enumeration.cubeUnrank line 389
58. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Enumeration.cubeUnrank_cubeRank line 392
59. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Enumeration.cubeRank_cubeUnrank line 395
60. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Enumeration.cubeUnrank_digit line 398
61. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Enumeration.cubeEquiv_val line 406
62. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Enumeration.pairIndex line 412
63. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Enumeration.pairIndex_val line 414
64. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Enumeration.pairCubeEquiv line 419
65. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Enumeration.pairCubeRank line 422
66. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Enumeration.pairCubeUnrank line 425
67. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Enumeration.pairCubeUnrank_pairCubeRank line 428
68. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Enumeration.pairCubeRank_pairCubeUnrank line 431
69. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Enumeration.pairCubeEquiv_val line 434
70. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Enumeration.inputCoordinateEquiv line 439
71. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Enumeration.fivePairTapesEquiv line 443
72. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Enumeration.localEventEquiv line 452
73. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Enumeration.eventEquiv line 457
74. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Enumeration.addressEquiv line 461
75. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Enumeration.vertexEquiv line 466
76. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Enumeration.dartEquiv line 471
77. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Enumeration.labelEquiv line 476
78. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Enumeration.labelEquiv_val line 478
79. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Enumeration.inputCoordinateEquiv_val line 482
80. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Enumeration.fivePairTapesEquiv_val line 487
81. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Enumeration.localEventEquiv_val line 495
82. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Enumeration.eventEquiv_val line 504
83. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Enumeration.addressEquiv_inl_val line 511
84. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Enumeration.addressEquiv_inr_val line 518
85. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Enumeration.vertexEquiv_event_val line 525
86. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Enumeration.vertexEquiv_vertexAddress_val line 529
87. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Enumeration.vertexEquiv_edgeAddress_val line 536
88. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Enumeration.dartEquiv_val line 544
89. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Enumeration.dartEquiv_reverse_val line 552
90. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Enumeration.ordered line 558
91. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Enumeration.ordered_length line 561
92. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Enumeration.mem_ordered line 564
93. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Enumeration.ordered_nodup line 569
94. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Enumeration.ordered_refl line 574
95. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Enumeration.ordered_bool line 576
96. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Enumeration.ordered_trans_finCongr line 578
97. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Enumeration.ordered_product line 584
98. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Enumeration.ordered_sum line 600
99. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Enumeration.localEvents line 620
100. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Enumeration.localEvents_length line 623
101. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Enumeration.ordered_event line 626
102. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Enumeration.ordered_dart line 633
103. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Enumeration.card_cube line 645
104. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Enumeration.card_pairCube line 648
105. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Enumeration.card_localEvent line 652
106. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Enumeration.card_event line 656
107. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Enumeration.card_address line 660
108. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Enumeration.card_vertex line 664
109. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Enumeration.card_dart line 669
110. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Enumeration.localCount_formula line 674
111. abbrev OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Queries.RawQuery line 683
112. abbrev OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Queries.LocalEvent line 686
113. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Queries.mask line 688
114. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Queries.xorTape line 691
115. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Queries.andTape line 693
116. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Queries.inputPairTape line 695
117. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Queries.query line 698
118. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Queries.globalize line 719
119. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Queries.mask_idempotent line 724
120. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Queries.mask_of_empty line 729
121. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Queries.query_is_masked line 735
122. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Queries.extendQuery line 745
123. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Queries.query_eq_extend_eventQueries line 751
124. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Queries.globalize_extendQuery line 766
125. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Queries.globalize_query line 776