OAI/Computability/DepthThree/RestrictionCylinders.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.DepthThreeLowerBound.Clause.eval_eq_of_scope_agree line 14
  2. theorem OAI.DepthThreeLowerBound.Clause.violation_eq_of_scope_agree line 29
  3. theorem OAI.DepthThreeLowerBound.simultaneous_violation_iff_cylinder line 34
  4. theorem OAI.DepthThreeLowerBound.violation_eq_of_covered line 65
  5. theorem OAI.DepthThreeLowerBound.coveredCount_eq_of_agree line 87
  6. theorem OAI.DepthThreeLowerBound.coveredCount_eq_on_larger_cylinder line 102
  7. def OAI.DepthThreeLowerBound.cylinderCNF line 109
  8. theorem OAI.DepthThreeLowerBound.cylinderCNF_eval_eq_true line 112
  9. theorem OAI.DepthThreeLowerBound.cylinderCNF_eval line 120
  10. theorem OAI.DepthThreeLowerBound.cylinderCNF_widthAtMost line 126
  11. theorem OAI.DepthThreeLowerBound.cylinderCNF_normalized line 135
  12. theorem OAI.DepthThreeLowerBound.fill_agree_outside_live line 152
  13. theorem OAI.DepthThreeLowerBound.simultaneous_restricted_violation_iff line 160