(no commit message)

[helm.git] / helm / software / matita / contribs / ng_assembly / freescale / exadecim.ma

diff --git a/helm/software/matita/contribs/ng_assembly/freescale/exadecim.ma b/helm/software/matita/contribs/ng_assembly/freescale/exadecim.ma
index 16fb11a16ecfe5b4aa95770aae28b263723899c1..a87cf99d2629956686cb41bb2d674b1fbd39a383 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/freescale/exadecim.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/exadecim.ma
@@ -871,601 +871,578 @@ ndefinition not_ex ≝
  | x8 ⇒ x7 | x9 ⇒ x6 | xA ⇒ x5 | xB ⇒ x4
  | xC ⇒ x3 | xD ⇒ x2 | xE ⇒ x1 | xF ⇒ x0 ].
 
-(* operatore somma con carry *)
-ndefinition plus_ex ≝
+(* operatore somma con data+carry → data+carry *)
+ndefinition plus_ex_dc_dc ≝
 λe1,e2:exadecim.λc:bool.
-  match c with
-   [ true ⇒
-      match e1 with
-       [ x0 ⇒
-           match e2 with
-            [ x0 ⇒ pair exadecim bool x1 false
-            | x1 ⇒ pair exadecim bool x2 false
-            | x2 ⇒ pair exadecim bool x3 false
-            | x3 ⇒ pair exadecim bool x4 false
-            | x4 ⇒ pair exadecim bool x5 false
-            | x5 ⇒ pair exadecim bool x6 false
-            | x6 ⇒ pair exadecim bool x7 false
-            | x7 ⇒ pair exadecim bool x8 false
-            | x8 ⇒ pair exadecim bool x9 false
-            | x9 ⇒ pair exadecim bool xA false
-            | xA ⇒ pair exadecim bool xB false
-            | xB ⇒ pair exadecim bool xC false
-            | xC ⇒ pair exadecim bool xD false
-            | xD ⇒ pair exadecim bool xE false
-            | xE ⇒ pair exadecim bool xF false
-            | xF ⇒ pair exadecim bool x0 true ] 
-       | x1 ⇒
-           match e2 with
-            [ x0 ⇒ pair exadecim bool x2 false
-            | x1 ⇒ pair exadecim bool x3 false
-            | x2 ⇒ pair exadecim bool x4 false
-            | x3 ⇒ pair exadecim bool x5 false
-            | x4 ⇒ pair exadecim bool x6 false
-            | x5 ⇒ pair exadecim bool x7 false
-            | x6 ⇒ pair exadecim bool x8 false
-            | x7 ⇒ pair exadecim bool x9 false
-            | x8 ⇒ pair exadecim bool xA false
-            | x9 ⇒ pair exadecim bool xB false
-            | xA ⇒ pair exadecim bool xC false
-            | xB ⇒ pair exadecim bool xD false
-            | xC ⇒ pair exadecim bool xE false
-            | xD ⇒ pair exadecim bool xF false
-            | xE ⇒ pair exadecim bool x0 true
-            | xF ⇒ pair exadecim bool x1 true ] 
-       | x2 ⇒
-           match e2 with
-            [ x0 ⇒ pair exadecim bool x3 false
-            | x1 ⇒ pair exadecim bool x4 false
-            | x2 ⇒ pair exadecim bool x5 false
-            | x3 ⇒ pair exadecim bool x6 false
-            | x4 ⇒ pair exadecim bool x7 false
-            | x5 ⇒ pair exadecim bool x8 false
-            | x6 ⇒ pair exadecim bool x9 false
-            | x7 ⇒ pair exadecim bool xA false
-            | x8 ⇒ pair exadecim bool xB false
-            | x9 ⇒ pair exadecim bool xC false
-            | xA ⇒ pair exadecim bool xD false
-            | xB ⇒ pair exadecim bool xE false
-            | xC ⇒ pair exadecim bool xF false
-            | xD ⇒ pair exadecim bool x0 true
-            | xE ⇒ pair exadecim bool x1 true
-            | xF ⇒ pair exadecim bool x2 true ] 
-       | x3 ⇒
-           match e2 with
-            [ x0 ⇒ pair exadecim bool x4 false
-            | x1 ⇒ pair exadecim bool x5 false
-            | x2 ⇒ pair exadecim bool x6 false
-            | x3 ⇒ pair exadecim bool x7 false
-            | x4 ⇒ pair exadecim bool x8 false
-            | x5 ⇒ pair exadecim bool x9 false
-            | x6 ⇒ pair exadecim bool xA false
-            | x7 ⇒ pair exadecim bool xB false
-            | x8 ⇒ pair exadecim bool xC false
-            | x9 ⇒ pair exadecim bool xD false
-            | xA ⇒ pair exadecim bool xE false
-            | xB ⇒ pair exadecim bool xF false
-            | xC ⇒ pair exadecim bool x0 true
-            | xD ⇒ pair exadecim bool x1 true
-            | xE ⇒ pair exadecim bool x2 true
-            | xF ⇒ pair exadecim bool x3 true ] 
-       | x4 ⇒
-           match e2 with
-            [ x0 ⇒ pair exadecim bool x5 false
-            | x1 ⇒ pair exadecim bool x6 false
-            | x2 ⇒ pair exadecim bool x7 false
-            | x3 ⇒ pair exadecim bool x8 false
-            | x4 ⇒ pair exadecim bool x9 false
-            | x5 ⇒ pair exadecim bool xA false
-            | x6 ⇒ pair exadecim bool xB false
-            | x7 ⇒ pair exadecim bool xC false
-            | x8 ⇒ pair exadecim bool xD false
-            | x9 ⇒ pair exadecim bool xE false
-            | xA ⇒ pair exadecim bool xF false
-            | xB ⇒ pair exadecim bool x0 true
-            | xC ⇒ pair exadecim bool x1 true
-            | xD ⇒ pair exadecim bool x2 true
-            | xE ⇒ pair exadecim bool x3 true
-            | xF ⇒ pair exadecim bool x4 true ] 
-       | x5 ⇒
-           match e2 with
-            [ x0 ⇒ pair exadecim bool x6 false
-            | x1 ⇒ pair exadecim bool x7 false
-            | x2 ⇒ pair exadecim bool x8 false
-            | x3 ⇒ pair exadecim bool x9 false
-            | x4 ⇒ pair exadecim bool xA false
-            | x5 ⇒ pair exadecim bool xB false
-            | x6 ⇒ pair exadecim bool xC false
-            | x7 ⇒ pair exadecim bool xD false
-            | x8 ⇒ pair exadecim bool xE false
-            | x9 ⇒ pair exadecim bool xF false
-            | xA ⇒ pair exadecim bool x0 true
-            | xB ⇒ pair exadecim bool x1 true
-            | xC ⇒ pair exadecim bool x2 true
-            | xD ⇒ pair exadecim bool x3 true
-            | xE ⇒ pair exadecim bool x4 true
-            | xF ⇒ pair exadecim bool x5 true ] 
-       | x6 ⇒
-           match e2 with
-            [ x0 ⇒ pair exadecim bool x7 false
-            | x1 ⇒ pair exadecim bool x8 false
-            | x2 ⇒ pair exadecim bool x9 false
-            | x3 ⇒ pair exadecim bool xA false
-            | x4 ⇒ pair exadecim bool xB false
-            | x5 ⇒ pair exadecim bool xC false
-            | x6 ⇒ pair exadecim bool xD false
-            | x7 ⇒ pair exadecim bool xE false
-            | x8 ⇒ pair exadecim bool xF false
-            | x9 ⇒ pair exadecim bool x0 true
-            | xA ⇒ pair exadecim bool x1 true
-            | xB ⇒ pair exadecim bool x2 true
-            | xC ⇒ pair exadecim bool x3 true
-            | xD ⇒ pair exadecim bool x4 true
-            | xE ⇒ pair exadecim bool x5 true
-            | xF ⇒ pair exadecim bool x6 true ] 
-       | x7 ⇒
-           match e2 with
-            [ x0 ⇒ pair exadecim bool x8 false
-            | x1 ⇒ pair exadecim bool x9 false
-            | x2 ⇒ pair exadecim bool xA false
-            | x3 ⇒ pair exadecim bool xB false
-            | x4 ⇒ pair exadecim bool xC false
-            | x5 ⇒ pair exadecim bool xD false
-            | x6 ⇒ pair exadecim bool xE false
-            | x7 ⇒ pair exadecim bool xF false
-            | x8 ⇒ pair exadecim bool x0 true
-            | x9 ⇒ pair exadecim bool x1 true
-            | xA ⇒ pair exadecim bool x2 true
-            | xB ⇒ pair exadecim bool x3 true
-            | xC ⇒ pair exadecim bool x4 true
-            | xD ⇒ pair exadecim bool x5 true
-            | xE ⇒ pair exadecim bool x6 true
-            | xF ⇒ pair exadecim bool x7 true ] 
-       | x8 ⇒
-           match e2 with
-            [ x0 ⇒ pair exadecim bool x9 false
-            | x1 ⇒ pair exadecim bool xA false
-            | x2 ⇒ pair exadecim bool xB false
-            | x3 ⇒ pair exadecim bool xC false
-            | x4 ⇒ pair exadecim bool xD false
-            | x5 ⇒ pair exadecim bool xE false
-            | x6 ⇒ pair exadecim bool xF false
-            | x7 ⇒ pair exadecim bool x0 true
-            | x8 ⇒ pair exadecim bool x1 true
-            | x9 ⇒ pair exadecim bool x2 true
-            | xA ⇒ pair exadecim bool x3 true
-            | xB ⇒ pair exadecim bool x4 true
-            | xC ⇒ pair exadecim bool x5 true
-            | xD ⇒ pair exadecim bool x6 true
-            | xE ⇒ pair exadecim bool x7 true
-            | xF ⇒ pair exadecim bool x8 true ] 
-       | x9 ⇒
-           match e2 with
-            [ x0 ⇒ pair exadecim bool xA false
-            | x1 ⇒ pair exadecim bool xB false
-            | x2 ⇒ pair exadecim bool xC false
-            | x3 ⇒ pair exadecim bool xD false
-            | x4 ⇒ pair exadecim bool xE false
-            | x5 ⇒ pair exadecim bool xF false
-            | x6 ⇒ pair exadecim bool x0 true
-            | x7 ⇒ pair exadecim bool x1 true
-            | x8 ⇒ pair exadecim bool x2 true
-            | x9 ⇒ pair exadecim bool x3 true
-            | xA ⇒ pair exadecim bool x4 true
-            | xB ⇒ pair exadecim bool x5 true
-            | xC ⇒ pair exadecim bool x6 true
-            | xD ⇒ pair exadecim bool x7 true
-            | xE ⇒ pair exadecim bool x8 true
-            | xF ⇒ pair exadecim bool x9 true ] 
-       | xA ⇒
-           match e2 with
-            [ x0 ⇒ pair exadecim bool xB false
-            | x1 ⇒ pair exadecim bool xC false
-            | x2 ⇒ pair exadecim bool xD false
-            | x3 ⇒ pair exadecim bool xE false
-            | x4 ⇒ pair exadecim bool xF false
-            | x5 ⇒ pair exadecim bool x0 true
-            | x6 ⇒ pair exadecim bool x1 true
-            | x7 ⇒ pair exadecim bool x2 true
-            | x8 ⇒ pair exadecim bool x3 true
-            | x9 ⇒ pair exadecim bool x4 true
-            | xA ⇒ pair exadecim bool x5 true
-            | xB ⇒ pair exadecim bool x6 true
-            | xC ⇒ pair exadecim bool x7 true
-            | xD ⇒ pair exadecim bool x8 true
-            | xE ⇒ pair exadecim bool x9 true
-            | xF ⇒ pair exadecim bool xA true ] 
-       | xB ⇒
-           match e2 with
-            [ x0 ⇒ pair exadecim bool xC false
-            | x1 ⇒ pair exadecim bool xD false
-            | x2 ⇒ pair exadecim bool xE false
-            | x3 ⇒ pair exadecim bool xF false
-            | x4 ⇒ pair exadecim bool x0 true
-            | x5 ⇒ pair exadecim bool x1 true
-            | x6 ⇒ pair exadecim bool x2 true
-            | x7 ⇒ pair exadecim bool x3 true
-            | x8 ⇒ pair exadecim bool x4 true
-            | x9 ⇒ pair exadecim bool x5 true
-            | xA ⇒ pair exadecim bool x6 true
-            | xB ⇒ pair exadecim bool x7 true
-            | xC ⇒ pair exadecim bool x8 true
-            | xD ⇒ pair exadecim bool x9 true
-            | xE ⇒ pair exadecim bool xA true
-            | xF ⇒ pair exadecim bool xB true ] 
-       | xC ⇒
-           match e2 with
-            [ x0 ⇒ pair exadecim bool xD false
-            | x1 ⇒ pair exadecim bool xE false
-            | x2 ⇒ pair exadecim bool xF false
-            | x3 ⇒ pair exadecim bool x0 true
-            | x4 ⇒ pair exadecim bool x1 true
-            | x5 ⇒ pair exadecim bool x2 true
-            | x6 ⇒ pair exadecim bool x3 true
-            | x7 ⇒ pair exadecim bool x4 true
-            | x8 ⇒ pair exadecim bool x5 true
-            | x9 ⇒ pair exadecim bool x6 true
-            | xA ⇒ pair exadecim bool x7 true
-            | xB ⇒ pair exadecim bool x8 true
-            | xC ⇒ pair exadecim bool x9 true
-            | xD ⇒ pair exadecim bool xA true
-            | xE ⇒ pair exadecim bool xB true
-            | xF ⇒ pair exadecim bool xC true ] 
-       | xD ⇒
-           match e2 with
-            [ x0 ⇒ pair exadecim bool xE false
-            | x1 ⇒ pair exadecim bool xF false
-            | x2 ⇒ pair exadecim bool x0 true
-            | x3 ⇒ pair exadecim bool x1 true
-            | x4 ⇒ pair exadecim bool x2 true
-            | x5 ⇒ pair exadecim bool x3 true
-            | x6 ⇒ pair exadecim bool x4 true
-            | x7 ⇒ pair exadecim bool x5 true
-            | x8 ⇒ pair exadecim bool x6 true
-            | x9 ⇒ pair exadecim bool x7 true
-            | xA ⇒ pair exadecim bool x8 true
-            | xB ⇒ pair exadecim bool x9 true
-            | xC ⇒ pair exadecim bool xA true
-            | xD ⇒ pair exadecim bool xB true
-            | xE ⇒ pair exadecim bool xC true
-            | xF ⇒ pair exadecim bool xD true ] 
-       | xE ⇒
-           match e2 with
-            [ x0 ⇒ pair exadecim bool xF false
-            | x1 ⇒ pair exadecim bool x0 true
-            | x2 ⇒ pair exadecim bool x1 true
-            | x3 ⇒ pair exadecim bool x2 true
-            | x4 ⇒ pair exadecim bool x3 true
-            | x5 ⇒ pair exadecim bool x4 true
-            | x6 ⇒ pair exadecim bool x5 true
-            | x7 ⇒ pair exadecim bool x6 true
-            | x8 ⇒ pair exadecim bool x7 true
-            | x9 ⇒ pair exadecim bool x8 true
-            | xA ⇒ pair exadecim bool x9 true
-            | xB ⇒ pair exadecim bool xA true
-            | xC ⇒ pair exadecim bool xB true
-            | xD ⇒ pair exadecim bool xC true
-            | xE ⇒ pair exadecim bool xD true
-            | xF ⇒ pair exadecim bool xE true ]
-       | xF ⇒
-           match e2 with
-            [ x0 ⇒ pair exadecim bool x0 true
-            | x1 ⇒ pair exadecim bool x1 true
-            | x2 ⇒ pair exadecim bool x2 true
-            | x3 ⇒ pair exadecim bool x3 true
-            | x4 ⇒ pair exadecim bool x4 true
-            | x5 ⇒ pair exadecim bool x5 true
-            | x6 ⇒ pair exadecim bool x6 true
-            | x7 ⇒ pair exadecim bool x7 true
-            | x8 ⇒ pair exadecim bool x8 true
-            | x9 ⇒ pair exadecim bool x9 true
-            | xA ⇒ pair exadecim bool xA true
-            | xB ⇒ pair exadecim bool xB true
-            | xC ⇒ pair exadecim bool xC true
-            | xD ⇒ pair exadecim bool xD true
-            | xE ⇒ pair exadecim bool xE true
-            | xF ⇒ pair exadecim bool xF true ] 
-       ]
-   | false ⇒
-      match e1 with
-       [ x0 ⇒
-           match e2 with
-            [ x0 ⇒ pair exadecim bool x0 false
-            | x1 ⇒ pair exadecim bool x1 false
-            | x2 ⇒ pair exadecim bool x2 false
-            | x3 ⇒ pair exadecim bool x3 false
-            | x4 ⇒ pair exadecim bool x4 false
-            | x5 ⇒ pair exadecim bool x5 false
-            | x6 ⇒ pair exadecim bool x6 false
-            | x7 ⇒ pair exadecim bool x7 false
-            | x8 ⇒ pair exadecim bool x8 false
-            | x9 ⇒ pair exadecim bool x9 false
-            | xA ⇒ pair exadecim bool xA false
-            | xB ⇒ pair exadecim bool xB false
-            | xC ⇒ pair exadecim bool xC false
-            | xD ⇒ pair exadecim bool xD false
-            | xE ⇒ pair exadecim bool xE false
-            | xF ⇒ pair exadecim bool xF false ] 
-       | x1 ⇒
-           match e2 with
-            [ x0 ⇒ pair exadecim bool x1 false
-            | x1 ⇒ pair exadecim bool x2 false
-            | x2 ⇒ pair exadecim bool x3 false
-            | x3 ⇒ pair exadecim bool x4 false
-            | x4 ⇒ pair exadecim bool x5 false
-            | x5 ⇒ pair exadecim bool x6 false
-            | x6 ⇒ pair exadecim bool x7 false
-            | x7 ⇒ pair exadecim bool x8 false
-            | x8 ⇒ pair exadecim bool x9 false
-            | x9 ⇒ pair exadecim bool xA false
-            | xA ⇒ pair exadecim bool xB false
-            | xB ⇒ pair exadecim bool xC false
-            | xC ⇒ pair exadecim bool xD false
-            | xD ⇒ pair exadecim bool xE false
-            | xE ⇒ pair exadecim bool xF false
-            | xF ⇒ pair exadecim bool x0 true ] 
-       | x2 ⇒
-           match e2 with
-            [ x0 ⇒ pair exadecim bool x2 false
-            | x1 ⇒ pair exadecim bool x3 false
-            | x2 ⇒ pair exadecim bool x4 false
-            | x3 ⇒ pair exadecim bool x5 false
-            | x4 ⇒ pair exadecim bool x6 false
-            | x5 ⇒ pair exadecim bool x7 false
-            | x6 ⇒ pair exadecim bool x8 false
-            | x7 ⇒ pair exadecim bool x9 false
-            | x8 ⇒ pair exadecim bool xA false
-            | x9 ⇒ pair exadecim bool xB false
-            | xA ⇒ pair exadecim bool xC false
-            | xB ⇒ pair exadecim bool xD false
-            | xC ⇒ pair exadecim bool xE false
-            | xD ⇒ pair exadecim bool xF false
-            | xE ⇒ pair exadecim bool x0 true
-            | xF ⇒ pair exadecim bool x1 true ] 
-       | x3 ⇒
-           match e2 with
-            [ x0 ⇒ pair exadecim bool x3 false
-            | x1 ⇒ pair exadecim bool x4 false
-            | x2 ⇒ pair exadecim bool x5 false
-            | x3 ⇒ pair exadecim bool x6 false
-            | x4 ⇒ pair exadecim bool x7 false
-            | x5 ⇒ pair exadecim bool x8 false
-            | x6 ⇒ pair exadecim bool x9 false
-            | x7 ⇒ pair exadecim bool xA false
-            | x8 ⇒ pair exadecim bool xB false
-            | x9 ⇒ pair exadecim bool xC false
-            | xA ⇒ pair exadecim bool xD false
-            | xB ⇒ pair exadecim bool xE false
-            | xC ⇒ pair exadecim bool xF false
-            | xD ⇒ pair exadecim bool x0 true
-            | xE ⇒ pair exadecim bool x1 true
-            | xF ⇒ pair exadecim bool x2 true ] 
-       | x4 ⇒
-           match e2 with
-            [ x0 ⇒ pair exadecim bool x4 false
-            | x1 ⇒ pair exadecim bool x5 false
-            | x2 ⇒ pair exadecim bool x6 false
-            | x3 ⇒ pair exadecim bool x7 false
-            | x4 ⇒ pair exadecim bool x8 false
-            | x5 ⇒ pair exadecim bool x9 false
-            | x6 ⇒ pair exadecim bool xA false
-            | x7 ⇒ pair exadecim bool xB false
-            | x8 ⇒ pair exadecim bool xC false
-            | x9 ⇒ pair exadecim bool xD false
-            | xA ⇒ pair exadecim bool xE false
-            | xB ⇒ pair exadecim bool xF false
-            | xC ⇒ pair exadecim bool x0 true
-            | xD ⇒ pair exadecim bool x1 true
-            | xE ⇒ pair exadecim bool x2 true
-            | xF ⇒ pair exadecim bool x3 true ] 
-       | x5 ⇒
-           match e2 with
-            [ x0 ⇒ pair exadecim bool x5 false
-            | x1 ⇒ pair exadecim bool x6 false
-            | x2 ⇒ pair exadecim bool x7 false
-            | x3 ⇒ pair exadecim bool x8 false
-            | x4 ⇒ pair exadecim bool x9 false
-            | x5 ⇒ pair exadecim bool xA false
-            | x6 ⇒ pair exadecim bool xB false
-            | x7 ⇒ pair exadecim bool xC false
-            | x8 ⇒ pair exadecim bool xD false
-            | x9 ⇒ pair exadecim bool xE false
-            | xA ⇒ pair exadecim bool xF false
-            | xB ⇒ pair exadecim bool x0 true
-            | xC ⇒ pair exadecim bool x1 true
-            | xD ⇒ pair exadecim bool x2 true
-            | xE ⇒ pair exadecim bool x3 true
-            | xF ⇒ pair exadecim bool x4 true ] 
-       | x6 ⇒
-           match e2 with
-            [ x0 ⇒ pair exadecim bool x6 false
-            | x1 ⇒ pair exadecim bool x7 false
-            | x2 ⇒ pair exadecim bool x8 false
-            | x3 ⇒ pair exadecim bool x9 false
-            | x4 ⇒ pair exadecim bool xA false
-            | x5 ⇒ pair exadecim bool xB false
-            | x6 ⇒ pair exadecim bool xC false
-            | x7 ⇒ pair exadecim bool xD false
-            | x8 ⇒ pair exadecim bool xE false
-            | x9 ⇒ pair exadecim bool xF false
-            | xA ⇒ pair exadecim bool x0 true
-            | xB ⇒ pair exadecim bool x1 true
-            | xC ⇒ pair exadecim bool x2 true
-            | xD ⇒ pair exadecim bool x3 true
-            | xE ⇒ pair exadecim bool x4 true
-            | xF ⇒ pair exadecim bool x5 true ] 
-       | x7 ⇒
-           match e2 with
-            [ x0 ⇒ pair exadecim bool x7 false
-            | x1 ⇒ pair exadecim bool x8 false
-            | x2 ⇒ pair exadecim bool x9 false
-            | x3 ⇒ pair exadecim bool xA false
-            | x4 ⇒ pair exadecim bool xB false
-            | x5 ⇒ pair exadecim bool xC false
-            | x6 ⇒ pair exadecim bool xD false
-            | x7 ⇒ pair exadecim bool xE false
-            | x8 ⇒ pair exadecim bool xF false
-            | x9 ⇒ pair exadecim bool x0 true
-            | xA ⇒ pair exadecim bool x1 true
-            | xB ⇒ pair exadecim bool x2 true
-            | xC ⇒ pair exadecim bool x3 true
-            | xD ⇒ pair exadecim bool x4 true
-            | xE ⇒ pair exadecim bool x5 true
-            | xF ⇒ pair exadecim bool x6 true ] 
-       | x8 ⇒
-           match e2 with
-            [ x0 ⇒ pair exadecim bool x8 false
-            | x1 ⇒ pair exadecim bool x9 false
-            | x2 ⇒ pair exadecim bool xA false
-            | x3 ⇒ pair exadecim bool xB false
-            | x4 ⇒ pair exadecim bool xC false
-            | x5 ⇒ pair exadecim bool xD false
-            | x6 ⇒ pair exadecim bool xE false
-            | x7 ⇒ pair exadecim bool xF false
-            | x8 ⇒ pair exadecim bool x0 true
-            | x9 ⇒ pair exadecim bool x1 true
-            | xA ⇒ pair exadecim bool x2 true
-            | xB ⇒ pair exadecim bool x3 true
-            | xC ⇒ pair exadecim bool x4 true
-            | xD ⇒ pair exadecim bool x5 true
-            | xE ⇒ pair exadecim bool x6 true
-            | xF ⇒ pair exadecim bool x7 true ] 
-       | x9 ⇒
-           match e2 with
-            [ x0 ⇒ pair exadecim bool x9 false
-            | x1 ⇒ pair exadecim bool xA false
-            | x2 ⇒ pair exadecim bool xB false
-            | x3 ⇒ pair exadecim bool xC false
-            | x4 ⇒ pair exadecim bool xD false
-            | x5 ⇒ pair exadecim bool xE false
-            | x6 ⇒ pair exadecim bool xF false
-            | x7 ⇒ pair exadecim bool x0 true
-            | x8 ⇒ pair exadecim bool x1 true
-            | x9 ⇒ pair exadecim bool x2 true
-            | xA ⇒ pair exadecim bool x3 true
-            | xB ⇒ pair exadecim bool x4 true
-            | xC ⇒ pair exadecim bool x5 true
-            | xD ⇒ pair exadecim bool x6 true
-            | xE ⇒ pair exadecim bool x7 true
-            | xF ⇒ pair exadecim bool x8 true ] 
-       | xA ⇒
-           match e2 with
-            [ x0 ⇒ pair exadecim bool xA false
-            | x1 ⇒ pair exadecim bool xB false
-            | x2 ⇒ pair exadecim bool xC false
-            | x3 ⇒ pair exadecim bool xD false
-            | x4 ⇒ pair exadecim bool xE false
-            | x5 ⇒ pair exadecim bool xF false
-            | x6 ⇒ pair exadecim bool x0 true
-            | x7 ⇒ pair exadecim bool x1 true
-            | x8 ⇒ pair exadecim bool x2 true
-            | x9 ⇒ pair exadecim bool x3 true
-            | xA ⇒ pair exadecim bool x4 true
-            | xB ⇒ pair exadecim bool x5 true
-            | xC ⇒ pair exadecim bool x6 true
-            | xD ⇒ pair exadecim bool x7 true
-            | xE ⇒ pair exadecim bool x8 true
-            | xF ⇒ pair exadecim bool x9 true ] 
-       | xB ⇒
-           match e2 with
-            [ x0 ⇒ pair exadecim bool xB false
-            | x1 ⇒ pair exadecim bool xC false
-            | x2 ⇒ pair exadecim bool xD false
-            | x3 ⇒ pair exadecim bool xE false
-            | x4 ⇒ pair exadecim bool xF false
-            | x5 ⇒ pair exadecim bool x0 true
-            | x6 ⇒ pair exadecim bool x1 true
-            | x7 ⇒ pair exadecim bool x2 true
-            | x8 ⇒ pair exadecim bool x3 true
-            | x9 ⇒ pair exadecim bool x4 true
-            | xA ⇒ pair exadecim bool x5 true
-            | xB ⇒ pair exadecim bool x6 true
-            | xC ⇒ pair exadecim bool x7 true
-            | xD ⇒ pair exadecim bool x8 true
-            | xE ⇒ pair exadecim bool x9 true
-            | xF ⇒ pair exadecim bool xA true ] 
-       | xC ⇒
-           match e2 with
-            [ x0 ⇒ pair exadecim bool xC false
-            | x1 ⇒ pair exadecim bool xD false
-            | x2 ⇒ pair exadecim bool xE false
-            | x3 ⇒ pair exadecim bool xF false
-            | x4 ⇒ pair exadecim bool x0 true
-            | x5 ⇒ pair exadecim bool x1 true
-            | x6 ⇒ pair exadecim bool x2 true
-            | x7 ⇒ pair exadecim bool x3 true
-            | x8 ⇒ pair exadecim bool x4 true
-            | x9 ⇒ pair exadecim bool x5 true
-            | xA ⇒ pair exadecim bool x6 true
-            | xB ⇒ pair exadecim bool x7 true
-            | xC ⇒ pair exadecim bool x8 true
-            | xD ⇒ pair exadecim bool x9 true
-            | xE ⇒ pair exadecim bool xA true
-            | xF ⇒ pair exadecim bool xB true ] 
-       | xD ⇒
-           match e2 with
-            [ x0 ⇒ pair exadecim bool xD false
-            | x1 ⇒ pair exadecim bool xE false
-            | x2 ⇒ pair exadecim bool xF false
-            | x3 ⇒ pair exadecim bool x0 true
-            | x4 ⇒ pair exadecim bool x1 true
-            | x5 ⇒ pair exadecim bool x2 true
-            | x6 ⇒ pair exadecim bool x3 true
-            | x7 ⇒ pair exadecim bool x4 true
-            | x8 ⇒ pair exadecim bool x5 true
-            | x9 ⇒ pair exadecim bool x6 true
-            | xA ⇒ pair exadecim bool x7 true
-            | xB ⇒ pair exadecim bool x8 true
-            | xC ⇒ pair exadecim bool x9 true
-            | xD ⇒ pair exadecim bool xA true
-            | xE ⇒ pair exadecim bool xB true
-            | xF ⇒ pair exadecim bool xC true ] 
-       | xE ⇒
-           match e2 with
-            [ x0 ⇒ pair exadecim bool xE false
-            | x1 ⇒ pair exadecim bool xF false
-            | x2 ⇒ pair exadecim bool x0 true
-            | x3 ⇒ pair exadecim bool x1 true
-            | x4 ⇒ pair exadecim bool x2 true
-            | x5 ⇒ pair exadecim bool x3 true
-            | x6 ⇒ pair exadecim bool x4 true
-            | x7 ⇒ pair exadecim bool x5 true
-            | x8 ⇒ pair exadecim bool x6 true
-            | x9 ⇒ pair exadecim bool x7 true
-            | xA ⇒ pair exadecim bool x8 true
-            | xB ⇒ pair exadecim bool x9 true
-            | xC ⇒ pair exadecim bool xA true
-            | xD ⇒ pair exadecim bool xB true
-            | xE ⇒ pair exadecim bool xC true
-            | xF ⇒ pair exadecim bool xD true ] 
-       | xF ⇒
-           match e2 with
-            [ x0 ⇒ pair exadecim bool xF false
-            | x1 ⇒ pair exadecim bool x0 true
-            | x2 ⇒ pair exadecim bool x1 true
-            | x3 ⇒ pair exadecim bool x2 true
-            | x4 ⇒ pair exadecim bool x3 true
-            | x5 ⇒ pair exadecim bool x4 true
-            | x6 ⇒ pair exadecim bool x5 true
-            | x7 ⇒ pair exadecim bool x6 true
-            | x8 ⇒ pair exadecim bool x7 true
-            | x9 ⇒ pair exadecim bool x8 true
-            | xA ⇒ pair exadecim bool x9 true
-            | xB ⇒ pair exadecim bool xA true
-            | xC ⇒ pair exadecim bool xB true
-            | xD ⇒ pair exadecim bool xC true
-            | xE ⇒ pair exadecim bool xD true
-            | xF ⇒ pair exadecim bool xE true ]
-       ]
-   ].
+ match c with
+  [ true ⇒ match e1 with
+   [ x0 ⇒ match e2 with
+    [ x0 ⇒ pair ?? x1 false | x1 ⇒ pair ?? x2 false | x2 ⇒ pair ?? x3 false | x3 ⇒ pair ?? x4 false
+    | x4 ⇒ pair ?? x5 false | x5 ⇒ pair ?? x6 false | x6 ⇒ pair ?? x7 false | x7 ⇒ pair ?? x8 false
+    | x8 ⇒ pair ?? x9 false | x9 ⇒ pair ?? xA false | xA ⇒ pair ?? xB false | xB ⇒ pair ?? xC false
+    | xC ⇒ pair ?? xD false | xD ⇒ pair ?? xE false | xE ⇒ pair ?? xF false | xF ⇒ pair ?? x0 true ] 
+   | x1 ⇒ match e2 with
+    [ x0 ⇒ pair ?? x2 false | x1 ⇒ pair ?? x3 false | x2 ⇒ pair ?? x4 false | x3 ⇒ pair ?? x5 false
+    | x4 ⇒ pair ?? x6 false | x5 ⇒ pair ?? x7 false | x6 ⇒ pair ?? x8 false | x7 ⇒ pair ?? x9 false
+    | x8 ⇒ pair ?? xA false | x9 ⇒ pair ?? xB false | xA ⇒ pair ?? xC false | xB ⇒ pair ?? xD false
+    | xC ⇒ pair ?? xE false | xD ⇒ pair ?? xF false | xE ⇒ pair ?? x0 true  | xF ⇒ pair ?? x1 true ] 
+   | x2 ⇒ match e2 with
+    [ x0 ⇒ pair ?? x3 false | x1 ⇒ pair ?? x4 false | x2 ⇒ pair ?? x5 false | x3 ⇒ pair ?? x6 false
+    | x4 ⇒ pair ?? x7 false | x5 ⇒ pair ?? x8 false | x6 ⇒ pair ?? x9 false | x7 ⇒ pair ?? xA false
+    | x8 ⇒ pair ?? xB false | x9 ⇒ pair ?? xC false | xA ⇒ pair ?? xD false | xB ⇒ pair ?? xE false
+    | xC ⇒ pair ?? xF false | xD ⇒ pair ?? x0 true  | xE ⇒ pair ?? x1 true  | xF ⇒ pair ?? x2 true ] 
+   | x3 ⇒ match e2 with
+    [ x0 ⇒ pair ?? x4 false | x1 ⇒ pair ?? x5 false | x2 ⇒ pair ?? x6 false | x3 ⇒ pair ?? x7 false
+    | x4 ⇒ pair ?? x8 false | x5 ⇒ pair ?? x9 false | x6 ⇒ pair ?? xA false | x7 ⇒ pair ?? xB false
+    | x8 ⇒ pair ?? xC false | x9 ⇒ pair ?? xD false | xA ⇒ pair ?? xE false | xB ⇒ pair ?? xF false
+    | xC ⇒ pair ?? x0 true  | xD ⇒ pair ?? x1 true  | xE ⇒ pair ?? x2 true  | xF ⇒ pair ?? x3 true ] 
+   | x4 ⇒ match e2 with
+    [ x0 ⇒ pair ?? x5 false | x1 ⇒ pair ?? x6 false | x2 ⇒ pair ?? x7 false | x3 ⇒ pair ?? x8 false
+    | x4 ⇒ pair ?? x9 false | x5 ⇒ pair ?? xA false | x6 ⇒ pair ?? xB false | x7 ⇒ pair ?? xC false
+    | x8 ⇒ pair ?? xD false | x9 ⇒ pair ?? xE false | xA ⇒ pair ?? xF false | xB ⇒ pair ?? x0 true
+    | xC ⇒ pair ?? x1 true  | xD ⇒ pair ?? x2 true  | xE ⇒ pair ?? x3 true  | xF ⇒ pair ?? x4 true ] 
+   | x5 ⇒ match e2 with
+    [ x0 ⇒ pair ?? x6 false | x1 ⇒ pair ?? x7 false | x2 ⇒ pair ?? x8 false | x3 ⇒ pair ?? x9 false
+    | x4 ⇒ pair ?? xA false | x5 ⇒ pair ?? xB false | x6 ⇒ pair ?? xC false | x7 ⇒ pair ?? xD false
+    | x8 ⇒ pair ?? xE false | x9 ⇒ pair ?? xF false | xA ⇒ pair ?? x0 true  | xB ⇒ pair ?? x1 true
+    | xC ⇒ pair ?? x2 true  | xD ⇒ pair ?? x3 true  | xE ⇒ pair ?? x4 true  | xF ⇒ pair ?? x5 true ] 
+   | x6 ⇒ match e2 with
+    [ x0 ⇒ pair ?? x7 false | x1 ⇒ pair ?? x8 false | x2 ⇒ pair ?? x9 false | x3 ⇒ pair ?? xA false
+    | x4 ⇒ pair ?? xB false | x5 ⇒ pair ?? xC false | x6 ⇒ pair ?? xD false | x7 ⇒ pair ?? xE false
+    | x8 ⇒ pair ?? xF false | x9 ⇒ pair ?? x0 true  | xA ⇒ pair ?? x1 true  | xB ⇒ pair ?? x2 true
+    | xC ⇒ pair ?? x3 true  | xD ⇒ pair ?? x4 true  | xE ⇒ pair ?? x5 true  | xF ⇒ pair ?? x6 true ] 
+   | x7 ⇒ match e2 with
+    [ x0 ⇒ pair ?? x8 false | x1 ⇒ pair ?? x9 false | x2 ⇒ pair ?? xA false | x3 ⇒ pair ?? xB false
+    | x4 ⇒ pair ?? xC false | x5 ⇒ pair ?? xD false | x6 ⇒ pair ?? xE false | x7 ⇒ pair ?? xF false
+    | x8 ⇒ pair ?? x0 true  | x9 ⇒ pair ?? x1 true  | xA ⇒ pair ?? x2 true  | xB ⇒ pair ?? x3 true
+    | xC ⇒ pair ?? x4 true  | xD ⇒ pair ?? x5 true  | xE ⇒ pair ?? x6 true  | xF ⇒ pair ?? x7 true ] 
+   | x8 ⇒ match e2 with
+    [ x0 ⇒ pair ?? x9 false | x1 ⇒ pair ?? xA false | x2 ⇒ pair ?? xB false | x3 ⇒ pair ?? xC false
+    | x4 ⇒ pair ?? xD false | x5 ⇒ pair ?? xE false | x6 ⇒ pair ?? xF false | x7 ⇒ pair ?? x0 true
+    | x8 ⇒ pair ?? x1 true  | x9 ⇒ pair ?? x2 true  | xA ⇒ pair ?? x3 true  | xB ⇒ pair ?? x4 true
+    | xC ⇒ pair ?? x5 true  | xD ⇒ pair ?? x6 true  | xE ⇒ pair ?? x7 true  | xF ⇒ pair ?? x8 true ] 
+   | x9 ⇒ match e2 with
+    [ x0 ⇒ pair ?? xA false | x1 ⇒ pair ?? xB false | x2 ⇒ pair ?? xC false | x3 ⇒ pair ?? xD false
+    | x4 ⇒ pair ?? xE false | x5 ⇒ pair ?? xF false | x6 ⇒ pair ?? x0 true  | x7 ⇒ pair ?? x1 true
+    | x8 ⇒ pair ?? x2 true  | x9 ⇒ pair ?? x3 true  | xA ⇒ pair ?? x4 true  | xB ⇒ pair ?? x5 true
+    | xC ⇒ pair ?? x6 true  | xD ⇒ pair ?? x7 true  | xE ⇒ pair ?? x8 true  | xF ⇒ pair ?? x9 true ] 
+   | xA ⇒ match e2 with
+    [ x0 ⇒ pair ?? xB false | x1 ⇒ pair ?? xC false | x2 ⇒ pair ?? xD false | x3 ⇒ pair ?? xE false
+    | x4 ⇒ pair ?? xF false | x5 ⇒ pair ?? x0 true  | x6 ⇒ pair ?? x1 true  | x7 ⇒ pair ?? x2 true
+    | x8 ⇒ pair ?? x3 true  | x9 ⇒ pair ?? x4 true  | xA ⇒ pair ?? x5 true  | xB ⇒ pair ?? x6 true
+    | xC ⇒ pair ?? x7 true  | xD ⇒ pair ?? x8 true  | xE ⇒ pair ?? x9 true  | xF ⇒ pair ?? xA true ] 
+   | xB ⇒ match e2 with
+    [ x0 ⇒ pair ?? xC false | x1 ⇒ pair ?? xD false | x2 ⇒ pair ?? xE false | x3 ⇒ pair ?? xF false
+    | x4 ⇒ pair ?? x0 true  | x5 ⇒ pair ?? x1 true  | x6 ⇒ pair ?? x2 true  | x7 ⇒ pair ?? x3 true
+    | x8 ⇒ pair ?? x4 true  | x9 ⇒ pair ?? x5 true  | xA ⇒ pair ?? x6 true  | xB ⇒ pair ?? x7 true
+    | xC ⇒ pair ?? x8 true  | xD ⇒ pair ?? x9 true  | xE ⇒ pair ?? xA true  | xF ⇒ pair ?? xB true ] 
+   | xC ⇒ match e2 with
+    [ x0 ⇒ pair ?? xD false | x1 ⇒ pair ?? xE false | x2 ⇒ pair ?? xF false | x3 ⇒ pair ?? x0 true
+    | x4 ⇒ pair ?? x1 true  | x5 ⇒ pair ?? x2 true  | x6 ⇒ pair ?? x3 true  | x7 ⇒ pair ?? x4 true
+    | x8 ⇒ pair ?? x5 true  | x9 ⇒ pair ?? x6 true  | xA ⇒ pair ?? x7 true  | xB ⇒ pair ?? x8 true
+    | xC ⇒ pair ?? x9 true  | xD ⇒ pair ?? xA true  | xE ⇒ pair ?? xB true  | xF ⇒ pair ?? xC true ] 
+   | xD ⇒ match e2 with
+    [ x0 ⇒ pair ?? xE false | x1 ⇒ pair ?? xF false | x2 ⇒ pair ?? x0 true  | x3 ⇒ pair ?? x1 true
+    | x4 ⇒ pair ?? x2 true  | x5 ⇒ pair ?? x3 true  | x6 ⇒ pair ?? x4 true  | x7 ⇒ pair ?? x5 true
+    | x8 ⇒ pair ?? x6 true  | x9 ⇒ pair ?? x7 true  | xA ⇒ pair ?? x8 true  | xB ⇒ pair ?? x9 true
+    | xC ⇒ pair ?? xA true  | xD ⇒ pair ?? xB true  | xE ⇒ pair ?? xC true  | xF ⇒ pair ?? xD true ] 
+   | xE ⇒ match e2 with
+    [ x0 ⇒ pair ?? xF false | x1 ⇒ pair ?? x0 true  | x2 ⇒ pair ?? x1 true  | x3 ⇒ pair ?? x2 true
+    | x4 ⇒ pair ?? x3 true  | x5 ⇒ pair ?? x4 true  | x6 ⇒ pair ?? x5 true  | x7 ⇒ pair ?? x6 true
+    | x8 ⇒ pair ?? x7 true  | x9 ⇒ pair ?? x8 true  | xA ⇒ pair ?? x9 true  | xB ⇒ pair ?? xA true
+    | xC ⇒ pair ?? xB true  | xD ⇒ pair ?? xC true  | xE ⇒ pair ?? xD true  | xF ⇒ pair ?? xE true ]
+   | xF ⇒ match e2 with
+    [ x0 ⇒ pair ?? x0 true  | x1 ⇒ pair ?? x1 true  | x2 ⇒ pair ?? x2 true  | x3 ⇒ pair ?? x3 true
+    | x4 ⇒ pair ?? x4 true  | x5 ⇒ pair ?? x5 true  | x6 ⇒ pair ?? x6 true  | x7 ⇒ pair ?? x7 true
+    | x8 ⇒ pair ?? x8 true  | x9 ⇒ pair ?? x9 true  | xA ⇒ pair ?? xA true  | xB ⇒ pair ?? xB true
+    | xC ⇒ pair ?? xC true  | xD ⇒ pair ?? xD true  | xE ⇒ pair ?? xE true  | xF ⇒ pair ?? xF true ] 
+   ]
+  | false ⇒ match e1 with
+   [ x0 ⇒ match e2 with
+    [ x0 ⇒ pair ?? x0 false | x1 ⇒ pair ?? x1 false | x2 ⇒ pair ?? x2 false | x3 ⇒ pair ?? x3 false
+    | x4 ⇒ pair ?? x4 false | x5 ⇒ pair ?? x5 false | x6 ⇒ pair ?? x6 false | x7 ⇒ pair ?? x7 false
+    | x8 ⇒ pair ?? x8 false | x9 ⇒ pair ?? x9 false | xA ⇒ pair ?? xA false | xB ⇒ pair ?? xB false
+    | xC ⇒ pair ?? xC false | xD ⇒ pair ?? xD false | xE ⇒ pair ?? xE false | xF ⇒ pair ?? xF false ] 
+   | x1 ⇒ match e2 with
+    [ x0 ⇒ pair ?? x1 false | x1 ⇒ pair ?? x2 false | x2 ⇒ pair ?? x3 false | x3 ⇒ pair ?? x4 false
+    | x4 ⇒ pair ?? x5 false | x5 ⇒ pair ?? x6 false | x6 ⇒ pair ?? x7 false | x7 ⇒ pair ?? x8 false
+    | x8 ⇒ pair ?? x9 false | x9 ⇒ pair ?? xA false | xA ⇒ pair ?? xB false | xB ⇒ pair ?? xC false
+    | xC ⇒ pair ?? xD false | xD ⇒ pair ?? xE false | xE ⇒ pair ?? xF false | xF ⇒ pair ?? x0 true ] 
+   | x2 ⇒ match e2 with
+    [ x0 ⇒ pair ?? x2 false | x1 ⇒ pair ?? x3 false | x2 ⇒ pair ?? x4 false | x3 ⇒ pair ?? x5 false
+    | x4 ⇒ pair ?? x6 false | x5 ⇒ pair ?? x7 false | x6 ⇒ pair ?? x8 false | x7 ⇒ pair ?? x9 false
+    | x8 ⇒ pair ?? xA false | x9 ⇒ pair ?? xB false | xA ⇒ pair ?? xC false | xB ⇒ pair ?? xD false
+    | xC ⇒ pair ?? xE false | xD ⇒ pair ?? xF false | xE ⇒ pair ?? x0 true  | xF ⇒ pair ?? x1 true ] 
+   | x3 ⇒ match e2 with
+    [ x0 ⇒ pair ?? x3 false | x1 ⇒ pair ?? x4 false | x2 ⇒ pair ?? x5 false | x3 ⇒ pair ?? x6 false
+    | x4 ⇒ pair ?? x7 false | x5 ⇒ pair ?? x8 false | x6 ⇒ pair ?? x9 false | x7 ⇒ pair ?? xA false
+    | x8 ⇒ pair ?? xB false | x9 ⇒ pair ?? xC false | xA ⇒ pair ?? xD false | xB ⇒ pair ?? xE false
+    | xC ⇒ pair ?? xF false | xD ⇒ pair ?? x0 true  | xE ⇒ pair ?? x1 true  | xF ⇒ pair ?? x2 true ] 
+   | x4 ⇒ match e2 with
+    [ x0 ⇒ pair ?? x4 false | x1 ⇒ pair ?? x5 false | x2 ⇒ pair ?? x6 false | x3 ⇒ pair ?? x7 false
+    | x4 ⇒ pair ?? x8 false | x5 ⇒ pair ?? x9 false | x6 ⇒ pair ?? xA false | x7 ⇒ pair ?? xB false
+    | x8 ⇒ pair ?? xC false | x9 ⇒ pair ?? xD false | xA ⇒ pair ?? xE false | xB ⇒ pair ?? xF false
+    | xC ⇒ pair ?? x0 true  | xD ⇒ pair ?? x1 true  | xE ⇒ pair ?? x2 true  | xF ⇒ pair ?? x3 true ] 
+   | x5 ⇒ match e2 with
+    [ x0 ⇒ pair ?? x5 false | x1 ⇒ pair ?? x6 false | x2 ⇒ pair ?? x7 false | x3 ⇒ pair ?? x8 false
+    | x4 ⇒ pair ?? x9 false | x5 ⇒ pair ?? xA false | x6 ⇒ pair ?? xB false | x7 ⇒ pair ?? xC false
+    | x8 ⇒ pair ?? xD false | x9 ⇒ pair ?? xE false | xA ⇒ pair ?? xF false | xB ⇒ pair ?? x0 true
+    | xC ⇒ pair ?? x1 true  | xD ⇒ pair ?? x2 true  | xE ⇒ pair ?? x3 true  | xF ⇒ pair ?? x4 true ] 
+   | x6 ⇒ match e2 with
+    [ x0 ⇒ pair ?? x6 false | x1 ⇒ pair ?? x7 false | x2 ⇒ pair ?? x8 false | x3 ⇒ pair ?? x9 false
+    | x4 ⇒ pair ?? xA false | x5 ⇒ pair ?? xB false | x6 ⇒ pair ?? xC false | x7 ⇒ pair ?? xD false
+    | x8 ⇒ pair ?? xE false | x9 ⇒ pair ?? xF false | xA ⇒ pair ?? x0 true  | xB ⇒ pair ?? x1 true
+    | xC ⇒ pair ?? x2 true  | xD ⇒ pair ?? x3 true  | xE ⇒ pair ?? x4 true  | xF ⇒ pair ?? x5 true ] 
+   | x7 ⇒ match e2 with
+    [ x0 ⇒ pair ?? x7 false | x1 ⇒ pair ?? x8 false | x2 ⇒ pair ?? x9 false | x3 ⇒ pair ?? xA false
+    | x4 ⇒ pair ?? xB false | x5 ⇒ pair ?? xC false | x6 ⇒ pair ?? xD false | x7 ⇒ pair ?? xE false
+    | x8 ⇒ pair ?? xF false | x9 ⇒ pair ?? x0 true  | xA ⇒ pair ?? x1 true  | xB ⇒ pair ?? x2 true
+    | xC ⇒ pair ?? x3 true  | xD ⇒ pair ?? x4 true  | xE ⇒ pair ?? x5 true  | xF ⇒ pair ?? x6 true ] 
+   | x8 ⇒ match e2 with
+    [ x0 ⇒ pair ?? x8 false | x1 ⇒ pair ?? x9 false | x2 ⇒ pair ?? xA false | x3 ⇒ pair ?? xB false
+    | x4 ⇒ pair ?? xC false | x5 ⇒ pair ?? xD false | x6 ⇒ pair ?? xE false | x7 ⇒ pair ?? xF false
+    | x8 ⇒ pair ?? x0 true  | x9 ⇒ pair ?? x1 true  | xA ⇒ pair ?? x2 true  | xB ⇒ pair ?? x3 true
+    | xC ⇒ pair ?? x4 true  | xD ⇒ pair ?? x5 true  | xE ⇒ pair ?? x6 true  | xF ⇒ pair ?? x7 true ] 
+   | x9 ⇒ match e2 with
+    [ x0 ⇒ pair ?? x9 false | x1 ⇒ pair ?? xA false | x2 ⇒ pair ?? xB false | x3 ⇒ pair ?? xC false
+    | x4 ⇒ pair ?? xD false | x5 ⇒ pair ?? xE false | x6 ⇒ pair ?? xF false | x7 ⇒ pair ?? x0 true
+    | x8 ⇒ pair ?? x1 true  | x9 ⇒ pair ?? x2 true  | xA ⇒ pair ?? x3 true  | xB ⇒ pair ?? x4 true
+    | xC ⇒ pair ?? x5 true  | xD ⇒ pair ?? x6 true  | xE ⇒ pair ?? x7 true  | xF ⇒ pair ?? x8 true ] 
+   | xA ⇒ match e2 with
+    [ x0 ⇒ pair ?? xA false | x1 ⇒ pair ?? xB false | x2 ⇒ pair ?? xC false | x3 ⇒ pair ?? xD false
+    | x4 ⇒ pair ?? xE false | x5 ⇒ pair ?? xF false | x6 ⇒ pair ?? x0 true  | x7 ⇒ pair ?? x1 true
+    | x8 ⇒ pair ?? x2 true  | x9 ⇒ pair ?? x3 true  | xA ⇒ pair ?? x4 true  | xB ⇒ pair ?? x5 true
+    | xC ⇒ pair ?? x6 true  | xD ⇒ pair ?? x7 true  | xE ⇒ pair ?? x8 true  | xF ⇒ pair ?? x9 true ] 
+   | xB ⇒ match e2 with
+    [ x0 ⇒ pair ?? xB false | x1 ⇒ pair ?? xC false | x2 ⇒ pair ?? xD false | x3 ⇒ pair ?? xE false
+    | x4 ⇒ pair ?? xF false | x5 ⇒ pair ?? x0 true  | x6 ⇒ pair ?? x1 true  | x7 ⇒ pair ?? x2 true
+    | x8 ⇒ pair ?? x3 true  | x9 ⇒ pair ?? x4 true  | xA ⇒ pair ?? x5 true  | xB ⇒ pair ?? x6 true
+    | xC ⇒ pair ?? x7 true  | xD ⇒ pair ?? x8 true  | xE ⇒ pair ?? x9 true  | xF ⇒ pair ?? xA true ] 
+   | xC ⇒ match e2 with
+    [ x0 ⇒ pair ?? xC false | x1 ⇒ pair ?? xD false | x2 ⇒ pair ?? xE false | x3 ⇒ pair ?? xF false
+    | x4 ⇒ pair ?? x0 true  | x5 ⇒ pair ?? x1 true  | x6 ⇒ pair ?? x2 true  | x7 ⇒ pair ?? x3 true
+    | x8 ⇒ pair ?? x4 true  | x9 ⇒ pair ?? x5 true  | xA ⇒ pair ?? x6 true  | xB ⇒ pair ?? x7 true
+    | xC ⇒ pair ?? x8 true  | xD ⇒ pair ?? x9 true  | xE ⇒ pair ?? xA true  | xF ⇒ pair ?? xB true ] 
+   | xD ⇒ match e2 with
+    [ x0 ⇒ pair ?? xD false | x1 ⇒ pair ?? xE false | x2 ⇒ pair ?? xF false | x3 ⇒ pair ?? x0 true
+    | x4 ⇒ pair ?? x1 true  | x5 ⇒ pair ?? x2 true  | x6 ⇒ pair ?? x3 true  | x7 ⇒ pair ?? x4 true
+    | x8 ⇒ pair ?? x5 true  | x9 ⇒ pair ?? x6 true  | xA ⇒ pair ?? x7 true  | xB ⇒ pair ?? x8 true
+    | xC ⇒ pair ?? x9 true  | xD ⇒ pair ?? xA true  | xE ⇒ pair ?? xB true  | xF ⇒ pair ?? xC true ] 
+   | xE ⇒ match e2 with
+    [ x0 ⇒ pair ?? xE false | x1 ⇒ pair ?? xF false | x2 ⇒ pair ?? x0 true  | x3 ⇒ pair ?? x1 true
+    | x4 ⇒ pair ?? x2 true  | x5 ⇒ pair ?? x3 true  | x6 ⇒ pair ?? x4 true  | x7 ⇒ pair ?? x5 true
+    | x8 ⇒ pair ?? x6 true  | x9 ⇒ pair ?? x7 true  | xA ⇒ pair ?? x8 true  | xB ⇒ pair ?? x9 true
+    | xC ⇒ pair ?? xA true  | xD ⇒ pair ?? xB true  | xE ⇒ pair ?? xC true  | xF ⇒ pair ?? xD true ] 
+   | xF ⇒ match e2 with
+    [ x0 ⇒ pair ?? xF false | x1 ⇒ pair ?? x0 true  | x2 ⇒ pair ?? x1 true  | x3 ⇒ pair ?? x2 true
+    | x4 ⇒ pair ?? x3 true  | x5 ⇒ pair ?? x4 true  | x6 ⇒ pair ?? x5 true  | x7 ⇒ pair ?? x6 true
+    | x8 ⇒ pair ?? x7 true  | x9 ⇒ pair ?? x8 true  | xA ⇒ pair ?? x9 true  | xB ⇒ pair ?? xA true
+    | xC ⇒ pair ?? xB true  | xD ⇒ pair ?? xC true  | xE ⇒ pair ?? xD true  | xF ⇒ pair ?? xE true ]
+   ]].
 
