Finite sets of signed primary literals

Repeated identical literals are represented once. Opposite literals on the same coordinate remain visible, so contradictions are handled without a normalization assumption on the original circuit.

def Algebraic.Cutwidth.Aggregate.Geometry.Joint.literalVars {V : Type u_1} [DecidableEq V] (literals : Finset (V × Bool)) : Finset V

The primary variables appearing in a finite collection of signed literals.

Equations

• Algebraic.Cutwidth.Aggregate.Geometry.Joint.literalVars literals = Finset.image Prod.fst literals

def Algebraic.Cutwidth.Aggregate.Geometry.Joint.evalLiterals {V : Type u_1} (literals : Finset (V × Bool)) (x : V → Bool) : Bool

A conjunction of the specified primary literals.

Equations

• Algebraic.Cutwidth.Aggregate.Geometry.Joint.evalLiterals literals x = decide (∀ t ∈ literals, x t.1 = t.2)

def Algebraic.Cutwidth.Aggregate.Geometry.Joint.ConsistentLiterals {V : Type u_1} (literals : Finset (V × Bool)) : Prop

All literals on a given variable require the same value.

Equations

• Algebraic.Cutwidth.Aggregate.Geometry.Joint.ConsistentLiterals literals = ∀ a ∈ literals, ∀ b ∈ literals, a.1 = b.1 → a.2 = b.2