(a) Vedi testi

(b) Vedi testi

(c)

Occorre aggiungere il seguente assioma e la seguente segola di inferenza
('<>' indica "diverso da", mentre '|' rappresenta la freccia in giu', mentre su 'a' e 'b' si suppone ci sia la freccetta che indica il vettore)
                             

                                a_1 = 0
              ____________________________________________
                   a, begin for xi do delta end  | a



    a_1 <> 0  (a_1,..,a_n), begin delta end (a_1 - 1,a'_2,..,a'_n)     ((a_1 - 1), a'_2,..,a'_n), for X1 delta b
________________________________________________________________________________________________________
               (a_1,..,a_n) begin for X1 delta end  | b