OAI/Computability/DirectedFeedback/Encoding/Queries.lean

GitHub source file

88 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.DFVSGames.Foundations.PCP.AlphabetTable.Queries.RawQuery line 11
2. abbrev OAI.DFVSGames.Foundations.PCP.AlphabetTable.Queries.LocalEvent line 14
3. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Queries.mask line 16
4. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Queries.xorTape line 19
5. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Queries.andTape line 21
6. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Queries.inputPairTape line 23
7. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Queries.query line 26
8. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Queries.globalize line 47
9. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Queries.mask_idempotent line 52
10. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Queries.mask_of_empty line 57
11. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Queries.query_is_masked line 63
12. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Queries.extendQuery line 73
13. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Queries.query_eq_extend_eventQueries line 79
14. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Queries.globalize_extendQuery line 94
15. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Queries.globalize_query line 104
16. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Relations.sameAddress line 122
17. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Relations.sameAddress_refl line 127
18. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Relations.globalize_eq_iff line 131
19. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Relations.eqProfile line 147
20. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Relations.eqProfile_refl line 150
21. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Relations.canonicalSlot line 153
22. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Relations.canonicalSlot_profile line 156
23. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Relations.canonicalSlot_le line 162
24. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Relations.RepeatedConsistent line 167
25. instance OAI.DFVSGames.Foundations.PCP.AlphabetTable.Relations.repeatedConsistentDecidable line 171
26. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Relations.incidenceAccept line 176
27. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Relations.predicate line 182
28. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Relations.relation line 188
29. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Relations.relationAt_relation line 195
30. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Relations.relation_reverse line 203
31. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Relations.oldPredicate line 211
32. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Relations.relationFromTable line 214
33. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Relations.oldPredicate_relationAt line 218
34. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Relations.relationFromTable_eq line 221
35. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Relations.eqProfile_query_iff line 230
36. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Relations.canonicalSlot_eq line 238
37. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Relations.repeatedConsistent_iff line 247
38. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Relations.verifier_accepts line 258
39. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Relations.incidenceAccept_eq line 265
40. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Relations.relationAt_relation_graph line 277
41. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Table.rowFromDart line 296
42. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Table.rows line 314
43. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Table.rows_at line 320
44. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Table.rows_reverseIndex line 326
45. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Table.dartRow_ext_inline_Table line 334
46. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Table.relation_ext_inline_Table line 344
47. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Table.rowFromDart_eq_graphRow line 356
48. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Table.rows_eq_graphRows line 394
49. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Table.rows_valid line 405
50. def OAI.DFVSGames.Foundations.PCP.AlphabetTable.Table.build line 409
51. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Table.build_vertices line 415
52. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Table.build_darts line 418
53. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Table.table_rows_congr_inline_Table line 421
54. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Table.semantics_rows_congr_inline_Table line 427
55. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Table.build_eq_ofEnumeratedGraph line 434
56. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Table.semantics_build line 442
57. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Table.decode_build line 450
58. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Table.edgeSatisfied_build line 458
59. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Table.rejectionCount_build line 471
60. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Table.perfect_completeness line 482
61. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Table.gap_transfer line 496
62. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Table.rowList_eq_ordered line 520
63. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Table.tableWords_eq_ordered line 529
64. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Table.rowList_length line 538
65. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Table.tableWords_length line 542
66. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTable.Table.tableBits_length_le line 547
67. abbrev OAI.DFVSGames.Foundations.PCP.AlphabetGraphBounds.OutputVertex line 563
68. abbrev OAI.DFVSGames.Foundations.PCP.AlphabetGraphBounds.OutputDart line 566
69. def OAI.DFVSGames.Foundations.PCP.AlphabetGraphBounds.localEventFactor line 568
70. def OAI.DFVSGames.Foundations.PCP.AlphabetGraphBounds.vertexFactor line 571
71. def OAI.DFVSGames.Foundations.PCP.AlphabetGraphBounds.dartFactor line 573
72. def OAI.DFVSGames.Foundations.PCP.AlphabetGraphBounds.sizeFactor line 575
73. theorem OAI.DFVSGames.Foundations.PCP.AlphabetGraphBounds.sizeFactor_positive line 577
74. theorem OAI.DFVSGames.Foundations.PCP.AlphabetGraphBounds.gap_transfer_real line 584
75. theorem OAI.DFVSGames.Foundations.PCP.AlphabetGraphBounds.card_output_vertex line 623
76. theorem OAI.DFVSGames.Foundations.PCP.AlphabetGraphBounds.card_output_dart line 633
77. theorem OAI.DFVSGames.Foundations.PCP.AlphabetGraphBounds.card_output_total line 640
78. theorem OAI.DFVSGames.Foundations.PCP.AlphabetGraphBounds.card_output_total_le line 648
79. theorem OAI.DFVSGames.Foundations.PCP.AlphabetGraphBounds.card_output_vertex_le line 666
80. theorem OAI.DFVSGames.Foundations.PCP.AlphabetGraphBounds.card_output_dart_le line 672
81. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTableBounds.gap_transfer_real line 687
82. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTableBounds.build_vertices line 715
83. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTableBounds.build_darts line 725
84. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTableBounds.build_total line 733
85. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTableBounds.build_total_le line 740
86. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTableBounds.build_vertices_le line 757
87. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTableBounds.build_darts_le line 762
88. theorem OAI.DFVSGames.Foundations.PCP.AlphabetTableBounds.sizeFactor_positive line 767