The wire graph of a closed set of wires

Fix a program over any signature whose gates have at most two arguments, and a closed set K of wires: a gate lies in K exactly when the wires it reads do. The wire graph of K has a vertex for every wire of K and, for a wire read by f ≥ 2 argument slots, f - 1 copy vertices of degree three through which the signal is routed. Its edges are the argument slots of the gates of K and the incoming edge of every copy vertex. This is the construction of Cutwidth.Wiring, freed from the binary basis and from the reachability restriction.

The main results are

• loopless, maxDegreeLE_three, connected: the hypotheses of the graph-ordering bound, the last one when K is nonempty and connected in the wire graph;
• card_forward_add_card_backward_le: for every set L of vertices, the forward and backward signals of the wires whose vertices lie in L number at most the edges of the cut of L. Every edge carries one signal, and the edges carrying a signal form a tree joining its wire to every gate reading it, so a signal crossing the split crosses the cut;
• card_edge_sub_card_vertex_le, card_vertex_le: the excess of edges over vertices is at most the number of gates minus the number of inputs in K, and there are at most i + 3 g vertices for i inputs and g gates in K.

theorem Algebraic.Cutwidth.MultiOutput.Internal.arity_le_of_fanInAtMost {σ : Signature} {n r s : ℕ} (p : Program σ n s) : p.FanInAtMost r → ∀ (g : Fin s), σ.Arity (p.lines g).op ≤ r

A gate of a program with fan-in at most r has at most r arguments.

structure Algebraic.Cutwidth.MultiOutput.Internal.ClosedSet {σ : Signature} {n s : ℕ} (p : Program σ n s) : Type

A closed set of wires: a gate lies in the set exactly when every wire it reads does.

• carrier : Finset (Wire n s)

  The wires of the set.

• closed (g : Fin s) (w : Wire n s) : p.Reads g w → (Wire.gate g ∈ self.carrier ↔ w ∈ self.carrier)

  A gate and each wire it reads lie on the same side.

@[reducible, inline]

abbrev Algebraic.Cutwidth.MultiOutput.Internal.WireGraph.Signal {σ : Signature} {n s : ℕ} {p : Program σ n s} (K : ClosedSet p) : Type

The wires of K: the signals of the wire graph.

Equations

• Algebraic.Cutwidth.MultiOutput.Internal.WireGraph.Signal K = ↥K.carrier

@[reducible, inline]

abbrev Algebraic.Cutwidth.MultiOutput.Internal.WireGraph.Slot {σ : Signature} {n s : ℕ} {p : Program σ n s} (K : ClosedSet p) : Type

The argument slots of the gates of K.

Equations

