OAI/Computability/DepthThree/Core.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.DepthThreeLowerBound.Clause line 9
  2. abbrev OAI.DepthThreeLowerBound.CNF line 10
  3. def OAI.DepthThreeLowerBound.Literal.compl line 16
  4. theorem OAI.DepthThreeLowerBound.Literal.eval_eq_true line 18
  5. theorem OAI.DepthThreeLowerBound.Literal.compl_compl line 21
  6. theorem OAI.DepthThreeLowerBound.Literal.eval_compl line 25
  7. def OAI.DepthThreeLowerBound.Clause.eval line 34
  8. def OAI.DepthThreeLowerBound.Clause.scope line 38
  9. def OAI.DepthThreeLowerBound.Clause.width line 42
  10. def OAI.DepthThreeLowerBound.Clause.Normalized line 44
  11. theorem OAI.DepthThreeLowerBound.Clause.eval_eq_true line 47
  12. theorem OAI.DepthThreeLowerBound.Clause.eval_empty line 52
  13. theorem OAI.DepthThreeLowerBound.Clause.scope_empty line 55
  14. theorem OAI.DepthThreeLowerBound.Clause.width_empty line 59
  15. theorem OAI.DepthThreeLowerBound.Clause.eval_singleton line 62
  16. theorem OAI.DepthThreeLowerBound.Clause.eval_mono line 67
  17. theorem OAI.DepthThreeLowerBound.Clause.Normalized.subset line 73
  18. theorem OAI.DepthThreeLowerBound.Clause.Normalized.fst_injOn line 78
  19. theorem OAI.DepthThreeLowerBound.Clause.Normalized.card_eq_width line 89
  20. theorem OAI.DepthThreeLowerBound.Clause.scope_mono line 94
  21. theorem OAI.DepthThreeLowerBound.Clause.width_mono line 98
  22. def OAI.DepthThreeLowerBound.CNF.eval line 105
  23. def OAI.DepthThreeLowerBound.CNF.WidthAtMost line 109
  24. def OAI.DepthThreeLowerBound.CNF.Normalized line 111
  25. theorem OAI.DepthThreeLowerBound.CNF.eval_eq_true line 113
  26. theorem OAI.DepthThreeLowerBound.CNF.eval_nil line 118
  27. theorem OAI.DepthThreeLowerBound.CNF.eval_cons line 121
  28. theorem OAI.DepthThreeLowerBound.CNF.eval_append line 134
  29. theorem OAI.DepthThreeLowerBound.CNF.eval_antitone line 140
  30. theorem OAI.DepthThreeLowerBound.CNF.WidthAtMost.mono line 145
  31. def OAI.DepthThreeLowerBound.indicator line 150
  32. def OAI.DepthThreeLowerBound.sign line 151
  33. theorem OAI.DepthThreeLowerBound.indicator_false line 153
  34. theorem OAI.DepthThreeLowerBound.indicator_true line 154
  35. theorem OAI.DepthThreeLowerBound.sign_false line 155
  36. theorem OAI.DepthThreeLowerBound.sign_true line 156
  37. theorem OAI.DepthThreeLowerBound.indicator_and line 158
  38. theorem OAI.DepthThreeLowerBound.indicator_nonneg line 162
  39. theorem OAI.DepthThreeLowerBound.indicator_le_one line 165