OAI/Computability/PerfectCompleteness/Machines/StatementCircuit.lean

GitHub source file

77 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.StatementCircuit.Expr line 16
  2. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.StatementCircuit.Expr.eval line 27
  3. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.StatementCircuit.Expr.eval_congr line 34
  4. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.StatementCircuit.Expr.rename line 39
  5. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.StatementCircuit.Expr.eval_rename line 46
  6. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.StatementCircuit.Expr.size line 50
  7. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.StatementCircuit.Expr.size_pos line 55
  8. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.StatementCircuit.Expr.size_rename line 58
  9. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.StatementCircuit.Expr.root line 62
  10. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.StatementCircuit.Expr.root_lt line 64
  11. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.StatementCircuit.Expr.root_not line 69
  12. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.StatementCircuit.Expr.root_and line 74
  13. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.StatementCircuit.Expr.root_or line 79
  14. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.StatementCircuit.Expr.gates line 84
  15. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.StatementCircuit.Expr.gates_length line 93
  16. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.StatementCircuit.Expr.ordered_singleton line 97
  17. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.StatementCircuit.Expr.gates_ordered line 101
  18. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.StatementCircuit.Expr.consistent_singleton line 129
  19. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.StatementCircuit.Expr.eval_of_consistent line 133
  20. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.StatementCircuit.Expr.circuit line 169
  21. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.StatementCircuit.Expr.circuit_eval line 175
  22. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.StatementCircuit.Expr.mux line 185
  23. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.StatementCircuit.Expr.eval_mux line 188
  24. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.StatementCircuit.Expr.disjoin line 192
  25. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.StatementCircuit.Expr.eval_disjoin_true line 196
  26. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.StatementCircuit.Expr.size_disjoin_le line 202
  27. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.StatementCircuit.bool_ext line 214
  28. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.StatementCircuit.table line 217
  29. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.StatementCircuit.eval_table line 221
  30. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.StatementCircuit.table₂ line 237
  31. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.StatementCircuit.eval_table₂ line 241
  32. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.StatementCircuit.size_table_le line 251
  33. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.StatementCircuit.size_table₂_le line 262
  34. structure OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.StatementCircuit.DataBits line 280
  35. structure OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.StatementCircuit.ResultBits line 284
  36. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.StatementCircuit.DataBits.Realizes line 288
  37. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.StatementCircuit.ResultBits.Realizes line 293
  38. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.StatementCircuit.readBits line 298
  39. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.StatementCircuit.eval_readBits line 302
  40. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.StatementCircuit.pushBits line 314
  41. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.StatementCircuit.peekBits line 321
  42. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.StatementCircuit.popBits line 326
  43. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.StatementCircuit.loadBits line 331
  44. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.StatementCircuit.muxResult line 336
  45. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.StatementCircuit.realizes_pushBits line 343
  46. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.StatementCircuit.realizes_peekBits line 362
  47. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.StatementCircuit.realizes_popBits line 373
  48. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.StatementCircuit.realizes_loadBits line 388
  49. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.StatementCircuit.realizes_muxResult line 394
  50. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.StatementCircuit.compileAux line 414
  51. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.StatementCircuit.compileAux_correct line 427
  52. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.StatementCircuit.InputBit line 466
  53. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.StatementCircuit.ConfigBit line 469
  54. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.StatementCircuit.inputBits line 472
  55. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.StatementCircuit.inputEncoding line 476
  56. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.StatementCircuit.configEncoding line 480
  57. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.StatementCircuit.resultExpr line 484
  58. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.StatementCircuit.inputBits_realizes line 491
  59. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.StatementCircuit.resultExpr_eval line 496
  60. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.StatementCircuit.transitionExpr line 505
  61. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.StatementCircuit.transitionExpr_eval line 509
  62. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.StatementCircuit.outputCircuit line 517
  63. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.StatementCircuit.outputCircuit_eval line 521
  64. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.StatementCircuit.DataBits.Bounded line 542
  65. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.StatementCircuit.ResultBits.Bounded line 545
  66. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.StatementCircuit.size_readBits_le line 548
  67. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.StatementCircuit.unaryCost line 557
  68. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.StatementCircuit.headCost line 560
  69. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.StatementCircuit.statementCost line 563
  70. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.StatementCircuit.pushBits_bounded line 574
  71. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.StatementCircuit.peekBits_bounded line 589
  72. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.StatementCircuit.popBits_bounded line 597
  73. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.StatementCircuit.loadBits_bounded line 611
  74. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.StatementCircuit.muxResult_bounded line 619
  75. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.StatementCircuit.compileAux_bounded line 630
  76. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.StatementCircuit.transitionExpr_size_le line 654
  77. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.StatementCircuit.outputCircuit_gates_le line 664