Correctness Proof

It remains to prove that the above method produces a normalised path as its output, given that the path P₁ was normalised. The proof is basically a proof by contradiction; we show that if the output path of the algorithm is not normalised, then the input path must also have not been normalised.

Given that the input is

$$P_{1} = x_{1},x_{2}, x_{3} \ldots x_{m}$$

The output of the algorithm is a path P₂, with the properties as shown in fig. 3.3

  

Figure 3.3: Properties of P₂

Any alias for P₂ is an alias for P₁ with b inserted at some point. So suppose we have a P₃, an alias for P₁

$$P_{3} = y_{1} \ldots y_{m}$$

We must have $P_{3} \ge P_{1}$, as P₁ is normalised. If P₃ = P₁, then we clearly cannot insert b at a valid point in order to decrease P₃, so assume from now on that P₃ > P₁. This gives us:-

$$P_{1} = x_{1},x_{2},x_{3}, \ldots x_{m} \quad P_{3} = y_{1},y_{2},y_{3}, \ldots y_{m}$$

$$\exists c \ge 0 \qquad \textrm{s.t.} \qquad x_{i} = y_{i} \qquad \forall i \le c$$

$$\textrm{and} \qquad ( x_{c+1} < y_{c+1})$$

Now suppose P'₃ is P₃ with b inserted at some point:

$$P'_{3} = y_{1} \ldots y_{k},b,y_{k+1} \ldots y_{m}$$

There are now several cases to consider depending on the relative sizes of (c,k,q). For each case we aim to show P'₃ > P₂, and conclude that P₂ must be normalised.