Release 0.5.9.

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

(**************************************************************************)
(*       ___                                                              *)
(*      ||M||                                                             *)
(*      ||A||       A project by Andrea Asperti                           *)
(*      ||T||                                                             *)
(*      ||I||       Developers:                                           *)
(*      ||T||         The HELM team.                                      *)
(*      ||A||         http://helm.cs.unibo.it                             *)
(*      \   /                                                             *)
(*       \ /        This file is distributed under the terms of the       *)
(*        v         GNU General Public License Version 2                  *)
(*                                                                        *)
(**************************************************************************)

(* ********************************************************************** *)
(*                          Progetto FreeScale                            *)
(*                                                                        *)
(*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
(*   Ultima modifica: 05/08/2009                                          *)
(*                                                                        *)
(* ********************************************************************** *)

include "num/bool.ma".
include "num/quatern.ma".
include "num/oct.ma".
include "common/prod.ma".
include "common/nat.ma".

(* *********** *)
(* ESADECIMALI *)
(* *********** *)

ninductive exadecim : Type ≝
  x0: exadecim
| x1: exadecim
| x2: exadecim
| x3: exadecim
| x4: exadecim
| x5: exadecim
| x6: exadecim
| x7: exadecim
| x8: exadecim
| x9: exadecim
| xA: exadecim
| xB: exadecim
| xC: exadecim
| xD: exadecim
| xE: exadecim
| xF: exadecim.

(* operatore = *)
ndefinition eq_ex ≝
λe1,e2:exadecim.
 match e1 with
  [ x0 ⇒ match e2 with [ x0 ⇒ true  | _ ⇒ false ]
  | x1 ⇒ match e2 with [ x1 ⇒ true  | _ ⇒ false ]
  | x2 ⇒ match e2 with [ x2 ⇒ true  | _ ⇒ false ]
  | x3 ⇒ match e2 with [ x3 ⇒ true  | _ ⇒ false ]
  | x4 ⇒ match e2 with [ x4 ⇒ true  | _ ⇒ false ]
  | x5 ⇒ match e2 with [ x5 ⇒ true  | _ ⇒ false ]
  | x6 ⇒ match e2 with [ x6 ⇒ true  | _ ⇒ false ]
  | x7 ⇒ match e2 with [ x7 ⇒ true  | _ ⇒ false ]
  | x8 ⇒ match e2 with [ x8 ⇒ true  | _ ⇒ false ]
  | x9 ⇒ match e2 with [ x9 ⇒ true  | _ ⇒ false ]
  | xA ⇒ match e2 with [ xA ⇒ true  | _ ⇒ false ]
  | xB ⇒ match e2 with [ xB ⇒ true  | _ ⇒ false ]
  | xC ⇒ match e2 with [ xC ⇒ true  | _ ⇒ false ]
  | xD ⇒ match e2 with [ xD ⇒ true  | _ ⇒ false ]
  | xE ⇒ match e2 with [ xE ⇒ true  | _ ⇒ false ]
  | xF ⇒ match e2 with [ xF ⇒ true  | _ ⇒ false ]
  ].

(* operatore < *)
ndefinition lt_ex ≝
λe1,e2:exadecim.
 match e1 with
  [ x0 ⇒ 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 ] 
  | x1 ⇒ 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 ] 
  | x2 ⇒ 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 ] 
  | x3 ⇒ 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 ] 
  | x4 ⇒ 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 ] 
  | x5 ⇒ 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 ] 
  | x6 ⇒ 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 ] 
  | 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 ⇒ false
   | x8 ⇒ false | 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 ⇒ false
   | x8 ⇒ false | x9 ⇒ false | 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 ⇒ false | x7 ⇒ false
   | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | 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 ⇒ false | x6 ⇒ false | x7 ⇒ false
   | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false 
   | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true ] 
  | xC ⇒ 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 ] 
  | xD ⇒ 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 ] 
  | xE ⇒ 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 ] 
  | xF ⇒ 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 ]
  ].

(* operatore ≤ *)
ndefinition le_ex ≝
λe1,e2:exadecim.
 match e1 with
  [ x0 ⇒ 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 ] 
  | x1 ⇒ 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 ] 
  | x2 ⇒ 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 ] 
  | x3 ⇒ 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 ] 
  | x4 ⇒ 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 ] 
  | x5 ⇒ 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 ] 
  | x6 ⇒ 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 ] 
  | x7 ⇒ 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 ] 
  | 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 ⇒ false
   | x8 ⇒ false | 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 ⇒ false | x7 ⇒ false
   | x8 ⇒ false | x9 ⇒ false | 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 ⇒ false | x6 ⇒ false | x7 ⇒ false
   | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ true 
   | xC ⇒ true  | xD ⇒ true  | xE ⇒ true  | xF ⇒ true ] 
  | xC ⇒ 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 ] 
  | xD ⇒ 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 ] 
  | xE ⇒ 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 ] 
  | xF ⇒ 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 ]
  ].

