def FABL.maxCutTemplate :
  FABL.CSPTemplate FABL.Sign

def FABL.maxThreeColoringTemplate :
  FABL.CSPTemplate (Fin 3)

def FABL.maxE3LinTemplate :
  FABL.CSPTemplate FABL.𝔽₂

def FABL.e3SatPredicate
  (negated values : Fin 3 → Bool) : Bool

def FABL.maxE3SatTemplate :
  FABL.CSPTemplate Bool

def FABL.maxThreeSatPredicateEval
  (p : FABL.MaxThreeSatPredicate)
  (values : Fin (↑p.fst + 1) → Bool) :
  Bool

def FABL.maxThreeSatTemplate :
  FABL.CSPTemplate Bool

def FABL.CSPTemplate.maxArity.{u, u_1}
  {D : Type u} (Ψ : FABL.CSPTemplate D) :
  ℕ

def FABL.CSPTemplate.unsatisfiedCost.{u, u_1}
  {D : Type u} (Ψ : FABL.CSPTemplate D)
  (p : Ψ.Predicate)
  (x : Fin (Ψ.arity p) → D) : ℕ

def FABL.CSPTemplate.toValuedCSP.{u, u_1}
  {D : Type u} (Ψ : FABL.CSPTemplate D) :
  ValuedCSP D ℕ

def FABL.CSPConstraint.toValuedTerm.{u, v,
    u_1}
  {D : Type u} {Ψ : FABL.CSPTemplate D}
  {V : Type v}
  (c : FABL.CSPConstraint Ψ V) :
  Ψ.toValuedCSP.Term V

def FABL.CSPInstance.toValuedInstance.{u, v,
    u_1}
  {D : Type u} {Ψ : FABL.CSPTemplate D}
  {V : Type v}
  (P : FABL.CSPInstance Ψ V) :
  Ψ.toValuedCSP.Instance V

def FABL.maxCutConstraintScope.{u}
  {V : Type u}
  (c :
    FABL.CSPConstraint FABL.maxCutTemplate
      V) :
  Fin 2 ↪ V

def FABL.twoVertexMaxCutConstraint :
  FABL.CSPConstraint FABL.maxCutTemplate
    (Fin 2)

def FABL.parallelEdgeMaxCutInstance :
  FABL.CSPInstance FABL.maxCutTemplate
    (Fin 2)

def FABL.CSPConstraint.Satisfied.{u, v, u_1}
  {D : Type u} {Ψ : FABL.CSPTemplate D}
  {V : Type v}
  (c : FABL.CSPConstraint Ψ V)
  (assignment : V → D) : Prop

def FABL.CSPConstraint.satisfiedIndicator.{u,
    v, u_1}
  {D : Type u} {Ψ : FABL.CSPTemplate D}
  {V : Type v}
  (c : FABL.CSPConstraint Ψ V)
  (assignment : V → D) : ℕ

def FABL.CSPConstraint.unsatisfiedIndicator.{u,
    v, u_1}
  {D : Type u} {Ψ : FABL.CSPTemplate D}
  {V : Type v}
  (c : FABL.CSPConstraint Ψ V)
  (assignment : V → D) : ℕ

def FABL.CSPInstance.satisfiedCount.{u, v,
    u_1}
  {D : Type u} {Ψ : FABL.CSPTemplate D}
  {V : Type v} (P : FABL.CSPInstance Ψ V)
  (assignment : V → D) : ℕ

def FABL.CSPInstance.unsatisfiedCost.{u, v,
    u_1}
  {D : Type u} {Ψ : FABL.CSPTemplate D}
  {V : Type v} (P : FABL.CSPInstance Ψ V)
  (assignment : V → D) : ℕ

def FABL.CSPInstance.value.{u, v, u_1}
  {D : Type u} {Ψ : FABL.CSPTemplate D}
  {V : Type v} (P : FABL.CSPInstance Ψ V)
  (assignment : V → D) : ℚ