-(* operatore somma senza carry *)
-ndefinition plus_exnc ≝
-λe1,e2:exadecim.fst ?? (plus_ex e1 e2 false).
+(* operatore somma con data → data+carry *)
+ndefinition plus_ex_d_dc ≝
+λe1,e2:exadecim.
+ match e1 with
+  [ x0 ⇒ match e2 with
+   [ x0 ⇒ pair ?? x0 false | x1 ⇒ pair ?? x1 false | x2 ⇒ pair ?? x2 false | x3 ⇒ pair ?? x3 false
+   | x4 ⇒ pair ?? x4 false | x5 ⇒ pair ?? x5 false | x6 ⇒ pair ?? x6 false | x7 ⇒ pair ?? x7 false
+   | x8 ⇒ pair ?? x8 false | x9 ⇒ pair ?? x9 false | xA ⇒ pair ?? xA false | xB ⇒ pair ?? xB false
+   | xC ⇒ pair ?? xC false | xD ⇒ pair ?? xD false | xE ⇒ pair ?? xE false | xF ⇒ pair ?? xF false ]  
+  | x1 ⇒ match e2 with
+   [ x0 ⇒ pair ?? x1 false | x1 ⇒ pair ?? x2 false | x2 ⇒ pair ?? x3 false | x3 ⇒ pair ?? x4 false
+   | x4 ⇒ pair ?? x5 false | x5 ⇒ pair ?? x6 false | x6 ⇒ pair ?? x7 false | x7 ⇒ pair ?? x8 false
+   | x8 ⇒ pair ?? x9 false | x9 ⇒ pair ?? xA false | xA ⇒ pair ?? xB false | xB ⇒ pair ?? xC false
+   | xC ⇒ pair ?? xD false | xD ⇒ pair ?? xE false | xE ⇒ pair ?? xF false | xF ⇒ pair ?? x0 true ] 
+  | x2 ⇒ match e2 with
+   [ x0 ⇒ pair ?? x2 false | x1 ⇒ pair ?? x3 false | x2 ⇒ pair ?? x4 false | x3 ⇒ pair ?? x5 false
+   | x4 ⇒ pair ?? x6 false | x5 ⇒ pair ?? x7 false | x6 ⇒ pair ?? x8 false | x7 ⇒ pair ?? x9 false
+   | x8 ⇒ pair ?? xA false | x9 ⇒ pair ?? xB false | xA ⇒ pair ?? xC false | xB ⇒ pair ?? xD false
+   | xC ⇒ pair ?? xE false | xD ⇒ pair ?? xF false | xE ⇒ pair ?? x0 true  | xF ⇒ pair ?? x1 true ] 
+  | x3 ⇒ match e2 with
+   [ x0 ⇒ pair ?? x3 false | x1 ⇒ pair ?? x4 false | x2 ⇒ pair ?? x5 false | x3 ⇒ pair ?? x6 false
+   | x4 ⇒ pair ?? x7 false | x5 ⇒ pair ?? x8 false | x6 ⇒ pair ?? x9 false | x7 ⇒ pair ?? xA false
+   | x8 ⇒ pair ?? xB false | x9 ⇒ pair ?? xC false | xA ⇒ pair ?? xD false | xB ⇒ pair ?? xE false
+   | xC ⇒ pair ?? xF false | xD ⇒ pair ?? x0 true  | xE ⇒ pair ?? x1 true  | xF ⇒ pair ?? x2 true ] 
+  | x4 ⇒ match e2 with
+   [ x0 ⇒ pair ?? x4 false | x1 ⇒ pair ?? x5 false | x2 ⇒ pair ?? x6 false | x3 ⇒ pair ?? x7 false
+   | x4 ⇒ pair ?? x8 false | x5 ⇒ pair ?? x9 false | x6 ⇒ pair ?? xA false | x7 ⇒ pair ?? xB false
+   | x8 ⇒ pair ?? xC false | x9 ⇒ pair ?? xD false | xA ⇒ pair ?? xE false | xB ⇒ pair ?? xF false
+   | xC ⇒ pair ?? x0 true  | xD ⇒ pair ?? x1 true  | xE ⇒ pair ?? x2 true  | xF ⇒ pair ?? x3 true ] 
+  | x5 ⇒ match e2 with
+   [ x0 ⇒ pair ?? x5 false | x1 ⇒ pair ?? x6 false | x2 ⇒ pair ?? x7 false | x3 ⇒ pair ?? x8 false
+   | x4 ⇒ pair ?? x9 false | x5 ⇒ pair ?? xA false | x6 ⇒ pair ?? xB false | x7 ⇒ pair ?? xC false
+   | x8 ⇒ pair ?? xD false | x9 ⇒ pair ?? xE false | xA ⇒ pair ?? xF false | xB ⇒ pair ?? x0 true
+   | xC ⇒ pair ?? x1 true  | xD ⇒ pair ?? x2 true  | xE ⇒ pair ?? x3 true  | xF ⇒ pair ?? x4 true ] 
+  | x6 ⇒ match e2 with
+   [ x0 ⇒ pair ?? x6 false | x1 ⇒ pair ?? x7 false | x2 ⇒ pair ?? x8 false | x3 ⇒ pair ?? x9 false
+   | x4 ⇒ pair ?? xA false | x5 ⇒ pair ?? xB false | x6 ⇒ pair ?? xC false | x7 ⇒ pair ?? xD false
+   | x8 ⇒ pair ?? xE false | x9 ⇒ pair ?? xF false | xA ⇒ pair ?? x0 true  | xB ⇒ pair ?? x1 true
+   | xC ⇒ pair ?? x2 true  | xD ⇒ pair ?? x3 true  | xE ⇒ pair ?? x4 true  | xF ⇒ pair ?? x5 true ] 
+  | x7 ⇒ match e2 with
+   [ x0 ⇒ pair ?? x7 false | x1 ⇒ pair ?? x8 false | x2 ⇒ pair ?? x9 false | x3 ⇒ pair ?? xA false
+   | x4 ⇒ pair ?? xB false | x5 ⇒ pair ?? xC false | x6 ⇒ pair ?? xD false | x7 ⇒ pair ?? xE false
+   | x8 ⇒ pair ?? xF false | x9 ⇒ pair ?? x0 true  | xA ⇒ pair ?? x1 true  | xB ⇒ pair ?? x2 true
+   | xC ⇒ pair ?? x3 true  | xD ⇒ pair ?? x4 true  | xE ⇒ pair ?? x5 true  | xF ⇒ pair ?? x6 true ] 
+  | x8 ⇒ match e2 with
+   [ x0 ⇒ pair ?? x8 false | x1 ⇒ pair ?? x9 false | x2 ⇒ pair ?? xA false | x3 ⇒ pair ?? xB false
+   | x4 ⇒ pair ?? xC false | x5 ⇒ pair ?? xD false | x6 ⇒ pair ?? xE false | x7 ⇒ pair ?? xF false
+   | x8 ⇒ pair ?? x0 true  | x9 ⇒ pair ?? x1 true  | xA ⇒ pair ?? x2 true  | xB ⇒ pair ?? x3 true
+   | xC ⇒ pair ?? x4 true  | xD ⇒ pair ?? x5 true  | xE ⇒ pair ?? x6 true  | xF ⇒ pair ?? x7 true ] 
+  | x9 ⇒ match e2 with
+   [ x0 ⇒ pair ?? x9 false | x1 ⇒ pair ?? xA false | x2 ⇒ pair ?? xB false | x3 ⇒ pair ?? xC false
+   | x4 ⇒ pair ?? xD false | x5 ⇒ pair ?? xE false | x6 ⇒ pair ?? xF false | x7 ⇒ pair ?? x0 true
+   | x8 ⇒ pair ?? x1 true  | x9 ⇒ pair ?? x2 true  | xA ⇒ pair ?? x3 true  | xB ⇒ pair ?? x4 true
+   | xC ⇒ pair ?? x5 true  | xD ⇒ pair ?? x6 true  | xE ⇒ pair ?? x7 true  | xF ⇒ pair ?? x8 true ] 
+  | xA ⇒ match e2 with
+   [ x0 ⇒ pair ?? xA false | x1 ⇒ pair ?? xB false | x2 ⇒ pair ?? xC false | x3 ⇒ pair ?? xD false
+   | x4 ⇒ pair ?? xE false | x5 ⇒ pair ?? xF false | x6 ⇒ pair ?? x0 true  | x7 ⇒ pair ?? x1 true
+   | x8 ⇒ pair ?? x2 true  | x9 ⇒ pair ?? x3 true  | xA ⇒ pair ?? x4 true  | xB ⇒ pair ?? x5 true
+   | xC ⇒ pair ?? x6 true  | xD ⇒ pair ?? x7 true  | xE ⇒ pair ?? x8 true  | xF ⇒ pair ?? x9 true ] 
+  | xB ⇒ match e2 with
+   [ x0 ⇒ pair ?? xB false | x1 ⇒ pair ?? xC false | x2 ⇒ pair ?? xD false | x3 ⇒ pair ?? xE false
+   | x4 ⇒ pair ?? xF false | x5 ⇒ pair ?? x0 true  | x6 ⇒ pair ?? x1 true  | x7 ⇒ pair ?? x2 true
+   | x8 ⇒ pair ?? x3 true  | x9 ⇒ pair ?? x4 true  | xA ⇒ pair ?? x5 true  | xB ⇒ pair ?? x6 true
+   | xC ⇒ pair ?? x7 true  | xD ⇒ pair ?? x8 true  | xE ⇒ pair ?? x9 true  | xF ⇒ pair ?? xA true ] 
+  | xC ⇒ match e2 with
+   [ x0 ⇒ pair ?? xC false | x1 ⇒ pair ?? xD false | x2 ⇒ pair ?? xE false | x3 ⇒ pair ?? xF false
+   | x4 ⇒ pair ?? x0 true  | x5 ⇒ pair ?? x1 true  | x6 ⇒ pair ?? x2 true  | x7 ⇒ pair ?? x3 true
+   | x8 ⇒ pair ?? x4 true  | x9 ⇒ pair ?? x5 true  | xA ⇒ pair ?? x6 true  | xB ⇒ pair ?? x7 true
+   | xC ⇒ pair ?? x8 true  | xD ⇒ pair ?? x9 true  | xE ⇒ pair ?? xA true  | xF ⇒ pair ?? xB true ] 
+  | xD ⇒ match e2 with
+   [ x0 ⇒ pair ?? xD false | x1 ⇒ pair ?? xE false | x2 ⇒ pair ?? xF false | x3 ⇒ pair ?? x0 true
+   | x4 ⇒ pair ?? x1 true  | x5 ⇒ pair ?? x2 true  | x6 ⇒ pair ?? x3 true  | x7 ⇒ pair ?? x4 true
+   | x8 ⇒ pair ?? x5 true  | x9 ⇒ pair ?? x6 true  | xA ⇒ pair ?? x7 true  | xB ⇒ pair ?? x8 true
+   | xC ⇒ pair ?? x9 true  | xD ⇒ pair ?? xA true  | xE ⇒ pair ?? xB true  | xF ⇒ pair ?? xC true ] 
+  | xE ⇒ match e2 with
+   [ x0 ⇒ pair ?? xE false | x1 ⇒ pair ?? xF false | x2 ⇒ pair ?? x0 true  | x3 ⇒ pair ?? x1 true
+   | x4 ⇒ pair ?? x2 true  | x5 ⇒ pair ?? x3 true  | x6 ⇒ pair ?? x4 true  | x7 ⇒ pair ?? x5 true
+   | x8 ⇒ pair ?? x6 true  | x9 ⇒ pair ?? x7 true  | xA ⇒ pair ?? x8 true  | xB ⇒ pair ?? x9 true
+   | xC ⇒ pair ?? xA true  | xD ⇒ pair ?? xB true  | xE ⇒ pair ?? xC true  | xF ⇒ pair ?? xD true ] 
+  | xF ⇒ match e2 with
+   [ x0 ⇒ pair ?? xF false | x1 ⇒ pair ?? x0 true  | x2 ⇒ pair ?? x1 true  | x3 ⇒ pair ?? x2 true
+   | x4 ⇒ pair ?? x3 true  | x5 ⇒ pair ?? x4 true  | x6 ⇒ pair ?? x5 true  | x7 ⇒ pair ?? x6 true
+   | x8 ⇒ pair ?? x7 true  | x9 ⇒ pair ?? x8 true  | xA ⇒ pair ?? x9 true  | xB ⇒ pair ?? xA true
+   | xC ⇒ pair ?? xB true  | xD ⇒ pair ?? xC true  | xE ⇒ pair ?? xD true  | xF ⇒ pair ?? xE true ]
+  ].
+
+(* operatore somma con data+carry → data *)
+ndefinition plus_ex_dc_d ≝
+λe1,e2:exadecim.λc:bool.
+ match c with
+  [ true ⇒ match e1 with
+   [ x0 ⇒ match e2 with
+    [ x0 ⇒ x1 | x1 ⇒ x2 | x2 ⇒ x3 | x3 ⇒ x4 | x4 ⇒ x5 | x5 ⇒ x6 | x6 ⇒ x7 | x7 ⇒ x8
+    | x8 ⇒ x9 | x9 ⇒ xA | xA ⇒ xB | xB ⇒ xC | xC ⇒ xD | xD ⇒ xE | xE ⇒ xF | xF ⇒ x0 ] 
+   | x1 ⇒ match e2 with
+    [ x0 ⇒ x2 | x1 ⇒ x3 | x2 ⇒ x4 | x3 ⇒ x5 | x4 ⇒ x6 | x5 ⇒ x7 | x6 ⇒ x8 | x7 ⇒ x9
+    | x8 ⇒ xA | x9 ⇒ xB | xA ⇒ xC | xB ⇒ xD | xC ⇒ xE | xD ⇒ xF | xE ⇒ x0 | xF ⇒ x1 ] 
+   | x2 ⇒ match e2 with
+    [ x0 ⇒ x3 | x1 ⇒ x4 | x2 ⇒ x5 | x3 ⇒ x6 | x4 ⇒ x7 | x5 ⇒ x8 | x6 ⇒ x9 | x7 ⇒ xA
+    | x8 ⇒ xB | x9 ⇒ xC | xA ⇒ xD | xB ⇒ xE | xC ⇒ xF | xD ⇒ x0 | xE ⇒ x1 | xF ⇒ x2 ]
+   | x3 ⇒ match e2 with
+    [ x0 ⇒ x4 | x1 ⇒ x5 | x2 ⇒ x6 | x3 ⇒ x7 | x4 ⇒ x8 | x5 ⇒ x9 | x6 ⇒ xA | x7 ⇒ xB
+    | x8 ⇒ xC | x9 ⇒ xD | xA ⇒ xE | xB ⇒ xF | xC ⇒ x0 | xD ⇒ x1 | xE ⇒ x2 | xF ⇒ x3 ]
+   | x4 ⇒ match e2 with
+    [ x0 ⇒ x5 | x1 ⇒ x6 | x2 ⇒ x7 | x3 ⇒ x8 | x4 ⇒ x9 | x5 ⇒ xA | x6 ⇒ xB | x7 ⇒ xC
+    | x8 ⇒ xD | x9 ⇒ xE | xA ⇒ xF | xB ⇒ x0 | xC ⇒ x1 | xD ⇒ x2 | xE ⇒ x3 | xF ⇒ x4 ]
+   | x5 ⇒ match e2 with
+    [ x0 ⇒ x6 | x1 ⇒ x7 | x2 ⇒ x8 | x3 ⇒ x9 | x4 ⇒ xA | x5 ⇒ xB | x6 ⇒ xC | x7 ⇒ xD
+    | x8 ⇒ xE | x9 ⇒ xF | xA ⇒ x0 | xB ⇒ x1 | xC ⇒ x2 | xD ⇒ x3 | xE ⇒ x4 | xF ⇒ x5 ]
+   | x6 ⇒ match e2 with
+    [ x0 ⇒ x7 | x1 ⇒ x8 | x2 ⇒ x9 | x3 ⇒ xA | x4 ⇒ xB | x5 ⇒ xC | x6 ⇒ xD | x7 ⇒ xE
+    | x8 ⇒ xF | x9 ⇒ x0 | xA ⇒ x1 | xB ⇒ x2 | xC ⇒ x3 | xD ⇒ x4 | xE ⇒ x5 | xF ⇒ x6 ]
+   | x7 ⇒ match e2 with
+    [ x0 ⇒ x8 | x1 ⇒ x9 | x2 ⇒ xA | x3 ⇒ xB | x4 ⇒ xC | x5 ⇒ xD | x6 ⇒ xE | x7 ⇒ xF
+    | x8 ⇒ x0 | x9 ⇒ x1 | xA ⇒ x2 | xB ⇒ x3 | xC ⇒ x4 | xD ⇒ x5 | xE ⇒ x6 | xF ⇒ x7 ]
+   | x8 ⇒ match e2 with
+    [ x0 ⇒ x9 | x1 ⇒ xA | x2 ⇒ xB | x3 ⇒ xC | x4 ⇒ xD | x5 ⇒ xE | x6 ⇒ xF | x7 ⇒ x0
+    | x8 ⇒ x1 | x9 ⇒ x2 | xA ⇒ x3 | xB ⇒ x4 | xC ⇒ x5 | xD ⇒ x6 | xE ⇒ x7 | xF ⇒ x8 ]
+   | x9 ⇒ match e2 with
+    [ x0 ⇒ xA | x1 ⇒ xB | x2 ⇒ xC | x3 ⇒ xD | x4 ⇒ xE | x5 ⇒ xF | x6 ⇒ x0 | x7 ⇒ x1
+    | x8 ⇒ x2 | x9 ⇒ x3 | xA ⇒ x4 | xB ⇒ x5 | xC ⇒ x6 | xD ⇒ x7 | xE ⇒ x8 | xF ⇒ x9 ]
+   | xA ⇒ match e2 with
+    [ x0 ⇒ xB | x1 ⇒ xC | x2 ⇒ xD | x3 ⇒ xE | x4 ⇒ xF | x5 ⇒ x0 | x6 ⇒ x1 | x7 ⇒ x2
+    | x8 ⇒ x3 | x9 ⇒ x4 | xA ⇒ x5 | xB ⇒ x6 | xC ⇒ x7 | xD ⇒ x8 | xE ⇒ x9 | xF ⇒ xA ]
+   | xB ⇒ match e2 with
+    [ x0 ⇒ xC | x1 ⇒ xD | x2 ⇒ xE | x3 ⇒ xF | x4 ⇒ x0 | x5 ⇒ x1 | x6 ⇒ x2 | x7 ⇒ x3
+    | x8 ⇒ x4 | x9 ⇒ x5 | xA ⇒ x6 | xB ⇒ x7 | xC ⇒ x8 | xD ⇒ x9 | xE ⇒ xA | xF ⇒ xB ]
+   | xC ⇒ match e2 with
+     [ x0 ⇒ xD | x1 ⇒ xE | x2 ⇒ xF | x3 ⇒ x0 | x4 ⇒ x1 | x5 ⇒ x2 | x6 ⇒ x3 | x7 ⇒ x4
+    | x8 ⇒ x5 | x9 ⇒ x6 | xA ⇒ x7 | xB ⇒ x8 | xC ⇒ x9 | xD ⇒ xA | xE ⇒ xB | xF ⇒ xC ]
+   | xD ⇒ match e2 with
+    [ x0 ⇒ xE | x1 ⇒ xF | x2 ⇒ x0 | x3 ⇒ x1 | x4 ⇒ x2 | x5 ⇒ x3 | x6 ⇒ x4 | x7 ⇒ x5
+    | x8 ⇒ x6 | x9 ⇒ x7 | xA ⇒ x8 | xB ⇒ x9 | xC ⇒ xA | xD ⇒ xB | xE ⇒ xC | xF ⇒ xD ]
+   | xE ⇒ match e2 with
+    [ x0 ⇒ xF | x1 ⇒ x0 | x2 ⇒ x1 | x3 ⇒ x2 | x4 ⇒ x3 | x5 ⇒ x4 | x6 ⇒ x5 | x7 ⇒ x6
+    | x8 ⇒ x7 | x9 ⇒ x8 | xA ⇒ x9 | xB ⇒ xA | xC ⇒ xB | xD ⇒ xC | xE ⇒ xD | xF ⇒ xE ]
+   | xF ⇒ match e2 with
+    [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3 | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x6 | x7 ⇒ x7
+    | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ xA | xB ⇒ xB | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ]
+   ]
+  | false ⇒ match e1 with
+   [ x0 ⇒ match e2 with
+    [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3 | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x6 | x7 ⇒ x7
+    | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ xA | xB ⇒ xB | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ] 
+   | x1 ⇒ match e2 with
+    [ x0 ⇒ x1 | x1 ⇒ x2 | x2 ⇒ x3 | x3 ⇒ x4 | x4 ⇒ x5 | x5 ⇒ x6 | x6 ⇒ x7 | x7 ⇒ x8
+    | x8 ⇒ x9 | x9 ⇒ xA | xA ⇒ xB | xB ⇒ xC | xC ⇒ xD | xD ⇒ xE | xE ⇒ xF | xF ⇒ x0 ] 
+   | x2 ⇒ match e2 with
+    [ x0 ⇒ x2 | x1 ⇒ x3 | x2 ⇒ x4 | x3 ⇒ x5 | x4 ⇒ x6 | x5 ⇒ x7 | x6 ⇒ x8 | x7 ⇒ x9
+    | x8 ⇒ xA | x9 ⇒ xB | xA ⇒ xC | xB ⇒ xD | xC ⇒ xE | xD ⇒ xF | xE ⇒ x0 | xF ⇒ x1 ] 
+   | x3 ⇒ match e2 with
+    [ x0 ⇒ x3 | x1 ⇒ x4 | x2 ⇒ x5 | x3 ⇒ x6 | x4 ⇒ x7 | x5 ⇒ x8 | x6 ⇒ x9 | x7 ⇒ xA
+    | x8 ⇒ xB | x9 ⇒ xC | xA ⇒ xD | xB ⇒ xE | xC ⇒ xF | xD ⇒ x0 | xE ⇒ x1 | xF ⇒ x2 ]
+   | x4 ⇒ match e2 with
+    [ x0 ⇒ x4 | x1 ⇒ x5 | x2 ⇒ x6 | x3 ⇒ x7 | x4 ⇒ x8 | x5 ⇒ x9 | x6 ⇒ xA | x7 ⇒ xB
+    | x8 ⇒ xC | x9 ⇒ xD | xA ⇒ xE | xB ⇒ xF | xC ⇒ x0 | xD ⇒ x1 | xE ⇒ x2 | xF ⇒ x3 ]
+   | x5 ⇒ match e2 with
+    [ x0 ⇒ x5 | x1 ⇒ x6 | x2 ⇒ x7 | x3 ⇒ x8 | x4 ⇒ x9 | x5 ⇒ xA | x6 ⇒ xB | x7 ⇒ xC
+    | x8 ⇒ xD | x9 ⇒ xE | xA ⇒ xF | xB ⇒ x0 | xC ⇒ x1 | xD ⇒ x2 | xE ⇒ x3 | xF ⇒ x4 ]
+   | x6 ⇒ match e2 with
+    [ x0 ⇒ x6 | x1 ⇒ x7 | x2 ⇒ x8 | x3 ⇒ x9 | x4 ⇒ xA | x5 ⇒ xB | x6 ⇒ xC | x7 ⇒ xD
+    | x8 ⇒ xE | x9 ⇒ xF | xA ⇒ x0 | xB ⇒ x1 | xC ⇒ x2 | xD ⇒ x3 | xE ⇒ x4 | xF ⇒ x5 ]
+   | x7 ⇒ match e2 with
+    [ x0 ⇒ x7 | x1 ⇒ x8 | x2 ⇒ x9 | x3 ⇒ xA | x4 ⇒ xB | x5 ⇒ xC | x6 ⇒ xD | x7 ⇒ xE
+    | x8 ⇒ xF | x9 ⇒ x0 | xA ⇒ x1 | xB ⇒ x2 | xC ⇒ x3 | xD ⇒ x4 | xE ⇒ x5 | xF ⇒ x6 ]
+   | x8 ⇒ match e2 with
+    [ x0 ⇒ x8 | x1 ⇒ x9 | x2 ⇒ xA | x3 ⇒ xB | x4 ⇒ xC | x5 ⇒ xD | x6 ⇒ xE | x7 ⇒ xF
+    | x8 ⇒ x0 | x9 ⇒ x1 | xA ⇒ x2 | xB ⇒ x3 | xC ⇒ x4 | xD ⇒ x5 | xE ⇒ x6 | xF ⇒ x7 ]
+   | x9 ⇒ match e2 with
+    [ x0 ⇒ x9 | x1 ⇒ xA | x2 ⇒ xB | x3 ⇒ xC | x4 ⇒ xD | x5 ⇒ xE | x6 ⇒ xF | x7 ⇒ x0
+    | x8 ⇒ x1 | x9 ⇒ x2 | xA ⇒ x3 | xB ⇒ x4 | xC ⇒ x5 | xD ⇒ x6 | xE ⇒ x7 | xF ⇒ x8 ]
+   | xA ⇒ match e2 with
+    [ x0 ⇒ xA | x1 ⇒ xB | x2 ⇒ xC | x3 ⇒ xD | x4 ⇒ xE | x5 ⇒ xF | x6 ⇒ x0 | x7 ⇒ x1
+    | x8 ⇒ x2 | x9 ⇒ x3 | xA ⇒ x4 | xB ⇒ x5 | xC ⇒ x6 | xD ⇒ x7 | xE ⇒ x8 | xF ⇒ x9 ]
+   | xB ⇒ match e2 with
+    [ x0 ⇒ xB | x1 ⇒ xC | x2 ⇒ xD | x3 ⇒ xE | x4 ⇒ xF | x5 ⇒ x0 | x6 ⇒ x1 | x7 ⇒ x2
+    | x8 ⇒ x3 | x9 ⇒ x4 | xA ⇒ x5 | xB ⇒ x6 | xC ⇒ x7 | xD ⇒ x8 | xE ⇒ x9 | xF ⇒ xA ]
+   | xC ⇒ match e2 with
+    [ x0 ⇒ xC | x1 ⇒ xD | x2 ⇒ xE | x3 ⇒ xF | x4 ⇒ x0 | x5 ⇒ x1 | x6 ⇒ x2 | x7 ⇒ x3
+    | x8 ⇒ x4 | x9 ⇒ x5 | xA ⇒ x6 | xB ⇒ x7 | xC ⇒ x8 | xD ⇒ x9 | xE ⇒ xA | xF ⇒ xB ]
+   | xD ⇒ match e2 with
+     [ x0 ⇒ xD | x1 ⇒ xE | x2 ⇒ xF | x3 ⇒ x0 | x4 ⇒ x1 | x5 ⇒ x2 | x6 ⇒ x3 | x7 ⇒ x4
+    | x8 ⇒ x5 | x9 ⇒ x6 | xA ⇒ x7 | xB ⇒ x8 | xC ⇒ x9 | xD ⇒ xA | xE ⇒ xB | xF ⇒ xC ]
+   | xE ⇒ match e2 with
+    [ x0 ⇒ xE | x1 ⇒ xF | x2 ⇒ x0 | x3 ⇒ x1 | x4 ⇒ x2 | x5 ⇒ x3 | x6 ⇒ x4 | x7 ⇒ x5
+    | x8 ⇒ x6 | x9 ⇒ x7 | xA ⇒ x8 | xB ⇒ x9 | xC ⇒ xA | xD ⇒ xB | xE ⇒ xC | xF ⇒ xD ]
+   | xF ⇒ match e2 with
+    [ x0 ⇒ xF | x1 ⇒ x0 | x2 ⇒ x1 | x3 ⇒ x2 | x4 ⇒ x3 | x5 ⇒ x4 | x6 ⇒ x5 | x7 ⇒ x6
+    | x8 ⇒ x7 | x9 ⇒ x8 | xA ⇒ x9 | xB ⇒ xA | xC ⇒ xB | xD ⇒ xC | xE ⇒ xD | xF ⇒ xE ]
+   ]].
+
+(* operatore somma con data → data *)
+ndefinition plus_ex_d_d ≝
+λe1,e2:exadecim.
+ match e1 with
+  [ x0 ⇒ match e2 with
+   [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3 | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x6 | x7 ⇒ x7
+   | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ xA | xB ⇒ xB | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ] 
+  | x1 ⇒ match e2 with
+   [ x0 ⇒ x1 | x1 ⇒ x2 | x2 ⇒ x3 | x3 ⇒ x4 | x4 ⇒ x5 | x5 ⇒ x6 | x6 ⇒ x7 | x7 ⇒ x8
+   | x8 ⇒ x9 | x9 ⇒ xA | xA ⇒ xB | xB ⇒ xC | xC ⇒ xD | xD ⇒ xE | xE ⇒ xF | xF ⇒ x0 ] 
+  | x2 ⇒ match e2 with
+   [ x0 ⇒ x2 | x1 ⇒ x3 | x2 ⇒ x4 | x3 ⇒ x5 | x4 ⇒ x6 | x5 ⇒ x7 | x6 ⇒ x8 | x7 ⇒ x9
+   | x8 ⇒ xA | x9 ⇒ xB | xA ⇒ xC | xB ⇒ xD | xC ⇒ xE | xD ⇒ xF | xE ⇒ x0 | xF ⇒ x1 ] 
+  | x3 ⇒ match e2 with
+   [ x0 ⇒ x3 | x1 ⇒ x4 | x2 ⇒ x5 | x3 ⇒ x6 | x4 ⇒ x7 | x5 ⇒ x8 | x6 ⇒ x9 | x7 ⇒ xA
+   | x8 ⇒ xB | x9 ⇒ xC | xA ⇒ xD | xB ⇒ xE | xC ⇒ xF | xD ⇒ x0 | xE ⇒ x1 | xF ⇒ x2 ]
+  | x4 ⇒ match e2 with
+   [ x0 ⇒ x4 | x1 ⇒ x5 | x2 ⇒ x6 | x3 ⇒ x7 | x4 ⇒ x8 | x5 ⇒ x9 | x6 ⇒ xA | x7 ⇒ xB
+   | x8 ⇒ xC | x9 ⇒ xD | xA ⇒ xE | xB ⇒ xF | xC ⇒ x0 | xD ⇒ x1 | xE ⇒ x2 | xF ⇒ x3 ]
+  | x5 ⇒ match e2 with
+   [ x0 ⇒ x5 | x1 ⇒ x6 | x2 ⇒ x7 | x3 ⇒ x8 | x4 ⇒ x9 | x5 ⇒ xA | x6 ⇒ xB | x7 ⇒ xC
+   | x8 ⇒ xD | x9 ⇒ xE | xA ⇒ xF | xB ⇒ x0 | xC ⇒ x1 | xD ⇒ x2 | xE ⇒ x3 | xF ⇒ x4 ]
+  | x6 ⇒ match e2 with
+   [ x0 ⇒ x6 | x1 ⇒ x7 | x2 ⇒ x8 | x3 ⇒ x9 | x4 ⇒ xA | x5 ⇒ xB | x6 ⇒ xC | x7 ⇒ xD
+   | x8 ⇒ xE | x9 ⇒ xF | xA ⇒ x0 | xB ⇒ x1 | xC ⇒ x2 | xD ⇒ x3 | xE ⇒ x4 | xF ⇒ x5 ]
+  | x7 ⇒ match e2 with
+   [ x0 ⇒ x7 | x1 ⇒ x8 | x2 ⇒ x9 | x3 ⇒ xA | x4 ⇒ xB | x5 ⇒ xC | x6 ⇒ xD | x7 ⇒ xE
+   | x8 ⇒ xF | x9 ⇒ x0 | xA ⇒ x1 | xB ⇒ x2 | xC ⇒ x3 | xD ⇒ x4 | xE ⇒ x5 | xF ⇒ x6 ]
+  | x8 ⇒ match e2 with
+   [ x0 ⇒ x8 | x1 ⇒ x9 | x2 ⇒ xA | x3 ⇒ xB | x4 ⇒ xC | x5 ⇒ xD | x6 ⇒ xE | x7 ⇒ xF
+   | x8 ⇒ x0 | x9 ⇒ x1 | xA ⇒ x2 | xB ⇒ x3 | xC ⇒ x4 | xD ⇒ x5 | xE ⇒ x6 | xF ⇒ x7 ]
+  | x9 ⇒ match e2 with
+   [ x0 ⇒ x9 | x1 ⇒ xA | x2 ⇒ xB | x3 ⇒ xC | x4 ⇒ xD | x5 ⇒ xE | x6 ⇒ xF | x7 ⇒ x0
+   | x8 ⇒ x1 | x9 ⇒ x2 | xA ⇒ x3 | xB ⇒ x4 | xC ⇒ x5 | xD ⇒ x6 | xE ⇒ x7 | xF ⇒ x8 ]
+  | xA ⇒ match e2 with
+   [ x0 ⇒ xA | x1 ⇒ xB | x2 ⇒ xC | x3 ⇒ xD | x4 ⇒ xE | x5 ⇒ xF | x6 ⇒ x0 | x7 ⇒ x1
+   | x8 ⇒ x2 | x9 ⇒ x3 | xA ⇒ x4 | xB ⇒ x5 | xC ⇒ x6 | xD ⇒ x7 | xE ⇒ x8 | xF ⇒ x9 ]
+  | xB ⇒ match e2 with
+   [ x0 ⇒ xB | x1 ⇒ xC | x2 ⇒ xD | x3 ⇒ xE | x4 ⇒ xF | x5 ⇒ x0 | x6 ⇒ x1 | x7 ⇒ x2
+   | x8 ⇒ x3 | x9 ⇒ x4 | xA ⇒ x5 | xB ⇒ x6 | xC ⇒ x7 | xD ⇒ x8 | xE ⇒ x9 | xF ⇒ xA ]
+  | xC ⇒ match e2 with
+   [ x0 ⇒ xC | x1 ⇒ xD | x2 ⇒ xE | x3 ⇒ xF | x4 ⇒ x0 | x5 ⇒ x1 | x6 ⇒ x2 | x7 ⇒ x3
+   | x8 ⇒ x4 | x9 ⇒ x5 | xA ⇒ x6 | xB ⇒ x7 | xC ⇒ x8 | xD ⇒ x9 | xE ⇒ xA | xF ⇒ xB ]
+  | xD ⇒ match e2 with
+   [ x0 ⇒ xD | x1 ⇒ xE | x2 ⇒ xF | x3 ⇒ x0 | x4 ⇒ x1 | x5 ⇒ x2 | x6 ⇒ x3 | x7 ⇒ x4
+   | x8 ⇒ x5 | x9 ⇒ x6 | xA ⇒ x7 | xB ⇒ x8 | xC ⇒ x9 | xD ⇒ xA | xE ⇒ xB | xF ⇒ xC ]
+  | xE ⇒ match e2 with
+   [ x0 ⇒ xE | x1 ⇒ xF | x2 ⇒ x0 | x3 ⇒ x1 | x4 ⇒ x2 | x5 ⇒ x3 | x6 ⇒ x4 | x7 ⇒ x5
+   | x8 ⇒ x6 | x9 ⇒ x7 | xA ⇒ x8 | xB ⇒ x9 | xC ⇒ xA | xD ⇒ xB | xE ⇒ xC | xF ⇒ xD ]
+  | xF ⇒ match e2 with
+   [ x0 ⇒ xF | x1 ⇒ x0 | x2 ⇒ x1 | x3 ⇒ x2 | x4 ⇒ x3 | x5 ⇒ x4 | x6 ⇒ x5 | x7 ⇒ x6
+   | x8 ⇒ x7 | x9 ⇒ x8 | xA ⇒ x9 | xB ⇒ xA | xC ⇒ xB | xD ⇒ xC | xE ⇒ xD | xF ⇒ xE ]
+  ].
+
+(* operatore somma con data+carry → carry *)
+ndefinition plus_ex_dc_c ≝
+λe1,e2:exadecim.λc:bool.
+ match c with
+  [ true ⇒ match e1 with
+   [ x0 ⇒ match e2 with
+    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ true  ] 
+   | x1 ⇒ match e2 with
+    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ false | xD ⇒ false | xE ⇒ true  | xF ⇒ true  ] 
+   | x2 ⇒ match e2 with
+    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ false | xD ⇒ true  | xE ⇒ true  | xF ⇒ true  ] 
+   | x3 ⇒ match e2 with
+    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true  ] 
+   | x4 ⇒ match e2 with
+    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ true  | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true  ] 
+   | x5 ⇒ match e2 with
+    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+    | x8 ⇒ false | x9 ⇒ false | xA ⇒ true  | xB ⇒ true  | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true  ] 
+   | x6 ⇒ match e2 with
+    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+    | x8 ⇒ false | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true  | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true  ] 
+   | x7 ⇒ match e2 with
+    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+    | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true  | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true  ] 
+   | x8 ⇒ match e2 with
+    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ true
+    | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true  | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true  ] 
+   | x9 ⇒ match e2 with
+    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ true  | x7 ⇒ true
+    | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true  | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true  ] 
+   | xA ⇒ match e2 with
+    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
+    | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true  | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true  ] 
+   | xB ⇒ match e2 with
+    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
+    | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true  | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true  ] 
+   | xC ⇒ match e2 with
+    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ true  | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
+    | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true  | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true  ] 
+   | xD ⇒ match e2 with
+    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ true  | x3 ⇒ true  | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
+    | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true  | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true  ] 
+   | xE ⇒ match e2 with
+    [ x0 ⇒ false | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true  | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
+    | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true  | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true  ]
+   | xF ⇒ match e2 with
+    [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true  | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
+    | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true  | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true  ]  
+   ]
+  | false ⇒ match e1 with
+   [ x0 ⇒ match e2 with
+    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] 
+   | x1 ⇒ match e2 with
+    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ true  ] 
+   | x2 ⇒ match e2 with
+    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ false | xD ⇒ false | xE ⇒ true  | xF ⇒ true  ] 
+   | x3 ⇒ match e2 with
+    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ false | xD ⇒ true  | xE ⇒ true  | xF ⇒ true  ] 
+   | x4 ⇒ match e2 with
+    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true  ] 
+   | x5 ⇒ match e2 with
+    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+    | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ true  | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true  ] 
+   | x6 ⇒ match e2 with
+    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+    | x8 ⇒ false | x9 ⇒ false | xA ⇒ true  | xB ⇒ true  | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true  ] 
+   | x7 ⇒ match e2 with
+    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+    | x8 ⇒ false | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true  | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true  ] 
+   | x8 ⇒ match e2 with
+    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+    | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true  | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true  ] 
+   | x9 ⇒ match e2 with
+    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ true
+    | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true  | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true  ] 
+   | xA ⇒ match e2 with
+    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ true  | x7 ⇒ true
+    | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true  | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true  ] 
+   | xB ⇒ match e2 with
+    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
+    | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true  | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true  ] 
+   | xC ⇒ match e2 with
+    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
+    | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true  | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true  ] 
+   | xD ⇒ match e2 with
+    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ true  | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
+    | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true  | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true  ] 
+   | xE ⇒ match e2 with
+    [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ true  | x3 ⇒ true  | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
+    | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true  | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true  ] 
+   | xF ⇒ match e2 with
+    [ x0 ⇒ false | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true  | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
+    | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true  | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true  ] 
+   ]].
 
