Fix a list of weighted edges on \(n\) vertices, and let \(u\) and \(v\) be two vertices. Recall that \(u\) and \(v\) are symmetrically adjacent when some edge in the list has \(\{ u, v\} \) as its pair of endpoints, in either order. If \(u\) and \(v\) are symmetrically adjacent, then so are \(v\) and \(u\).

Fix \(n \in \mathbb {N}\) and two vertices \(u, v \in \mathrm{Fin}\, n\), and let \(e_1\) and \(e_2\) be lists of weighted edges on \(n\) vertices such that every edge of \(e_1\) also occurs in \(e_2\). If \(u\) and \(v\) are symmetrically adjacent in \(e_1\) — that is, some edge of \(e_1\) has endpoints \(\{ u,v\} \) in either order — then \(u\) and \(v\) are symmetrically adjacent in \(e_2\).

Let \(\mathit{edges}\) be a list of weighted edges on \(n\) vertices, and call two vertices reachable when they are joined by a path along these edges (in the sense of the reflexive–transitive closure of symmetric adjacency). Then reachability is symmetric: for all vertices \(u, v\), if \(u\) is reachable from \(v\), then \(v\) is reachable from \(u\).

Fix \(n\), let \(e_1\) and \(e_2\) be lists of weighted edges on the vertex set \(\mathrm{Fin}\, n\), and let \(u, v : \mathrm{Fin}\, n\). Suppose \(u\) and \(v\) are connected by a path through the edges of \(e_1\), and that every edge of \(e_1\) also occurs in \(e_2\). Then \(u\) and \(v\) are connected by a path through the edges of \(e_2\).

Let \(\mathit{edges}\) be a list of weighted edges on \(n\) vertices, and let \(e\) be a weighted edge belonging to \(\mathit{edges}\). Then the endpoints \(u\) and \(v\) of \(e\) satisfy \(\mathtt{Reach}\, \mathit{edges}\, u\, v\); that is, they are connected by a path through \(\mathit{edges}\).

Let \(\mathit{edges}\) and \(\mathit{edges}'\) be two lists of weighted edges on \(n\) vertices, and suppose that whenever two vertices \(a\) and \(b\) are symmetrically adjacent in \(\mathit{edges}\) — that is, some edge of \(\mathit{edges}\) has endpoints \(\{ a,b\} \) — the vertices \(a\) and \(b\) are connected by a path through \(\mathit{edges}'\). Then for any vertices \(u\) and \(v\), if \(u\) and \(v\) are connected by a path through \(\mathit{edges}\), they are also connected by a path through \(\mathit{edges}'\).

Let \(g\) be a weighted edge on \(n\) vertices with endpoints \(p\) and \(q\), let \(\mathit{rest}\) be a list of weighted edges on the same \(n\) vertices, and let \(a\) and \(b\) be vertices; say two vertices are \(\mathit{rest}\)-connected when they are joined by a path using only the edges in \(\mathit{rest}\). Then \(a\) and \(b\) are joined by a path through the edges of the list obtained by prepending \(g\) to \(\mathit{rest}\) if and only if at least one of the following holds: \(a\) and \(b\) are \(\mathit{rest}\)-connected; or \(a\) is \(\mathit{rest}\)-connected to \(p\) while \(q\) is \(\mathit{rest}\)-connected to \(b\); or \(a\) is \(\mathit{rest}\)-connected to \(q\) while \(p\) is \(\mathit{rest}\)-connected to \(b\).

Fix \(n \in \mathbb {N}\), and let \(l_1\) and \(l_2\) be two lists of weighted edges on the vertex set \(\mathrm{Fin}\, n\) that have the same members, i.e. \(x \in l_1 \Leftrightarrow x \in l_2\) for every weighted edge \(x\). Then for any vertices \(a, b \in \mathrm{Fin}\, n\), the vertex \(b\) is reachable from \(a\) through the edges of \(l_1\) if and only if it is reachable from \(a\) through the edges of \(l_2\).

Over any number of vertices \(n\), the total weight of the empty list of weighted edges is \(0\); that is, the sum of the weights of no edges is \(\sum _{e \in [\, ]} e.\mathit{weight} = 0\).

Let \(\mathit{edges}\) be a list of weighted edges over \(n\) vertices, and let \(e\) be a weighted edge occurring in \(\mathit{edges}\). Then the total weight of \(\mathit{edges}\) equals the weight of \(e\) plus the total weight of the list obtained by deleting the first occurrence of \(e\) from \(\mathit{edges}\).