Finite Sequences in Set Form Acyclic Graph

This article is complete as far as it goes, but it could do with expansion. In particular: These actually form a tree. You can help $\mathsf{Pr} \infty \mathsf{fWiki}$ by adding this information. To discuss this page in more detail, feel free to use the talk page. When this work has been completed, you may remove this instance of {{Expand}} from the code. If you would welcome a second opinion as to whether your work is correct, add a call to {{Proofread}} the page.

Although this article appears correct, it's inelegant. There has to be a better way of doing it. In particular: The descriptions of $E$ are both fairly awful. You can help $\mathsf{Pr} \infty \mathsf{fWiki}$ by redesigning it. To discuss this page in more detail, feel free to use the talk page. When this work has been completed, you may remove this instance of {{Improve}} from the code. If you would welcome a second opinion as to whether your work is correct, add a call to {{Proofread}} the page.

Theorem

Let $S$ be a set.

Let $V$ be the set of finite sequences in $S$.

Let $E$ be the set of unordered pairs $\set {p, q}$ of elements of $V$ such that either:

$q$ is formed by extending $p$ by one element or

$p$ is formed by extending $q$ by one element.

That is:

$\card {\Dom p \symdif \Dom q} = 1$, where $\symdif$ is symmetric difference

$p \restriction D = q \restriction D$, where $D = \Dom p \cap \Dom q$

Then $T = \struct{V, E}$ is an acyclic graph.

Proof

This theorem requires a proof. You can help $\mathsf{Pr} \infty \mathsf{fWiki}$ by crafting such a proof. To discuss this page in more detail, feel free to use the talk page. When this work has been completed, you may remove this instance of {{ProofWanted}} from the code. If you would welcome a second opinion as to whether your work is correct, add a call to {{Proofread}} the page.