143 In natural variables s and n prove
P ⇐ if n=0 then ok else n:= n–1. s:= s+2n–n. t:= t+1. P fi
where P = sʹ′ = s + 2n – n×(n–1)/2 – 1 ∧ nʹ′=0 ∧ tʹ′ = t+n .
§ Proof by parts (3 of them) and by cases (2 of them), so 6 things to prove. First part, first case, starting with the right side:
n=0 ∧ ok expand ok = n=0 ∧ nʹ′=n ∧ sʹ′=s ∧ tʹ′=t arithmetic and specialization ⇒ sʹ′ = s + 2n – n×(n–1)/2 – 1
First part, last case:
n>0 ∧ (n:= n–1. s:= s+2n–n. t:= t+1. sʹ′ = s + 2n – n×(n–1)/2 – 1)
Substitution Law 3 times
= n>0 ∧ sʹ′ = s + 2n–1 – (n–1) + 2n–1 – (n–1)×(n–1–1)/2 – 1 arithmetic
= n>0 ∧ sʹ′ = s + 2n – n×(n–1)/2 – 1 ⇒ sʹ′ = s + 2n – n×(n–1)/2 – 1
Middle part, first case:
n=0 ∧ ok
= n=0 ∧ nʹ′=n ∧ sʹ′=s ∧ tʹ′=t ⇒ nʹ′=0
Middle part, last case:
n>0 ∧ (n:= n–1. s:= s+2n–n. t:= t+1. nʹ′=0) = n>0 ∧ nʹ′=0
⇒ nʹ′=0
Last part, first case:
n=0 ∧ ok
= n=0 ∧ nʹ′=n ∧ sʹ′=s ∧ tʹ′=t ⇒ tʹ′=t+n
Last part, last case:
n>0 ∧ (n:= n–1. s:= s+2n–n. t:= t+1. tʹ′ = t+n) = n>0 ∧ tʹ′ = t+1+n–1
⇒ tʹ′=t+n
specialization
expand ok transitivity and specialization
Substitution Law 3 times specialization
expand ok arithmetic and specialization
Substitution Law 3 times arithmetic and specialization