(* operatore > *)
ndefinition gt_ex ≝
λ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 ⇒ true  | 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 ] 
  | x2 ⇒ match e2 with
   [ x0 ⇒ true  | x1 ⇒ true  | 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 ] 
  | x3 ⇒ match e2 with
   [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | 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 ] 
  | x4 ⇒ match e2 with
   [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true 
   | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
   | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false 
   | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] 
  | x5 ⇒ match e2 with
   [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true 
   | x4 ⇒ true  | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
   | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false 
   | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] 
  | x6 ⇒ match e2 with
   [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true 
   | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ false | x7 ⇒ false
   | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false 
   | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] 
  | x7 ⇒ match e2 with
   [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true 
   | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ false
   | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false 
   | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
  | x8 ⇒ match e2 with
   [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true 
   | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
   | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false 
   | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
  | x9 ⇒ match e2 with
   [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true 
   | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
   | x8 ⇒ true  | x9 ⇒ false | xA ⇒ false | xB ⇒ false 
   | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
  | xA ⇒ match e2 with
   [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true 
   | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
   | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ false | xB ⇒ false 
   | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
  | xB ⇒ 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 ⇒ false 
   | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
  | xC ⇒ 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 ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
  | xD ⇒ 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 ⇒ false | xE ⇒ false | xF ⇒ false ]
  | xE ⇒ 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 ⇒ false | xF ⇒ false ]
  | 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 ⇒ false ]
  ].

(* operatore ≥ *)
ndefinition ge_ex ≝
λe1,e2:exadecim.
 match e1 with
  [ x0 ⇒ match e2 with
   [ x0 ⇒ true  | 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 ⇒ true  | x1 ⇒ true  | 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 ] 
  | x2 ⇒ match e2 with
   [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | 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 ] 
  | x3 ⇒ match e2 with
   [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true 
   | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
   | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false 
   | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] 
  | x4 ⇒ match e2 with
   [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true 
   | x4 ⇒ true  | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
   | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false 
   | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] 
  | x5 ⇒ match e2 with
   [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true 
   | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ false | x7 ⇒ false
   | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false 
   | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] 
  | x6 ⇒ match e2 with
   [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true 
   | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ false
   | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false 
   | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ] 
  | x7 ⇒ match e2 with
   [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true 
   | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
   | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false 
   | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
  | x8 ⇒ match e2 with
   [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true 
   | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
   | x8 ⇒ true  | x9 ⇒ false | xA ⇒ false | xB ⇒ false 
   | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
  | x9 ⇒ match e2 with
   [ x0 ⇒ true  | x1 ⇒ true  | x2 ⇒ true  | x3 ⇒ true 
   | x4 ⇒ true  | x5 ⇒ true  | x6 ⇒ true  | x7 ⇒ true
   | x8 ⇒ true  | x9 ⇒ true  | xA ⇒ false | xB ⇒ false 
   | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
  | xA ⇒ 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 ⇒ false 
   | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
  | xB ⇒ 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 ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
  | xC ⇒ 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 ⇒ false | xE ⇒ false | xF ⇒ false ]
  | xD ⇒ 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 ⇒ false | xF ⇒ false ]
  | xE ⇒ 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 ⇒ false ]
  | 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 ]
  ].

