OAI/Computability/DepthThree/SparseNormalize.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.DepthThreeLowerBound.Clause.eval_of_not_normalized line 12
  2. theorem OAI.DepthThreeLowerBound.CNF.eval_of_empty_mem line 22
  3. def OAI.DepthThreeLowerBound.sparseNormalizedFamily line 30
  4. theorem OAI.DepthThreeLowerBound.mem_sparseNormalizedFamily line 34
  5. theorem OAI.DepthThreeLowerBound.bool_eq_of_true_iff line 39

    Also declared: OAI/Computability/DepthThree/SparseBranch.lean:64 (same declaration text).

  6. theorem OAI.DepthThreeLowerBound.sparseNormalizedFamily_eval line 42
  7. theorem OAI.DepthThreeLowerBound.sparseMinimalFamily_eval line 55
  8. structure OAI.DepthThreeLowerBound.SparseNormalization line 63
  9. def OAI.DepthThreeLowerBound.sparseNormalizeOfNoEmpty line 71
  10. theorem OAI.DepthThreeLowerBound.exists_sparseNormalization_or_false line 97