OAI/Combinatorics/IndependentSets/PCP/CompareLoop.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.CompareLoop.Label line 14
  2. instance OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.CompareLoop.(instance at line 19) line 19
  3. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.CompareLoop.statement line 26
  4. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.CompareLoop.compareProgram_at line 45
  5. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.CompareLoop.compareWordsInTime line 55
  6. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.CompareLoop.comparisonTime line 111
  7. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.CompareLoop.encodeWord_eq_iff line 114
  8. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.CompareLoop.compareInTime line 123
  9. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.CompareLoop.comparisonTime_le line 140
  10. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.CompareLoop.comparisonTime_le_of_lt line 147
  11. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.CompareLoop.compareWordsInTime_bounded line 154
  12. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.CompareLoop.rowLoop line 173
  13. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.CompareLoop.rowState line 176
  14. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.CompareLoop.rowLoop_eq_graph line 179
  15. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.CompareLoop.rowContext_eq line 185
  16. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.CompareLoop.compareRowInTime line 192
  17. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.CompareLoop.relationFromRowState line 210