OAI/Combinatorics/IndependentSets/Machines/RawInitialMachineCleanup.lean
8 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.IndependentSetsGames.Foundations.PCP.RawInitialMachineCleanup.trace_transline 11 - theorem
OAI.IndependentSetsGames.Foundations.PCP.RawInitialMachineCleanup.incrementIndexTraceline 15 - theorem
OAI.IndependentSetsGames.Foundations.PCP.RawInitialMachineCleanup.cleanupTraceline 21 - def
OAI.IndependentSetsGames.Foundations.PCP.RawInitialMachineCleanup.cleanupInTimeline 104 - theorem
OAI.IndependentSetsGames.Foundations.PCP.RawInitialMachineBody.trace_transline 124 - theorem
OAI.IndependentSetsGames.Foundations.PCP.RawInitialMachineBody.guardTrace_succline 128 - theorem
OAI.IndependentSetsGames.Foundations.PCP.RawInitialMachineBody.guardTrace_zeroline 143 - theorem
OAI.IndependentSetsGames.Foundations.PCP.RawInitialMachineBody.bodyTraceline 157