(* operatore and *)
ndefinition and_ex ≝
λe1,e2:exadecim.match e1 with
 [ x0 ⇒ match e2 with
  [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x0 | x3 ⇒ x0 
  | x4 ⇒ x0 | x5 ⇒ x0 | x6 ⇒ x0 | x7 ⇒ x0
  | x8 ⇒ x0 | x9 ⇒ x0 | xA ⇒ x0 | xB ⇒ x0 
  | xC ⇒ x0 | xD ⇒ x0 | xE ⇒ x0 | xF ⇒ x0 ]
 | x1 ⇒ match e2 with
  [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x0 | x3 ⇒ x1 
  | x4 ⇒ x0 | x5 ⇒ x1 | x6 ⇒ x0 | x7 ⇒ x1
  | x8 ⇒ x0 | x9 ⇒ x1 | xA ⇒ x0 | xB ⇒ x1 
  | xC ⇒ x0 | xD ⇒ x1 | xE ⇒ x0 | xF ⇒ x1 ]
 | x2 ⇒ match e2 with
  [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x2 | x3 ⇒ x2 
  | x4 ⇒ x0 | x5 ⇒ x0 | x6 ⇒ x2 | x7 ⇒ x2
  | x8 ⇒ x0 | x9 ⇒ x0 | xA ⇒ x2 | xB ⇒ x2 
  | xC ⇒ x0 | xD ⇒ x0 | xE ⇒ x2 | xF ⇒ x2 ]
 | x3 ⇒ match e2 with
  [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3 
  | x4 ⇒ x0 | x5 ⇒ x1 | x6 ⇒ x2 | x7 ⇒ x3
  | x8 ⇒ x0 | x9 ⇒ x1 | xA ⇒ x2 | xB ⇒ x3 
  | xC ⇒ x0 | xD ⇒ x1 | xE ⇒ x2 | xF ⇒ x3 ]
 | x4 ⇒ match e2 with
  [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x0 | x3 ⇒ x0 
  | x4 ⇒ x4 | x5 ⇒ x4 | x6 ⇒ x4 | x7 ⇒ x4
  | x8 ⇒ x0 | x9 ⇒ x0 | xA ⇒ x0 | xB ⇒ x0 
  | xC ⇒ x4 | xD ⇒ x4 | xE ⇒ x4 | xF ⇒ x4 ]
 | x5 ⇒ match e2 with
  [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x0 | x3 ⇒ x1 
  | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x4 | x7 ⇒ x5
  | x8 ⇒ x0 | x9 ⇒ x1 | xA ⇒ x0 | xB ⇒ x1 
  | xC ⇒ x4 | xD ⇒ x5 | xE ⇒ x4 | xF ⇒ x5 ]
 | x6 ⇒ match e2 with
  [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x2 | x3 ⇒ x2 
  | x4 ⇒ x4 | x5 ⇒ x4 | x6 ⇒ x6 | x7 ⇒ x6
  | x8 ⇒ x0 | x9 ⇒ x0 | xA ⇒ x2 | xB ⇒ x2 
  | xC ⇒ x4 | xD ⇒ x4 | xE ⇒ x6 | xF ⇒ x6 ]
 | x7 ⇒ match e2 with
  [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3 
  | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x6 | x7 ⇒ x7
  | x8 ⇒ x0 | x9 ⇒ x1 | xA ⇒ x2 | xB ⇒ x3 
  | xC ⇒ x4 | xD ⇒ x5 | xE ⇒ x6 | xF ⇒ x7 ]
 | x8 ⇒ match e2 with
  [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x0 | x3 ⇒ x0 
  | x4 ⇒ x0 | x5 ⇒ x0 | x6 ⇒ x0 | x7 ⇒ x0
  | x8 ⇒ x8 | x9 ⇒ x8 | xA ⇒ x8 | xB ⇒ x8 
  | xC ⇒ x8 | xD ⇒ x8 | xE ⇒ x8 | xF ⇒ x8 ]
 | x9 ⇒ match e2 with
  [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x0 | x3 ⇒ x1 
  | x4 ⇒ x0 | x5 ⇒ x1 | x6 ⇒ x0 | x7 ⇒ x1
  | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ x8 | xB ⇒ x9 
  | xC ⇒ x8 | xD ⇒ x9 | xE ⇒ x8 | xF ⇒ x9 ]
 | xA ⇒ match e2 with
  [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x2 | x3 ⇒ x2 
  | x4 ⇒ x0 | x5 ⇒ x0 | x6 ⇒ x2 | x7 ⇒ x2
  | x8 ⇒ x8 | x9 ⇒ x8 | xA ⇒ xA | xB ⇒ xA 
  | xC ⇒ x8 | xD ⇒ x8 | xE ⇒ xA | xF ⇒ xA ]
 | xB ⇒ match e2 with
  [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3 
  | x4 ⇒ x0 | x5 ⇒ x1 | x6 ⇒ x2 | x7 ⇒ x3
  | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ xA | xB ⇒ xB 
  | xC ⇒ x8 | xD ⇒ x9 | xE ⇒ xA | xF ⇒ xB ]
 | xC ⇒ match e2 with
  [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x0 | x3 ⇒ x0 
  | x4 ⇒ x4 | x5 ⇒ x4 | x6 ⇒ x4 | x7 ⇒ x4
  | x8 ⇒ x8 | x9 ⇒ x8 | xA ⇒ x8 | xB ⇒ x8 
  | xC ⇒ xC | xD ⇒ xC | xE ⇒ xC | xF ⇒ xC ] 
 | xD ⇒ match e2 with
  [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x0 | x3 ⇒ x1 
  | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x4 | x7 ⇒ x5
  | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ x8 | xB ⇒ x9 
  | xC ⇒ xC | xD ⇒ xD | xE ⇒ xC | xF ⇒ xD ] 
 | xE ⇒ match e2 with
  [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x2 | x3 ⇒ x2 
  | x4 ⇒ x4 | x5 ⇒ x4 | x6 ⇒ x6 | x7 ⇒ x6
  | x8 ⇒ x8 | x9 ⇒ x8 | xA ⇒ xA | xB ⇒ xA 
  | xC ⇒ xC | xD ⇒ xC | xE ⇒ xE | 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 ]
 ]. 

