Prendiamo l'assioma
__________________________________________________________________________________
{(r≥0 ∧ b>0 ∧ a=b*(q-1)+r ∧ r≥b )[(q+1)/q]} q:=(q+1) {r≥0 ∧ b>0 ∧ a=b*(q-1)+r ∧ r≥b}
che corrisponde a
__________________________________________________________________________________
{(r≥0 ∧ b>0 ∧ a=b*(q+1-1)+r ∧ r≥b) } q:=(q+1) {r≥0 ∧ b>0 ∧ a=b*(q-1)+r ∧ r≥b}
Poiche' in logica si puo' dimostrare la seguente implicazione
(r≥0 ∧ b>0 ∧ a=b*q+r ∧ r≥b) → (r≥0 ∧ b>0 ∧ a=b*(q+1-1)+r ∧ r≥b)
possiamo utilizzare la regola per il rafforzamento della precondizione ed ottenere il giudizio
(1) {r≥0 ∧ b>0 ∧ a=b*q+r ∧ r≥b } q:=(q+1) {r≥0 ∧ b>0 ∧ a=b*(q-1)+r ∧ r≥b}
Ora consideriamo l'assioma
________________________________________________________________________________________
{(r+b≥0 ∧ b>0 ∧ a=b*(q-1)+(r+b) ∧ r≥0 )[(r-b)/r]} r:=r-b {r+b≥0 ∧ b>0 ∧ a=b*(q-1)+(r+b) ∧ r≥0 )
che corrisponde a
__________________________________________________________________________________
{r-b+b≥0 ∧ b>0 ∧ a=b*(q-1)+(r-b+b) ∧ r-b≥0 } r:=r-b {r+b≥0 ∧ b>0 ∧ a=b*(q-1)+(r+b) ∧ r≥0}
Poiche' in logica si puo' dimostrare che
(r≥0 ∧ b>0 ∧ a=b*(q-1)+r ∧ r≥b) → (r-b+b≥0 ∧ b>0 ∧ a=b*(q-1)+(r-b+b) ∧ r-b≥0)
possiamo utilizzare la regola per il rafforzamento della precondizione ed ottenere il giudizio
(2) {r≥0 ∧ b>0 ∧ a=b*(q-1)+r ∧ r≥b } r:=r-b {r+b≥0 ∧ b>0 ∧ a=b*(q-1)+(r+b) ∧ r≥0}
a questo punto, usando i giudizi (1) e (2) come premesse della regola per la sequenza
di istruzioni, otteniamo
{r≥0 ∧ b>0 ∧ a=b*q+r ∧ r≥b } q:=(q+1);r:=r-b {r+b≥0 ∧ b>0 ∧ a=b*(q-1)+(r+b) ∧ r≥0}
Poiche' in logica si puo' dimostrare che
(r+b≥0 ∧ b>0 ∧ a=b*(q-1)+(r+b) ∧ r≥0) → (r≥0 ∧ b>0 ∧ a=b*q+r)
possiamo utilizzare la regola per l'indebolimento della postcondizione ed ottenere quello che
volevamo, cioe'
{r≥0 ∧ b>0 ∧ a=b*q+r ∧ r≥b } q:=(q+1);r:=r-b {r≥0 ∧ b>0 ∧ a=b*q+r}