OAI/Combinatorics/IndependentSets/Machines/Initialization.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Initialization.inputTapes line 14
  2. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Initialization.rowsBits line 18
  3. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Initialization.headerBits line 21
  4. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Initialization.setupTapes line 25
  5. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Initialization.loopTapes line 33
  6. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Initialization.loopStart line 42
  7. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Initialization.setupResult_eq line 46
  8. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Initialization.headerResult_eq line 52
  9. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Initialization.machineInitial_eq line 57
  10. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Initialization.setupInTime line 67
  11. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Initialization.headerView_at line 86
  12. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Initialization.headerInTime line 96
  13. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Initialization.time line 134
  14. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Initialization.time_eq line 136
  15. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Initialization.initializeInTime line 140