-(* operatore carry della somma *)
-ndefinition plus_exc ≝
-λe1,e2:exadecim.snd ?? (plus_ex e1 e2 false).
+(* operatore somma con data → carry *)
+ndefinition plus_ex_d_c ≝
+λe1,e2:exadecim.
+ match e1 with
+  [ x0 ⇒ match e2 with
+   [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+   | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] 
+  | x1 ⇒ match e2 with
+   [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+   | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ true  ] 
+  | x2 ⇒ match e2 with
+   [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+   | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ false | xD ⇒ false | xE ⇒ true  | xF ⇒ true  ] 
+  | x3 ⇒ match e2 with
+   [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+   | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ false | xD ⇒ true  | xE ⇒ true  | xF ⇒ true  ] 
+  | x4 ⇒ match e2 with
+   [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+   | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true  ] 
+  | x5 ⇒ match e2 with
+   [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+   | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ true  | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true  ] 
+  | x6 ⇒ match e2 with
+   [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+   | x8 ⇒ false | x9 ⇒ false | xA ⇒ true  | xB ⇒ true  | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true  ] 
+  | x7 ⇒ match e2 with
+   [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+   | x8 ⇒ false | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true  | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true  ] 
+  | x8 ⇒ match e2 with
+   [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+   | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true  | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true  ] 
+  | x9 ⇒ match e2 with
+   [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ true
+   | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true  | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true  ] 
+  | xA ⇒ match e2 with
+   [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ true  | x7 ⇒ true
+   | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true  | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true  ] 
+  | xB ⇒ match e2 with
+   [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
+   | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true  | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true  ] 
+  | xC ⇒ match e2 with
+   [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
+   | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true  | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true  ] 
+  | xD ⇒ match e2 with
+   [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ true  | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
+   | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true  | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true  ] 
+  | xE ⇒ match e2 with
+   [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ true  | x3 ⇒ true  | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
+   | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true  | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true  ] 
+  | xF ⇒ match e2 with
+   [ x0 ⇒ false | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true  | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
+   | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ true  | xB ⇒ true  | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true  ] 
+  ].
 
 (* operatore Most Significant Bit *)
 ndefinition MSB_ex ≝