User:Jshflynn/Levi's lemma case 1
Theorem
Let $\Sigma$ be an alphabet.
Let $\Sigma^{*}$ denote the Kleene star of $\Sigma$ and $\circ$ denote concatenation. Then:
- $
\forall v, w, x, y \in \Sigma^{*}: $$ $$ v \circ w = x \circ y \text{ and } \operatorname{len}(v) \ge \operatorname{len}(x) $$ $$ \implies \exists ! z \in \Sigma^{*}: v = x \circ z \text{ and } y = z \circ w $
Proof
From the definition of word equality:
- $\forall i: (v \circ w)_i = (x \circ y)_i$
By the definition of concatenation, up to $i = \operatorname{len}(x)$ we have $x_i = v_i$.
If $\operatorname{len}(v) = \operatorname{len}(x)$ then $z = \lambda$.
That this is unique follows from Empty Word is Unique.
For the other cases we will show, by induction, that the infix $t$ of $(x \circ z)$ defined as $t_i = (x \circ y)_{\operatorname{len}(x)+i}$ for $i \in [1..\operatorname{len}(v)-\operatorname{len}(x)]$ is the unique infix
satisfying $z$.
For the base case where $\operatorname{len}(v) = \operatorname{len}(x) + 1$ then $t = (x \circ y)_{\operatorname{len}(x)+1}$.
This is unique as it is a single letter of $\Sigma$ and being an element of a set it is defined to be unique.
For the the inductive step, we suppose there exists a $k \in [1..\operatorname{len}(v)-\operatorname{len}(x) - 1]$ such that $\operatorname{len}(v) = \operatorname{len}(x) + k$ and that there exists a unique infix $t$ satisfying $z$.
Then for $\operatorname{len}(v) = \operatorname{len}(x) + k + 1$ we define $t'$ as $t \circ (x \circ y)_{\operatorname{len}(x)+\operatorname{len}(t) + 1}$.
$t'$ uniquely satisfies $z$ up to $t'_{\operatorname{len}(t)}$ by hypothesis.
The remaining letter satisfies $z$ and is unique by being a single letter.
Hence the result.
$\blacksquare$