(* operatore or *)
ndefinition or_ex ≝
λ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 ⇒ x1 | x2 ⇒ x3 | x3 ⇒ x3 
  | x4 ⇒ x5 | x5 ⇒ x5 | x6 ⇒ x7 | x7 ⇒ x7
  | x8 ⇒ x9 | x9 ⇒ x9 | xA ⇒ xB | xB ⇒ xB 
  | xC ⇒ xD | xD ⇒ xD | xE ⇒ xF | xF ⇒ xF ]
 | x2 ⇒ match e2 with
  [ x0 ⇒ x2 | x1 ⇒ x3 | x2 ⇒ x2 | x3 ⇒ x3 
  | x4 ⇒ x6 | x5 ⇒ x7 | x6 ⇒ x6 | x7 ⇒ x7
  | x8 ⇒ xA | x9 ⇒ xB | xA ⇒ xA | xB ⇒ xB 
  | xC ⇒ xE | xD ⇒ xF | xE ⇒ xE | xF ⇒ xF ]
 | x3 ⇒ match e2 with
  [ x0 ⇒ x3 | x1 ⇒ x3 | x2 ⇒ x3 | x3 ⇒ x3 
  | x4 ⇒ x7 | x5 ⇒ x7 | x6 ⇒ x7 | x7 ⇒ x7
  | x8 ⇒ xB | x9 ⇒ xB | xA ⇒ xB | xB ⇒ xB 
  | xC ⇒ xF | xD ⇒ xF | xE ⇒ xF | xF ⇒ xF ]
 | x4 ⇒ match e2 with
  [ x0 ⇒ x4 | x1 ⇒ x5 | x2 ⇒ x6 | x3 ⇒ x7 
  | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x6 | x7 ⇒ x7
  | x8 ⇒ xC | x9 ⇒ xD | xA ⇒ xE | xB ⇒ xF 
  | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ]
 | x5 ⇒ match e2 with
  [ x0 ⇒ x5 | x1 ⇒ x5 | x2 ⇒ x7 | x3 ⇒ x7 
  | x4 ⇒ x5 | x5 ⇒ x5 | x6 ⇒ x7 | x7 ⇒ x7
  | x8 ⇒ xD | x9 ⇒ xD | xA ⇒ xF | xB ⇒ xF 
  | xC ⇒ xD | xD ⇒ xD | xE ⇒ xF | xF ⇒ xF ]
 | x6 ⇒ match e2 with
  [ x0 ⇒ x6 | x1 ⇒ x7 | x2 ⇒ x6 | x3 ⇒ x7 
  | x4 ⇒ x6 | x5 ⇒ x7 | x6 ⇒ x6 | x7 ⇒ x7
  | x8 ⇒ xE | x9 ⇒ xF | xA ⇒ xE | xB ⇒ xF 
  | xC ⇒ xE | xD ⇒ xF | xE ⇒ xE | xF ⇒ xF ]
 | x7 ⇒ match e2 with
  [ x0 ⇒ x7 | x1 ⇒ x7 | x2 ⇒ x7 | x3 ⇒ x7 
  | x4 ⇒ x7 | x5 ⇒ x7 | x6 ⇒ x7 | x7 ⇒ x7
  | x8 ⇒ xF | x9 ⇒ xF | xA ⇒ xF | xB ⇒ xF 
  | xC ⇒ xF | xD ⇒ xF | xE ⇒ xF | xF ⇒ xF ]
 | x8 ⇒ match e2 with
  [ x0 ⇒ x8 | x1 ⇒ x9 | x2 ⇒ xA | x3 ⇒ xB 
  | x4 ⇒ xC | x5 ⇒ xD | x6 ⇒ xE | x7 ⇒ xF
  | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ xA | xB ⇒ xB 
  | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ]
 | x9 ⇒ match e2 with
  [ x0 ⇒ x9 | x1 ⇒ x9 | x2 ⇒ xB | x3 ⇒ xB 
  | x4 ⇒ xD | x5 ⇒ xD | x6 ⇒ xF | x7 ⇒ xF
  | x8 ⇒ x9 | x9 ⇒ x9 | xA ⇒ xB | xB ⇒ xB 
  | xC ⇒ xD | xD ⇒ xD | xE ⇒ xF | xF ⇒ xF ]
 | xA ⇒ match e2 with
  [ x0 ⇒ xA | x1 ⇒ xB | x2 ⇒ xA | x3 ⇒ xB 
  | x4 ⇒ xE | x5 ⇒ xF | x6 ⇒ xE | x7 ⇒ xF
  | x8 ⇒ xA | x9 ⇒ xB | xA ⇒ xA | xB ⇒ xB 
  | xC ⇒ xE | xD ⇒ xF | xE ⇒ xE | xF ⇒ xF ]
 | xB ⇒ match e2 with
  [ x0 ⇒ xB | x1 ⇒ xB | x2 ⇒ xB | x3 ⇒ xB 
  | x4 ⇒ xF | x5 ⇒ xF | x6 ⇒ xF | x7 ⇒ xF
  | x8 ⇒ xB | x9 ⇒ xB | xA ⇒ xB | xB ⇒ xB 
  | xC ⇒ xF | xD ⇒ xF | xE ⇒ xF | xF ⇒ xF ]
 | xC ⇒ match e2 with
  [ x0 ⇒ xC | x1 ⇒ xD | x2 ⇒ xE | x3 ⇒ xF 
  | x4 ⇒ xC | x5 ⇒ xD | x6 ⇒ xE | x7 ⇒ xF
  | x8 ⇒ xC | x9 ⇒ xD | xA ⇒ xE | xB ⇒ xF 
  | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ]
 | xD ⇒ match e2 with
  [ x0 ⇒ xD | x1 ⇒ xD | x2 ⇒ xF | x3 ⇒ xF 
  | x4 ⇒ xD | x5 ⇒ xD | x6 ⇒ xF | x7 ⇒ xF
  | x8 ⇒ xD | x9 ⇒ xD | xA ⇒ xF | xB ⇒ xF 
  | xC ⇒ xD | xD ⇒ xD | xE ⇒ xF | xF ⇒ xF ]
 | xE ⇒ match e2 with
  [ x0 ⇒ xE | x1 ⇒ xF | x2 ⇒ xE | x3 ⇒ xF 
  | x4 ⇒ xE | x5 ⇒ xF | x6 ⇒ xE | x7 ⇒ xF
  | x8 ⇒ xE | x9 ⇒ xF | xA ⇒ xE | xB ⇒ xF 
  | xC ⇒ xE | xD ⇒ xF | xE ⇒ xE | xF ⇒ xF ]
 | xF ⇒ match e2 with
  [ x0 ⇒ xF | x1 ⇒ xF | x2 ⇒ xF | x3 ⇒ xF 
  | x4 ⇒ xF | x5 ⇒ xF | x6 ⇒ xF | x7 ⇒ xF
  | x8 ⇒ xF | x9 ⇒ xF | xA ⇒ xF | xB ⇒ xF 
  | xC ⇒ xF | xD ⇒ xF | xE ⇒ xF | xF ⇒ xF ]
 ].

