OAI/Computability/DepthThree/CircuitNormalization.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DepthThreeLowerBound.RawClause.literalPart line 14
  2. def OAI.DepthThreeLowerBound.RawClause.literals line 18
  3. theorem OAI.DepthThreeLowerBound.RawClause.mem_literals line 22
  4. theorem OAI.DepthThreeLowerBound.RawClause.eval_true_iff line 36
  5. def OAI.DepthThreeLowerBound.RawClause.normalize line 50
  6. theorem OAI.DepthThreeLowerBound.RawClause.normalized_of_normalize_eq_some line 54
  7. theorem OAI.DepthThreeLowerBound.RawClause.normalize_eval line 65
  8. def OAI.DepthThreeLowerBound.Circuit3.middleCNF line 88
  9. theorem OAI.DepthThreeLowerBound.Circuit3.mem_middleCNF line 91
  10. theorem OAI.DepthThreeLowerBound.Circuit3.middleCNF_normalized line 95
  11. theorem OAI.DepthThreeLowerBound.Circuit3.middleCNF_length_le_bottomCount line 101
  12. theorem OAI.DepthThreeLowerBound.Circuit3.middleCNF_length_le_gateCount line 108
  13. theorem OAI.DepthThreeLowerBound.Circuit3.eval_middleCNF line 112
  14. theorem OAI.DepthThreeLowerBound.Circuit3.eval_eq_true_iff_middleCNF line 130
  15. theorem OAI.DepthThreeLowerBound.Circuit3.middleCNF_implies_output line 134