def FABL.CSPInstance.optimalAssignment.{u, v,
    u_1}
  {D : Type u} {Ψ : FABL.CSPTemplate D}
  {V : Type v} [Finite D] [Nonempty D]
  [Finite V] (P : FABL.CSPInstance Ψ V) :
  V → D

def FABL.CSPInstance.optimum.{u, v, u_1}
  {D : Type u} {Ψ : FABL.CSPTemplate D}
  {V : Type v} [Finite D] [Nonempty D]
  [Finite V] (P : FABL.CSPInstance Ψ V) :
  ℚ

def FABL.CSPInstance.Satisfiable.{u, v, u_1}
  {D : Type u} {Ψ : FABL.CSPTemplate D}
  {V : Type v} [Finite D] [Nonempty D]
  [Finite V] (P : FABL.CSPInstance Ψ V) :
  Prop

def FABL.UniformStringTester.constraint.{u, v,
    u_1, u_2}
  {D : Type u} {Ψ : FABL.CSPTemplate D}
  {V : Type v}
  (T : FABL.UniformStringTester Ψ V)
  (seed : T.Seed) : FABL.CSPConstraint Ψ V

def FABL.UniformStringTester.toCSPInstance.{u,
    v, u_1, u_2}
  {D : Type u} {Ψ : FABL.CSPTemplate D}
  {V : Type v}
  (T : FABL.UniformStringTester Ψ V) :
  FABL.CSPInstance Ψ V

def FABL.UniformStringTester.acceptance.{u, v,
    u_1, u_2}
  {D : Type u} {Ψ : FABL.CSPTemplate D}
  {V : Type v}
  (T : FABL.UniformStringTester Ψ V)
  (assignment : V → D) : ℚ

def FABL.maxAtMostThreeLinTemplate :
  FABL.CSPTemplate FABL.𝔽₂

def FABL.oddWeightPartialSumCSPPredicate
  {m : ℕ}
  (seed :
    FABL.OddWeightPartialSumCheckSeed m) :
  FABL.MaxThreeLinPredicate

def FABL.oddWeightPartialSumCSPScope {m : ℕ}
  (seed :
    FABL.OddWeightPartialSumCheckSeed m) :
  Fin
      (FABL.maxAtMostThreeLinTemplate.arity
        (FABL.oddWeightPartialSumCSPPredicate
          seed)) ↪
    FABL.OddWeightPartialSumVariable m

def FABL.oddWeightPartialSumUniformStringTester
  (m : ℕ) :
  FABL.UniformStringTester
    FABL.maxAtMostThreeLinTemplate
    (FABL.OddWeightPartialSumVariable m)

def FABL.oddWeightPartialSumCSPAssignment
  {m : ℕ} (w : Fin (m + 2) → Bool)
  (proof : Fin (m + 1) → Bool) :
  FABL.OddWeightPartialSumVariable m →
    FABL.𝔽₂

def FABL.blrQueryTriple {n : ℕ}
  (x y : FABL.F₂Cube n) :
  Fin 3 → FABL.F₂Cube n

def FABL.BLRQueriesCollide {n : ℕ}
  (x y : FABL.F₂Cube n) : Prop

def FABL.blrCSPConstraint {n : ℕ}
  (x y : FABL.F₂Cube n) :
  FABL.CSPConstraint
    FABL.maxAtMostThreeLinTemplate
    (FABL.F₂Cube n)

def FABL.blrCSPPredicate {n : ℕ}
  (x y : FABL.F₂Cube n) :
  FABL.MaxThreeLinPredicate

def FABL.blrCSPScope {n : ℕ}
  (x y : FABL.F₂Cube n) :
  Fin
      (FABL.maxAtMostThreeLinTemplate.arity
        (FABL.blrCSPPredicate x y)) ↪
    FABL.F₂Cube n

def FABL.blrUniformStringTester (n : ℕ)
  (hn : 2 ≤ n) :
  FABL.UniformStringTester
    FABL.maxAtMostThreeLinTemplate
    (FABL.F₂Cube n)