(* operatore xor *)
ndefinition xor_ex ≝
λ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 ⇒ x0 | x2 ⇒ x3 | x3 ⇒ x2 
  | x4 ⇒ x5 | x5 ⇒ x4 | x6 ⇒ x7 | x7 ⇒ x6
  | x8 ⇒ x9 | x9 ⇒ x8 | xA ⇒ xB | xB ⇒ xA 
  | xC ⇒ xD | xD ⇒ xC | xE ⇒ xF | xF ⇒ xE ] 
 | x2 ⇒ match e2 with
  [ x0 ⇒ x2 | x1 ⇒ x3 | x2 ⇒ x0 | x3 ⇒ x1 
  | x4 ⇒ x6 | x5 ⇒ x7 | x6 ⇒ x4 | x7 ⇒ x5
  | x8 ⇒ xA | x9 ⇒ xB | xA ⇒ x8 | xB ⇒ x9 
  | xC ⇒ xE | xD ⇒ xF | xE ⇒ xC | xF ⇒ xD ] 
 | x3 ⇒ match e2 with
  [ x0 ⇒ x3 | x1 ⇒ x2 | x2 ⇒ x1 | x3 ⇒ x0 
  | x4 ⇒ x7 | x5 ⇒ x6 | x6 ⇒ x5 | x7 ⇒ x4
  | x8 ⇒ xB | x9 ⇒ xA | xA ⇒ x9 | xB ⇒ x8 
  | xC ⇒ xF | xD ⇒ xE | xE ⇒ xD | xF ⇒ xC ] 
 | x4 ⇒ match e2 with
  [ x0 ⇒ x4 | x1 ⇒ x5 | x2 ⇒ x6 | x3 ⇒ x7 
  | x4 ⇒ x0 | x5 ⇒ x1 | x6 ⇒ x2 | x7 ⇒ x3
  | x8 ⇒ xC | x9 ⇒ xD | xA ⇒ xE | xB ⇒ xF 
  | xC ⇒ x8 | xD ⇒ x9 | xE ⇒ xA | xF ⇒ xB ] 
 | x5 ⇒ match e2 with
  [ x0 ⇒ x5 | x1 ⇒ x4 | x2 ⇒ x7 | x3 ⇒ x6 
  | x4 ⇒ x1 | x5 ⇒ x0 | x6 ⇒ x3 | x7 ⇒ x2
  | x8 ⇒ xD | x9 ⇒ xC | xA ⇒ xF | xB ⇒ xE 
  | xC ⇒ x9 | xD ⇒ x8 | xE ⇒ xB | xF ⇒ xA ] 
 | x6 ⇒ match e2 with
  [ x0 ⇒ x6 | x1 ⇒ x7 | x2 ⇒ x4 | x3 ⇒ x5 
  | x4 ⇒ x2 | x5 ⇒ x3 | x6 ⇒ x0 | x7 ⇒ x1
  | x8 ⇒ xE | x9 ⇒ xF | xA ⇒ xC | xB ⇒ xD 
  | xC ⇒ xA | xD ⇒ xB | xE ⇒ x8 | xF ⇒ x9 ] 
 | x7 ⇒ match e2 with
  [ x0 ⇒ x7 | x1 ⇒ x6 | x2 ⇒ x5 | x3 ⇒ x4 
  | x4 ⇒ x3 | x5 ⇒ x2 | x6 ⇒ x1 | x7 ⇒ x0
  | x8 ⇒ xF | x9 ⇒ xE | xA ⇒ xD | xB ⇒ xC 
  | xC ⇒ xB | xD ⇒ xA | xE ⇒ x9 | xF ⇒ x8 ] 
 | 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 ⇒ x8 | x2 ⇒ xB | x3 ⇒ xA 
  | x4 ⇒ xD | x5 ⇒ xC | x6 ⇒ xF | x7 ⇒ xE
  | x8 ⇒ x1 | x9 ⇒ x0 | xA ⇒ x3 | xB ⇒ x2 
  | xC ⇒ x5 | xD ⇒ x4 | xE ⇒ x7 | xF ⇒ x6 ] 
 | xA ⇒ match e2 with
  [ x0 ⇒ xA | x1 ⇒ xB | x2 ⇒ x8 | x3 ⇒ x9 
  | x4 ⇒ xE | x5 ⇒ xF | x6 ⇒ xC | x7 ⇒ xD
  | x8 ⇒ x2 | x9 ⇒ x3 | xA ⇒ x0 | xB ⇒ x1 
  | xC ⇒ x6 | xD ⇒ x7 | xE ⇒ x4 | xF ⇒ x5 ] 
 | xB ⇒ match e2 with
  [ x0 ⇒ xB | x1 ⇒ xA | x2 ⇒ x9 | x3 ⇒ x8 
  | x4 ⇒ xF | x5 ⇒ xE | x6 ⇒ xD | x7 ⇒ xC
  | x8 ⇒ x3 | x9 ⇒ x2 | xA ⇒ x1 | xB ⇒ x0 
  | xC ⇒ x7 | xD ⇒ x6 | xE ⇒ x5 | xF ⇒ x4 ]
 | xC ⇒ match e2 with
  [ x0 ⇒ xC | x1 ⇒ xD | x2 ⇒ xE | x3 ⇒ xF 
  | x4 ⇒ x8 | x5 ⇒ x9 | x6 ⇒ xA | x7 ⇒ xB
  | x8 ⇒ x4 | x9 ⇒ x5 | xA ⇒ x6 | xB ⇒ x7 
  | xC ⇒ x0 | xD ⇒ x1 | xE ⇒ x2 | xF ⇒ x3 ] 
 | xD ⇒ match e2 with
  [ x0 ⇒ xD | x1 ⇒ xC | x2 ⇒ xF | x3 ⇒ xE 
  | x4 ⇒ x9 | x5 ⇒ x8 | x6 ⇒ xB | x7 ⇒ xA
  | x8 ⇒ x5 | x9 ⇒ x4 | xA ⇒ x7 | xB ⇒ x6 
  | xC ⇒ x1 | xD ⇒ x0 | xE ⇒ x3 | xF ⇒ x2 ]
 | xE ⇒ match e2 with
  [ x0 ⇒ xE | x1 ⇒ xF | x2 ⇒ xC | x3 ⇒ xD 
  | x4 ⇒ xA | x5 ⇒ xB | x6 ⇒ x8 | x7 ⇒ x9
  | x8 ⇒ x6 | x9 ⇒ x7 | xA ⇒ x4 | xB ⇒ x5 
  | xC ⇒ x2 | xD ⇒ x3 | xE ⇒ x0 | xF ⇒ x1 ] 
 | xF ⇒ match e2 with
  [ x0 ⇒ xF | x1 ⇒ xE | x2 ⇒ xD | x3 ⇒ xC 
  | x4 ⇒ xB | x5 ⇒ xA | x6 ⇒ x9 | x7 ⇒ x8
  | x8 ⇒ x7 | x9 ⇒ x6 | xA ⇒ x5 | xB ⇒ x4 
  | xC ⇒ x3 | xD ⇒ x2 | xE ⇒ x1 | xF ⇒ x0 ] 
 ].

