OAI/Computability/VertexCover/Encoding/MachineComposition.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.UniqueGames.Foundations.Complexity.MachineComposition.advance line 42
2. theorem OAI.UniqueGames.Foundations.Complexity.MachineComposition.advance_none line 45
3. theorem OAI.UniqueGames.Foundations.Complexity.MachineComposition.advance_some line 48
4. theorem OAI.UniqueGames.Foundations.Complexity.MachineComposition.advance_iterate_none line 51
5. theorem OAI.UniqueGames.Foundations.Complexity.MachineComposition.liftSuccessfulTrace line 57
6. def OAI.UniqueGames.Foundations.Complexity.MachineComposition.liftExecutionInTime line 81
7. theorem OAI.UniqueGames.Foundations.Complexity.MachineComposition.liftExecutionInTime_steps line 95
8. def OAI.UniqueGames.Foundations.Complexity.MachineComposition.embeddedExecution line 102
9. theorem OAI.UniqueGames.Foundations.Complexity.MachineComposition.natPolynomial_eval_mono line 120
10. def OAI.UniqueGames.Foundations.Complexity.MachineComposition.compositionPolynomial line 129
11. theorem OAI.UniqueGames.Foundations.Complexity.MachineComposition.compositionBudget_le line 132
12. def OAI.UniqueGames.Foundations.Complexity.MachineComposition.fourPhaseExecution line 143