theorem FABL.Literal.eval_eq_neg_one_iff {n : ℕ}
  (ℓ : FABL.Literal n)
  (x : FABL.SignCube n) :
  ℓ.eval x = -1 ↔ x ℓ.index = ℓ.required

theorem FABL.DNFTerm.eval_eq_neg_one_iff {n : ℕ}
  (T : FABL.DNFTerm n)
  (x : FABL.SignCube n) :
  T.eval x = -1 ↔
    ∀ ℓ ∈ T.literals,
      x ℓ.index = ℓ.required

theorem FABL.DNFFormula.eval_eq_neg_one_iff
  {n : ℕ} (φ : FABL.DNFFormula n)
  (x : FABL.SignCube n) :
  φ.eval x = -1 ↔
    ∃ T ∈ φ.terms, T.eval x = -1

theorem FABL.sort3ReducedDNF_toBooleanFunction :
  FABL.sort3ReducedDNF.toBooleanFunction =
    FABL.sort3

theorem FABL.sort3DNF_toBooleanFunction :
  FABL.sort3DNF.toBooleanFunction =
    FABL.sort3

theorem FABL.size_sort3ReducedDNF :
  FABL.sort3ReducedDNF.size = 3

theorem FABL.width_sort3ReducedDNF :
  FABL.sort3ReducedDNF.width = 2

theorem FABL.size_sort3DNF :
  FABL.sort3DNF.size = 4

theorem FABL.width_sort3DNF :
  FABL.sort3DNF.width = 2

theorem FABL.DNFTerm.width_minterm {n : ℕ}
  (x : FABL.SignCube n) :
  (FABL.DNFTerm.minterm x).width = n

theorem FABL.DNFTerm.eval_minterm_eq_neg_one_iff
  {n : ℕ} (x y : FABL.SignCube n) :
  (FABL.DNFTerm.minterm x).eval y = -1 ↔
    y = x

theorem FABL.size_mintermDNF_le {n : ℕ}
  (f : FABL.BooleanFunction n) :
  (FABL.mintermDNF f).size ≤ 2 ^ n

theorem FABL.width_mintermDNF_le {n : ℕ}
  (f : FABL.BooleanFunction n) :
  (FABL.mintermDNF f).width ≤ n

theorem FABL.mintermDNF_toBooleanFunction {n : ℕ}
  (f : FABL.BooleanFunction n) :
  (FABL.mintermDNF f).toBooleanFunction =
    f

theorem FABL.exists_DNFFormula_size_width_bound
  {n : ℕ} (f : FABL.BooleanFunction n) :
  ∃ φ,
    φ.size ≤ 2 ^ n ∧
      φ.width ≤ n ∧
        φ.toBooleanFunction = f

theorem FABL.hasDNFSizeLE_two_pow {n : ℕ}
  (f : FABL.BooleanFunction n) :
  FABL.HasDNFSizeLE f (2 ^ n)

theorem FABL.hasDNFWidthLE_dimension {n : ℕ}
  (f : FABL.BooleanFunction n) :
  FABL.HasDNFWidthLE f n

theorem FABL.hasDNFSizeLE_DNFsize {n : ℕ}
  (f : FABL.BooleanFunction n) :
  FABL.HasDNFSizeLE f (FABL.DNFsize f)

theorem FABL.hasDNFWidthLE_DNFwidth {n : ℕ}
  (f : FABL.BooleanFunction n) :
  FABL.HasDNFWidthLE f (FABL.DNFwidth f)

theorem FABL.CNFFormula.clauseEval_neg_iff_termEval
  {n : ℕ} (C : FABL.DNFTerm n)
  (x : FABL.SignCube n) :
  (FABL.CNFFormula.clauseEval C fun i =>
        -x i) =
      1 ↔
    C.eval x = -1

theorem FABL.CNFFormula.switchAndOr_toBooleanFunction
  {n : ℕ} (ψ : FABL.CNFFormula n) :
  ψ.switchAndOr.toBooleanFunction =
    FABL.CNFFormula.booleanDual
      ψ.toBooleanFunction

theorem FABL.hasDNFSizeWidth_of_hasCNFSizeWidth
  {n : ℕ} {f : FABL.BooleanFunction n}
  {s w : ℕ} (hs : FABL.HasCNFSizeLE f s)
  (hw : FABL.HasCNFWidthLE f w) :
  FABL.HasDNFSizeLE
      (FABL.CNFFormula.booleanDual f) s ∧
    FABL.HasDNFWidthLE
      (FABL.CNFFormula.booleanDual f) w

theorem FABL.F₂DecisionTree.Path.width_toDNFTerm
  {n : ℕ}
  (path :
    FABL.F₂DecisionTree.Path n
      FABL.Sign) :
  path.toDNFTerm.width = path.length

theorem FABL.F₂DecisionTree.Path.eval_toDNFTerm_eq_neg_one_iff
  {n : ℕ}
  (path :
    FABL.F₂DecisionTree.Path n FABL.Sign)
  (x : FABL.SignCube n) :
  path.toDNFTerm.eval x = -1 ↔
    path.Matches
      ((FABL.binaryCubeSignEquiv n).symm
        x)

theorem FABL.F₂DecisionTree.Path.width_toCNFClause
  {n : ℕ}
  (path :
    FABL.F₂DecisionTree.Path n
      FABL.Sign) :
  path.toCNFClause.width = path.length

theorem FABL.F₂DecisionTree.Path.clauseEval_toCNFClause_eq_one_iff
  {n : ℕ}
  (path :
    FABL.F₂DecisionTree.Path n FABL.Sign)
  (x : FABL.SignCube n) :
  FABL.CNFFormula.clauseEval
        path.toCNFClause x =
      1 ↔
    path.Matches
      ((FABL.binaryCubeSignEquiv n).symm
        x)

