OAI/Combinatorics/IndependentSets/PCP/Cleanup.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Cleanup.Alphabet line 14
2. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Cleanup.finish line 16
3. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Cleanup.instruction line 21
4. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Cleanup.instruction_drain line 30
5. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Cleanup.instruction_finish line 38
6. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Cleanup.clearTapes line 43
7. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Cleanup.actualCost line 48
8. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Cleanup.clearTapes_apply line 54
9. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Cleanup.clearTapes_selected line 67
10. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Cleanup.clearTapes_unselected line 71
11. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Cleanup.actualCost_le line 77
12. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Cleanup.cleanupTrace line 93
13. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Cleanup.cleanupInTime line 118
14. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Cleanup.program line 134
15. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Cleanup.machine line 138
16. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Cleanup.machineInTime line 150
17. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Cleanup.clearTapes_outputOnly line 161
18. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Cleanup.machineHaltInTime line 173