Dobbiamo dimostrare

{a >= 0 ^ b > 0} q := 0; r := a; {r >= 0 ^ b > 0 ^ (a = b * q + r)}


Sia   A' = r >= 0 ^ b > 0 ^ (a = b * q + r)[a/r][0/q] ( = a >= 0 ^ b > 0 ^ (a = b * 0 + a) )
e sia  B = r >= 0 ^ b > 0 ^ (a = b * q + r)[a/r]


Abbiamo che il seguente e' un assioma
 
      ------------------
        {A'} q := 0 {B}

 
Inoltre, indicando 

B' = r >= 0 ^ b > 0 ^ (a = b * q + r)

il seguente e' un assioma

        ------------------
          {B} r := a {B'}


A questo punto, poiche' 
si puo' dimostrare che A -> A',
dove A = a >= 0 ^ b > 0

una dimostrazione per 

{a >= 0 ^ b > 0} q := 0; r := a; {r >= 0 ^ b > 0 ^ (a = b * q + r)}

si ottiene nel modo seguente

                     ------------------
      A -> A'          {A'} q := 0 {B}
    ------------------------------------       --------------------
               {A} q := 0 {B}                  {B} r := a {B'}
  ---------------------------------------------------------------------
    {a >= 0 ^ b > 0} q := 0; r := a; {r >= 0 ^ b > 0 ^ (a = b * q + r)}

Tale derivazione, descritta in dettaglio, e' quindi QUESTA (by S.Veneziano, file pdf).