Rendezés

Legyen T tetszőleges rendezett típus és X = seq(T), legyen továbbá x : X. Rendezzük át az x sorozatot úgy, hogy az elemei növekedő sorrendben legyenek.

A = X, x : X.
B = X, x′ : X.
Q_{x′} = (x = x′),
R_{x′} = (x ∈ perm(x′) ∧ ρ(x, 0, x.dom))
ρ(x, i, j) = (∀k, l(i < k < l ≤ j) : x_{k} ≤ x_{l}),
μ(x, i, j) = (∀k, l(1 ≤ k ≤ i < l ≤ j) : x_{k} ≤ x_{l})

P_{x′} = (x ∈ perm(x′) ∧ 0 ≤ k ≤ x.dom ∧ ρ(x, k, x.dom) ∧ μ(x, k, x.dom)).

k := x.dom ; k ≠ 0 ; \overline{\frac{UJSZELET}{k := m}}

P′ = (ρ(x, m, l) ∧ μ(x, m, l) ∧ m < l ∧ 1 ≤ l ≤ k ∧ P_{x′})

”UJSZELET”::=

m, l := 0, 1 ; l ≠ k ; \overline{\  x_{l+1} < x_{l}  / ; \begin{aligned}m, x_{l}, x_{l+1} := l, x_{l+1}, x_{l} \\ & SKIP \end{aligned} ; l := l + 1}

Q_{x′} ⇒ P_{x′}^{k←x.dom} = lf (k := x.dom, P_{x′})

1. P_{x′} ⇒ P_{x′}

2. P_{x′} ∧ ¬π ⇒ R miatt ¬π : k = 0, azaz π : k ≠ 0 alkalmas választás

3. P_{x′} ∧ π ⇒ t > 0 feltételhez t : k megfelelő

Alkalmas S programot kell találni, amelyre:

4. P_{x′} ∧ π ⇒ lf (S, P_{x′}) és

5. ∀t_{0} ∈ Z : P_{x′} ∧ π ∧ t ≤ t_{0} + 1 ⇒ lf (S, t ≤ t_{0})

Typeset by AMS-TEX

P′ ∧ l = k ⇒ P_{x′}^{k←m} = lf (k := m, P_{x′})

Tehát olyan S′ programot kell találni, amelyre:

P_{x′} ∧ π ⇒ lf (S′, P′ ∧ l = k). Ekkor

P_{x′} ∧ π ⇒ lf ((S′; k := m), P_{x′}) teljesül.

P_{x′} ∧ π ⇒ P′^{m,l←0,1} ⇒ lf (m, l := 0, 1, P′)

1’. P′ ⇒ P′ 2’. P′ ∧ ¬π′ ⇒ P′ ∧ l = k miatt ¬π′ : l = k, azaz π′ : l ≠ k alkalmas

választás.

3’. P′ ∧ π′ ⇒ t′ > 0 feltételhez t : k − l megfelelő.

Keressük S′-t (S′_{1}; S′_{2}) alakban, ahol S′_{2} : l := l + 1.

4’. P′∧π′ ⇒ lf (S′_{1}, P′^{l←l+1}) alapján kell S′_{1}-t meghatározni úgy, hogy l az S′_{1}-re konstans függvény legyen. Ekkor 5’ automatikusan teljesül S′_{2} választása miatt.

Könnyen belátható, hogy S′_{1} : IF(x_{l+1} < x_{l} : m, x_{l}, x_{l+1} := l, x_{l+1}, x_{l}; ¬(x_{l+1} < x_{l}) : SKIP) megfelelő választás.

Így P_{x′} ∧ π ⇒ lf ((m, l := 0, 1; DO′), P′ ∧ l = k) , ahol DO′ : DO(l ≠ k : (S′_{1}; S′_{2})). Ezért P_{x′} ∧ π ⇒ lf (((m, l := 0, 1; DO′); k := m), P_{x′}) , azaz S : ((m, l := 0, 1; DO′); k := m) választással 4. teljesül.

Ugyanakkor P′ ∧ l = k ⇒ m < k miatt ∀t_{0} ∈ Z : P_{x′} ∧ π ∧ t ≤ t_{0} + 1 ⇒ lf ((m, l := 0, 1; DO′), m < k) , de mivel a k

konstans függvény az (m, l := 0, 1; DO′) programban és t : k, ezért ∀t_{0} ∈ Z : P_{x′} ∧ π ∧ t ≤ t_{0} + 1 ⇒ lf ((m, l := 0, 1; DO′), m ≤ t_{0}) = lf ((m, l := 0, 1; DO′), (k ≤ t_{0})^{k←m}),

tehát

∀t_{0} ∈ Z : P_{x′} ∧ π ∧ t ≤ t_{0} + 1 ⇒ lf (((m, l := 0, 1; DO′); k := m), t ≤ t_{0}) , azaz S : ((m, l := 0, 1; DO′); k := m) választással 5. is teljesül.

q. e. d.