OAI/Combinatorics/IndependentSets/PCP/LoopInitialization.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.LoopInitialization.initialization_ready line 12
2. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Loop.zeroGuardInTime line 45
3. structure OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Loop.LoopResult line 59
4. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Loop.runRemaining line 71
5. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Loop.prefixTime line 103
6. structure OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Loop.PrefixResult line 106
7. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Loop.runPrefix line 116
8. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Loop.PrefixResult.reversed line 139
9. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Loop.PrefixResult.output line 143