OAI/Combinatorics/IndependentSets/PCP/Semantics.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Relations.eqProfile_query_iff line 15
2. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Relations.canonicalSlot_eq line 23
3. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Relations.repeatedConsistent_iff line 32
4. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Relations.verifier_accepts line 43
5. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Relations.incidenceAccept_eq line 50
6. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Relations.relationAt_relation_graph line 62
7. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Table.rowFromDart line 78
8. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Table.rows line 96
9. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Table.rows_at line 102
10. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Table.rows_reverseIndex line 108
11. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Table.dartRow_ext line 116
12. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Table.relation_ext line 126