OAI/Computability/DepthThree/Circuit.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DepthThreeLowerBound.GateInput.subst line 13
  2. def OAI.DepthThreeLowerBound.GateInput.assignment line 19
  3. theorem OAI.DepthThreeLowerBound.GateInput.eval_subst line 24
  4. theorem OAI.DepthThreeLowerBound.RawClause.eval_eq_true line 36
  5. theorem OAI.DepthThreeLowerBound.RawClause.eval_map_subst line 41
  6. theorem OAI.DepthThreeLowerBound.Circuit3.middleEval_eq_true line 59
  7. theorem OAI.DepthThreeLowerBound.Circuit3.eval_eq_true line 65
  8. theorem OAI.DepthThreeLowerBound.Circuit3.bottomCount_le_gateCount line 70
  9. theorem OAI.DepthThreeLowerBound.Circuit3.middleCount_le_gateCount line 73
  10. theorem OAI.DepthThreeLowerBound.Circuit3.middle_card_le_gateCount line 76
  11. theorem OAI.DepthThreeLowerBound.Circuit3.top_card_le_gateCount line 80
  12. def OAI.DepthThreeLowerBound.Circuit3.subst line 83
  13. theorem OAI.DepthThreeLowerBound.Circuit3.gateCount_subst line 90
  14. theorem OAI.DepthThreeLowerBound.Circuit3.middleEval_subst line 93
  15. theorem OAI.DepthThreeLowerBound.Circuit3.eval_subst line 100
  16. theorem OAI.DepthThreeLowerBound.Circuit3.computes_subst line 106