OAI/Computability/MinUncut/Machines/Relations.lean

GitHub source file

73 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Relations.sameAddress line 13
2. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Relations.sameAddress_refl line 18
3. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Relations.globalize_eq_iff line 22
4. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Relations.eqProfile line 38
5. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Relations.eqProfile_refl line 41
6. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Relations.canonicalSlot line 44
7. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Relations.canonicalSlot_profile line 47
8. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Relations.canonicalSlot_le line 53
9. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Relations.RepeatedConsistent line 58
10. instance OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Relations.repeatedConsistentDecidable line 62
11. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Relations.incidenceAccept line 67
12. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Relations.predicate line 73
13. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Relations.relation line 79
14. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Relations.relationAt_relation line 86
15. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Relations.relation_reverse line 94
16. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Relations.oldPredicate line 102
17. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Relations.relationFromTable line 105
18. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Relations.oldPredicate_relationAt line 109
19. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Relations.relationFromTable_eq line 112
20. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Relations.eqProfile_query_iff line 120
21. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Relations.canonicalSlot_eq line 128
22. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Relations.repeatedConsistent_iff line 137
23. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Relations.verifier_accepts line 148
24. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Relations.incidenceAccept_eq line 155
25. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Relations.relationAt_relation_graph line 167
26. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Table.rowFromDart line 184
27. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Table.rows line 202
28. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Table.rows_at line 208
29. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Table.rows_reverseIndex line 214
30. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Table.dartRow_ext line 222
31. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Table.relation_ext line 232
32. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Table.rowFromDart_eq_graphRow line 243
33. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Table.rows_eq_graphRows line 283
34. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Table.rows_valid line 294
35. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Table.build line 298
36. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Table.build_vertices line 304
37. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Table.build_darts line 307
38. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Table.table_rows_congr line 310
39. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Table.semantics_rows_congr line 316
40. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Table.build_eq_ofEnumeratedGraph line 323
41. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Table.semantics_build line 331
42. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Table.decode_build line 339
43. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Table.edgeSatisfied_build line 347
44. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Table.rejectionCount_build line 360
45. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Table.perfect_completeness line 371
46. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Table.gap_transfer line 385
47. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Table.rowList_eq_ordered line 409
48. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Table.tableWords_eq_ordered line 418
49. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Table.rowList_length line 427
50. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Table.tableWords_length line 431
51. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Table.tableBits_length_le line 436
52. abbrev OAI.MinUncutGames.Foundations.PCP.AlphabetGraphBounds.OutputVertex line 450
53. abbrev OAI.MinUncutGames.Foundations.PCP.AlphabetGraphBounds.OutputDart line 453
54. def OAI.MinUncutGames.Foundations.PCP.AlphabetGraphBounds.localEventFactor line 455
55. def OAI.MinUncutGames.Foundations.PCP.AlphabetGraphBounds.vertexFactor line 458
56. def OAI.MinUncutGames.Foundations.PCP.AlphabetGraphBounds.dartFactor line 460
57. def OAI.MinUncutGames.Foundations.PCP.AlphabetGraphBounds.sizeFactor line 462
58. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetGraphBounds.sizeFactor_positive line 464
59. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetGraphBounds.gap_transfer_real line 471
60. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetGraphBounds.card_output_vertex line 510
61. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetGraphBounds.card_output_dart line 519
62. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetGraphBounds.card_output_total line 525
63. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetGraphBounds.card_output_total_le line 532
64. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetGraphBounds.card_output_vertex_le line 549
65. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetGraphBounds.card_output_dart_le line 554
66. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTableBounds.gap_transfer_real line 567
67. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTableBounds.build_vertices line 595
68. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTableBounds.build_darts line 605
69. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTableBounds.build_total line 613
70. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTableBounds.build_total_le line 620
71. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTableBounds.build_vertices_le line 637
72. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTableBounds.build_darts_le line 642
73. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTableBounds.sizeFactor_positive line 647