+(* divisione senza segno (secondo la logica delle ALU): (quoziente resto) overflow *)
+nlet rec div_b8_ex_aux (divd:byte8) (divs:byte8) (molt:exadecim) (q:exadecim) (n:nat) on n ≝
+ let w' ≝ plus_b8_d_d divd (compl_b8 divs) in
+ match n with
+ [ O ⇒ match le_b8 divs divd with
+ [ true ⇒ triple … (or_ex molt q) (cnL ? w') (⊖ (eq_ex (cnH ? w') x0))
+ | false ⇒ triple … q (cnL ? divd) (⊖ (eq_ex (cnH ? divd) x0)) ]
+ | S n' ⇒ match le_b8 divs divd with
+ [ true ⇒ div_b8_ex_aux w' (ror_b8 divs) (ror_ex molt) (or_ex molt q) n'
+ | false ⇒ div_b8_ex_aux divd (ror_b8 divs) (ror_ex molt) q n' ]].
+
+ndefinition div_b8_ex ≝
+λb:byte8.λe:exadecim.match eq_ex e x0 with
+(* la combinazione n/0 e' illegale, segnala solo overflow senza dare risultato *)
+ [ true ⇒ triple … xF (cnL ? b) true
+ | false ⇒ match eq_b8 b 〈x0,x0〉 with
+(* 0 diviso qualsiasi cosa diverso da 0 da' q=0 r=0 o=false *)
+ [ true ⇒ triple … 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_b8_ex_aux b (nat_it ? rol_b8 〈x0,e〉 nat3) x8 x0 nat3 ]].