OAI/Combinatorics/IndependentSets/Machines/RawInitialMachineFinish.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.IndependentSetsGames.Foundations.PCP.RawInitialMachineFinish.tapes line 10
2. def OAI.IndependentSetsGames.Foundations.PCP.RawInitialMachineFinish.finishTapes line 18
3. theorem OAI.IndependentSetsGames.Foundations.PCP.RawInitialMachineFinish.trace_trans line 21
4. theorem OAI.IndependentSetsGames.Foundations.PCP.RawInitialMachineFinish.trueRelationWords line 25
5. theorem OAI.IndependentSetsGames.Foundations.PCP.RawInitialMachineFinish.dummyBits_length line 32
6. theorem OAI.IndependentSetsGames.Foundations.PCP.RawInitialMachineFinish.update_reversed line 40
7. theorem OAI.IndependentSetsGames.Foundations.PCP.RawInitialMachineFinish.cleanupTrace line 46
8. theorem OAI.IndependentSetsGames.Foundations.PCP.RawInitialMachineFinish.resetReverseTrace line 95
9. theorem OAI.IndependentSetsGames.Foundations.PCP.RawInitialMachineFinish.update_finish line 126
10. theorem OAI.IndependentSetsGames.Foundations.PCP.RawInitialMachineFinish.copyFinishTrace line 130
11. theorem OAI.IndependentSetsGames.Foundations.PCP.RawInitialMachineFinish.closeDummyTailTrace line 146
12. theorem OAI.IndependentSetsGames.Foundations.PCP.RawInitialMachineFinish.closeDummyReverseTrace line 155
13. theorem OAI.IndependentSetsGames.Foundations.PCP.RawInitialMachineFinish.dummyRelationTrace line 164
14. theorem OAI.IndependentSetsGames.Foundations.PCP.RawInitialMachineFinish.dummyTrace line 175
15. theorem OAI.IndependentSetsGames.Foundations.PCP.RawInitialMachineFinish.finishTrace line 212
16. def OAI.IndependentSetsGames.Foundations.PCP.RawInitialMachineFinish.finishInTime line 230