By simplification using the cardinality of the product type \(\mathrm{Bool} \times \mathrm{Fin}(W)\), we have \(|\mathrm{Bool}| \cdot |\mathrm{Fin}(W)| = 2 \cdot W\).

We simplify the definition of support vertices. We first establish that the filter \(\{ v \in \mathrm{Univ} \mid v_1 = \mathtt{false}\} \) equals the product set \(\{ \mathtt{false}\} \times \mathrm{Fin}(W)\) by extensionality on pairs \((b, i)\). Rewriting with this equality, the cardinality of the product is \(|\{ \mathtt{false}\} | \cdot |\mathrm{Fin}(W)| = 1 \cdot W = W\).

We simplify the definition of dummy vertices. We first establish that the filter \(\{ v \in \mathrm{Univ} \mid v_1 = \mathtt{true}\} \) equals the product set \(\{ \mathtt{true}\} \times \mathrm{Fin}(W)\) by extensionality on pairs \((b, i)\). Rewriting with this equality, the cardinality of the product is \(|\{ \mathtt{true}\} | \cdot |\mathrm{Fin}(W)| = 1 \cdot W = W\).

Symmetry: Let \(x, y\) be vertices with \(\mathrm{shorPathAdj}(x, y)\). We decompose \(h\) into three cases. Case 1: If \(x_1 \neq y_1\) and \(x_2 = y_2\), then \(y_1 \neq x_1\) and \(y_2 = x_2\), so \(\mathrm{shorPathAdj}(y, x)\) holds by the first disjunct. Case 2: If \(x_1 = y_1 = \mathtt{true}\) and \(x_2 + 1 = y_2\), then \(\mathrm{shorPathAdj}(y, x)\) holds by the third disjunct. Case 3: Symmetric to Case 2.

Irreflexivity: Suppose \(\mathrm{shorPathAdj}(x, x)\). Case 1: \(x_1 \neq x_1\), a contradiction. Cases 2 and 3: \(x_2 + 1 = x_2\), which is impossible by integer arithmetic.

Symmetry: We decompose the adjacency into three cases. Case 1: cross edge symmetry follows from \(\mathrm{Ne.symm}\) and equality symmetry. Cases 2 and 3: forward star edges become backward star edges and vice versa.

Irreflexivity: Suppose \(\mathrm{shorStarAdj}(x, x)\). Case 1: \(x_1 \neq x_1\), a contradiction. Cases 2 and 3: \(x_2 = 0\) and \(x_2 {\gt} 0\) simultaneously, which is impossible by integer arithmetic.

We case-split on \(e\). For \(\mathrm{cross}(i)\): this is a cross edge, and the adjacency follows from the first disjunct of \(\mathrm{shorPathAdj}\) since \(\mathtt{false} \neq \mathtt{true}\) and the indices agree. For \(\mathrm{dummyPath}(i)\): this is a path edge between dummy vertices, and the adjacency follows from the second disjunct since both components are \(\mathtt{true}\) and \(i + 1 = i + 1\).

We case-split on \(e\). For \(\mathrm{cross}(i)\): the adjacency follows from the first disjunct of \(\mathrm{shorStarAdj}\) since \(\mathtt{false} \neq \mathtt{true}\) and the indices agree. For \(\mathrm{dummyStar}(i)\): both components are \(\mathtt{true}\), the first index is \(0\), and \(i+1 {\gt} 0\) by \(\mathrm{Nat.succ\_ pos}\), so the second disjunct applies.

This follows directly from the symmetry of the graph applied to the adjacency of the endpoints.

This follows directly from the symmetry of the graph applied to the adjacency of the endpoints.

The universe of \(\mathrm{ShorEdgePath}(W)\) is the disjoint union of \(\mathrm{cross}\)-edges and \(\mathrm{dummyPath}\)-edges. We first establish that the image sets of the two constructors are disjoint: if \(e\) is in both images, then a cross edge equals a dummy path edge, which is impossible by constructor disjointness. Using the cardinality of a disjoint union, the total count is \(|\mathrm{Fin}(W)| + |\mathrm{Fin}(W-1)| = W + (W-1) = 2W - 1\), where injectivity of each constructor ensures the image has the same size as the domain.

The argument is identical to the path case. The universe of \(\mathrm{ShorEdgeStar}(W)\) decomposes into the disjoint images of \(\mathrm{cross}\) and \(\mathrm{dummyStar}\). By injectivity and disjointness, the count is \(W + (W-1) = 2W - 1\).

Assuming \(W \ge 1\), we verify \(2W - 1 + 1 = 2W\) by integer arithmetic.

