Occorre aggiungere il seguente assioma e le seguenti regole di inferenza. (rappresentiamo con a la 'a' sormontata dalla freccetta che indica il vettore)


a1 = 0
____________________________________________
a, begin for X1 do δ end ⇓ a



a1 ≠ 0        (a1,..,an), begin δ end ⇓ (a1 ,a'2,..,a'n)        ((a1 - 1), a2',..,an'),begin for X1 δ end ⇓ b
________________________________________________________________________________________________________
(a1,..,an) begin for X1 δ end ⇓ b



a1 ≠ 0       a1 ≠ a1'       (a1,..,a1), begin δ end ⇓ (a'1,a'2,..,a1')        (a'1 , a'2,..,a'n), begin for X1 δ end ⇓ b
________________________________________________________________________________________________________
(a1,..,an), begin for X1 δ end ⇓ b