OAI/Computability/MinUncut/PCP/RawInitialPredicate.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MinUncutGames.Foundations.PCP.RawInitialRows.Signs line 10
  2. abbrev OAI.MinUncutGames.Foundations.PCP.RawInitialRows.Names line 11
  3. def OAI.MinUncutGames.Foundations.PCP.RawInitialRows.clauseSigns line 13
  4. def OAI.MinUncutGames.Foundations.PCP.RawInitialRows.clauseNames line 16
  5. def OAI.MinUncutGames.Foundations.PCP.RawInitialRows.nameWord line 19
  6. def OAI.MinUncutGames.Foundations.PCP.RawInitialRows.decodedLabel line 24
  7. def OAI.MinUncutGames.Foundations.PCP.RawInitialRows.incidencePredicate line 27
  8. def OAI.MinUncutGames.Foundations.PCP.RawInitialRows.relationPredicate line 35
  9. def OAI.MinUncutGames.Foundations.PCP.RawInitialRows.relationWordsFor line 40
  10. theorem OAI.MinUncutGames.Foundations.PCP.RawInitialRows.relationWordsFor_length line 43
  11. def OAI.MinUncutGames.Foundations.PCP.RawInitialRows.incidenceWords line 47
  12. def OAI.MinUncutGames.Foundations.PCP.RawInitialRows.clauseWords line 53
  13. def OAI.MinUncutGames.Foundations.PCP.RawInitialRows.dummyWords line 61
  14. def OAI.MinUncutGames.Foundations.PCP.RawInitialRows.orderedList line 64
  15. theorem OAI.MinUncutGames.Foundations.PCP.RawInitialRows.orderedList_cast line 67
  16. theorem OAI.MinUncutGames.Foundations.PCP.RawInitialRows.orderedList_prod line 72
  17. theorem OAI.MinUncutGames.Foundations.PCP.RawInitialRows.orderedList_sum line 96
  18. def OAI.MinUncutGames.Foundations.PCP.RawInitialRows.clauseDarts line 110
  19. theorem OAI.MinUncutGames.Foundations.PCP.RawInitialRows.orderedList_dartOrder line 115
  20. def OAI.MinUncutGames.Foundations.PCP.RawInitialRows.rowFor line 128
  21. theorem OAI.MinUncutGames.Foundations.PCP.RawInitialRows.rowList_table line 134
  22. theorem OAI.MinUncutGames.Foundations.PCP.RawInitialRows.rowWords_incidence line 140
  23. theorem OAI.MinUncutGames.Foundations.PCP.RawInitialRows.rowWords_dummy line 160
  24. theorem OAI.MinUncutGames.Foundations.PCP.RawInitialRows.clauseDarts_rowWords line 173
  25. theorem OAI.MinUncutGames.Foundations.PCP.RawInitialRows.tableWords_eq line 179