Connectivity: We use the characterization of connectedness. First, all dummy vertices \((\mathtt{true}, i)\) are mutually reachable via the path: by induction on the indices, if \(a \le b\), we can reach \((\mathtt{true}, \langle b, \cdot \rangle )\) from \((\mathtt{true}, \langle a, \cdot \rangle )\) by following consecutive path edges. For the base case (\(b = 0\)), we must have \(a = 0\) and reachability is reflexive. For the inductive step, we use the inductive hypothesis to reach \((\mathtt{true}, \langle b', \cdot \rangle )\) and then take one path step to \((\mathtt{true}, \langle b'+1, \cdot \rangle )\). Every vertex \((s, i)\) connects to its dummy partner \((\mathtt{true}, i)\) via a cross edge (for \(s = \mathtt{false}\)) or trivially (for \(s = \mathtt{true}\)). Combining these, any two vertices \(x, y\) are reachable: from \(x\) to its dummy partner, through the path, and from the partner of \(y\) back to \(y\). The graph is nonempty since \((\mathtt{false}, 0)\) exists when \(W \ge 2\).

Support nonempty: The vertex \((\mathtt{false}, 0)\) belongs to \(\operatorname {supportVertices}(W)\) since \(W \ge 2\).

By case analysis on \(e\): if \(e = \mathrm{cross}(i)\) then \(\mathrm{isCrossEdge}\) returns \(\mathtt{true}\); if \(e = \mathrm{dummyPath}(i)\) then \(\mathrm{isDummyEdge}\) returns \(\mathtt{true}\). This is verified by simplification using the definitions.

By case analysis on \(e\): if \(e = \mathrm{cross}(i)\) then \(\mathrm{isDummyEdge}(e) = \mathtt{false}\); if \(e = \mathrm{dummyPath}(i)\) then \(\mathrm{isCrossEdge}(e) = \mathtt{false}\). In both cases, the conjunction is false.

We first establish that the set of cross edges equals the image of \(\mathrm{Fin}(W)\) under the \(\mathrm{cross}\) constructor. By extensionality, an edge \(e\) is in the filter if and only if \(e = \mathrm{cross}(i)\) for some \(i\). Then by injectivity of \(\mathrm{cross}\), the image has cardinality \(|\mathrm{Fin}(W)| = W\).

We first establish that the set of dummy edges equals the image of \(\mathrm{Fin}(W-1)\) under the \(\mathrm{dummyPath}\) constructor. By extensionality, an edge \(e\) is in the filter if and only if \(e = \mathrm{dummyPath}(i)\) for some \(i\). Then by injectivity of \(\mathrm{dummyPath}\), the image has cardinality \(|\mathrm{Fin}(W-1)| = W - 1\).

Unfolding \(\mathrm{shorPathAdj}\), the first disjunct is satisfied: \(\mathtt{false} \neq \mathtt{true}\) and the indices agree.

This holds by reflexivity from the definition of \(\mathrm{shorPathEdgeEndpoints}\).

This follows by integer arithmetic: \((W - 1) + 1 = W\).

The witness is \(e = \mathrm{dummyPath}(i)\). By definition, \(\mathrm{isDummyEdge}(\mathrm{dummyPath}(i)) = \mathtt{true}\) and the endpoints are \((\mathtt{true}, i)\) and \((\mathtt{true}, i+1)\), all holding by reflexivity.

Unfolding \(\mathrm{shorPathAdj}\), the first disjunct applies: \(\mathtt{true} \neq \mathtt{false}\) (by \(\mathrm{Bool.noConfusion}\)) and the indices agree.

For each \(i\), the first adjacency follows from \(\mathrm{support\_ vertex\_ cross\_ adj}\) and the second from \(\mathrm{gaussLaw\_ at\_ dummy\_ involves\_ cross}\).

Let \(v\) be given. By simplification, the sum over the indicator function evaluating to \(1\) at \(v\) gives exactly \(1\).

The five components follow directly from the previously established results: \(\mathrm{cross\_ edge\_ count}\) for (1), \(\mathrm{dummy\_ path\_ edge\_ count}\) for (2), \(\mathrm{cross\_ edge\_ matching}\) for (3), reflexivity for (4), and \(\mathrm{shorStyle\_ edge\_ count\_ path}\) for (5).

Unfolding \(\mathrm{shorStarAdj}\), the second disjunct applies: both components are \(\mathtt{true}\), the first index is \(0\), and \(j + 1 {\gt} 0\) by \(\mathrm{Nat.succ\_ pos}\).

Rewriting both sides using \(\mathrm{shorStyle\_ edge\_ count\_ star}\) and \(\mathrm{shorStyle\_ edge\_ count\_ path}\), both equal \(2W - 1\).

This follows directly from \(\mathrm{gaussLaw\_ product\_ vertexSupport\_ all\_ ones}\) applied to the \(\mathrm{ShorPathGraphWithCycles}(W)\) instance.

This follows directly from \(\mathrm{gaussLaw\_ product\_ edgeSupport\_ zero}\) applied to the \(\mathrm{ShorPathGraphWithCycles}(W)\) instance.

This follows directly from \(\mathrm{gaussLaw\_ product\_ is\_ L}\) applied to the \(\mathrm{ShorPathGraphWithCycles}(W)\) instance, which combines the two previous results.