OAI/Combinatorics/IndependentSets/Machines/RawInitialMachineStart.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.IndependentSetsGames.Foundations.PCP.RawInitialMachineStart.inputTapes line 10
2. def OAI.IndependentSetsGames.Foundations.PCP.RawInitialMachineStart.firstTapes line 14
3. def OAI.IndependentSetsGames.Foundations.PCP.RawInitialMachineStart.counterTapes line 19
4. def OAI.IndependentSetsGames.Foundations.PCP.RawInitialMachineStart.headerTapes line 25
5. def OAI.IndependentSetsGames.Foundations.PCP.RawInitialMachineStart.startTapes line 32
6. theorem OAI.IndependentSetsGames.Foundations.PCP.RawInitialMachineStart.initList_eq line 40
7. theorem OAI.IndependentSetsGames.Foundations.PCP.RawInitialMachineStart.trace_trans line 49
8. theorem OAI.IndependentSetsGames.Foundations.PCP.RawInitialMachineStart.readCountersTrace line 53
9. theorem OAI.IndependentSetsGames.Foundations.PCP.RawInitialMachineStart.headersTrace line 87
10. theorem OAI.IndependentSetsGames.Foundations.PCP.RawInitialMachineStart.initializeIndexTrace line 106
11. theorem OAI.IndependentSetsGames.Foundations.PCP.RawInitialMachineStart.startTrace line 118
12. theorem OAI.IndependentSetsGames.Foundations.PCP.RawInitialMachineStart.formulaStartTrace line 128
13. def OAI.IndependentSetsGames.Foundations.PCP.RawInitialMachineStart.startInTime line 138
14. def OAI.IndependentSetsGames.Foundations.PCP.RawInitialMachineStart.formulaStartInTime line 147