OAI/Computability/DepthThree/SparseCounting.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DepthThreeLowerBound.clausesOfSize line 18
  2. def OAI.DepthThreeLowerBound.literalOccurrences line 21
  3. theorem OAI.DepthThreeLowerBound.mem_clausesOfSize line 25
  4. theorem OAI.DepthThreeLowerBound.clausesOfSize_subset line 32
  5. theorem OAI.DepthThreeLowerBound.clausesOfSize_mono line 38
  6. theorem OAI.DepthThreeLowerBound.clausesOfSize_eq_self line 45
  7. theorem OAI.DepthThreeLowerBound.clausesOfSize_eq_empty line 52
  8. theorem OAI.DepthThreeLowerBound.literalOccurrences_mono line 59
  9. theorem OAI.DepthThreeLowerBound.literalOccurrences_le_card line 64
  10. theorem OAI.DepthThreeLowerBound.literalOccurrences_one_le line 69
  11. theorem OAI.DepthThreeLowerBound.clausesOfSize_union line 85
  12. theorem OAI.DepthThreeLowerBound.literalOccurrences_union_le line 90
  13. theorem OAI.DepthThreeLowerBound.clausesOfSize_card_le line 98
  14. theorem OAI.DepthThreeLowerBound.subsumed_by_clause_card_le line 112
  15. theorem OAI.DepthThreeLowerBound.deleted_clausesOfSize_card_le line 125
  16. def OAI.DepthThreeLowerBound.subsumedOfSize line 142
  17. theorem OAI.DepthThreeLowerBound.subsumedOfSize_card_le line 146
  18. theorem OAI.DepthThreeLowerBound.clausesOfSize_update_balance line 156
  19. theorem OAI.DepthThreeLowerBound.literalOccurrences_update_le line 205