OAI/Combinatorics/IndependentSets/PCP/ReadRelation.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.ReadRelation.Alphabet line 15
  2. abbrev OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.ReadRelation.State line 16
  3. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.ReadRelation.relationEquiv line 18
  4. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.ReadRelation.relationFintype line 24
  5. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.ReadRelation.stateFintype line 27
  6. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.ReadRelation.readSlot line 32
  7. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.ReadRelation.stepAux_readSlot line 42
  8. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.ReadRelation.readSlots line 52
  9. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.ReadRelation.indexedWords line 58
  10. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.ReadRelation.fillSlots line 61
  11. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.ReadRelation.fillSlots_preserves_correct line 67
  12. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.ReadRelation.fillSlots_mem line 79
  13. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.ReadRelation.fillSlots_finRange line 92
  14. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.ReadRelation.indexedWords_finRange line 99
  15. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.ReadRelation.stepAux_readSlots line 111
  16. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.ReadRelation.readRelation line 127
  17. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.ReadRelation.stepAux_readRelation line 132
  18. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.ReadRelation.stepAux_readRelation_fromTapes line 143
  19. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.ReadRelation.readSlots_pushBound line 157
  20. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.ReadRelation.readRelation_pushBound line 167
  21. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.ReadRelation.parser line 173
  22. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.ReadRelation.parser_pushBound line 178
  23. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.ReadRelation.parserStep line 183
  24. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.ReadRelation.parserTrace line 197
  25. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.ReadRelation.parserInTime line 209