+λdw:word32.match MSB_w32 dw with
+ [ true ⇒ succ_w32 (not_w32 dw)
+ | false ⇒ not_w32 (pred_w32 dw) ].
+
+(*
+ operatore moltiplicazione senza segno: b*b=[0x00000000,0xFFFE0001]
+ ... in pratica (〈a:b〉*〈c:d〉) = (a*c)<<16+(a*d)<<8+(b*c)<<8+(b*d)
+*)
+ndefinition mul_w16 ≝
+λw1,w2:word16.match w1 with
+[ mk_word16 b1h b1l ⇒ match w2 with
+[ mk_word16 b2h b2l ⇒ match mul_b8 b1l b2l with
+[ mk_word16 t1_h t1_l ⇒ match mul_b8 b1h b2l with
+[ mk_word16 t2_h t2_l ⇒ match mul_b8 b2h b1l with
+[ mk_word16 t3_h t3_l ⇒ match mul_b8 b1h b2h with
+[ mk_word16 t4_h t4_l ⇒
+ plus_w32_d_d
+ (plus_w32_d_d
+ (plus_w32_d_d 〈〈〈x0,x0〉:t3_h〉.〈t3_l:〈x0,x0〉〉〉 〈〈〈x0,x0〉:t2_h〉.〈t2_l:〈x0,x0〉〉〉) 〈〈t4_h:t4_l〉.〈〈x0,x0〉:〈x0,x0〉〉〉)〈〈〈x0,x0〉:〈x0,x0〉〉.〈t1_h:t1_l〉〉
+]]]]]].
+
+(* divisione senza segno (secondo la logica delle ALU): (quoziente resto) overflow *)
+nlet rec div_w16_aux (divd:word32) (divs:word32) (molt:word16) (q:word16) (c:nat) on c ≝
+ let w' ≝ plus_w32_d_d divd (compl_w32 divs) in
+ match c with
+ [ O ⇒ match le_w32 divs divd with
+ [ true ⇒ triple … (or_w16 molt q) (w32l w') (⊖ (eq_w16 (w32h w') 〈〈x0,x0〉:〈x0,x0〉〉))
+ | false ⇒ triple … q (w32l divd) (⊖ (eq_w16 (w32h divd) 〈〈x0,x0〉:〈x0,x0〉〉)) ]
+ | S c' ⇒ match le_w32 divs divd with
+ [ true ⇒ div_w16_aux w' (ror_w32 divs) (ror_w16 molt) (or_w16 molt q) c'
+ | false ⇒ div_w16_aux divd (ror_w32 divs) (ror_w16 molt) q c' ]].
+
+ndefinition div_w16 ≝
+λw:word32.λb:word16.match eq_w16 b 〈〈x0,x0〉:〈x0,x0〉〉 with
+(*
+ la combinazione n/0 e' illegale, segnala solo overflow senza dare risultato
+*)
+ [ true ⇒ triple … 〈〈xF,xF〉:〈xF,xF〉〉 (w32l w) true
+ | false ⇒ match eq_w32 w 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:〈x0,x0〉〉〉 with
+(* 0 diviso qualsiasi cosa diverso da 0 da' q=0 r=0 o=false *)
+ [ true ⇒ triple … 〈〈x0,x0〉:〈x0,x0〉〉 〈〈x0,x0〉:〈x0,x0〉〉 false
+(* 1) e' una divisione sensata che produrra' overflow/risultato *)
+(* 2) parametri: dividendo, divisore, moltiplicatore, quoziente, contatore *)
+(* 3) ad ogni ciclo il divisore e il moltiplicatore vengono scalati di 1 a dx *)
+(* 4) il moltiplicatore e' la quantita' aggiunta al quoziente se il divisore *)
+(* puo' essere sottratto al dividendo *)
+ | false ⇒ div_w16_aux w (rol_w32_n 〈〈〈x0,x0〉:〈x0,x0〉〉.b〉 nat15) 〈〈x8,x0〉:〈x0,x0〉〉 〈〈x0,x0〉:〈x0,x0〉〉 nat15 ]].
+
+(* operatore x in [inf,sup] *)