OAI/Computability/DepthThree/RestrictionNormalization.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.DepthThreeLowerBound.Clause.eval_true_of_not_normalized line 14
  2. def OAI.DepthThreeLowerBound.Clause.forbiddenValue line 25
  3. theorem OAI.DepthThreeLowerBound.Clause.forbiddenValue_ne_literal line 29
  4. theorem OAI.DepthThreeLowerBound.Clause.eval_eq_false_iff line 38
  5. theorem OAI.DepthThreeLowerBound.Clause.eval_eq_false_iff_forbidden line 51
  6. def OAI.DepthThreeLowerBound.Clause.violation line 70
  7. theorem OAI.DepthThreeLowerBound.Clause.violation_eq_true line 72
  8. theorem OAI.DepthThreeLowerBound.Clause.violation_eq_true_iff_forbidden line 76
  9. def OAI.DepthThreeLowerBound.CNF.normalize line 85
  10. theorem OAI.DepthThreeLowerBound.CNF.mem_normalize line 89
  11. theorem OAI.DepthThreeLowerBound.CNF.normalize_normalized line 94
  12. theorem OAI.DepthThreeLowerBound.CNF.normalize_widthAtMost line 98
  13. theorem OAI.DepthThreeLowerBound.CNF.eval_normalize line 103