OAI/Computability/PerfectCompleteness/Machines/MachineCircuit.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.MachineCircuit.bool_ext line 17
2. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.MachineCircuit.StepSafe line 20
3. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.MachineCircuit.liveCase line 23
4. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.MachineCircuit.stickyExpr line 28
5. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.MachineCircuit.absorbing_live line 35
6. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.MachineCircuit.absorbing_halted line 46
7. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.MachineCircuit.liveCase_eval line 56
8. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.MachineCircuit.stickyExpr_eval line 70
9. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.MachineCircuit.configEncoding_injective line 100
10. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.MachineCircuit.programCost line 124
11. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.MachineCircuit.statementCost_le_programCost line 128
12. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.MachineCircuit.expressionCost line 134
13. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.MachineCircuit.one_le_expressionCost line 138
14. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.MachineCircuit.stickyExpr_size_le line 143