(* operatore rotazione destra con carry *)
ndefinition rcr_ex ≝
λe:exadecim.λc:bool.match c with
 [ true ⇒ match e with
  [ x0 ⇒ pair exadecim bool x8 false | x1 ⇒ pair exadecim bool x8 true
  | x2 ⇒ pair exadecim bool x9 false | x3 ⇒ pair exadecim bool x9 true
  | x4 ⇒ pair exadecim bool xA false | x5 ⇒ pair exadecim bool xA true
  | x6 ⇒ pair exadecim bool xB false | x7 ⇒ pair exadecim bool xB true
  | x8 ⇒ pair exadecim bool xC false | x9 ⇒ pair exadecim bool xC true
  | xA ⇒ pair exadecim bool xD false | xB ⇒ pair exadecim bool xD true
  | xC ⇒ pair exadecim bool xE false | xD ⇒ pair exadecim bool xE true
  | xE ⇒ pair exadecim bool xF false | xF ⇒ pair exadecim bool xF true ]
 | false ⇒ match e with 
  [ x0 ⇒ pair exadecim bool x0 false | x1 ⇒ pair exadecim bool x0 true
  | x2 ⇒ pair exadecim bool x1 false | x3 ⇒ pair exadecim bool x1 true
  | x4 ⇒ pair exadecim bool x2 false | x5 ⇒ pair exadecim bool x2 true
  | x6 ⇒ pair exadecim bool x3 false | x7 ⇒ pair exadecim bool x3 true
  | x8 ⇒ pair exadecim bool x4 false | x9 ⇒ pair exadecim bool x4 true
  | xA ⇒ pair exadecim bool x5 false | xB ⇒ pair exadecim bool x5 true
  | xC ⇒ pair exadecim bool x6 false | xD ⇒ pair exadecim bool x6 true
  | xE ⇒ pair exadecim bool x7 false | xF ⇒ pair exadecim bool x7 true ]
 ].

