OAI/Combinatorics/IndependentSets/Machines/MachineComposition.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.IndependentSetsGames.Foundations.Complexity.MachineComposition.advance line 8
2. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineComposition.advance_none line 11
3. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineComposition.advance_some line 14
4. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineComposition.advance_iterate_none line 17
5. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineComposition.liftSuccessfulTrace line 23
6. def OAI.IndependentSetsGames.Foundations.Complexity.MachineComposition.liftExecutionInTime line 47
7. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineComposition.liftExecutionInTime_steps line 61
8. def OAI.IndependentSetsGames.Foundations.Complexity.MachineComposition.embeddedExecution line 68
9. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineComposition.natPolynomial_eval_mono line 86
10. def OAI.IndependentSetsGames.Foundations.Complexity.MachineComposition.compositionPolynomial line 95
11. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineComposition.compositionBudget_le line 98
12. def OAI.IndependentSetsGames.Foundations.Complexity.MachineComposition.fourPhaseExecution line 109