OAI/Combinatorics/IndependentSets/PCP/Queries.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Queries.RawQuery line 11
  2. abbrev OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Queries.LocalEvent line 14
  3. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Queries.mask line 16
  4. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Queries.xorTape line 19
  5. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Queries.andTape line 21
  6. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Queries.inputPairTape line 23
  7. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Queries.query line 26
  8. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Queries.globalize line 47
  9. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Queries.mask_idempotent line 52
  10. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Queries.mask_of_empty line 57
  11. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Queries.query_is_masked line 63
  12. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Queries.extendQuery line 73
  13. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Queries.query_eq_extend_eventQueries line 79
  14. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Queries.globalize_extendQuery line 94
  15. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Queries.globalize_query line 104
  16. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Relations.sameAddress line 120
  17. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Relations.sameAddress_refl line 125
  18. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Relations.globalize_eq_iff line 129
  19. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Relations.eqProfile line 145
  20. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Relations.eqProfile_refl line 148
  21. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Relations.canonicalSlot line 151
  22. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Relations.canonicalSlot_profile line 154
  23. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Relations.canonicalSlot_le line 160
  24. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Relations.RepeatedConsistent line 165
  25. instance OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Relations.repeatedConsistentDecidable line 169
  26. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Relations.incidenceAccept line 174
  27. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Relations.predicate line 180
  28. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Relations.relation line 186
  29. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Relations.relationAt_relation line 193
  30. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Relations.relation_reverse line 201
  31. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Relations.oldPredicate line 209
  32. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Relations.relationFromTable line 212
  33. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Relations.oldPredicate_relationAt line 216
  34. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Relations.relationFromTable_eq line 219