OAI/Computability/PerfectCompleteness/Machines/CircuitLemmas.lean

GitHub source file

111 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.Gate line 20
  2. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.Gate.Bounded line 27
  3. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.Gate.eval line 33
  4. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.Gate.bounded_mono line 40
  5. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.Gate.eval_congr line 48
  6. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.Ordered line 57
  7. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.Consistent line 60
  8. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ordered_nil line 63
  9. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ordered_cons line 67
  10. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.consistent_nil line 87
  11. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.consistent_cons line 92
  12. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.consistent_append line 112
  13. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.run line 121
  14. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.run_eq_of_lt line 125
  15. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.run_append line 133
  16. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.run_singleton line 141
  17. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.run_singleton_here line 144
  18. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.run_singleton_other line 147
  19. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.Ordered.append line 151
  20. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.run_consistent line 162
  21. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.run_unique line 178
  22. structure OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.Circuit line 202
  23. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.Circuit.wires line 208
  24. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.inputEnv line 210
  25. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.Circuit.evalWires line 213
  26. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.Circuit.eval line 216
  27. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.Circuit.evalWires_input line 219
  28. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.Circuit.evalWires_consistent line 224
  29. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.Consistent.congr line 228
  30. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.unitClause line 240
  31. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.gateClauses line 243
  32. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.gateClauses_length line 263
  33. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.gateClauses_correct line 267
  34. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.Circuit.gateAt line 294
  35. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.Circuit.gateOutput line 296
  36. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.Circuit.gateBounded line 299
  37. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.Circuit.gateBlock line 304
  38. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.Circuit.toFormula line 307
  39. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.Circuit.toFormula_variables line 311
  40. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.Circuit.toFormula_clause_count line 314
  41. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.Circuit.toFormula_satisfied_iff line 327
  42. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.Circuit.restrictAssignment line 360
  43. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.Circuit.toFormula_satisfiable_iff_eval line 364
  44. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.Circuit.toFormula_extending_iff_eval line 389
  45. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.Bounds.pairLengthPolynomial line 426
  46. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.Bounds.horizonPolynomial line 429
  47. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.Bounds.capacityPolynomial line 432
  48. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.Bounds.pairLengthPolynomial_eval line 435
  49. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.Bounds.horizonPolynomial_eval line 439
  50. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.Bounds.capacityPolynomial_eval line 443
  51. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.Bounds.paired_length_le line 448
  52. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.Bounds.one_le_pairLength line 454
  53. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.Bounds.pairLength_le_capacity line 459
  54. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.Bounds.one_le_capacity line 464
  55. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.Bounds.transition_prefix_le_capacity line 468
  56. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.Bounds.verifier_time_le_horizon line 483
  57. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.Bounds.horizon_monotone line 489
  58. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.Bounds.capacity_monotone line 493
  59. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.Bounds.execution_stack_length_le_capacity line 497
  60. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.Bounds.stackCapacity_le_polynomial line 517
  61. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.Bounds.run_stack_length_le_capacity line 526
  62. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.Bounds.run_statement_budget_le_capacity line 535
  63. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.Bounds.configurationWidthPolynomial line 546
  64. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.Bounds.transitionGatesPolynomial line 550
  65. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.Bounds.tableauGatesPolynomial line 554
  66. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.Bounds.configurationWidthPolynomial_eval line 559
  67. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.Bounds.transitionGatesPolynomial_eval line 565
  68. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.Bounds.tableauGatesPolynomial_eval line 571
  69. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.Bounds.formulaBitsPolynomial line 579
  70. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.Bounds.formulaBitsPolynomial_eval line 582
  71. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.Bounds.formulaBits_length_le_polynomial line 588
  72. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.Bounds.circuitVariablesPolynomial line 599
  73. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.Bounds.circuitClausesPolynomial line 602
  74. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.Bounds.circuitBitsPolynomial line 605
  75. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.Bounds.circuitVariablesPolynomial_eval line 609
  76. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.Bounds.circuitClausesPolynomial_eval line 613
  77. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.Bounds.circuitBitsPolynomial_eval line 617
  78. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.Bounds.circuit_formulaBits_length_le line 623
  79. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.Bounds.circuit_formulaBits_length_le_polynomial line 633
  80. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.Bounds.toFormula_bits_length_le line 643
  81. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.Bounds.toFormula_bits_length_le_polynomial line 651
  82. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitProducerModel.gateTemplate line 671
  83. structure OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitProducerModel.Record line 685
  84. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitProducerModel.Record.slot line 692
  85. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitProducerModel.Record.words line 698
  86. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitProducerModel.Record.bits line 701
  87. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitProducerModel.Record.fieldValue line 703
  88. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitProducerModel.templateWords line 710
  89. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitProducerModel.Record.outputWords line 714
  90. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitProducerModel.Record.outputBits line 715
  91. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitProducerModel.outputWords line 717
  92. inductive OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitProducerModel.Tape line 720
  93. inductive OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitProducerModel.Context line 725
  94. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitProducerModel.State line 731
  95. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitProducerModel.Alphabet line 732
  96. inductive OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitProducerModel.Label line 734
  97. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitProducerModel.defaultControl line 749
  98. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitProducerModel.initialState line 750
  99. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitProducerModel.headerTape line 752
  100. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitProducerModel.headerNext line 758
  101. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitProducerModel.contextSource line 762
  102. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitProducerModel.affineEmit line 769
  103. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitProducerModel.literalEmit line 773
  104. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitProducerModel.emission line 777
  105. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitProducerModel.contextNext line 782
  106. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitProducerModel.cleanupNext line 789
  107. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitProducerModel.drain line 792
  108. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitProducerModel.resetGoto line 798
  109. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitProducerModel.tagDecoder line 801
  110. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitProducerModel.program line 810
  111. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitProducerModel.machine line 833