A tétel direkt levezetése

\begin{matrix}A : & Σ & × & ℕ_{0} & × & 𝕃 & × & 𝕃 \\ i & m & u & l \end{matrix}

\begin{matrix}B : & \{(0, . & .., 0)\} & × & \{(σ_{1} − 1, . & .., σ_{n} − 1)\} \\ i′_{1} & i′_{2} \end{matrix}

Q : (T RUE)

R : ((u ↔ ∃j ∈ [i′_{1}..i′_{2}] : \overline{ρ}(j)) ∧
∧ (u → (i ∈ [i′_{1}..i′_{2}] ∧ \overline{ρ}(i) ∧ ∀j ∈ [i′_{1}..i) : ¬\overline{ρ}(j))))

Legyen

P :(i ∈ [i′_{1}..i′_{2}] ∧ (∀j ∈ [i′_{1}..i) : ¬\overline{ρ}(j)) ∧

∧ (u ↔ ∃j ∈ [i′_{1}..i] : \overline{ρ}(j)) ∧ ∧ m ∈ [1..n] ∧

∧ (¬u → (i ≠ i′_{2} → (∀k ∈ [1..m) : \overline{ρ}_{k}(i) ∧ ¬\overline{ρ}_{m}(i) ∧ ∀k ∈ [m + 1..n] : i_{k} = 0))) ∧

∧ (u → (m = n ∧ ∀k ∈ [1..n] : \overline{ρ}_{k}(i))))

1. Q ⇏ P ugyanakkor Q ⇒ lf(i := (0, ..., 0), i = (0, ..., 0)) Könnyen látható, hogy i = (0, ..., 0) ⇏ P. Keresni kell olyan S programot, amelyre i = (0, ..., 0) ⇒ lf(S, P). Legyen

P′ : (i = (0, ..., 0) ∧ m ∈ [0..n] ∧ ∀k ∈ [1..m) : \overline{ρ}_{k}(i) ∧
∧ (u ↔ ∀k ∈ [1..m] : \overline{ρ}_{k}(i)))

1’. i = (0, ..., 0) ⇒ P′^{m,u←0,↑}. 2’. P′ ∧ ¬π ⇒ P teljesül, ha ¬π : ¬u ∨ m ≥ n.

Tehát π : u ∧ m < n alkalmas választás.

Typeset by A_{M}S-TEX 3’. P′ ∧ π ⇒ t > 0 teljesül, ha t : n − m.

4’. P′ ∧ π ⇒ P′^{u←\overline{ρ}_{m+1}(i)} ⇔ lf(S_{1}, P′^{m←m+1})

ahol S_{1} : u := \overline{ρ}_{m+1}(i), Mindebből már könnyen belátható, hogy

Q ⇒ lf((i := (0, ..., 0); (m, u := 0, ↑; DO(u∧m < n : (u := \overline{ρ}_{m+1}(i); m := m+1)))), P)

2. P ∧ ¬π ⇒ R ha ¬π : u ∨ i = (σ_{1} − 1, ..., σ_{n} − 1). Tehát π : ¬u ∧ i ≠ (σ_{1} − 1, ..., σ_{n} − 1) alkalmas választás.

3. P ∧ π ⇒ t > 0 teljesül, ha t : |(i..i′_{2}]|.

4. Igazolni kell, hogy P ∧ π ⇒ lf(S_{1}, P′′), illetve P′′ ⇒ lf(S_{2}, P), ahol

P′′ : (i ∈[i′_{1}..i′_{2}] ∧ (∀j ∈ [i′_{1}..i) : ¬\overline{ρ}(j)) ∧
∧ m ∈ [1..n] ∧
∧ ∀k ∈ [1..m) : \overline{ρ}_{k}(i) ∧
∧ (i ≠ i′_{2} → ∀k ∈ [m + 1..n] : i_{k} = 0))

Legyen

