OAI/Combinatorics/IndependentSets/PCP/Semantics2.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Table.rowFromDart_eq_graphRow line 9
  2. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Table.rows_eq_graphRows line 42
  3. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Table.rows_valid line 53
  4. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Table.build line 57
  5. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Table.build_vertices line 63
  6. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Table.build_darts line 66
  7. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Table.table_rows_congr line 69
  8. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Table.semantics_rows_congr line 75
  9. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Table.build_eq_ofEnumeratedGraph line 82
  10. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Table.semantics_build line 90
  11. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Table.decode_build line 98
  12. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Table.edgeSatisfied_build line 106
  13. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Table.rejectionCount_build line 119
  14. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Table.perfect_completeness line 130
  15. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Table.gap_transfer line 144
  16. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Table.rowList_eq_ordered line 168
  17. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Table.tableWords_eq_ordered line 177
  18. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Table.rowList_length line 186
  19. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Table.tableWords_length line 190
  20. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Table.tableBits_length_le line 195