theorem FABL.F₂DecisionTree.size_toDNFFormula_le
  {n : ℕ} {available : Finset (Fin n)}
  (T :
    FABL.F₂DecisionTree n FABL.Sign
      available) :
  T.toDNFFormula.size ≤ T.leafCount

theorem FABL.F₂DecisionTree.width_toDNFFormula_le
  {n : ℕ} {available : Finset (Fin n)}
  (T :
    FABL.F₂DecisionTree n FABL.Sign
      available) :
  T.toDNFFormula.width ≤ T.depth

theorem FABL.F₂DecisionTree.toDNFFormula_toBooleanFunction
  {n : ℕ} {available : Finset (Fin n)}
  (T :
    FABL.F₂DecisionTree n FABL.Sign
      available) :
  T.toDNFFormula.toBooleanFunction =
    FABL.booleanFunctionOfBinary T.eval

theorem FABL.F₂DecisionTree.hasDNFSizeWidth_of_decisionTree
  {n : ℕ} {available : Finset (Fin n)}
  (T :
    FABL.F₂DecisionTree n FABL.Sign
      available) :
  FABL.HasDNFSizeLE
      (FABL.booleanFunctionOfBinary
        T.eval)
      T.leafCount ∧
    FABL.HasDNFWidthLE
      (FABL.booleanFunctionOfBinary
        T.eval)
      T.depth

theorem FABL.F₂DecisionTree.hasDNFSizeWidth_of_computes
  {n : ℕ}
  (T : FABL.DecisionTree n FABL.Sign)
  (f : FABL.BooleanFunction n)
  (hT :
    FABL.F₂DecisionTree.Computes T
      (FABL.binaryOfBooleanFunction f)) :
  FABL.HasDNFSizeLE f
      (FABL.F₂DecisionTree.leafCount T) ∧
    FABL.HasDNFWidthLE f
      (FABL.F₂DecisionTree.depth T)

theorem FABL.F₂DecisionTree.size_toCNFFormula_le
  {n : ℕ} {available : Finset (Fin n)}
  (T :
    FABL.F₂DecisionTree n FABL.Sign
      available) :
  T.toCNFFormula.size ≤ T.leafCount

theorem FABL.F₂DecisionTree.width_toCNFFormula_le
  {n : ℕ} {available : Finset (Fin n)}
  (T :
    FABL.F₂DecisionTree n FABL.Sign
      available) :
  T.toCNFFormula.width ≤ T.depth

theorem FABL.F₂DecisionTree.eval_toCNFFormula_eq_one
  {n : ℕ} {available : Finset (Fin n)}
  (T :
    FABL.F₂DecisionTree n FABL.Sign
      available)
  (x : FABL.SignCube n) :
  T.toCNFFormula.eval x = 1 ↔
    ∃ path ∈ T.paths,
      path.output = 1 ∧
        path.Matches
          ((FABL.binaryCubeSignEquiv
                n).symm
            x)

theorem FABL.F₂DecisionTree.toCNFFormula_toBooleanFunction
  {n : ℕ} {available : Finset (Fin n)}
  (T :
    FABL.F₂DecisionTree n FABL.Sign
      available) :
  T.toCNFFormula.toBooleanFunction =
    FABL.booleanFunctionOfBinary T.eval

theorem FABL.F₂DecisionTree.hasCNFSizeWidth_of_decisionTree
  {n : ℕ} {available : Finset (Fin n)}
  (T :
    FABL.F₂DecisionTree n FABL.Sign
      available) :
  FABL.HasCNFSizeLE
      (FABL.booleanFunctionOfBinary
        T.eval)
      T.leafCount ∧
    FABL.HasCNFWidthLE
      (FABL.booleanFunctionOfBinary
        T.eval)
      T.depth

theorem FABL.F₂DecisionTree.hasCNFSizeWidth_of_computes
  {n : ℕ}
  (T : FABL.DecisionTree n FABL.Sign)
  (f : FABL.BooleanFunction n)
  (hT :
    FABL.F₂DecisionTree.Computes T
      (FABL.binaryOfBooleanFunction f)) :
  FABL.HasCNFSizeLE f
      (FABL.F₂DecisionTree.leafCount T) ∧
    FABL.HasCNFWidthLE f
      (FABL.F₂DecisionTree.depth T)

theorem FABL.exists_DNF_of_decisionTree {n : ℕ}
  (f : FABL.BooleanFunction n) (s k : ℕ)
  (T : FABL.DecisionTree n FABL.Sign)
  (hT :
    FABL.F₂DecisionTree.Computes T
      (FABL.binaryOfBooleanFunction f))
  (hs :
    FABL.F₂DecisionTree.leafCount T ≤ s)
  (hk : FABL.F₂DecisionTree.depth T ≤ k) :
  FABL.HasDNFSizeLE f s ∧
    FABL.HasDNFWidthLE f k

theorem FABL.exists_CNF_of_decisionTree {n : ℕ}
  (f : FABL.BooleanFunction n) (s k : ℕ)
  (T : FABL.DecisionTree n FABL.Sign)
  (hT :
    FABL.F₂DecisionTree.Computes T
      (FABL.binaryOfBooleanFunction f))
  (hs :
    FABL.F₂DecisionTree.leafCount T ≤ s)
  (hk : FABL.F₂DecisionTree.depth T ≤ k) :
  FABL.HasCNFSizeLE f s ∧
    FABL.HasCNFWidthLE f k

theorem FABL.size_sort3DecisionTreeDNFPrinted :
  FABL.sort3DecisionTreeDNFPrinted.size =
    4