X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly2%2Fnum%2Fexadecim.ma;fp=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly2%2Fnum%2Fexadecim.ma;h=72f81d0d2c63d854a601627e4c4804f14860b991;hb=bd112857523fc543c78cd29b74417585033ec464;hp=0000000000000000000000000000000000000000;hpb=c49f650fe86d8ff5d388418e9f603549d765a2ea;p=helm.git diff --git a/helm/software/matita/contribs/ng_assembly2/num/exadecim.ma b/helm/software/matita/contribs/ng_assembly2/num/exadecim.ma new file mode 100755 index 000000000..72f81d0d2 --- /dev/null +++ b/helm/software/matita/contribs/ng_assembly2/num/exadecim.ma @@ -0,0 +1,1583 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* Sviluppo: 2008-2010 *) +(* *) +(* ********************************************************************** *) + +include "num/comp_ext.ma". +include "num/bool_lemmas.ma". +include "num/oct.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. + +(* 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. + +(* 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 Most Significant Bit *) +ndefinition getMSB_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 ]. + +ndefinition setMSB_ex ≝ +λe:exadecim.match e 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 ]. + +ndefinition clrMSB_ex ≝ +λe:exadecim.match e 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 ]. + +(* operatore Least Significant Bit *) +ndefinition getLSB_ex ≝ +λe:exadecim.match e with + [ x0 ⇒ false | x1 ⇒ true | x2 ⇒ false | x3 ⇒ true + | x4 ⇒ false | x5 ⇒ true | x6 ⇒ false | x7 ⇒ true + | x8 ⇒ false | x9 ⇒ true | xA ⇒ false | xB ⇒ true + | xC ⇒ false | xD ⇒ true | xE ⇒ false | xF ⇒ true ]. + +ndefinition setLSB_ex ≝ +λe:exadecim.match e 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 ]. + +ndefinition clrLSB_ex ≝ +λe:exadecim.match e 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 ]. + +(* operatore rotazione destra con carry *) +ndefinition rcr_ex ≝ +λc:bool.λe:exadecim.match c with + [ true ⇒ match e with + [ x0 ⇒ pair … false x8 | x1 ⇒ pair … true x8 + | x2 ⇒ pair … false x9 | x3 ⇒ pair … true x9 + | x4 ⇒ pair … false xA | x5 ⇒ pair … true xA + | x6 ⇒ pair … false xB | x7 ⇒ pair … true xB + | x8 ⇒ pair … false xC | x9 ⇒ pair … true xC + | xA ⇒ pair … false xD | xB ⇒ pair … true xD + | xC ⇒ pair … false xE | xD ⇒ pair … true xE + | xE ⇒ pair … false xF | xF ⇒ pair … true xF ] + | false ⇒ match e with + [ x0 ⇒ pair … false x0 | x1 ⇒ pair … true x0 + | x2 ⇒ pair … false x1 | x3 ⇒ pair … true x1 + | x4 ⇒ pair … false x2 | x5 ⇒ pair … true x2 + | x6 ⇒ pair … false x3 | x7 ⇒ pair … true x3 + | x8 ⇒ pair … false x4 | x9 ⇒ pair … true x4 + | xA ⇒ pair … false x5 | xB ⇒ pair … true x5 + | xC ⇒ pair … false x6 | xD ⇒ pair … true x6 + | xE ⇒ pair … false x7 | xF ⇒ pair … true x7 ] + ]. + +(* operatore shift destro *) +ndefinition shr_ex ≝ +λe:exadecim.match e with + [ x0 ⇒ pair … false x0 | x1 ⇒ pair … true x0 + | x2 ⇒ pair … false x1 | x3 ⇒ pair … true x1 + | x4 ⇒ pair … false x2 | x5 ⇒ pair … true x2 + | x6 ⇒ pair … false x3 | x7 ⇒ pair … true x3 + | x8 ⇒ pair … false x4 | x9 ⇒ pair … true x4 + | xA ⇒ pair … false x5 | xB ⇒ pair … true x5 + | xC ⇒ pair … false x6 | xD ⇒ pair … true x6 + | xE ⇒ pair … false x7 | xF ⇒ pair … true x7 ]. + +(* 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 sinistra con carry *) +ndefinition rcl_ex ≝ +λc:bool.λe:exadecim.match c with + [ true ⇒ match e with + [ x0 ⇒ pair … false x1 | x1 ⇒ pair … false x3 + | x2 ⇒ pair … false x5 | x3 ⇒ pair … false x7 + | x4 ⇒ pair … false x9 | x5 ⇒ pair … false xB + | x6 ⇒ pair … false xD | x7 ⇒ pair … false xF + | x8 ⇒ pair … true x1 | x9 ⇒ pair … true x3 + | xA ⇒ pair … true x5 | xB ⇒ pair … true x7 + | xC ⇒ pair … true x9 | xD ⇒ pair … true xB + | xE ⇒ pair … true xD | xF ⇒ pair … true xF ] + | false ⇒ match e with + [ x0 ⇒ pair … false x0 | x1 ⇒ pair … false x2 + | x2 ⇒ pair … false x4 | x3 ⇒ pair … false x6 + | x4 ⇒ pair … false x8 | x5 ⇒ pair … false xA + | x6 ⇒ pair … false xC | x7 ⇒ pair … false xE + | x8 ⇒ pair … true x0 | x9 ⇒ pair … true x2 + | xA ⇒ pair … true x4 | xB ⇒ pair … true x6 + | xC ⇒ pair … true x8 | xD ⇒ pair … true xA + | xE ⇒ pair … true xC | xF ⇒ pair … true xE ] + ]. + +(* operatore shift sinistro *) +ndefinition shl_ex ≝ +λe:exadecim.match e with + [ x0 ⇒ pair … false x0 | x1 ⇒ pair … false x2 + | x2 ⇒ pair … false x4 | x3 ⇒ pair … false x6 + | x4 ⇒ pair … false x8 | x5 ⇒ pair … false xA + | x6 ⇒ pair … false xC | x7 ⇒ pair … false xE + | x8 ⇒ pair … true x0 | x9 ⇒ pair … true x2 + | xA ⇒ pair … true x4 | xB ⇒ pair … true x6 + | xC ⇒ pair … true x8 | xD ⇒ pair … true xA + | xE ⇒ pair … true xC | xF ⇒ pair … true xE ]. + +(* 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 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 ≝ +λc:bool.λe1,e2:exadecim. + match c with + [ true ⇒ match e1 with + [ x0 ⇒ match e2 with + [ x0 ⇒ pair … false x1 | x1 ⇒ pair … false x2 | x2 ⇒ pair … false x3 | x3 ⇒ pair … false x4 + | x4 ⇒ pair … false x5 | x5 ⇒ pair … false x6 | x6 ⇒ pair … false x7 | x7 ⇒ pair … false x8 + | x8 ⇒ pair … false x9 | x9 ⇒ pair … false xA | xA ⇒ pair … false xB | xB ⇒ pair … false xC + | xC ⇒ pair … false xD | xD ⇒ pair … false xE | xE ⇒ pair … false xF | xF ⇒ pair … true x0 ] + | x1 ⇒ match e2 with + [ x0 ⇒ pair … false x2 | x1 ⇒ pair … false x3 | x2 ⇒ pair … false x4 | x3 ⇒ pair … false x5 + | x4 ⇒ pair … false x6 | x5 ⇒ pair … false x7 | x6 ⇒ pair … false x8 | x7 ⇒ pair … false x9 + | x8 ⇒ pair … false xA | x9 ⇒ pair … false xB | xA ⇒ pair … false xC | xB ⇒ pair … false xD + | xC ⇒ pair … false xE | xD ⇒ pair … false xF | xE ⇒ pair … true x0 | xF ⇒ pair … true x1 ] + | x2 ⇒ match e2 with + [ x0 ⇒ pair … false x3 | x1 ⇒ pair … false x4 | x2 ⇒ pair … false x5 | x3 ⇒ pair … false x6 + | x4 ⇒ pair … false x7 | x5 ⇒ pair … false x8 | x6 ⇒ pair … false x9 | x7 ⇒ pair … false xA + | x8 ⇒ pair … false xB | x9 ⇒ pair … false xC | xA ⇒ pair … false xD | xB ⇒ pair … false xE + | xC ⇒ pair … false xF | xD ⇒ pair … true x0 | xE ⇒ pair … true x1 | xF ⇒ pair … true x2 ] + | x3 ⇒ match e2 with + [ x0 ⇒ pair … false x4 | x1 ⇒ pair … false x5 | x2 ⇒ pair … false x6 | x3 ⇒ pair … false x7 + | x4 ⇒ pair … false x8 | x5 ⇒ pair … false x9 | x6 ⇒ pair … false xA | x7 ⇒ pair … false xB + | x8 ⇒ pair … false xC | x9 ⇒ pair … false xD | xA ⇒ pair … false xE | xB ⇒ pair … false xF + | xC ⇒ pair … true x0 | xD ⇒ pair … true x1 | xE ⇒ pair … true x2 | xF ⇒ pair … true x3 ] + | x4 ⇒ match e2 with + [ x0 ⇒ pair … false x5 | x1 ⇒ pair … false x6 | x2 ⇒ pair … false x7 | x3 ⇒ pair … false x8 + | x4 ⇒ pair … false x9 | x5 ⇒ pair … false xA | x6 ⇒ pair … false xB | x7 ⇒ pair … false xC + | x8 ⇒ pair … false xD | x9 ⇒ pair … false xE | xA ⇒ pair … false xF | xB ⇒ pair … true x0 + | xC ⇒ pair … true x1 | xD ⇒ pair … true x2 | xE ⇒ pair … true x3 | xF ⇒ pair … true x4 ] + | x5 ⇒ match e2 with + [ x0 ⇒ pair … false x6 | x1 ⇒ pair … false x7 | x2 ⇒ pair … false x8 | x3 ⇒ pair … false x9 + | x4 ⇒ pair … false xA | x5 ⇒ pair … false xB | x6 ⇒ pair … false xC | x7 ⇒ pair … false xD + | x8 ⇒ pair … false xE | x9 ⇒ pair … false xF | xA ⇒ pair … true x0 | xB ⇒ pair … true x1 + | xC ⇒ pair … true x2 | xD ⇒ pair … true x3 | xE ⇒ pair … true x4 | xF ⇒ pair … true x5 ] + | x6 ⇒ match e2 with + [ x0 ⇒ pair … false x7 | x1 ⇒ pair … false x8 | x2 ⇒ pair … false x9 | x3 ⇒ pair … false xA + | x4 ⇒ pair … false xB | x5 ⇒ pair … false xC | x6 ⇒ pair … false xD | x7 ⇒ pair … false xE + | x8 ⇒ pair … false xF | x9 ⇒ pair … true x0 | xA ⇒ pair … true x1 | xB ⇒ pair … true x2 + | xC ⇒ pair … true x3 | xD ⇒ pair … true x4 | xE ⇒ pair … true x5 | xF ⇒ pair … true x6 ] + | x7 ⇒ match e2 with + [ x0 ⇒ pair … false x8 | x1 ⇒ pair … false x9 | x2 ⇒ pair … false xA | x3 ⇒ pair … false xB + | x4 ⇒ pair … false xC | x5 ⇒ pair … false xD | x6 ⇒ pair … false xE | x7 ⇒ pair … false xF + | x8 ⇒ pair … true x0 | x9 ⇒ pair … true x1 | xA ⇒ pair … true x2 | xB ⇒ pair … true x3 + | xC ⇒ pair … true x4 | xD ⇒ pair … true x5 | xE ⇒ pair … true x6 | xF ⇒ pair … true x7 ] + | x8 ⇒ match e2 with + [ x0 ⇒ pair … false x9 | x1 ⇒ pair … false xA | x2 ⇒ pair … false xB | x3 ⇒ pair … false xC + | x4 ⇒ pair … false xD | x5 ⇒ pair … false xE | x6 ⇒ pair … false xF | x7 ⇒ pair … true x0 + | x8 ⇒ pair … true x1 | x9 ⇒ pair … true x2 | xA ⇒ pair … true x3 | xB ⇒ pair … true x4 + | xC ⇒ pair … true x5 | xD ⇒ pair … true x6 | xE ⇒ pair … true x7 | xF ⇒ pair … true x8 ] + | x9 ⇒ match e2 with + [ x0 ⇒ pair … false xA | x1 ⇒ pair … false xB | x2 ⇒ pair … false xC | x3 ⇒ pair … false xD + | x4 ⇒ pair … false xE | x5 ⇒ pair … false xF | x6 ⇒ pair … true x0 | x7 ⇒ pair … true x1 + | x8 ⇒ pair … true x2 | x9 ⇒ pair … true x3 | xA ⇒ pair … true x4 | xB ⇒ pair … true x5 + | xC ⇒ pair … true x6 | xD ⇒ pair … true x7 | xE ⇒ pair … true x8 | xF ⇒ pair … true x9 ] + | xA ⇒ match e2 with + [ x0 ⇒ pair … false xB | x1 ⇒ pair … false xC | x2 ⇒ pair … false xD | x3 ⇒ pair … false xE + | x4 ⇒ pair … false xF | x5 ⇒ pair … true x0 | x6 ⇒ pair … true x1 | x7 ⇒ pair … true x2 + | x8 ⇒ pair … true x3 | x9 ⇒ pair … true x4 | xA ⇒ pair … true x5 | xB ⇒ pair … true x6 + | xC ⇒ pair … true x7 | xD ⇒ pair … true x8 | xE ⇒ pair … true x9 | xF ⇒ pair … true xA ] + | xB ⇒ match e2 with + [ x0 ⇒ pair … false xC | x1 ⇒ pair … false xD | x2 ⇒ pair … false xE | x3 ⇒ pair … false xF + | x4 ⇒ pair … true x0 | x5 ⇒ pair … true x1 | x6 ⇒ pair … true x2 | x7 ⇒ pair … true x3 + | x8 ⇒ pair … true x4 | x9 ⇒ pair … true x5 | xA ⇒ pair … true x6 | xB ⇒ pair … true x7 + | xC ⇒ pair … true x8 | xD ⇒ pair … true x9 | xE ⇒ pair … true xA | xF ⇒ pair … true xB ] + | xC ⇒ match e2 with + [ x0 ⇒ pair … false xD | x1 ⇒ pair … false xE | x2 ⇒ pair … false xF | x3 ⇒ pair … true x0 + | x4 ⇒ pair … true x1 | x5 ⇒ pair … true x2 | x6 ⇒ pair … true x3 | x7 ⇒ pair … true x4 + | x8 ⇒ pair … true x5 | x9 ⇒ pair … true x6 | xA ⇒ pair … true x7 | xB ⇒ pair … true x8 + | xC ⇒ pair … true x9 | xD ⇒ pair … true xA | xE ⇒ pair … true xB | xF ⇒ pair … true xC ] + | xD ⇒ match e2 with + [ x0 ⇒ pair … false xE | x1 ⇒ pair … false xF | x2 ⇒ pair … true x0 | x3 ⇒ pair … true x1 + | x4 ⇒ pair … true x2 | x5 ⇒ pair … true x3 | x6 ⇒ pair … true x4 | x7 ⇒ pair … true x5 + | x8 ⇒ pair … true x6 | x9 ⇒ pair … true x7 | xA ⇒ pair … true x8 | xB ⇒ pair … true x9 + | xC ⇒ pair … true xA | xD ⇒ pair … true xB | xE ⇒ pair … true xC | xF ⇒ pair … true xD ] + | xE ⇒ match e2 with + [ x0 ⇒ pair … false xF | x1 ⇒ pair … true x0 | x2 ⇒ pair … true x1 | x3 ⇒ pair … true x2 + | x4 ⇒ pair … true x3 | x5 ⇒ pair … true x4 | x6 ⇒ pair … true x5 | x7 ⇒ pair … true x6 + | x8 ⇒ pair … true x7 | x9 ⇒ pair … true x8 | xA ⇒ pair … true x9 | xB ⇒ pair … true xA + | xC ⇒ pair … true xB | xD ⇒ pair … true xC | xE ⇒ pair … true xD | xF ⇒ pair … true xE ] + | xF ⇒ match e2 with + [ x0 ⇒ pair … true x0 | x1 ⇒ pair … true x1 | x2 ⇒ pair … true x2 | x3 ⇒ pair … true x3 + | x4 ⇒ pair … true x4 | x5 ⇒ pair … true x5 | x6 ⇒ pair … true x6 | x7 ⇒ pair … true x7 + | x8 ⇒ pair … true x8 | x9 ⇒ pair … true x9 | xA ⇒ pair … true xA | xB ⇒ pair … true xB + | xC ⇒ pair … true xC | xD ⇒ pair … true xD | xE ⇒ pair … true xE | xF ⇒ pair … true xF ] + ] + | false ⇒ match e1 with + [ x0 ⇒ match e2 with + [ x0 ⇒ pair … false x0 | x1 ⇒ pair … false x1 | x2 ⇒ pair … false x2 | x3 ⇒ pair … false x3 + | x4 ⇒ pair … false x4 | x5 ⇒ pair … false x5 | x6 ⇒ pair … false x6 | x7 ⇒ pair … false x7 + | x8 ⇒ pair … false x8 | x9 ⇒ pair … false x9 | xA ⇒ pair … false xA | xB ⇒ pair … false xB + | xC ⇒ pair … false xC | xD ⇒ pair … false xD | xE ⇒ pair … false xE | xF ⇒ pair … false xF ] + | x1 ⇒ match e2 with + [ x0 ⇒ pair … false x1 | x1 ⇒ pair … false x2 | x2 ⇒ pair … false x3 | x3 ⇒ pair … false x4 + | x4 ⇒ pair … false x5 | x5 ⇒ pair … false x6 | x6 ⇒ pair … false x7 | x7 ⇒ pair … false x8 + | x8 ⇒ pair … false x9 | x9 ⇒ pair … false xA | xA ⇒ pair … false xB | xB ⇒ pair … false xC + | xC ⇒ pair … false xD | xD ⇒ pair … false xE | xE ⇒ pair … false xF | xF ⇒ pair … true x0 ] + | x2 ⇒ match e2 with + [ x0 ⇒ pair … false x2 | x1 ⇒ pair … false x3 | x2 ⇒ pair … false x4 | x3 ⇒ pair … false x5 + | x4 ⇒ pair … false x6 | x5 ⇒ pair … false x7 | x6 ⇒ pair … false x8 | x7 ⇒ pair … false x9 + | x8 ⇒ pair … false xA | x9 ⇒ pair … false xB | xA ⇒ pair … false xC | xB ⇒ pair … false xD + | xC ⇒ pair … false xE | xD ⇒ pair … false xF | xE ⇒ pair … true x0 | xF ⇒ pair … true x1 ] + | x3 ⇒ match e2 with + [ x0 ⇒ pair … false x3 | x1 ⇒ pair … false x4 | x2 ⇒ pair … false x5 | x3 ⇒ pair … false x6 + | x4 ⇒ pair … false x7 | x5 ⇒ pair … false x8 | x6 ⇒ pair … false x9 | x7 ⇒ pair … false xA + | x8 ⇒ pair … false xB | x9 ⇒ pair … false xC | xA ⇒ pair … false xD | xB ⇒ pair … false xE + | xC ⇒ pair … false xF | xD ⇒ pair … true x0 | xE ⇒ pair … true x1 | xF ⇒ pair … true x2 ] + | x4 ⇒ match e2 with + [ x0 ⇒ pair … false x4 | x1 ⇒ pair … false x5 | x2 ⇒ pair … false x6 | x3 ⇒ pair … false x7 + | x4 ⇒ pair … false x8 | x5 ⇒ pair … false x9 | x6 ⇒ pair … false xA | x7 ⇒ pair … false xB + | x8 ⇒ pair … false xC | x9 ⇒ pair … false xD | xA ⇒ pair … false xE | xB ⇒ pair … false xF + | xC ⇒ pair … true x0 | xD ⇒ pair … true x1 | xE ⇒ pair … true x2 | xF ⇒ pair … true x3 ] + | x5 ⇒ match e2 with + [ x0 ⇒ pair … false x5 | x1 ⇒ pair … false x6 | x2 ⇒ pair … false x7 | x3 ⇒ pair … false x8 + | x4 ⇒ pair … false x9 | x5 ⇒ pair … false xA | x6 ⇒ pair … false xB | x7 ⇒ pair … false xC + | x8 ⇒ pair … false xD | x9 ⇒ pair … false xE | xA ⇒ pair … false xF | xB ⇒ pair … true x0 + | xC ⇒ pair … true x1 | xD ⇒ pair … true x2 | xE ⇒ pair … true x3 | xF ⇒ pair … true x4 ] + | x6 ⇒ match e2 with + [ x0 ⇒ pair … false x6 | x1 ⇒ pair … false x7 | x2 ⇒ pair … false x8 | x3 ⇒ pair … false x9 + | x4 ⇒ pair … false xA | x5 ⇒ pair … false xB | x6 ⇒ pair … false xC | x7 ⇒ pair … false xD + | x8 ⇒ pair … false xE | x9 ⇒ pair … false xF | xA ⇒ pair … true x0 | xB ⇒ pair … true x1 + | xC ⇒ pair … true x2 | xD ⇒ pair … true x3 | xE ⇒ pair … true x4 | xF ⇒ pair … true x5 ] + | x7 ⇒ match e2 with + [ x0 ⇒ pair … false x7 | x1 ⇒ pair … false x8 | x2 ⇒ pair … false x9 | x3 ⇒ pair … false xA + | x4 ⇒ pair … false xB | x5 ⇒ pair … false xC | x6 ⇒ pair … false xD | x7 ⇒ pair … false xE + | x8 ⇒ pair … false xF | x9 ⇒ pair … true x0 | xA ⇒ pair … true x1 | xB ⇒ pair … true x2 + | xC ⇒ pair … true x3 | xD ⇒ pair … true x4 | xE ⇒ pair … true x5 | xF ⇒ pair … true x6 ] + | x8 ⇒ match e2 with + [ x0 ⇒ pair … false x8 | x1 ⇒ pair … false x9 | x2 ⇒ pair … false xA | x3 ⇒ pair … false xB + | x4 ⇒ pair … false xC | x5 ⇒ pair … false xD | x6 ⇒ pair … false xE | x7 ⇒ pair … false xF + | x8 ⇒ pair … true x0 | x9 ⇒ pair … true x1 | xA ⇒ pair … true x2 | xB ⇒ pair … true x3 + | xC ⇒ pair … true x4 | xD ⇒ pair … true x5 | xE ⇒ pair … true x6 | xF ⇒ pair … true x7 ] + | x9 ⇒ match e2 with + [ x0 ⇒ pair … false x9 | x1 ⇒ pair … false xA | x2 ⇒ pair … false xB | x3 ⇒ pair … false xC + | x4 ⇒ pair … false xD | x5 ⇒ pair … false xE | x6 ⇒ pair … false xF | x7 ⇒ pair … true x0 + | x8 ⇒ pair … true x1 | x9 ⇒ pair … true x2 | xA ⇒ pair … true x3 | xB ⇒ pair … true x4 + | xC ⇒ pair … true x5 | xD ⇒ pair … true x6 | xE ⇒ pair … true x7 | xF ⇒ pair … true x8 ] + | xA ⇒ match e2 with + [ x0 ⇒ pair … false xA | x1 ⇒ pair … false xB | x2 ⇒ pair … false xC | x3 ⇒ pair … false xD + | x4 ⇒ pair … false xE | x5 ⇒ pair … false xF | x6 ⇒ pair … true x0 | x7 ⇒ pair … true x1 + | x8 ⇒ pair … true x2 | x9 ⇒ pair … true x3 | xA ⇒ pair … true x4 | xB ⇒ pair … true x5 + | xC ⇒ pair … true x6 | xD ⇒ pair … true x7 | xE ⇒ pair … true x8 | xF ⇒ pair … true x9 ] + | xB ⇒ match e2 with + [ x0 ⇒ pair … false xB | x1 ⇒ pair … false xC | x2 ⇒ pair … false xD | x3 ⇒ pair … false xE + | x4 ⇒ pair … false xF | x5 ⇒ pair … true x0 | x6 ⇒ pair … true x1 | x7 ⇒ pair … true x2 + | x8 ⇒ pair … true x3 | x9 ⇒ pair … true x4 | xA ⇒ pair … true x5 | xB ⇒ pair … true x6 + | xC ⇒ pair … true x7 | xD ⇒ pair … true x8 | xE ⇒ pair … true x9 | xF ⇒ pair … true xA ] + | xC ⇒ match e2 with + [ x0 ⇒ pair … false xC | x1 ⇒ pair … false xD | x2 ⇒ pair … false xE | x3 ⇒ pair … false xF + | x4 ⇒ pair … true x0 | x5 ⇒ pair … true x1 | x6 ⇒ pair … true x2 | x7 ⇒ pair … true x3 + | x8 ⇒ pair … true x4 | x9 ⇒ pair … true x5 | xA ⇒ pair … true x6 | xB ⇒ pair … true x7 + | xC ⇒ pair … true x8 | xD ⇒ pair … true x9 | xE ⇒ pair … true xA | xF ⇒ pair … true xB ] + | xD ⇒ match e2 with + [ x0 ⇒ pair … false xD | x1 ⇒ pair … false xE | x2 ⇒ pair … false xF | x3 ⇒ pair … true x0 + | x4 ⇒ pair … true x1 | x5 ⇒ pair … true x2 | x6 ⇒ pair … true x3 | x7 ⇒ pair … true x4 + | x8 ⇒ pair … true x5 | x9 ⇒ pair … true x6 | xA ⇒ pair … true x7 | xB ⇒ pair … true x8 + | xC ⇒ pair … true x9 | xD ⇒ pair … true xA | xE ⇒ pair … true xB | xF ⇒ pair … true xC ] + | xE ⇒ match e2 with + [ x0 ⇒ pair … false xE | x1 ⇒ pair … false xF | x2 ⇒ pair … true x0 | x3 ⇒ pair … true x1 + | x4 ⇒ pair … true x2 | x5 ⇒ pair … true x3 | x6 ⇒ pair … true x4 | x7 ⇒ pair … true x5 + | x8 ⇒ pair … true x6 | x9 ⇒ pair … true x7 | xA ⇒ pair … true x8 | xB ⇒ pair … true x9 + | xC ⇒ pair … true xA | xD ⇒ pair … true xB | xE ⇒ pair … true xC | xF ⇒ pair … true xD ] + | xF ⇒ match e2 with + [ x0 ⇒ pair … false xF | x1 ⇒ pair … true x0 | x2 ⇒ pair … true x1 | x3 ⇒ pair … true x2 + | x4 ⇒ pair … true x3 | x5 ⇒ pair … true x4 | x6 ⇒ pair … true x5 | x7 ⇒ pair … true x6 + | x8 ⇒ pair … true x7 | x9 ⇒ pair … true x8 | xA ⇒ pair … true x9 | xB ⇒ pair … true xA + | xC ⇒ pair … true xB | xD ⇒ pair … true xC | xE ⇒ pair … true xD | xF ⇒ pair … true xE ] + ]]. + +(* operatore somma con data → data+carry *) +ndefinition plus_ex_d_dc ≝ +λe1,e2:exadecim. + match e1 with + [ x0 ⇒ match e2 with + [ x0 ⇒ pair … false x0 | x1 ⇒ pair … false x1 | x2 ⇒ pair … false x2 | x3 ⇒ pair … false x3 + | x4 ⇒ pair … false x4 | x5 ⇒ pair … false x5 | x6 ⇒ pair … false x6 | x7 ⇒ pair … false x7 + | x8 ⇒ pair … false x8 | x9 ⇒ pair … false x9 | xA ⇒ pair … false xA | xB ⇒ pair … false xB + | xC ⇒ pair … false xC | xD ⇒ pair … false xD | xE ⇒ pair … false xE | xF ⇒ pair … false xF ] + | x1 ⇒ match e2 with + [ x0 ⇒ pair … false x1 | x1 ⇒ pair … false x2 | x2 ⇒ pair … false x3 | x3 ⇒ pair … false x4 + | x4 ⇒ pair … false x5 | x5 ⇒ pair … false x6 | x6 ⇒ pair … false x7 | x7 ⇒ pair … false x8 + | x8 ⇒ pair … false x9 | x9 ⇒ pair … false xA | xA ⇒ pair … false xB | xB ⇒ pair … false xC + | xC ⇒ pair … false xD | xD ⇒ pair … false xE | xE ⇒ pair … false xF | xF ⇒ pair … true x0 ] + | x2 ⇒ match e2 with + [ x0 ⇒ pair … false x2 | x1 ⇒ pair … false x3 | x2 ⇒ pair … false x4 | x3 ⇒ pair … false x5 + | x4 ⇒ pair … false x6 | x5 ⇒ pair … false x7 | x6 ⇒ pair … false x8 | x7 ⇒ pair … false x9 + | x8 ⇒ pair … false xA | x9 ⇒ pair … false xB | xA ⇒ pair … false xC | xB ⇒ pair … false xD + | xC ⇒ pair … false xE | xD ⇒ pair … false xF | xE ⇒ pair … true x0 | xF ⇒ pair … true x1 ] + | x3 ⇒ match e2 with + [ x0 ⇒ pair … false x3 | x1 ⇒ pair … false x4 | x2 ⇒ pair … false x5 | x3 ⇒ pair … false x6 + | x4 ⇒ pair … false x7 | x5 ⇒ pair … false x8 | x6 ⇒ pair … false x9 | x7 ⇒ pair … false xA + | x8 ⇒ pair … false xB | x9 ⇒ pair … false xC | xA ⇒ pair … false xD | xB ⇒ pair … false xE + | xC ⇒ pair … false xF | xD ⇒ pair … true x0 | xE ⇒ pair … true x1 | xF ⇒ pair … true x2 ] + | x4 ⇒ match e2 with + [ x0 ⇒ pair … false x4 | x1 ⇒ pair … false x5 | x2 ⇒ pair … false x6 | x3 ⇒ pair … false x7 + | x4 ⇒ pair … false x8 | x5 ⇒ pair … false x9 | x6 ⇒ pair … false xA | x7 ⇒ pair … false xB + | x8 ⇒ pair … false xC | x9 ⇒ pair … false xD | xA ⇒ pair … false xE | xB ⇒ pair … false xF + | xC ⇒ pair … true x0 | xD ⇒ pair … true x1 | xE ⇒ pair … true x2 | xF ⇒ pair … true x3 ] + | x5 ⇒ match e2 with + [ x0 ⇒ pair … false x5 | x1 ⇒ pair … false x6 | x2 ⇒ pair … false x7 | x3 ⇒ pair … false x8 + | x4 ⇒ pair … false x9 | x5 ⇒ pair … false xA | x6 ⇒ pair … false xB | x7 ⇒ pair … false xC + | x8 ⇒ pair … false xD | x9 ⇒ pair … false xE | xA ⇒ pair … false xF | xB ⇒ pair … true x0 + | xC ⇒ pair … true x1 | xD ⇒ pair … true x2 | xE ⇒ pair … true x3 | xF ⇒ pair … true x4 ] + | x6 ⇒ match e2 with + [ x0 ⇒ pair … false x6 | x1 ⇒ pair … false x7 | x2 ⇒ pair … false x8 | x3 ⇒ pair … false x9 + | x4 ⇒ pair … false xA | x5 ⇒ pair … false xB | x6 ⇒ pair … false xC | x7 ⇒ pair … false xD + | x8 ⇒ pair … false xE | x9 ⇒ pair … false xF | xA ⇒ pair … true x0 | xB ⇒ pair … true x1 + | xC ⇒ pair … true x2 | xD ⇒ pair … true x3 | xE ⇒ pair … true x4 | xF ⇒ pair … true x5 ] + | x7 ⇒ match e2 with + [ x0 ⇒ pair … false x7 | x1 ⇒ pair … false x8 | x2 ⇒ pair … false x9 | x3 ⇒ pair … false xA + | x4 ⇒ pair … false xB | x5 ⇒ pair … false xC | x6 ⇒ pair … false xD | x7 ⇒ pair … false xE + | x8 ⇒ pair … false xF | x9 ⇒ pair … true x0 | xA ⇒ pair … true x1 | xB ⇒ pair … true x2 + | xC ⇒ pair … true x3 | xD ⇒ pair … true x4 | xE ⇒ pair … true x5 | xF ⇒ pair … true x6 ] + | x8 ⇒ match e2 with + [ x0 ⇒ pair … false x8 | x1 ⇒ pair … false x9 | x2 ⇒ pair … false xA | x3 ⇒ pair … false xB + | x4 ⇒ pair … false xC | x5 ⇒ pair … false xD | x6 ⇒ pair … false xE | x7 ⇒ pair … false xF + | x8 ⇒ pair … true x0 | x9 ⇒ pair … true x1 | xA ⇒ pair … true x2 | xB ⇒ pair … true x3 + | xC ⇒ pair … true x4 | xD ⇒ pair … true x5 | xE ⇒ pair … true x6 | xF ⇒ pair … true x7 ] + | x9 ⇒ match e2 with + [ x0 ⇒ pair … false x9 | x1 ⇒ pair … false xA | x2 ⇒ pair … false xB | x3 ⇒ pair … false xC + | x4 ⇒ pair … false xD | x5 ⇒ pair … false xE | x6 ⇒ pair … false xF | x7 ⇒ pair … true x0 + | x8 ⇒ pair … true x1 | x9 ⇒ pair … true x2 | xA ⇒ pair … true x3 | xB ⇒ pair … true x4 + | xC ⇒ pair … true x5 | xD ⇒ pair … true x6 | xE ⇒ pair … true x7 | xF ⇒ pair … true x8 ] + | xA ⇒ match e2 with + [ x0 ⇒ pair … false xA | x1 ⇒ pair … false xB | x2 ⇒ pair … false xC | x3 ⇒ pair … false xD + | x4 ⇒ pair … false xE | x5 ⇒ pair … false xF | x6 ⇒ pair … true x0 | x7 ⇒ pair … true x1 + | x8 ⇒ pair … true x2 | x9 ⇒ pair … true x3 | xA ⇒ pair … true x4 | xB ⇒ pair … true x5 + | xC ⇒ pair … true x6 | xD ⇒ pair … true x7 | xE ⇒ pair … true x8 | xF ⇒ pair … true x9 ] + | xB ⇒ match e2 with + [ x0 ⇒ pair … false xB | x1 ⇒ pair … false xC | x2 ⇒ pair … false xD | x3 ⇒ pair … false xE + | x4 ⇒ pair … false xF | x5 ⇒ pair … true x0 | x6 ⇒ pair … true x1 | x7 ⇒ pair … true x2 + | x8 ⇒ pair … true x3 | x9 ⇒ pair … true x4 | xA ⇒ pair … true x5 | xB ⇒ pair … true x6 + | xC ⇒ pair … true x7 | xD ⇒ pair … true x8 | xE ⇒ pair … true x9 | xF ⇒ pair … true xA ] + | xC ⇒ match e2 with + [ x0 ⇒ pair … false xC | x1 ⇒ pair … false xD | x2 ⇒ pair … false xE | x3 ⇒ pair … false xF + | x4 ⇒ pair … true x0 | x5 ⇒ pair … true x1 | x6 ⇒ pair … true x2 | x7 ⇒ pair … true x3 + | x8 ⇒ pair … true x4 | x9 ⇒ pair … true x5 | xA ⇒ pair … true x6 | xB ⇒ pair … true x7 + | xC ⇒ pair … true x8 | xD ⇒ pair … true x9 | xE ⇒ pair … true xA | xF ⇒ pair … true xB ] + | xD ⇒ match e2 with + [ x0 ⇒ pair … false xD | x1 ⇒ pair … false xE | x2 ⇒ pair … false xF | x3 ⇒ pair … true x0 + | x4 ⇒ pair … true x1 | x5 ⇒ pair … true x2 | x6 ⇒ pair … true x3 | x7 ⇒ pair … true x4 + | x8 ⇒ pair … true x5 | x9 ⇒ pair … true x6 | xA ⇒ pair … true x7 | xB ⇒ pair … true x8 + | xC ⇒ pair … true x9 | xD ⇒ pair … true xA | xE ⇒ pair … true xB | xF ⇒ pair … true xC ] + | xE ⇒ match e2 with + [ x0 ⇒ pair … false xE | x1 ⇒ pair … false xF | x2 ⇒ pair … true x0 | x3 ⇒ pair … true x1 + | x4 ⇒ pair … true x2 | x5 ⇒ pair … true x3 | x6 ⇒ pair … true x4 | x7 ⇒ pair … true x5 + | x8 ⇒ pair … true x6 | x9 ⇒ pair … true x7 | xA ⇒ pair … true x8 | xB ⇒ pair … true x9 + | xC ⇒ pair … true xA | xD ⇒ pair … true xB | xE ⇒ pair … true xC | xF ⇒ pair … true xD ] + | xF ⇒ match e2 with + [ x0 ⇒ pair … false xF | x1 ⇒ pair … true x0 | x2 ⇒ pair … true x1 | x3 ⇒ pair … true x2 + | x4 ⇒ pair … true x3 | x5 ⇒ pair … true x4 | x6 ⇒ pair … true x5 | x7 ⇒ pair … true x6 + | x8 ⇒ pair … true x7 | x9 ⇒ pair … true x8 | xA ⇒ pair … true x9 | xB ⇒ pair … true xA + | xC ⇒ pair … true xB | xD ⇒ pair … true xC | xE ⇒ pair … true xD | xF ⇒ pair … true xE ] + ]. + +(* operatore somma con data+carry → data *) +ndefinition plus_ex_dc_d ≝ +λc:bool.λe1,e2:exadecim. + 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 ≝ +λc:bool.λe1,e2:exadecim. + 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 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 abs *) +ndefinition abs_ex ≝ +λe:exadecim.match getMSB_ex e with + [ true ⇒ compl_ex e | false ⇒ e ]. + +(* operatore x in [inf,sup] o in sup],[inf *) +ndefinition inrange_ex ≝ +λx,inf,sup:exadecim. + match le_ex inf sup with + [ true ⇒ and_bool | false ⇒ or_bool ] + (le_ex inf x) (le_ex x sup). + +(* 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)))))))))))))) + ]. + +(* 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 ]. + +(* esadecimali xNNNN → ottali *) +ndefinition oct_of_exL ≝ +λn.match n with + [ x0 ⇒ o0 | x1 ⇒ o1 | x2 ⇒ o2 | x3 ⇒ o3 | x4 ⇒ o4 | x5 ⇒ o5 | x6 ⇒ o6 | x7 ⇒ o7 + | x8 ⇒ o0 | x9 ⇒ o1 | xA ⇒ o2 | xB ⇒ o3 | xC ⇒ o4 | xD ⇒ o5 | xE ⇒ o6 | xF ⇒ o7 ]. + +(* esadecimali NNNNx → ottali *) +ndefinition oct_of_exH ≝ +λn.match n with + [ x0 ⇒ o0 | x1 ⇒ o0 | x2 ⇒ o1 | x3 ⇒ o1 | x4 ⇒ o2 | x5 ⇒ o2 | x6 ⇒ o3 | x7 ⇒ o3 + | x8 ⇒ o4 | x9 ⇒ o4 | xA ⇒ o5 | xB ⇒ o5 | xC ⇒ o6 | xD ⇒ o6 | xE ⇒ o7 | xF ⇒ o7 ]. + +ndefinition exadecim_destruct_aux ≝ +Πe1,e2.ΠP:Prop.ΠH:e1 = e2. + match eq_ex e1 e2 with [ true ⇒ P → P | false ⇒ P ]. + +ndefinition exadecim_destruct : exadecim_destruct_aux. + #e1; #e2; #P; #H; + nrewrite < H; + nelim e1; + nnormalize; + napply (λx.x). +nqed. + +nlemma eq_to_eqex : ∀n1,n2.n1 = n2 → eq_ex n1 n2 = true. + #n1; #n2; #H; + nrewrite > H; + nelim n2; + nnormalize; + napply refl_eq. +nqed. + +nlemma neqex_to_neq : ∀n1,n2.eq_ex n1 n2 = false → n1 ≠ n2. + #n1; #n2; #H; + napply (not_to_not (n1 = n2) (eq_ex n1 n2 = true) …); + ##[ ##1: napply (eq_to_eqex n1 n2) + ##| ##2: napply (eqfalse_to_neqtrue … H) + ##] +nqed. + +nlemma eqex_to_eq : ∀n1,n2.eq_ex n1 n2 = true → n1 = n2. + #n1; #n2; + ncases n1; + ncases n2; + nnormalize; + ##[ ##1,18,35,52,69,86,103,120,137,154,171,188,205,222,239,256: #H; napply refl_eq + ##| ##*: #H; (*ndestruct lentissima...*) napply (bool_destruct … H) + ##] +nqed. + +nlemma neq_to_neqex : ∀n1,n2.n1 ≠ n2 → eq_ex n1 n2 = false. + #n1; #n2; #H; + napply (neqtrue_to_eqfalse (eq_ex n1 n2)); + napply (not_to_not (eq_ex n1 n2 = true) (n1 = n2) ? H); + napply (eqex_to_eq n1 n2). +nqed. + +nlemma decidable_ex : ∀x,y:exadecim.decidable (x = y). + #x; #y; nnormalize; + napply (or2_elim (eq_ex x y = true) (eq_ex x y = false) ? (decidable_bexpr ?)); + ##[ ##1: #H; napply (or2_intro1 (x = y) (x ≠ y) (eqex_to_eq … H)) + ##| ##2: #H; napply (or2_intro2 (x = y) (x ≠ y) (neqex_to_neq … H)) + ##] +nqed. + +nlemma symmetric_eqex : symmetricT exadecim bool eq_ex. + #n1; #n2; + napply (or2_elim (n1 = n2) (n1 ≠ n2) ? (decidable_ex n1 n2)); + ##[ ##1: #H; nrewrite > H; napply refl_eq + ##| ##2: #H; nrewrite > (neq_to_neqex n1 n2 H); + napply (symmetric_eq ? (eq_ex n2 n1) false); + napply (neq_to_neqex n2 n1 (symmetric_neq ? n1 n2 H)) + ##] +nqed. + +nlemma exadecim_is_comparable : comparable. + @ exadecim + ##[ napply x0 + ##| napply forall_ex + ##| napply eq_ex + ##| napply eqex_to_eq + ##| napply eq_to_eqex + ##| napply neqex_to_neq + ##| napply neq_to_neqex + ##| napply decidable_ex + ##| napply symmetric_eqex + ##] +nqed. + +unification hint 0 ≔ ⊢ carr exadecim_is_comparable ≡ exadecim. + +nlemma exadecim_is_comparable_ext : comparable_ext. + napply mk_comparable_ext; + ##[ napply exadecim_is_comparable + ##| napply lt_ex + ##| napply le_ex + ##| napply gt_ex + ##| napply ge_ex + ##| napply and_ex + ##| napply or_ex + ##| napply xor_ex + ##| napply getMSB_ex + ##| napply setMSB_ex + ##| napply clrMSB_ex + ##| napply getLSB_ex + ##| napply setLSB_ex + ##| napply clrLSB_ex + ##| napply rcr_ex + ##| napply shr_ex + ##| napply ror_ex + ##| napply rcl_ex + ##| napply shl_ex + ##| napply rol_ex + ##| napply not_ex + ##| napply plus_ex_dc_dc + ##| napply plus_ex_d_dc + ##| napply plus_ex_dc_d + ##| napply plus_ex_d_d + ##| napply plus_ex_dc_c + ##| napply plus_ex_d_c + ##| napply pred_ex + ##| napply succ_ex + ##| napply compl_ex + ##| napply abs_ex + ##| napply inrange_ex + ##] +nqed. + +unification hint 0 ≔ ⊢ carr (comp_base exadecim_is_comparable_ext) ≡ exadecim.