OAI/Computability/MinUncut/PCP/PoweringOpinionTables.lean

GitHub source file

116 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MinUncutGames.Foundations.PCP.PoweringOpinionTables.match_in_tail line 14
2. def OAI.MinUncutGames.Foundations.PCP.PoweringOpinionTables.firstIndex line 21
3. theorem OAI.MinUncutGames.Foundations.PCP.PoweringOpinionTables.get_firstIndex line 28
4. theorem OAI.MinUncutGames.Foundations.PCP.PoweringOpinionTables.firstIndex_matches line 41
5. theorem OAI.MinUncutGames.Foundations.PCP.PoweringOpinionTables.firstIndex_is_first line 46
6. abbrev OAI.MinUncutGames.Foundations.PCP.PoweringOpinionTables.AddressIndex line 62
7. def OAI.MinUncutGames.Foundations.PCP.PoweringOpinionTables.addressIndex line 66
8. theorem OAI.MinUncutGames.Foundations.PCP.PoweringOpinionTables.addressIndex_get line 73
9. theorem OAI.MinUncutGames.Foundations.PCP.PoweringOpinionTables.addressIndex_matches line 82
10. theorem OAI.MinUncutGames.Foundations.PCP.PoweringOpinionTables.addressIndex_is_first line 88
11. theorem OAI.MinUncutGames.Foundations.PCP.PoweringOpinionTables.addressIndex_lt line 94
12. abbrev OAI.MinUncutGames.Foundations.PCP.PoweringOpinionTables.LabelTable line 100
13. def OAI.MinUncutGames.Foundations.PCP.PoweringOpinionTables.labelTable line 102
14. theorem OAI.MinUncutGames.Foundations.PCP.PoweringOpinionTables.labelTable_get line 105
15. theorem OAI.MinUncutGames.Foundations.PCP.PoweringOpinionTables.labelTable_addressIndex line 110
16. structure OAI.MinUncutGames.Foundations.PCP.PoweringOpinionTables.WalkOpinionRow line 117
17. abbrev OAI.MinUncutGames.Foundations.PCP.PoweringOpinionTables.WalkRows line 122
18. def OAI.MinUncutGames.Foundations.PCP.PoweringOpinionTables.walkRows line 124
19. theorem OAI.MinUncutGames.Foundations.PCP.PoweringOpinionTables.walkRows_edge line 131
20. theorem OAI.MinUncutGames.Foundations.PCP.PoweringOpinionTables.walkRows_tail_value line 136
21. theorem OAI.MinUncutGames.Foundations.PCP.PoweringOpinionTables.walkRows_head_value line 144
22. theorem OAI.MinUncutGames.Foundations.PCP.PoweringOpinionTables.walkRows_length line 152
23. def OAI.MinUncutGames.Foundations.PCP.PoweringOpinionTables.rowsAccepts line 157
24. theorem OAI.MinUncutGames.Foundations.PCP.PoweringOpinionTables.rowsAccepts_walkRows line 162
25. abbrev OAI.MinUncutGames.Foundations.PCP.GenericGraphTables.Label line 180
26. abbrev OAI.MinUncutGames.Foundations.PCP.GenericGraphTables.RelationTable line 181
27. def OAI.MinUncutGames.Foundations.PCP.GenericGraphTables.relationIndex line 185
28. theorem OAI.MinUncutGames.Foundations.PCP.GenericGraphTables.relationIndex_val line 187
29. def OAI.MinUncutGames.Foundations.PCP.GenericGraphTables.relationAt line 190
30. def OAI.MinUncutGames.Foundations.PCP.GenericGraphTables.relationOf line 193
31. theorem OAI.MinUncutGames.Foundations.PCP.GenericGraphTables.relationAt_relationOf line 196
32. structure OAI.MinUncutGames.Foundations.PCP.GenericGraphTables.DartRow line 200
33. abbrev OAI.MinUncutGames.Foundations.PCP.GenericGraphTables.Rows line 205
34. def OAI.MinUncutGames.Foundations.PCP.GenericGraphTables.reverseAt line 207
35. def OAI.MinUncutGames.Foundations.PCP.GenericGraphTables.acceptsAt line 210
36. def OAI.MinUncutGames.Foundations.PCP.GenericGraphTables.Valid line 213
37. instance OAI.MinUncutGames.Foundations.PCP.GenericGraphTables.(instance at line 217) line 217
38. structure OAI.MinUncutGames.Foundations.PCP.GenericGraphTables.Table line 221
39. def OAI.MinUncutGames.Foundations.PCP.GenericGraphTables.rowList line 227
40. theorem OAI.MinUncutGames.Foundations.PCP.GenericGraphTables.rowList_length line 229
41. def OAI.MinUncutGames.Foundations.PCP.GenericGraphTables.semantics line 232
42. theorem OAI.MinUncutGames.Foundations.PCP.GenericGraphTables.semantics_reverse line 243
43. theorem OAI.MinUncutGames.Foundations.PCP.GenericGraphTables.semantics_tail line 246
44. theorem OAI.MinUncutGames.Foundations.PCP.GenericGraphTables.semantics_accepts line 249
45. def OAI.MinUncutGames.Foundations.PCP.GenericGraphTables.graphRows line 252
46. theorem OAI.MinUncutGames.Foundations.PCP.GenericGraphTables.reverseAt_graphRows line 255
47. theorem OAI.MinUncutGames.Foundations.PCP.GenericGraphTables.acceptsAt_graphRows line 260
48. theorem OAI.MinUncutGames.Foundations.PCP.GenericGraphTables.graphRows_valid line 265
49. def OAI.MinUncutGames.Foundations.PCP.GenericGraphTables.ofGraph line 273
50. theorem OAI.MinUncutGames.Foundations.PCP.GenericGraphTables.semantics_ofGraph_reverse line 276
51. theorem OAI.MinUncutGames.Foundations.PCP.GenericGraphTables.semantics_ofGraph_tail line 281
52. theorem OAI.MinUncutGames.Foundations.PCP.GenericGraphTables.semantics_ofGraph_accepts line 287
53. theorem OAI.MinUncutGames.Foundations.PCP.GenericGraphTables.semantics_ofGraph_edgeSatisfied line 292
54. theorem OAI.MinUncutGames.Foundations.PCP.GenericGraphTables.constraintGraph_ext line 297
55. theorem OAI.MinUncutGames.Foundations.PCP.GenericGraphTables.semantics_ofGraph line 311
56. theorem OAI.MinUncutGames.Foundations.PCP.GenericGraphTables.semantics_ofGraph_rejectionCount line 320
57. def OAI.MinUncutGames.Foundations.PCP.GenericGraphTables.enumeratedGraph line 326
58. theorem OAI.MinUncutGames.Foundations.PCP.GenericGraphTables.enumeratedGraph_edgeSatisfied line 342
59. theorem OAI.MinUncutGames.Foundations.PCP.GenericGraphTables.enumeratedGraph_rejectionCount line 350
60. def OAI.MinUncutGames.Foundations.PCP.GenericGraphTables.ofEnumeratedGraph line 362
61. def OAI.MinUncutGames.Foundations.PCP.GenericGraphTables.bitWord line 366
62. def OAI.MinUncutGames.Foundations.PCP.GenericGraphTables.parseBit line 368
63. theorem OAI.MinUncutGames.Foundations.PCP.GenericGraphTables.parseBit_bitWord line 373
64. theorem OAI.MinUncutGames.Foundations.PCP.GenericGraphTables.parseBits_bitWords line 376
65. def OAI.MinUncutGames.Foundations.PCP.GenericGraphTables.relationWords line 382
66. theorem OAI.MinUncutGames.Foundations.PCP.GenericGraphTables.relationWords_length line 384
67. def OAI.MinUncutGames.Foundations.PCP.GenericGraphTables.parseRelation line 387
68. theorem OAI.MinUncutGames.Foundations.PCP.GenericGraphTables.parseRelation_encoded line 393
69. def OAI.MinUncutGames.Foundations.PCP.GenericGraphTables.rowWords line 400
70. def OAI.MinUncutGames.Foundations.PCP.GenericGraphTables.parseRow line 403
71. theorem OAI.MinUncutGames.Foundations.PCP.GenericGraphTables.parseRow_encoded line 411
72. def OAI.MinUncutGames.Foundations.PCP.GenericGraphTables.parseRows line 419
73. theorem OAI.MinUncutGames.Foundations.PCP.GenericGraphTables.parseRows_encoded line 427
74. def OAI.MinUncutGames.Foundations.PCP.GenericGraphTables.tableWords line 433
75. def OAI.MinUncutGames.Foundations.PCP.GenericGraphTables.tableBits line 436
76. def OAI.MinUncutGames.Foundations.PCP.GenericGraphTables.decodeTableWords line 438
77. theorem OAI.MinUncutGames.Foundations.PCP.GenericGraphTables.decodeTableWords_encoded line 449
78. def OAI.MinUncutGames.Foundations.PCP.GenericGraphTables.decodeTableBits line 457
79. theorem OAI.MinUncutGames.Foundations.PCP.GenericGraphTables.decodeTableBits_encoded line 460
80. def OAI.MinUncutGames.Foundations.PCP.GenericGraphTables.encoding line 464
81. theorem OAI.MinUncutGames.Foundations.PCP.GenericGraphTables.tableBits_injective line 469
82. theorem OAI.MinUncutGames.Foundations.PCP.GenericGraphTables.rowWords_length line 471
83. theorem OAI.MinUncutGames.Foundations.PCP.GenericGraphTables.rowsWords_length line 477
84. theorem OAI.MinUncutGames.Foundations.PCP.GenericGraphTables.tableWords_length line 483
85. theorem OAI.MinUncutGames.Foundations.PCP.GenericGraphTables.tableWords_length_le_bits line 488
86. theorem OAI.MinUncutGames.Foundations.PCP.GenericGraphTables.relationBits_length_le line 493
87. theorem OAI.MinUncutGames.Foundations.PCP.GenericGraphTables.rowBits_length_le line 501
88. theorem OAI.MinUncutGames.Foundations.PCP.GenericGraphTables.rowsBits_length_le line 510
89. theorem OAI.MinUncutGames.Foundations.PCP.GenericGraphTables.tableBits_length_le line 520
90. theorem OAI.MinUncutGames.Foundations.PCP.GenericGraphTables.vertices_le_tableBits_length line 529
91. theorem OAI.MinUncutGames.Foundations.PCP.GenericGraphTables.darts_le_tableBits_length line 535
92. def OAI.MinUncutGames.Foundations.PCP.PoweringTables.labelCount line 549
93. def OAI.MinUncutGames.Foundations.PCP.PoweringTables.dartCount line 551
94. def OAI.MinUncutGames.Foundations.PCP.PoweringTables.mathematicalGraph line 553
95. def OAI.MinUncutGames.Foundations.PCP.PoweringTables.rowAccepts line 559
96. theorem OAI.MinUncutGames.Foundations.PCP.PoweringTables.rowAccepts_eq line 568
97. def OAI.MinUncutGames.Foundations.PCP.PoweringTables.table line 578
98. theorem OAI.MinUncutGames.Foundations.PCP.PoweringTables.table_vertices line 583
99. theorem OAI.MinUncutGames.Foundations.PCP.PoweringTables.table_darts line 586
100. theorem OAI.MinUncutGames.Foundations.PCP.PoweringTables.semantics_table line 589
101. theorem OAI.MinUncutGames.Foundations.PCP.PoweringTables.table_accepts line 595
102. theorem OAI.MinUncutGames.Foundations.PCP.PoweringTables.table_reverse line 603
103. def OAI.MinUncutGames.Foundations.PCP.PoweringTables.outputBits line 615
104. def OAI.MinUncutGames.Foundations.PCP.PoweringTables.transform line 618
105. theorem OAI.MinUncutGames.Foundations.PCP.PoweringCounting.constraint_rejection_mean_eq_count line 632
106. theorem OAI.MinUncutGames.Foundations.PCP.PoweringCounting.constraint_rejection_lower_iff line 647
107. theorem OAI.MinUncutGames.Foundations.PCP.PoweringCounting.edgeDensity_eq_bit_mean line 656
108. theorem OAI.MinUncutGames.Foundations.PCP.PoweringCounting.base_edgeDensity_eq_rejection_count line 670
109. theorem OAI.MinUncutGames.Foundations.PCP.PoweringCounting.base_count_lower_to_density line 688
110. theorem OAI.MinUncutGames.Foundations.PCP.PoweringCounting.powered_rejection_mean_eq_count line 698
111. theorem OAI.MinUncutGames.Foundations.PCP.PoweringCounting.path_rejection_mean_eq_count line 708
112. theorem OAI.MinUncutGames.Foundations.PCP.PoweringCounting.powered_density_lower_to_count line 719
113. theorem OAI.MinUncutGames.Foundations.PCP.PoweringCounting.natCard_dart line 731
114. theorem OAI.MinUncutGames.Foundations.PCP.PoweringCounting.fintypeCard_dart line 735
115. theorem OAI.MinUncutGames.Foundations.PCP.PoweringCounting.natCard_poweredAlphabet line 740
116. theorem OAI.MinUncutGames.Foundations.PCP.PoweringCounting.natCard_finitePortAlphabet line 745