Substitution of variables and constants into clauses and CNFs

Normalize substituted clauses and discard clauses that become identically true.

noncomputable def Complexity.DepthThreeLowerBound.Clause.subst {V : Type u_1} {W : Type u_2} (α : V → W ⊕ Bool) (C : Clause V) : Option (Clause W)

Substitute inputs and normalize a clause; none denotes a tautology.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Complexity.DepthThreeLowerBound.CNF.subst {V : Type u_1} {W : Type u_2} (H : CNF V) (α : V → W ⊕ Bool) : CNF W

Substitute inputs into every clause and discard resulting tautologies.

Equations

• H.subst α = List.filterMap (Complexity.DepthThreeLowerBound.Clause.subst α) H