(* operatore shift destro *)
ndefinition shr_ex ≝
λe:exadecim.match e with 
 [ x0 ⇒ pair exadecim bool x0 false | x1 ⇒ pair exadecim bool x0 true
 | x2 ⇒ pair exadecim bool x1 false | x3 ⇒ pair exadecim bool x1 true
 | x4 ⇒ pair exadecim bool x2 false | x5 ⇒ pair exadecim bool x2 true
 | x6 ⇒ pair exadecim bool x3 false | x7 ⇒ pair exadecim bool x3 true
 | x8 ⇒ pair exadecim bool x4 false | x9 ⇒ pair exadecim bool x4 true
 | xA ⇒ pair exadecim bool x5 false | xB ⇒ pair exadecim bool x5 true
 | xC ⇒ pair exadecim bool x6 false | xD ⇒ pair exadecim bool x6 true
 | xE ⇒ pair exadecim bool x7 false | xF ⇒ pair exadecim bool x7 true ].

(* operatore rotazione destra *)
ndefinition ror_ex ≝
λe:exadecim.match e with 
 [ x0 ⇒ x0 | x1 ⇒ x8 | x2 ⇒ x1 | x3 ⇒ x9
 | x4 ⇒ x2 | x5 ⇒ xA | x6 ⇒ x3 | x7 ⇒ xB 
 | x8 ⇒ x4 | x9 ⇒ xC | xA ⇒ x5 | xB ⇒ xD 
 | xC ⇒ x6 | xD ⇒ xE | xE ⇒ x7 | xF ⇒ xF ].

(* operatore rotazione destra n-volte *)
nlet rec ror_ex_n (e:exadecim) (n:nat) on n ≝
 match n with
  [ O ⇒ e
  | S n' ⇒ ror_ex_n (ror_ex e) n' ].

(* operatore rotazione sinistra con carry *)
ndefinition rcl_ex ≝
λe:exadecim.λc:bool.match c with
 [ true ⇒ match e with
  [ x0 ⇒ pair exadecim bool x1 false | x1 ⇒ pair exadecim bool x3 false
  | x2 ⇒ pair exadecim bool x5 false | x3 ⇒ pair exadecim bool x7 false
  | x4 ⇒ pair exadecim bool x9 false | x5 ⇒ pair exadecim bool xB false
  | x6 ⇒ pair exadecim bool xD false | x7 ⇒ pair exadecim bool xF false
  | x8 ⇒ pair exadecim bool x1 true  | x9 ⇒ pair exadecim bool x3 true
  | xA ⇒ pair exadecim bool x5 true  | xB ⇒ pair exadecim bool x7 true
  | xC ⇒ pair exadecim bool x9 true  | xD ⇒ pair exadecim bool xB true
  | xE ⇒ pair exadecim bool xD true  | xF ⇒ pair exadecim bool xF true ]
 | false ⇒ match e with
  [ x0 ⇒ pair exadecim bool x0 false | x1 ⇒ pair exadecim bool x2 false
  | x2 ⇒ pair exadecim bool x4 false | x3 ⇒ pair exadecim bool x6 false
  | x4 ⇒ pair exadecim bool x8 false | x5 ⇒ pair exadecim bool xA false
  | x6 ⇒ pair exadecim bool xC false | x7 ⇒ pair exadecim bool xE false
  | x8 ⇒ pair exadecim bool x0 true  | x9 ⇒ pair exadecim bool x2 true
  | xA ⇒ pair exadecim bool x4 true  | xB ⇒ pair exadecim bool x6 true
  | xC ⇒ pair exadecim bool x8 true  | xD ⇒ pair exadecim bool xA true
  | xE ⇒ pair exadecim bool xC true  | xF ⇒ pair exadecim bool xE true ]
 ].

(* operatore shift sinistro *)
ndefinition shl_ex ≝
λe:exadecim.match e with
 [ x0 ⇒ pair exadecim bool x0 false | x1 ⇒ pair exadecim bool x2 false
 | x2 ⇒ pair exadecim bool x4 false | x3 ⇒ pair exadecim bool x6 false
 | x4 ⇒ pair exadecim bool x8 false | x5 ⇒ pair exadecim bool xA false
 | x6 ⇒ pair exadecim bool xC false | x7 ⇒ pair exadecim bool xE false
 | x8 ⇒ pair exadecim bool x0 true  | x9 ⇒ pair exadecim bool x2 true
 | xA ⇒ pair exadecim bool x4 true  | xB ⇒ pair exadecim bool x6 true
 | xC ⇒ pair exadecim bool x8 true  | xD ⇒ pair exadecim bool xA true
 | xE ⇒ pair exadecim bool xC true  | xF ⇒ pair exadecim bool xE true ].