\overline{P} : (i ∈[i′_{1}..i′_{2}] ∧ (∀j ∈ [i′_{1}..i) : ¬\overline{ρ}(j)) ∧
∧ m ∈ [1..n] ∧
∧ ∀k ∈ [1..m) : \overline{ρ}_{k}(i) ∧
∧ (u ↔ ∀k ∈ [1..m] : \overline{ρ}_{k}(i) ∧
∧ (¬u → (i ≠ i′_{2} → ∀k ∈ [m + 1..n] : i_{k} = 0)))

1’. P′′ ⇒ \overline{P}^{m,u←m−1,↑} 2’. \overline{P} ∧ ¬\overline{π} ⇒ P ha ¬\overline{π} : ¬u ∨ m ≥ n

tehát \overline{π} : u ∧ m < n alkalmas választás. 3’. \overline{P} ∧ \overline{π} ⇒ t > 0 teljesül, ha t : n − m.

4’. \overline{P} ∧ \overline{π} ⇒ lf(S_{1}, \overline{P}^{m←m+1}) teljesül, ha S_{1} : u := \overline{ρ}_{m+1}(i),

ugyanis \overline{P} ∧ \overline{π} ⇒ \overline{P}^{m←m+1}^{u←\overline{ρ}_{m+1}}. Tehát

P′′ ⇒ lf((m, u ← m − 1, ↑; DO(u ∧ m < n, (u := \overline{ρ}_{m+1}; m := m + 1))), P)

Könnyen látható, hogy P ∧ π ∧ [i_{1,..,m}] = (σ_{1} − 1, ..., σ_{m} − 1) ⇒ P′′^{i←(σ_{1}−1,...,σ_{n}−1)}, tehát P ∧ π ∧ [i_{1,..,m}] = (σ_{1} − 1, ..., σ_{m} − 1) ⇒ lf(i := (σ_{1} − 1, ..., σ_{n} − 1) , P′′). Legyen

\overline{\overline{P}} : (i ∈[i′_{1}..i′_{2}] ∧ m ∈ [1..n] ∧
∧ ∀k ∈ (m, n] : i_{k} = 0 ∧
∧ ∃k ∈ [1..m] : i_{m} ≠ σ_{m} − 1 ∧
∧ (l ↔ ∃k ∈ [m..n] : i_{k} ≠ 0) ∧
∧ (l → ∀k ∈ [1..m) : \overline{ρ}_{k}(i)) ∧
∧ (¬l → ∀k ∈ [1..m − 1) : \overline{ρ}_{k}(i)) ∧
∧ (l → ∀j ∈ [i′_{1}..(i_{1}, ...i_{m}, 0, ..., 0)) : ¬\overline{ρ}(j)) ∧
∧ (¬l ↔ ∀j ∈ [i′_{1}..([i_{1,...m}]^{+}, 0, ..., 0)) : ¬\overline{ρ}(j)))

1’. P ∧ π ∧ [i_{1,..,m}] ≠ (σ_{1} − 1, ..., σ_{m} − 1) ⇒ \overline{\overline{P}}^{m,l←m+1,↓} 2’. \overline{\overline{P}} ∧ ¬\overline{\overline{π}} ⇒ P′′, ha \overline{\overline{π}} : l. 3’. \overline{\overline{P}} ∧ \overline{\overline{π}} ⇒ t > 0 teljesül, ha t : m 4’. \overline{\overline{P}} ∧ \overline{\overline{π}} ∧ i_{m−1} = σ_{m−1} ⇒ \overline{\overline{P}}^{m←m−1}^{i_{m−1}←0},

hasonlóan

\overline{\overline{P}} ∧ \overline{\overline{π}} ∧ i_{m−1} ≠ σ_{m−1} ⇒ \overline{\overline{P}}^{m←m−1}^{i_{m−1},l←i_{m−1}−1,↑}. Tehát P ∧ π ∧ [i_{1,..,m}] ≠ (σ_{1} − 1, ..., σ_{m} − 1) ⇒

lf((m, l := m + 1, ↓; DO(¬l, (IF(i_{m−1} = σ_{m−1} − 1 : i_{m−1} := 0, i_{m−1} ≠ σ_{m−1} − 1 : i_{m−1}, l := i_{m−1} + 1, ↑); m := m − 1))) , P′′).

Mindezekből már következik, hogy a származtatott program valóban megoldása a feladatnak.