A feladat specifikációja:

Legyen 𝕏 : vekt(ℕ, {0, 1, 2, ..., 9}).

A ={ℕ_{0} \atop n}×ℕ s×𝕏 x

B ={ℕ \atop n′}

Q : (n = n′)

R : (n′ = ∑_{j=x.lob}^{x.hib} x[j] · 10^{(x.hib−j)} ∧ s = szjsz(n′) ∧ n′ = x.dom)

Keressük a megoldást adó programot ciklus formában, ahol

P : (s ∈ [0..x.dom] ∧ n′ = x.dom ∧

∧ n′ = ( ∑_{x.hib−s+1}^{x.hib} x[j] · 10^{(x.hib−j)}) + n · 10^{s} ∧ ∀j ∈ [x.lob..x.hib − s] : x[j] = 0 ∧

∧ n > 0 → szjsz(n′) = szjsz(n) + s ∧ n = 0 → szjsz(n′) = s)

1. Q ⇏ P, de Q ⇒ P^{s,x←0,(1,<0_{1},0_{2},....,0_{n}>)}. Innen adódik, hogy Q ⇒ lf(s, x := 0, (1, < 0_{1}, 0_{2}, ...., 0_{n} >), P)

2. A ciklus levezetési szabálya második feltétele: P ∧ ¬π ⇒ R teljesül, ha ¬π : (n = 0). Ezért π : (n > 0) alkalmas választás.

3. A ciklus levezetési szabálya harmadik feltétele: P ∧ π ⇒ t > 0 teljesül, ha t : n a π választása miatt.

4. és 5. Belátható, hogy P ∧ n > 0 ⇒ ((s + 1) ∈ [0..x.dom] ∧ n′ = x.dom ∧

∧ n′ = (n mod 10) · 10^{s} + ( ∑_{x.hib−s+1}^{x.hib} x[j] · 10^{(x.hib−j)}) + (n div 10) · 10^{(s+1)} ∧

∧ ∀j ∈ [x.lob..x.hib − (s + 1)] : x[j] = 0 ∧ ∧ (n div 10) > 0 → szjsz(n′) = szjsz((n div 10)) + (s + 1) ∧ ∧ (n div 10) = 0 → szjsz(n′) = (s + 1)) ezért P ∧ π ⇒ P^{n,s,x[x.hib−s]←(n div 10),s+1,(n mod 10)}) Innen adódik, hogy P ∧ π ⇒ lf(n, s, x[x.hib − s] := (n div 10), s + 1, (n mod 10), P)

Egy lehetséges megoldás tehát a következő program:

s, x := 0, (1, < 0_{1}, 0_{2}, ...., 0_{n} >) ; n > 0 ; \overline{n, s, x[x.hib − s] := (n div 10), s + 1, (n mod 10)}

Legyen 𝕏 : fun(ℕ, {0, 1, 2, ..., 9}).

A ={ℕ_{0} \atop n}×ℕ s×𝕏 x

B ={ℕ \atop n′}

Q : (n = n′)

R : (n′ = ∑_{j=x.lob}^{x.hib} x[j] · 10^{(x.hib−j)} ∧ x[x.lob] ≠ 0 ∧ s = szjsz(n′))

Keressük a megoldást adó programot ciklus formában, ahol

P : (n′ = ( ∑_{x.lob}^{x.hib} x[j] · 10^{(x.hib−j)}) + n · 10^{(x.hib−x.lob+1)} ∧ s = x.hib − x.lob + 1 ∧

∧ n > 0 → szjsz(n′) = szjsz(n) + s ∧ n = 0 → szjsz(n′) = s)

1. Q ⇏ P, de Q ⇒ P^{s,x←0,(n,<>)}.

Innen adódik, hogy Q ⇒ lf(s, x := 0, (n, <>), P)

2. A ciklus levezetési szabálya második feltétele: P ∧ ¬π ⇒ R teljesül, ha ¬π : (n = 0). Ezért π : (n > 0) alkalmas választás.

3. A ciklus levezetési szabálya harmadik feltétele: P ∧ π ⇒ t > 0 teljesül, ha t : n a π választása miatt.

4. és 5. Belátható, hogy P ∧ n > 0 ⇒

(n′ = (n mod 10) · 10^{(x.hib−(x.lob−1))} + ( ∑_{x.lob}^{x.hib} x[j] · 10^{(x.hib−j)}) +

+ (n div 10) · 10^{(x.hib−(x.lob−1)+1)} ∧ ∧ (s + 1) = x.hib − (x.lob − 1) + 1 = 0 ∧ ∧ (n div 10) > 0 → szjsz(n′) = szjsz((n div 10)) + (s + 1) ∧ ∧ (n div 10) = 0 → szjsz(n′) = (s + 1)) ezért P ∧ π ⇒ P^{n,s,x←(n div 10),s+1,x:loext((n mod 10))})

Innen adódik, hogy P ∧ π ⇒ lf(n, s, x := (n div 10), s + 1, x : loext((n mod 10)), P)

Egy lehetséges megoldás tehát a következő program:

s, x := 0, (n, <>) ; n > 0 ; \overline{n, s, x := (n div 10), s + 1, x : loext((n mod 10))}