OAI/Computability/PerfectCompleteness/Machines/WitnessCircuit.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.WitnessCircuit.bool_ext line 12
2. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.WitnessCircuit.eval_disjoin_ofFn_true line 15
3. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.WitnessCircuit.selectorExpr line 26
4. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.WitnessCircuit.payloadExpr line 29
5. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.WitnessCircuit.eval_selectorExpr line 32
6. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.WitnessCircuit.eval_payloadExpr line 35
7. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.WitnessCircuit.nonemptyExpr line 38
8. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.WitnessCircuit.clashPairExpr line 41
9. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.WitnessCircuit.clashExpr line 44
10. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.WitnessCircuit.validityExpr line 47
11. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.WitnessCircuit.eval_nonemptyExpr line 50
12. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.WitnessCircuit.eval_clashPairExpr line 54
13. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.WitnessCircuit.eval_clashExpr line 59
14. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.WitnessCircuit.eval_validityExpr line 64
15. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.WitnessCircuit.presenceExpr line 83
16. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.WitnessCircuit.eval_presenceExpr line 87
17. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.WitnessCircuit.payloadSymbolExpr line 97
18. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.WitnessCircuit.eval_payloadSymbolExpr line 102
19. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.WitnessCircuit.inputCellExpr line 108
20. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.WitnessCircuit.eval_inputCellExpr line 118
21. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.WitnessCircuit.size_selectorExpr line 134
22. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.WitnessCircuit.size_payloadExpr line 137
23. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.WitnessCircuit.size_mux line 140
24. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.WitnessCircuit.size_nonemptyExpr_le line 145
25. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.WitnessCircuit.size_clashPairExpr_le line 153
26. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.WitnessCircuit.size_clashExpr_le line 157
27. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.WitnessCircuit.size_validityExpr_le line 174
28. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.WitnessCircuit.size_presenceExpr_le line 180
29. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.WitnessCircuit.size_payloadSymbolExpr line 189
30. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.WitnessCircuit.size_inputCellExpr_le line 194
31. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.WitnessCircuit.initialCellExpr line 216
32. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.WitnessCircuit.eval_initialCellExpr line 225
33. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.WitnessCircuit.initExpr line 238
34. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.WitnessCircuit.eval_initExpr line 245
35. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.WitnessCircuit.size_initialCellExpr_le line 257
36. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.WitnessCircuit.size_initExpr_le line 268
37. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.WitnessCircuit.validityCircuit line 280
38. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.WitnessCircuit.validityCircuit_eval line 282
39. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.WitnessCircuit.validityCircuit_gates_le line 288