OAI/Combinatorics/IndependentSets/PCP/Finish.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Finish.afterReversal line 13
2. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Finish.afterReversal_output line 16
3. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Finish.afterReversal_reversed line 20
4. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Finish.finishBudget line 24
5. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Finish.reverseInTime line 27
6. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Finish.cleared_eq_haltList line 41
7. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Finish.cleanupInTime line 48
8. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Finish.finishInTime line 64
9. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Finish.afterReversal_selected_length_le line 85
10. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Finish.stackLength_after_prefix line 92
11. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Finish.finishBudget_le_of_prefix line 104
12. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Finish.completedPolynomial line 126
13. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Finish.finishAfterPrefix line 131
14. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Finish.finishAfterPolynomialPrefix line 147