+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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: *)
-(* Cosimo Oliboni, oliboni@cs.unibo.it *)
-(* *)
-(* Questo materiale fa parte della tesi: *)
-(* "Formalizzazione Interattiva dei Microcontroller a 8bit FreeScale" *)
-(* *)
-(* data ultima modifica 15/11/2007 *)
-(* ********************************************************************** *)
-
-include "freescale/extra.ma".
-
-(* ***************************** *)
-(* DEFINIZIONE DEGLI ESADECIMALI *)
-(* ***************************** *)
-
-inductive 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 = *)
-definition eq_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 ⇒ false | 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 ⇒ false | x1 ⇒ false | 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 ⇒ false | x1 ⇒ false | x2 ⇒ false | 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 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
- | 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 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
- | x4 ⇒ false | 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 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
- | x4 ⇒ false | x5 ⇒ false | 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 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
- | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ true
- | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
- | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
- | x8 ⇒ match e2 with
- [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
- | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
- | x8 ⇒ true | x9 ⇒ false | xA ⇒ false | xB ⇒ false
- | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
- | 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 ⇒ false | xB ⇒ false
- | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
- | 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 ⇒ false
- | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
- | 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 ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
- | 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 ⇒ false | xE ⇒ false | xF ⇒ false ]
- | 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 ⇒ false | xF ⇒ false ]
- | 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 ⇒ false ]
- | 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 < *)
-definition 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 ≤ *)
-definition 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 > *)
-definition 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 ≥ *)
-definition 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 *)
-definition 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 *)
-definition 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 *)
-definition 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 *)
-definition 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 *)
-definition 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 *)
-definition 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 *)
-let 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 *)
-definition 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 *)
-definition 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 *)
-definition 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 *)
-let 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 *)
-definition 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 carry *)
-definition plus_ex ≝
-λ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 ]
- ]
- ].
-
-(* operatore somma senza carry *)
-definition plus_exnc ≝
-λe1,e2:exadecim.fst ?? (plus_ex e1 e2 false).
-
-(* operatore carry della somma *)
-definition plus_exc ≝
-λe1,e2:exadecim.snd ?? (plus_ex e1 e2 false).
-
-(* operatore Most Significant Bit *)
-definition 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 ].
-
-(* esadecimali → naturali *)
-definition nat_of_exadecim ≝
-λe:exadecim.
- match e with
- [ x0 ⇒ 0 | x1 ⇒ 1 | x2 ⇒ 2 | x3 ⇒ 3 | x4 ⇒ 4 | x5 ⇒ 5 | x6 ⇒ 6 | x7 ⇒ 7
- | x8 ⇒ 8 | x9 ⇒ 9 | xA ⇒ 10 | xB ⇒ 11 | xC ⇒ 12 | xD ⇒ 13 | xE ⇒ 14 | xF ⇒ 15 ].
-
-coercion cic:/matita/freescale/exadecim/nat_of_exadecim.con.
-
-(* naturali → esadecimali *)
-let rec exadecim_of_nat n ≝
- match n with [ O ⇒ x0 | S n ⇒
- match n with [ O ⇒ x1 | S n ⇒
- match n with [ O ⇒ x2 | S n ⇒
- match n with [ O ⇒ x3 | S n ⇒
- match n with [ O ⇒ x4 | S n ⇒
- match n with [ O ⇒ x5 | S n ⇒
- match n with [ O ⇒ x6 | S n ⇒
- match n with [ O ⇒ x7 | S n ⇒
- match n with [ O ⇒ x8 | S n ⇒
- match n with [ O ⇒ x9 | S n ⇒
- match n with [ O ⇒ xA | S n ⇒
- match n with [ O ⇒ xB | S n ⇒
- match n with [ O ⇒ xC | S n ⇒
- match n with [ O ⇒ xD | S n ⇒
- match n with [ O ⇒ xE | S n ⇒
- match n with [ O ⇒ xF | S n ⇒ exadecim_of_nat n ]]]]]]]]]]]]]]]].
-
-(* operatore predecessore *)
-definition 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 *)
-definition 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 *)
-definition 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 ].
-
-(* iteratore sugli esadecimali *)
-definition forall_exadecim ≝ λ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.
-
-(* ********************** *)
-(* TEOREMI/LEMMMI/ASSIOMI *)
-(* ********************** *)
-
-(* ESPERIMENTO UTILIZZO DELL'ITERATORE *)
-
-(*
-lemma forall_exadecim_eqProp_left_aux :
- ∀P.(∀e:exadecim.P e = true) →
- ((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) = true).
- intros;
- elim H; elim P; [ 2: reflexivity; ] elim H; elim P; [ 2: reflexivity; ]
- elim H; elim P; [ 2: reflexivity; ] elim H; elim P; [ 2: reflexivity; ]
- elim H; elim P; [ 2: reflexivity; ] elim H; elim P; [ 2: reflexivity; ]
- elim H; elim P; [ 2: reflexivity; ] elim H; elim P; [ 2: reflexivity; ]
- elim H; elim P; [ 2: reflexivity; ] elim H; elim P; [ 2: reflexivity; ]
- elim H; elim P; [ 2: reflexivity; ] elim H; elim P; [ 2: reflexivity; ]
- elim H; elim P; [ 2: reflexivity; ] elim H; elim P; [ 2: reflexivity; ]
- elim H; elim P; [ 2: reflexivity; ] elim H; elim P; [ 2: reflexivity; ]
- reflexivity.
-qed.
-
-lemma forall_exadecim_eqProp_left :
- ∀P.(∀e:exadecim. P e = true) → (forall_exadecim (λe.P e) = true).
- intro;
- elim P 0;
- [ simplify; intro; apply forall_exadecim_eqProp_left_aux; apply H; |
- simplify; intro; apply forall_exadecim_eqProp_left_aux; apply H; |
- autobatch; ].
-qed.
-
-lemma forall_exadecim_eqProp_right_aux :
- ∀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) = true) →
- (∀e:exadecim.P e = true).
- elim daemon.
-qed.
-
-lemma forall_exadecim_eqProp_right :
- ∀P.(forall_exadecim (λe.P e) = true) → (∀e:exadecim.P e = true).
- intro;
- elim P 0;
- [ simplify; intro; apply forall_exadecim_eqProp_right_aux; apply H; |
- simplify; intro; apply forall_exadecim_eqProp_right_aux; apply H; |
- autobatch; ].
-qed.
-
-lemma lt_nat_of_exadecim_16_forall: ∀e.ltb (nat_of_exadecim e) 16 = true.
- apply forall_exadecim_eqProp_right;
- reflexivity;
-qed.
-*)
-
-(* FINE DELL'ESPERIMENTO *)
-
-lemma lt_nat_of_exadecim_16: ∀e.nat_of_exadecim e < 16.
- intro;
- elim e;
- simplify;
- autobatch depth=17.
-qed.
-
-lemma exadecim_of_nat_mod:
- ∀n.exadecim_of_nat n = exadecim_of_nat (n \mod 16).
- intros;
- apply (nat_elim1 n); intro;
- cases m; [ intro; reflexivity | ];
- cases n1; [ intro; reflexivity | ];
- cases n2; [ intro; reflexivity | ];
- cases n3; [ intro; reflexivity | ];
- cases n4; [ intro; reflexivity | ];
- cases n5; [ intro; reflexivity | ];
- cases n6; [ intro; reflexivity | ];
- cases n7; [ intro; reflexivity | ];
- cases n8; [ intro; reflexivity | ];
- cases n9; [ intro; reflexivity | ];
- cases n10; [ intro; reflexivity | ];
- cases n11; [ intro; reflexivity | ];
- cases n12; [ intro; reflexivity | ];
- cases n13; [ intro; reflexivity | ];
- cases n14; [ intro; reflexivity | ];
- cases n15; [ intro; reflexivity | ];
- intros;
- change in ⊢ (? ? % ?) with (exadecim_of_nat n16);
- change in ⊢ (? ? ? (? (? % ?))) with (16 + n16);
- rewrite > mod_plus;
- change in ⊢ (? ? ? (? (? % ?))) with (n16 \mod 16);
- rewrite < mod_mod;
- [ apply H;
- unfold lt;
- autobatch.
- | autobatch
- ]
-qed.
-
-lemma nat_of_exadecim_exadecim_of_nat:
- ∀n. nat_of_exadecim (exadecim_of_nat n) = n \mod 16.
- intro;
- rewrite > exadecim_of_nat_mod;
- generalize in match (lt_mod_m_m n 16 ?); [2: autobatch | ]
- generalize in match (n \mod 16); intro;
- cases n1; [ intro; reflexivity | ];
- cases n2; [ intro; reflexivity | ];
- cases n3; [ intro; reflexivity | ];
- cases n4; [ intro; reflexivity | ];
- cases n5; [ intro; reflexivity | ];
- cases n6; [ intro; reflexivity | ];
- cases n7; [ intro; reflexivity | ];
- cases n8; [ intro; reflexivity | ];
- cases n9; [ intro; reflexivity | ];
- cases n10; [ intro; reflexivity | ];
- cases n11 [ intro; reflexivity | ];
- cases n12; [ intro; reflexivity | ];
- cases n13; [ intro; reflexivity | ];
- cases n14; [ intro; reflexivity | ];
- cases n15; [ intro; reflexivity | ];
- cases n16; [ intro; reflexivity | ];
- intro;
- unfold lt in H;
- cut False;
- [ elim Hcut
- | autobatch
- ]
-qed.
-
-lemma exadecim_of_nat_nat_of_exadecim:
- ∀e.exadecim_of_nat (nat_of_exadecim e) = e.
- intro;
- elim e;
- reflexivity.
-qed.
-
-lemma plusex_ok:
- ∀b1,b2,c.
- match plus_ex b1 b2 c with
- [ pair r c' ⇒ b1 + b2 + nat_of_bool c = nat_of_exadecim r + nat_of_bool c' * 16 ].
- intros;
- elim b1; (elim b2; (elim c; normalize; reflexivity)).
-qed.
-
-lemma eq_eqex_S_x0_false:
- ∀n. n < 15 → eq_ex x0 (exadecim_of_nat (S n)) = false.
- intro;
- cases n 0; [ intro; simplify; reflexivity | clear n];
- cases n1 0; [ intro; simplify; reflexivity | clear n1];
- cases n 0; [ intro; simplify; reflexivity | clear n];
- cases n1 0; [ intro; simplify; reflexivity | clear n1];
- cases n 0; [ intro; simplify; reflexivity | clear n];
- cases n1 0; [ intro; simplify; reflexivity | clear n1];
- cases n 0; [ intro; simplify; reflexivity | clear n];
- cases n1 0; [ intro; simplify; reflexivity | clear n1];
- cases n 0; [ intro; simplify; reflexivity | clear n];
- cases n1 0; [ intro; simplify; reflexivity | clear n1];
- cases n 0; [ intro; simplify; reflexivity | clear n];
- cases n1 0; [ intro; simplify; reflexivity | clear n1];
- cases n 0; [ intro; simplify; reflexivity | clear n];
- cases n1 0; [ intro; simplify; reflexivity | clear n1];
- cases n 0; [ intro; simplify; reflexivity | clear n];
- intro;
- unfold lt in H;
- cut (S n1 ≤ 0);
- [ elim (not_le_Sn_O ? Hcut)
- | do 15 (apply le_S_S_to_le);
- assumption
- ]
-qed.
-
-lemma eqex_true_to_eq: ∀b,b'. eq_ex b b' = true → b=b'.
- intros 2;
- elim b 0;
- elim b' 0;
- simplify;
- intro;
- first [ reflexivity | destruct H ].
-qed.
-
-lemma eqex_false_to_not_eq: ∀b,b'. eq_ex b b' = false → b ≠ b'.
- intros 2;
- elim b 0;
- elim b' 0;
- simplify;
- intro;
- try (destruct H);
- intro K;
- destruct K.
-qed.
-
-(* nuovi *)
-
-lemma ok_lt_ex : ∀e1,e2:exadecim.
- lt_ex e1 e2 = ltb e1 e2.
- intros;
- elim e1;
- elim e2;
- simplify;
- reflexivity.
- qed.
-
-lemma ok_le_ex : ∀e1,e2:exadecim.
- le_ex e1 e2 = leb e1 e2.
- intros;
- elim e1;
- elim e2;
- simplify;
- reflexivity.
- qed.
-
-lemma ok_gt_ex : ∀e1,e2:exadecim.
- gt_ex e1 e2 = notb (leb e1 e2).
- intros;
- elim e1;
- elim e2;
- simplify;
- reflexivity.
- qed.
-
-lemma ok_ge_ex : ∀e1,e2:exadecim.
- ge_ex e1 e2 = notb (ltb e1 e2).
- intros;
- elim e1;
- elim e2;
- simplify;
- reflexivity.
- qed.
-
-lemma ok_pred_ex : ∀e:exadecim.
- pred_ex e = plus_exnc e xF.
- intros;
- elim e;
- simplify;
- reflexivity.
- qed.
-
-lemma ok_succ_ex : ∀e:exadecim.
- succ_ex e = plus_exnc e x1.
- intros;
- elim e;
- simplify;
- reflexivity.
- qed.
-
-lemma ok_rcr_ex : ∀e:exadecim.∀b:bool.
- rcr_ex e b =
- pair exadecim bool
- (exadecim_of_nat ((e/2)+match b with [ true ⇒ 8 | false ⇒ 0]))
- (eqb (mod e 2) 1).
- intros;
- elim e;
- elim b;
- simplify in ⊢ (? ? ? (? ? ? (? (? ? %)) ?));
- simplify in ⊢ (? ? ? (? ? ? ? %));
- simplify in ⊢ (? ? ? (? ? ? % ?));
- simplify in ⊢ (? ? % ?);
- reflexivity;
-qed.
-
-lemma ok_rcl_ex : ∀e:exadecim.∀b:bool.
- rcl_ex e b =
- pair exadecim bool
- (exadecim_of_nat ((mod (e*2) 16)+match b with [ true ⇒ 1 | false ⇒ 0]))
- (notb (ltb e 8)).
- intros;
- elim e;
- elim b;
- simplify in ⊢ (? ? ? (? ? ? (? (? ? %)) ?));
- simplify in ⊢ (? ? ? (? ? ? % ?));
- simplify in ⊢ (? ? ? (? ? ? ? (? %)));
- simplify in ⊢ (? ? ? (? ? ? ? %));
- simplify in ⊢ (? ? % ?);
- reflexivity.
- qed.
-
-lemma ok_shr_ex : ∀e:exadecim.
- shr_ex e =
- pair exadecim bool
- (exadecim_of_nat (e/2))
- (eqb (mod e 2) 1).
- intros;
- elim e;
- simplify in ⊢ (? ? ? (? ? ? % ?));
- simplify in ⊢ (? ? ? (? ? ? ? %));
- simplify in ⊢ (? ? % ?);
- reflexivity.
-qed.
-
-lemma ok_shl_ex : ∀e:exadecim.
- shl_ex e =
- pair exadecim bool
- (exadecim_of_nat (mod (e*2) 16))
- (notb (ltb e 8)).
- intros;
- elim e;
- simplify in ⊢ (? ? ? (? ? ? % ?));
- simplify in ⊢ (? ? ? (? ? ? ? (? %)));
- simplify in ⊢ (? ? ? (? ? ? ? %));
- simplify in ⊢ (? ? % ?);
- reflexivity.
-qed.
-
-lemma ok_not_ex : ∀e:exadecim.
- e + (not_ex e) = 15.
- intros;
- elim e;
- simplify;
- reflexivity.
-qed.
-
-lemma ok_compl_ex : ∀e:exadecim.
- e + (compl_ex e) = match gt_ex e x0 with [ true ⇒ 16 | false ⇒ 0 ].
- intros;
- elim e;
- simplify;
- reflexivity.
-qed.
-
-lemma ok_MSB_ex : ∀e:exadecim.
- MSB_ex e = notb (ltb e 8).
- intros;
- elim e;
- simplify;
- reflexivity.
-qed.
projects / helm.git / blobdiff