• Algebraic.Cutwidth.MultiOutput.Internal.WireGraph.Slot K = { t : (g : Fin s) × Fin (σ.Arity (p.lines g).op) // Cslib.Circuits.Wire.gate t.fst ∈ K.carrier }

def Algebraic.Cutwidth.MultiOutput.Internal.WireGraph.slotWire {σ : Signature} {n s : ℕ} {p : Program σ n s} (K : ClosedSet p) (t : Slot K) : Wire n s

The wire read by a slot.

Equations

• Algebraic.Cutwidth.MultiOutput.Internal.WireGraph.slotWire K t = (p.lines (↑t).fst).wires (↑t).snd

theorem Algebraic.Cutwidth.MultiOutput.Internal.WireGraph.reads_slotWire {σ : Signature} {n s : ℕ} {p : Program σ n s} (K : ClosedSet p) (t : Slot K) : p.Reads (↑t).fst (slotWire K t)

def Algebraic.Cutwidth.MultiOutput.Internal.WireGraph.slotSignal {σ : Signature} {n s : ℕ} {p : Program σ n s} (K : ClosedSet p) (t : Slot K) : Signal K

The signal read by a slot.

Equations

• Algebraic.Cutwidth.MultiOutput.Internal.WireGraph.slotSignal K t = ⟨Algebraic.Cutwidth.MultiOutput.Internal.WireGraph.slotWire K t, ⋯⟩

def Algebraic.Cutwidth.MultiOutput.Internal.WireGraph.slotGate {σ : Signature} {n s : ℕ} {p : Program σ n s} (K : ClosedSet p) (t : Slot K) : Signal K

The gate owning a slot.

Equations

• Algebraic.Cutwidth.MultiOutput.Internal.WireGraph.slotGate K t = ⟨Cslib.Circuits.Wire.gate (↑t).fst, ⋯⟩

noncomputable def Algebraic.Cutwidth.MultiOutput.Internal.WireGraph.slots {σ : Signature} {n s : ℕ} {p : Program σ n s} (K : ClosedSet p) (w : Signal K) : Finset (Slot K)

The slots fed by a signal.

Equations

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

theorem Algebraic.Cutwidth.MultiOutput.Internal.WireGraph.mem_slots {σ : Signature} {n s : ℕ} {p : Program σ n s} (K : ClosedSet p) {w : Signal K} {t : Slot K} : t ∈ slots K w ↔ slotSignal K t = w

noncomputable def Algebraic.Cutwidth.MultiOutput.Internal.WireGraph.fanout {σ : Signature} {n s : ℕ} {p : Program σ n s} (K : ClosedSet p) (w : Signal K) : ℕ

The number of slots fed by a signal.

Equations

• Algebraic.Cutwidth.MultiOutput.Internal.WireGraph.fanout K w = (Algebraic.Cutwidth.MultiOutput.Internal.WireGraph.slots K w).card

theorem Algebraic.Cutwidth.MultiOutput.Internal.WireGraph.fanout_pos_of_slot {σ : Signature} {n s : ℕ} {p : Program σ n s} (K : ClosedSet p) (t : Slot K) : 0 < fanout K (slotSignal K t)

@[reducible, inline]

abbrev Algebraic.Cutwidth.MultiOutput.Internal.WireGraph.Copy {σ : Signature} {n s : ℕ} {p : Program σ n s} (K : ClosedSet p) : Type

A signal feeding f ≥ 2 slots is routed through f - 1 copy vertices.

Equations

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

@[reducible, inline]

abbrev Algebraic.Cutwidth.MultiOutput.Internal.WireGraph.Vertex {σ : Signature} {n s : ℕ} {p : Program σ n s} (K : ClosedSet p) : Type

Vertices: the wires of K and the copy vertices.

Equations

• Algebraic.Cutwidth.MultiOutput.Internal.WireGraph.Vertex K = (Algebraic.Cutwidth.MultiOutput.Internal.WireGraph.Signal K ⊕ Algebraic.Cutwidth.MultiOutput.Internal.WireGraph.Copy K)

@[reducible, inline]

abbrev Algebraic.Cutwidth.MultiOutput.Internal.WireGraph.Edge {σ : Signature} {n s : ℕ} {p : Program σ n s} (K : ClosedSet p) : Type

Edges: the slots of the gates of K and the incoming edges of the copy vertices.

Equations

• Algebraic.Cutwidth.MultiOutput.Internal.WireGraph.Edge K = (Algebraic.Cutwidth.MultiOutput.Internal.WireGraph.Slot K ⊕ Algebraic.Cutwidth.MultiOutput.Internal.WireGraph.Copy K)

noncomputable def Algebraic.Cutwidth.MultiOutput.Internal.WireGraph.slotIndex {σ : Signature} {n s : ℕ} {p : Program σ n s} (K : ClosedSet p) (t : Slot K) : ℕ

The position of a slot among the slots of its signal.

Equations

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

theorem Algebraic.Cutwidth.MultiOutput.Internal.WireGraph.slotIndex_lt {σ : Signature} {n s : ℕ} {p : Program σ n s} (K : ClosedSet p) (t : Slot K) : slotIndex K t < fanout K (slotSignal K t)

theorem Algebraic.Cutwidth.MultiOutput.Internal.WireGraph.slotIndex_injective {σ : Signature} {n s : ℕ} {p : Program σ n s} (K : ClosedSet p) {t t' : Slot K} (hsignal : slotSignal K t = slotSignal K t') (hindex : slotIndex K t = slotIndex K t') : t = t'

Slots of one signal are determined by their positions.

noncomputable def Algebraic.Cutwidth.MultiOutput.Internal.WireGraph.copyIndex {σ : Signature} {n s : ℕ} {p : Program σ n s} (K : ClosedSet p) (t : Slot K) : ℕ

The copy vertex at which a slot is attached, when its signal has fan-out at least two: slots in order, with the last two slots sharing the last copy.

Equations

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

theorem Algebraic.Cutwidth.MultiOutput.Internal.WireGraph.copyIndex_lt {σ : Signature} {n s : ℕ} {p : Program σ n s} (K : ClosedSet p) (t : Slot K) (h : 2 ≤ fanout K (slotSignal K t)) : copyIndex K t < fanout K (slotSignal K t) - 1

noncomputable def Algebraic.Cutwidth.MultiOutput.Internal.WireGraph.fst {σ : Signature} {n s : ℕ} {p : Program σ n s} (K : ClosedSet p) : Edge K → Vertex K

The first endpoint of an edge: the signal vertex or copy vertex supplying it.

Equations

• One or more equations did not get rendered due to their size.
• Algebraic.Cutwidth.MultiOutput.Internal.WireGraph.fst K (Sum.inr ⟨w, k⟩) = if h : ↑k = 0 then Sum.inl w else Sum.inr ⟨w, ⟨↑k - 1, ⋯⟩⟩

def Algebraic.Cutwidth.MultiOutput.Internal.WireGraph.snd {σ : Signature} {n s : ℕ} {p : Program σ n s} (K : ClosedSet p) : Edge K → Vertex K

The second endpoint of an edge: the gate owning a slot, or the copy vertex.

Equations

• Algebraic.Cutwidth.MultiOutput.Internal.WireGraph.snd K (Sum.inl t) = Sum.inl (Algebraic.Cutwidth.MultiOutput.Internal.WireGraph.slotGate K t)
• Algebraic.Cutwidth.MultiOutput.Internal.WireGraph.snd K (Sum.inr c) = Sum.inr c

def Algebraic.Cutwidth.MultiOutput.Internal.WireGraph.signal {σ : Signature} {n s : ℕ} {p : Program σ n s} (K : ClosedSet p) : Edge K → Signal K

The signal carried by an edge.

Equations

• Algebraic.Cutwidth.MultiOutput.Internal.WireGraph.signal K (Sum.inl t) = Algebraic.Cutwidth.MultiOutput.Internal.WireGraph.slotSignal K t
• Algebraic.Cutwidth.MultiOutput.Internal.WireGraph.signal K (Sum.inr ⟨w, k⟩) = w

noncomputable def Algebraic.Cutwidth.MultiOutput.Internal.WireGraph.graph {σ : Signature} {n s : ℕ} {p : Program σ n s} (K : ClosedSet p) : Multigraph (Vertex K) (Edge K)

The wire graph of K.

Equations

• Algebraic.Cutwidth.MultiOutput.Internal.WireGraph.graph K = { fst := Algebraic.Cutwidth.MultiOutput.Internal.WireGraph.fst K, snd := Algebraic.Cutwidth.MultiOutput.Internal.WireGraph.snd K }

theorem Algebraic.Cutwidth.MultiOutput.Internal.WireGraph.fst_inl_of_two_le {σ : Signature} {n s : ℕ} {p : Program σ n s} (K : ClosedSet p) (t : Slot K) (h : 2 ≤ fanout K (slotSignal K t)) : fst K (Sum.inl t) = Sum.inr ⟨slotSignal K t, ⟨copyIndex K t, ⋯⟩⟩

theorem Algebraic.Cutwidth.MultiOutput.Internal.WireGraph.fst_inl_of_not_two_le {σ : Signature} {n s : ℕ} {p : Program σ n s} (K : ClosedSet p) (t : Slot K) (h : ¬2 ≤ fanout K (slotSignal K t)) : fst K (Sum.inl t) = Sum.inl (slotSignal K t)

theorem Algebraic.Cutwidth.MultiOutput.Internal.WireGraph.fst_inr_zero {σ : Signature} {n s : ℕ} {p : Program σ n s} (K : ClosedSet p) (w : Signal K) (h : 0 < fanout K w - 1) : fst K (Sum.inr ⟨w, ⟨0, h⟩⟩) = Sum.inl w

theorem Algebraic.Cutwidth.MultiOutput.Internal.WireGraph.fst_inr_succ {σ : Signature} {n s : ℕ} {p : Program σ n s} (K : ClosedSet p) (w : Signal K) (k : ℕ) (h : k + 1 < fanout K w - 1) : fst K (Sum.inr ⟨w, ⟨k + 1, h⟩⟩) = Sum.inr ⟨w, ⟨k, ⋯⟩⟩

Walks along one signal

def Algebraic.Cutwidth.MultiOutput.Internal.WireGraph.SignalAdj {σ : Signature} {n s : ℕ} {p : Program σ n s} (K : ClosedSet p) (w : Signal K) (u v : Vertex K) : Prop

Two vertices are joined by an edge carrying the signal w.

Equations

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

theorem Algebraic.Cutwidth.MultiOutput.Internal.WireGraph.signalAdj_of_edge {σ : Signature} {n s : ℕ} {p : Program σ n s} (K : ClosedSet p) (e : Edge K) : SignalAdj K (signal K e) (fst K e) (snd K e)

An edge joins its endpoints along its own signal.

theorem Algebraic.Cutwidth.MultiOutput.Internal.WireGraph.SignalAdj.symm {σ : Signature} {n s : ℕ} {p : Program σ n s} (K : ClosedSet p) {w : Signal K} {u v : Vertex K} (h : SignalAdj K w u v) : SignalAdj K w v u

theorem Algebraic.Cutwidth.MultiOutput.Internal.WireGraph.reflTransGen_signalAdj_symm {σ : Signature} {n s : ℕ} {p : Program σ n s} (K : ClosedSet p) {w : Signal K} {u v : Vertex K} (h : Relation.ReflTransGen (SignalAdj K w) u v) : Relation.ReflTransGen (SignalAdj K w) v u

theorem Algebraic.Cutwidth.MultiOutput.Internal.WireGraph.adj_of_signalAdj {σ : Signature} {n s : ℕ} {p : Program σ n s} (K : ClosedSet p) {w : Signal K} {u v : Vertex K} (h : SignalAdj K w u v) : (graph K).Adj u v

An edge carrying a signal is an edge of the graph.

theorem Algebraic.Cutwidth.MultiOutput.Internal.WireGraph.reflTransGen_adj_of_signalAdj {σ : Signature} {n s : ℕ} {p : Program σ n s} (K : ClosedSet p) {w : Signal K} {u v : Vertex K} (h : Relation.ReflTransGen (SignalAdj K w) u v) : Relation.ReflTransGen (graph K).Adj u v

theorem Algebraic.Cutwidth.MultiOutput.Internal.WireGraph.signal_reaches_copy {σ : Signature} {n s : ℕ} {p : Program σ n s} (K : ClosedSet p) (w : Signal K) (m : ℕ) (hm : m < fanout K w - 1) : Relation.ReflTransGen (SignalAdj K w) (Sum.inl w) (Sum.inr ⟨w, ⟨m, hm⟩⟩)

Every copy vertex of a signal is joined to the signal's vertex along its copy chain.

theorem Algebraic.Cutwidth.MultiOutput.Internal.WireGraph.signal_reaches_gate {σ : Signature} {n s : ℕ} {p : Program σ n s} (K : ClosedSet p) (t : Slot K) : Relation.ReflTransGen (SignalAdj K (slotSignal K t)) (Sum.inl (slotSignal K t)) (Sum.inl (slotGate K t))

The vertex of a signal is joined to the vertex of every gate reading it, along edges carrying the signal.

theorem Algebraic.Cutwidth.MultiOutput.Internal.WireGraph.exists_mem_cut_of_reflTransGen {σ : Signature} {n s : ℕ} {p : Program σ n s} (K : ClosedSet p) (L : Finset (Vertex K)) {w : Signal K} {u v : Vertex K} (h : Relation.ReflTransGen (SignalAdj K w) u v) (huv : ¬(u ∈ L ↔ v ∈ L)) : ∃ e ∈ (graph K).cut L, signal K e = w

A walk along one signal between the two sides of a vertex set crosses its cut with an edge carrying that signal.

Signals crossing a cut

noncomputable def Algebraic.Cutwidth.MultiOutput.Internal.WireGraph.wiresIn {σ : Signature} {n s : ℕ} {p : Program σ n s} (K : ClosedSet p) (L : Finset (Vertex K)) : Finset (Wire n s)

The wires of K whose vertices lie in L.

Equations

• Algebraic.Cutwidth.MultiOutput.Internal.WireGraph.wiresIn K L = {w ∈ K.carrier | ∃ (h : w ∈ K.carrier), Sum.inl ⟨w, h⟩ ∈ L}

theorem Algebraic.Cutwidth.MultiOutput.Internal.WireGraph.mem_wiresIn {σ : Signature} {n s : ℕ} {p : Program σ n s} (K : ClosedSet p) {L : Finset (Vertex K)} {w : Wire n s} : w ∈ wiresIn K L ↔ ∃ (h : w ∈ K.carrier), Sum.inl ⟨w, h⟩ ∈ L

theorem Algebraic.Cutwidth.MultiOutput.Internal.WireGraph.wiresIn_subset {σ : Signature} {n s : ℕ} {p : Program σ n s} (K : ClosedSet p) (L : Finset (Vertex K)) : wiresIn K L ⊆ K.carrier

theorem Algebraic.Cutwidth.MultiOutput.Internal.WireGraph.exists_cut_edge {σ : Signature} {n s : ℕ} {p : Program σ n s} (K : ClosedSet p) (L : Finset (Vertex K)) {g : Fin s} {w : Wire n s} (hr : p.Reads g w) (hg : Wire.gate g ∈ K.carrier) (hside : ¬(w ∈ wiresIn K L ↔ Wire.gate g ∈ wiresIn K L)) : ∃ e ∈ (graph K).cut L, ↑(signal K e) = w

A gate of K reading a wire on the other side of the split yields a cut edge carrying that wire's signal.

theorem Algebraic.Cutwidth.MultiOutput.Internal.WireGraph.card_forward_add_card_backward_le {σ : Signature} {n s : ℕ} {p : Program σ n s} (K : ClosedSet p) (L : Finset (Vertex K)) : (SingleCut.forward p (wiresIn K L)).card + (SingleCut.backward p (wiresIn K L)).card ≤ ((graph K).cut L).card

Crossing signals are bounded by the cut. For every set L of vertices, the forward and backward signals of the wires whose vertices lie in L number at most the edges of the cut of L.

Graph properties

theorem Algebraic.Cutwidth.MultiOutput.Internal.WireGraph.loopless {σ : Signature} {n s : ℕ} {p : Program σ n s} (K : ClosedSet p) : (graph K).Loopless

No edge joins a vertex to itself.

noncomputable def Algebraic.Cutwidth.MultiOutput.Internal.WireGraph.outEdges {σ : Signature} {n s : ℕ} {p : Program σ n s} (K : ClosedSet p) (v : Vertex K) : Finset (Edge K)

The edges leaving a vertex.

Equations

• Algebraic.Cutwidth.MultiOutput.Internal.WireGraph.outEdges K v = {e : Algebraic.Cutwidth.MultiOutput.Internal.WireGraph.Edge K | Algebraic.Cutwidth.MultiOutput.Internal.WireGraph.fst K e = v}

noncomputable def Algebraic.Cutwidth.MultiOutput.Internal.WireGraph.inEdges {σ : Signature} {n s : ℕ} {p : Program σ n s} (K : ClosedSet p) (v : Vertex K) : Finset (Edge K)

The edges entering a vertex.

Equations

• Algebraic.Cutwidth.MultiOutput.Internal.WireGraph.inEdges K v = {e : Algebraic.Cutwidth.MultiOutput.Internal.WireGraph.Edge K | Algebraic.Cutwidth.MultiOutput.Internal.WireGraph.snd K e = v}

theorem Algebraic.Cutwidth.MultiOutput.Internal.WireGraph.mem_outEdges {σ : Signature} {n s : ℕ} {p : Program σ n s} (K : ClosedSet p) {v : Vertex K} {e : Edge K} : e ∈ outEdges K v ↔ fst K e = v

theorem Algebraic.Cutwidth.MultiOutput.Internal.WireGraph.mem_inEdges {σ : Signature} {n s : ℕ} {p : Program σ n s} (K : ClosedSet p) {v : Vertex K} {e : Edge K} : e ∈ inEdges K v ↔ snd K e = v

theorem Algebraic.Cutwidth.MultiOutput.Internal.WireGraph.edgesAt_subset {σ : Signature} {n s : ℕ} {p : Program σ n s} (K : ClosedSet p) (v : Vertex K) : (graph K).edgesAt v ⊆ outEdges K v ∪ inEdges K v

theorem Algebraic.Cutwidth.MultiOutput.Internal.WireGraph.card_inEdges_inl_le {σ : Signature} {n s : ℕ} {p : Program σ n s} (K : ClosedSet p) (hp : p.FanInAtMost 2) (w : Signal K) : (inEdges K (Sum.inl w)).card ≤ 2

A signal vertex receives at most two edges: the slots of its gate.

theorem Algebraic.Cutwidth.MultiOutput.Internal.WireGraph.card_outEdges_inl_le {σ : Signature} {n s : ℕ} {p : Program σ n s} (K : ClosedSet p) (w : Signal K) : (outEdges K (Sum.inl w)).card ≤ 1

At most one edge leaves a signal vertex.

theorem Algebraic.Cutwidth.MultiOutput.Internal.WireGraph.card_inEdges_inr_le {σ : Signature} {n s : ℕ} {p : Program σ n s} (K : ClosedSet p) (c : Copy K) : (inEdges K (Sum.inr c)).card ≤ 1

Exactly one edge enters a copy vertex.

theorem Algebraic.Cutwidth.MultiOutput.Internal.WireGraph.copyIndex_le_slotIndex {σ : Signature} {n s : ℕ} {p : Program σ n s} (K : ClosedSet p) (t : Slot K) : copyIndex K t ≤ slotIndex K t

A slot attached to a copy vertex has its position at least the copy's.

theorem Algebraic.Cutwidth.MultiOutput.Internal.WireGraph.card_outEdges_inr_le {σ : Signature} {n s : ℕ} {p : Program σ n s} (K : ClosedSet p) (w : Signal K) (k : Fin (fanout K w - 1)) : (outEdges K (Sum.inr ⟨w, k⟩)).card ≤ 2

At most two edges leave a copy vertex: the next copy edge and its slots.

theorem Algebraic.Cutwidth.MultiOutput.Internal.WireGraph.maxDegreeLE_three {σ : Signature} {n s : ℕ} {p : Program σ n s} (K : ClosedSet p) (hp : p.FanInAtMost 2) : (graph K).MaxDegreeLE 3

Every vertex has at most three incident edges.

theorem Algebraic.Cutwidth.MultiOutput.Internal.WireGraph.reflTransGen_adj_of_linked {σ : Signature} {n s : ℕ} {p : Program σ n s} (K : ClosedSet p) {u v : Wire n s} (h : Linked p u v) (hu : u ∈ K.carrier) (hv : v ∈ K.carrier) : Relation.ReflTransGen (graph K).Adj (Sum.inl ⟨u, hu⟩) (Sum.inl ⟨v, hv⟩)

Linked wires of K are joined in the wire graph.

theorem Algebraic.Cutwidth.MultiOutput.Internal.WireGraph.exists_reflTransGen_adj_of_reflTransGen {σ : Signature} {n s : ℕ} {p : Program σ n s} (K : ClosedSet p) {u v : Wire n s} (h : Relation.ReflTransGen (Linked p) u v) (hu : u ∈ K.carrier) : ∃ (hv : v ∈ K.carrier), Relation.ReflTransGen (graph K).Adj (Sum.inl ⟨u, hu⟩) (Sum.inl ⟨v, hv⟩)

Paths of linked wires starting in K stay in K and lift to the wire graph.

theorem Algebraic.Cutwidth.MultiOutput.Internal.WireGraph.connected {σ : Signature} {n s : ℕ} {p : Program σ n s} (K : ClosedSet p) (hne : K.carrier.Nonempty) (hconn : ∀ u ∈ K.carrier, ∀ v ∈ K.carrier, Relation.ReflTransGen (Linked p) u v) : (graph K).Connected

The wire graph of a nonempty set of wires connected in the program's wire graph is connected.

Counting vertices and edges

theorem Algebraic.Cutwidth.MultiOutput.Internal.WireGraph.card_slot_le {σ : Signature} {n s : ℕ} {p : Program σ n s} (K : ClosedSet p) (hp : p.FanInAtMost 2) : Fintype.card (Slot K) ≤ 2 * (gatesIn K.carrier).card

The slots of K number at most twice its gates.

theorem Algebraic.Cutwidth.MultiOutput.Internal.WireGraph.card_signal {σ : Signature} {n s : ℕ} {p : Program σ n s} (K : ClosedSet p) : Fintype.card (Signal K) = (SingleCut.inputsIn K.carrier).card + (gatesIn K.carrier).card

The signals of K are its inputs and its gates.

theorem Algebraic.Cutwidth.MultiOutput.Internal.WireGraph.card_copy_le {σ : Signature} {n s : ℕ} {p : Program σ n s} (K : ClosedSet p) : Fintype.card (Copy K) ≤ Fintype.card (Slot K)

There are no more copy vertices than slots.

theorem Algebraic.Cutwidth.MultiOutput.Internal.WireGraph.card_edge_sub_card_vertex_le {σ : Signature} {n s : ℕ} {p : Program σ n s} (K : ClosedSet p) (hp : p.FanInAtMost 2) : ↑(Fintype.card (Edge K)) - ↑(Fintype.card (Vertex K)) ≤ ↑(gatesIn K.carrier).card - ↑(SingleCut.inputsIn K.carrier).card

The excess of edges over vertices is at most the gates minus the inputs of K.

theorem Algebraic.Cutwidth.MultiOutput.Internal.WireGraph.card_vertex_le {σ : Signature} {n s : ℕ} {p : Program σ n s} (K : ClosedSet p) (hp : p.FanInAtMost 2) : Fintype.card (Vertex K) ≤ (SingleCut.inputsIn K.carrier).card + 3 * (gatesIn K.carrier).card

The wire graph of K has at most i + 3 g vertices for i inputs and g gates in K.