(* operatore rotazione sinistra *)
ndefinition rol_ex ≝
λe:exadecim.match e with
 [ x0 ⇒ x0 | x1 ⇒ x2 | x2 ⇒ x4 | x3 ⇒ x6
 | x4 ⇒ x8 | x5 ⇒ xA | x6 ⇒ xC | x7 ⇒ xE
 | x8 ⇒ x1 | x9 ⇒ x3 | xA ⇒ x5 | xB ⇒ x7
 | xC ⇒ x9 | xD ⇒ xB | xE ⇒ xD | xF ⇒ xF ].

(* operatore rotazione sinistra n-volte *)
nlet rec rol_ex_n (e:exadecim) (n:nat) on n ≝
 match n with
  [ O ⇒ e
  | S n' ⇒ rol_ex_n (rol_ex e) n' ].

(* operatore not/complemento a 1 *)
ndefinition not_ex ≝
λe:exadecim.match e with
 [ x0 ⇒ xF | x1 ⇒ xE | x2 ⇒ xD | x3 ⇒ xC
 | x4 ⇒ xB | x5 ⇒ xA | x6 ⇒ x9 | x7 ⇒ x8
 | x8 ⇒ x7 | x9 ⇒ x6 | xA ⇒ x5 | xB ⇒ x4
 | xC ⇒ x3 | xD ⇒ x2 | xE ⇒ x1 | xF ⇒ x0 ].

(* 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 … 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 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 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 ≝
λe:exadecim.match e 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 ].

(* operatore predecessore *)
ndefinition pred_ex ≝
λe:exadecim.
 match e 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 successore *)
ndefinition succ_ex ≝
λe:exadecim.
 match e 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 ].

(* operatore neg/complemento a 2 *)
ndefinition compl_ex ≝
λe:exadecim.match e with
 [ x0 ⇒ x0 | x1 ⇒ xF | x2 ⇒ xE | x3 ⇒ xD
 | x4 ⇒ xC | x5 ⇒ xB | x6 ⇒ xA | x7 ⇒ x9
 | x8 ⇒ x8 | x9 ⇒ x7 | xA ⇒ x6 | xB ⇒ x5
 | xC ⇒ x4 | xD ⇒ x3 | xE ⇒ x2 | xF ⇒ x1 ].

(* operatore x in [inf,sup] *)
ndefinition inrange_ex ≝
λx,inf,sup:exadecim.(le_ex inf x) ⊗ (le_ex x sup).

(* iteratore sugli esadecimali *)
ndefinition forall_ex ≝ λP.
 P x0 ⊗ P x1 ⊗ P x2 ⊗ P x3 ⊗ P x4 ⊗ P x5 ⊗ P x6 ⊗ P x7 ⊗
 P x8 ⊗ P x9 ⊗ P xA ⊗ P xB ⊗ P xC ⊗ P xD ⊗ P xE ⊗ P xF.

(* esadecimali ricorsivi *)
ninductive rec_exadecim : exadecim → Type ≝
  ex_O : rec_exadecim x0
| ex_S : ∀n.rec_exadecim n → rec_exadecim (succ_ex n).

(* esadecimali → esadecimali ricorsivi *)
ndefinition ex_to_recex ≝
λn.match n return λx.rec_exadecim x with
 [ x0 ⇒ ex_O
 | x1 ⇒ ex_S ? ex_O
 | x2 ⇒ ex_S ? (ex_S ? ex_O)
 | x3 ⇒ ex_S ? (ex_S ? (ex_S ? ex_O))
 | x4 ⇒ ex_S ? (ex_S ? (ex_S ? (ex_S ? ex_O)))
 | x5 ⇒ ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? ex_O))))
 | x6 ⇒ ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? ex_O)))))
 | x7 ⇒ ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? ex_O))))))
 | x8 ⇒ ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? ex_O)))))))
 | x9 ⇒ ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? ex_O))))))))
 | xA ⇒ ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? ex_O)))))))))
 | xB ⇒ ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? ex_O))))))))))
 | xC ⇒ ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? ex_O)))))))))))
 | xD ⇒ ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? ex_O))))))))))))
 | xE ⇒ ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? ex_O)))))))))))))
 | xF ⇒ ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? ex_O))))))))))))))
 ].

(* quaternari → esadecimali *)
ndefinition ex_of_qu ≝
λn.match n with
 [ q0 ⇒ x0 | q1 ⇒ x1 | q2 ⇒ x2 | q3 ⇒ x3 ].

(* ottali → esadecimali *)
ndefinition ex_of_oct ≝
λn.match n with
 [ o0 ⇒ x0 | o1 ⇒ x1 | o2 ⇒ x2 | o3 ⇒ x3 | o4 ⇒ x4 | o5 ⇒ x5 | o6 ⇒ x6 | o7 ⇒ x7 ].