--- /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 *)
+(* Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* *)
+(* ********************************************************************** *)
+
+include "num/bool.ma".
+
+(* ****** *)
+(* OPTION *)
+(* ****** *)
+
+ninductive option (A:Type) : Type ≝
+ None : option A
+| Some : A → option A.
+
+ndefinition eq_option ≝
+λT.λop1,op2:option T.λf:T → T → bool.
+ match op1 with
+ [ None ⇒ match op2 with [ None ⇒ true | Some _ ⇒ false ]
+ | Some x1 ⇒ match op2 with [ None ⇒ false | Some x2 ⇒ f x1 x2 ]
+ ].
+
+(* option map = match ... with [ None ⇒ None ? | Some .. ⇒ .. ] *)
+ndefinition opt_map ≝
+λT1,T2:Type.λt:option T1.λf:T1 → option T2.
+ match t with [ None ⇒ None ? | Some x ⇒ (f x) ].
--- /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 *)
+(* Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* *)
+(* ********************************************************************** *)
+
+include "common/option.ma".
+include "num/bool_lemmas.ma".
+
+(* ****** *)
+(* OPTION *)
+(* ****** *)
+
+nlemma option_destruct_some_some : ∀T.∀x1,x2:T.Some T x1 = Some T x2 → x1 = x2.
+ #T; #x1; #x2; #H;
+ nchange with (match Some T x2 with [ None ⇒ False | Some a ⇒ x1 = a ]);
+ nrewrite < H;
+ nnormalize;
+ napply refl_eq.
+nqed.
+
+nlemma option_destruct_some_none : ∀T.∀x:T.Some T x = None T → False.
+ #T; #x; #H;
+ nchange with (match Some T x with [ None ⇒ True | Some a ⇒ False ]);
+ nrewrite > H;
+ nnormalize;
+ napply I.
+nqed.
+
+nlemma option_destruct_none_some : ∀T.∀x:T.None T = Some T x → False.
+ #T; #x; #H;
+ nchange with (match Some T x with [ None ⇒ True | Some a ⇒ False ]);
+ nrewrite < H;
+ nnormalize;
+ napply I.
+nqed.
+
+nlemma symmetric_eqoption :
+∀T:Type.∀op1,op2:option T.∀f:T → T → bool.
+ (symmetricT T bool f) →
+ (eq_option T op1 op2 f = eq_option T op2 op1 f).
+ #T; #op1; #op2; #f; #H;
+ nelim op1;
+ nelim op2;
+ nnormalize;
+ ##[ ##1: napply refl_eq
+ ##| ##2,3: #H; napply refl_eq
+ ##| ##4: #a; #a0;
+ nrewrite > (H a0 a);
+ napply refl_eq
+ ##]
+nqed.
+
+nlemma eq_to_eqoption :
+∀T.∀op1,op2:option T.∀f:T → T → bool.
+ (∀x1,x2:T.x1 = x2 → f x1 x2 = true) →
+ (op1 = op2 → eq_option T op1 op2 f = true).
+ #T; #op1; #op2; #f; #H;
+ nelim op1;
+ nelim op2;
+ nnormalize;
+ ##[ ##1: #H1; napply refl_eq
+ ##| ##2: #a; #H1; nelim (option_destruct_none_some ?? H1)
+ ##| ##3: #a; #H1; nelim (option_destruct_some_none ?? H1)
+ ##| ##4: #a; #a0; #H1;
+ nrewrite > (H … (option_destruct_some_some … H1));
+ napply refl_eq
+ ##]
+nqed.
+
+nlemma eqoption_to_eq :
+∀T.∀op1,op2:option T.∀f:T → T → bool.
+ (∀x1,x2:T.f x1 x2 = true → x1 = x2) →
+ (eq_option T op1 op2 f = true → op1 = op2).
+ #T; #op1; #op2; #f; #H;
+ nelim op1;
+ nelim op2;
+ nnormalize;
+ ##[ ##1: #H1; napply refl_eq
+ ##| ##2,3: #a; #H1; napply (bool_destruct … H1)
+ ##| ##4: #a; #a0; #H1;
+ nrewrite > (H … H1);
+ napply refl_eq
+ ##]
+nqed.
+
+nlemma neq_to_neqoption :
+∀T.∀op1,op2:option T.∀f:T → T → bool.
+ (∀x1,x2:T.x1 ≠ x2 → f x1 x2 = false) →
+ (op1 ≠ op2 → eq_option T op1 op2 f = false).
+ #T; #op1; #op2; #f; #H;
+ nelim op1;
+ nelim op2;
+ nnormalize;
+ ##[ ##1: #H1; napply False_ind; napply (H1 (refl_eq …))
+ ##| ##2,3: #a; #H1; napply refl_eq
+ ##| ##4: #a; #a0; #H1;
+ napply H;
+ napply (neqf_to_neq … a0 a (λx.Some ? x) H1)
+ ##]
+nqed.
+
+nlemma neqoption_to_neq :
+∀T.∀op1,op2:option T.∀f:T → T → bool.
+ (∀x1,x2:T.f x1 x2 = false → x1 ≠ x2) →
+ (eq_option T op1 op2 f = false → op1 ≠ op2).
+ #T; #op1; #op2; #f; #H;
+ nelim op1;
+ nelim op2;
+ nnormalize;
+ ##[ ##1: #H1; napply (bool_destruct … H1)
+ ##| ##2: #a; #H1; #H2; napply (option_destruct_none_some ? a H2)
+ ##| ##3: #a; #H1; #H2; napply (option_destruct_some_none ? a H2)
+ ##| ##4: #a; #a0; #H1; #H2;
+ napply (H a0 a H1);
+ napply (option_destruct_some_some ? a0 a H2)
+ ##]
+nqed.
--- /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 *)
+(* Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* *)
+(* ********************************************************************** *)
+
+include "num/bool.ma".
+
+(* ***** *)
+(* TUPLE *)
+(* ***** *)
+
+ninductive ProdT (T1:Type) (T2:Type) : Type ≝
+ pair : T1 → T2 → ProdT T1 T2.
+
+ndefinition fst ≝
+λT1,T2:Type.λp:ProdT T1 T2.match p with [ pair x _ ⇒ x ].
+
+ndefinition snd ≝
+λT1,T2:Type.λp:ProdT T1 T2.match p with [ pair _ x ⇒ x ].
+
+ndefinition eq_pair ≝
+λT1,T2:Type.λp1,p2:ProdT T1 T2.
+λf1:T1 → T1 → bool.λf2:T2 → T2 → bool.
+ match p1 with [ pair x1 y1 ⇒
+ match p2 with [ pair x2 y2 ⇒
+ (f1 x1 x2) ⊗ (f2 y1 y2) ]].
+
+ninductive Prod3T (T1:Type) (T2:Type) (T3:Type) : Type ≝
+triple : T1 → T2 → T3 → Prod3T T1 T2 T3.
+
+ndefinition fst3T ≝
+λT1.λT2.λT3.λp:Prod3T T1 T2 T3.match p with [ triple x _ _ ⇒ x ].
+
+ndefinition snd3T ≝
+λT1.λT2.λT3.λp:Prod3T T1 T2 T3.match p with [ triple _ x _ ⇒ x ].
+
+ndefinition thd3T ≝
+λT1.λT2.λT3.λp:Prod3T T1 T2 T3.match p with [ triple _ _ x ⇒ x ].
+
+ndefinition eq_triple ≝
+λT1,T2,T3:Type.λp1,p2:Prod3T T1 T2 T3.
+λf1:T1 → T1 → bool.λf2:T2 → T2 → bool.λf3:T3 → T3 → bool.
+ match p1 with [ triple x1 y1 z1 ⇒
+ match p2 with [ triple x2 y2 z2 ⇒
+ (f1 x1 x2) ⊗ (f2 y1 y2) ⊗ (f3 z1 z2) ]].
+
+ninductive Prod4T (T1:Type) (T2:Type) (T3:Type) (T4:Type) : Type ≝
+quadruple : T1 → T2 → T3 → T4 → Prod4T T1 T2 T3 T4.
+
+ndefinition fst4T ≝
+λT1.λT2.λT3.λT4.λp:Prod4T T1 T2 T3 T4.match p with [ quadruple x _ _ _ ⇒ x ].
+
+ndefinition snd4T ≝
+λT1.λT2.λT3.λT4.λp:Prod4T T1 T2 T3 T4.match p with [ quadruple _ x _ _ ⇒ x ].
+
+ndefinition thd4T ≝
+λT1.λT2.λT3.λT4.λp:Prod4T T1 T2 T3 T4.match p with [ quadruple _ _ x _ ⇒ x ].
+
+ndefinition fth4T ≝
+λT1.λT2.λT3.λT4.λp:Prod4T T1 T2 T3 T4.match p with [ quadruple _ _ _ x ⇒ x ].
+
+ndefinition eq_quadruple ≝
+λT1,T2,T3,T4:Type.λp1,p2:Prod4T T1 T2 T3 T4.
+λf1:T1 → T1 → bool.λf2:T2 → T2 → bool.λf3:T3 → T3 → bool.λf4:T4 → T4 → bool.
+ match p1 with [ quadruple x1 y1 z1 w1 ⇒
+ match p2 with [ quadruple x2 y2 z2 w2 ⇒
+ (f1 x1 x2) ⊗ (f2 y1 y2) ⊗ (f3 z1 z2) ⊗ (f4 w1 w2) ]].
+
+ninductive Prod5T (T1:Type) (T2:Type) (T3:Type) (T4:Type) (T5:Type) : Type ≝
+quintuple : T1 → T2 → T3 → T4 → T5 → Prod5T T1 T2 T3 T4 T5.
+
+ndefinition fst5T ≝
+λT1.λT2.λT3.λT4.λT5.λp:Prod5T T1 T2 T3 T4 T5.match p with [ quintuple x _ _ _ _ ⇒ x ].
+
+ndefinition snd5T ≝
+λT1.λT2.λT3.λT4.λT5.λp:Prod5T T1 T2 T3 T4 T5.match p with [ quintuple _ x _ _ _ ⇒ x ].
+
+ndefinition thd5T ≝
+λT1.λT2.λT3.λT4.λT5.λp:Prod5T T1 T2 T3 T4 T5.match p with [ quintuple _ _ x _ _ ⇒ x ].
+
+ndefinition frth5T ≝
+λT1.λT2.λT3.λT4.λT5.λp:Prod5T T1 T2 T3 T4 T5.match p with [ quintuple _ _ _ x _ ⇒ x ].
+
+ndefinition ffth5T ≝
+λT1.λT2.λT3.λT4.λT5.λp:Prod5T T1 T2 T3 T4 T5.match p with [ quintuple _ _ _ _ x ⇒ x ].
+
+ndefinition eq_quintuple ≝
+λT1,T2,T3,T4,T5:Type.λp1,p2:Prod5T T1 T2 T3 T4 T5.
+λf1:T1 → T1 → bool.λf2:T2 → T2 → bool.λf3:T3 → T3 → bool.λf4:T4 → T4 → bool.λf5:T5 → T5 → bool.
+ match p1 with [ quintuple x1 y1 z1 w1 v1 ⇒
+ match p2 with [ quintuple x2 y2 z2 w2 v2 ⇒
+ (f1 x1 x2) ⊗ (f2 y1 y2) ⊗ (f3 z1 z2) ⊗ (f4 w1 w2) ⊗ (f5 v1 v2) ]].
--- /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 *)
+(* Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* *)
+(* ********************************************************************** *)
+
+include "common/prod.ma".
+include "num/bool_lemmas.ma".
+
+(* ***** *)
+(* TUPLE *)
+(* ***** *)
+
+nlemma pair_destruct_1 :
+∀T1,T2.∀x1,x2:T1.∀y1,y2:T2.
+ pair T1 T2 x1 y1 = pair T1 T2 x2 y2 → x1 = x2.
+ #T1; #T2; #x1; #x2; #y1; #y2; #H;
+ nchange with (match pair T1 T2 x2 y2 with [ pair a _ ⇒ x1 = a ]);
+ nrewrite < H;
+ nnormalize;
+ napply refl_eq.
+nqed.
+
+nlemma pair_destruct_2 :
+∀T1,T2.∀x1,x2:T1.∀y1,y2:T2.
+ pair T1 T2 x1 y1 = pair T1 T2 x2 y2 → y1 = y2.
+ #T1; #T2; #x1; #x2; #y1; #y2; #H;
+ nchange with (match pair T1 T2 x2 y2 with [ pair _ b ⇒ y1 = b ]);
+ nrewrite < H;
+ nnormalize;
+ napply refl_eq.
+nqed.
+
+nlemma symmetric_eqpair :
+∀T1,T2:Type.∀p1,p2:ProdT T1 T2.
+∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.
+ (symmetricT T1 bool f1) →
+ (symmetricT T2 bool f2) →
+ (eq_pair T1 T2 p1 p2 f1 f2 = eq_pair T1 T2 p2 p1 f1 f2).
+ #T1; #T2; #p1; #p2; #f1; #f2; #H; #H1;
+ nelim p1;
+ #x1; #y1;
+ nelim p2;
+ #x2; #y2;
+ nnormalize;
+ nrewrite > (H x1 x2);
+ ncases (f1 x2 x1);
+ nnormalize;
+ ##[ ##1: nrewrite > (H1 y1 y2); napply refl_eq
+ ##| ##2: napply refl_eq
+ ##]
+nqed.
+
+nlemma eq_to_eqpair :
+∀T1,T2.∀p1,p2:ProdT T1 T2.
+∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.
+ (∀x1,x2:T1.x1 = x2 → f1 x1 x2 = true) →
+ (∀y1,y2:T2.y1 = y2 → f2 y1 y2 = true) →
+ (p1 = p2 → eq_pair T1 T2 p1 p2 f1 f2 = true).
+ #T1; #T2; #p1; #p2; #f1; #f2; #H1; #H2;
+ nelim p1;
+ #x1; #y1;
+ nelim p2;
+ #x2; #y2; #H;
+ nnormalize;
+ nrewrite > (H1 … (pair_destruct_1 … H));
+ nnormalize;
+ nrewrite > (H2 … (pair_destruct_2 … H));
+ napply refl_eq.
+nqed.
+
+nlemma eqpair_to_eq :
+∀T1,T2.∀p1,p2:ProdT T1 T2.
+∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.
+ (∀x1,x2:T1.f1 x1 x2 = true → x1 = x2) →
+ (∀y1,y2:T2.f2 y1 y2 = true → y1 = y2) →
+ (eq_pair T1 T2 p1 p2 f1 f2 = true → p1 = p2).
+ #T1; #T2; #p1; #p2; #f1; #f2; #H1; #H2;
+ nelim p1;
+ #x1; #y1;
+ nelim p2;
+ #x2; #y2; #H;
+ nnormalize in H:(%);
+ nletin K ≝ (H1 x1 x2);
+ ncases (f1 x1 x2) in H:(%) K:(%);
+ nnormalize;
+ #H3;
+ ##[ ##2: napply (bool_destruct … H3) ##]
+ #H4;
+ nrewrite > (H4 (refl_eq …));
+ nrewrite > (H2 y1 y2 H3);
+ napply refl_eq.
+nqed.
+
+nlemma triple_destruct_1 :
+∀T1,T2,T3.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.
+ triple T1 T2 T3 x1 y1 z1 = triple T1 T2 T3 x2 y2 z2 → x1 = x2.
+ #T1; #T2; #T3; #x1; #x2; #y1; #y2; #z1; #z2; #H;
+ nchange with (match triple T1 T2 T3 x2 y2 z2 with [ triple a _ _ ⇒ x1 = a ]);
+ nrewrite < H;
+ nnormalize;
+ napply refl_eq.
+nqed.
+
+nlemma triple_destruct_2 :
+∀T1,T2,T3.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.
+ triple T1 T2 T3 x1 y1 z1 = triple T1 T2 T3 x2 y2 z2 → y1 = y2.
+ #T1; #T2; #T3; #x1; #x2; #y1; #y2; #z1; #z2; #H;
+ nchange with (match triple T1 T2 T3 x2 y2 z2 with [ triple _ b _ ⇒ y1 = b ]);
+ nrewrite < H;
+ nnormalize;
+ napply refl_eq.
+nqed.
+
+nlemma triple_destruct_3 :
+∀T1,T2,T3.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.
+ triple T1 T2 T3 x1 y1 z1 = triple T1 T2 T3 x2 y2 z2 → z1 = z2.
+ #T1; #T2; #T3; #x1; #x2; #y1; #y2; #z1; #z2; #H;
+ nchange with (match triple T1 T2 T3 x2 y2 z2 with [ triple _ _ c ⇒ z1 = c ]);
+ nrewrite < H;
+ nnormalize;
+ napply refl_eq.
+nqed.
+
+nlemma symmetric_eqtriple :
+∀T1,T2,T3:Type.∀p1,p2:Prod3T T1 T2 T3.
+∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.
+ (symmetricT T1 bool f1) →
+ (symmetricT T2 bool f2) →
+ (symmetricT T3 bool f3) →
+ (eq_triple T1 T2 T3 p1 p2 f1 f2 f3 = eq_triple T1 T2 T3 p2 p1 f1 f2 f3).
+ #T1; #T2; #T3; #p1; #p2; #f1; #f2; #f3; #H; #H1; #H2;
+ nelim p1;
+ #x1; #y1; #z1;
+ nelim p2;
+ #x2; #y2; #z2;
+ nnormalize;
+ nrewrite > (H x1 x2);
+ ncases (f1 x2 x1);
+ nnormalize;
+ ##[ ##1: nrewrite > (H1 y1 y2);
+ ncases (f2 y2 y1);
+ nnormalize;
+ ##[ ##1: nrewrite > (H2 z1 z2); napply refl_eq
+ ##| ##2: napply refl_eq
+ ##]
+ ##| ##2: napply refl_eq
+ ##]
+nqed.
+
+nlemma eq_to_eqtriple :
+∀T1,T2,T3.∀p1,p2:Prod3T T1 T2 T3.
+∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.
+ (∀x1,x2:T1.x1 = x2 → f1 x1 x2 = true) →
+ (∀y1,y2:T2.y1 = y2 → f2 y1 y2 = true) →
+ (∀z1,z2:T3.z1 = z2 → f3 z1 z2 = true) →
+ (p1 = p2 → eq_triple T1 T2 T3 p1 p2 f1 f2 f3 = true).
+ #T1; #T2; #T3; #p1; #p2; #f1; #f2; #f3; #H1; #H2; #H3;
+ nelim p1;
+ #x1; #y1; #z1;
+ nelim p2;
+ #x2; #y2; #z2; #H;
+ nnormalize;
+ nrewrite > (H1 … (triple_destruct_1 … H));
+ nnormalize;
+ nrewrite > (H2 … (triple_destruct_2 … H));
+ nnormalize;
+ nrewrite > (H3 … (triple_destruct_3 … H));
+ napply refl_eq.
+nqed.
+
+nlemma eqtriple_to_eq :
+∀T1,T2,T3.∀p1,p2:Prod3T T1 T2 T3.
+∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.
+ (∀x1,x2:T1.f1 x1 x2 = true → x1 = x2) →
+ (∀y1,y2:T2.f2 y1 y2 = true → y1 = y2) →
+ (∀z1,z2:T3.f3 z1 z2 = true → z1 = z2) →
+ (eq_triple T1 T2 T3 p1 p2 f1 f2 f3 = true → p1 = p2).
+ #T1; #T2; #T3; #p1; #p2; #f1; #f2; #f3; #H1; #H2; #H3;
+ nelim p1;
+ #x1; #y1; #z1;
+ nelim p2;
+ #x2; #y2; #z2; #H;
+ nnormalize in H:(%);
+ nletin K ≝ (H1 x1 x2);
+ ncases (f1 x1 x2) in H:(%) K:(%);
+ nnormalize;
+ ##[ ##2: #H4; napply (bool_destruct … H4) ##]
+ nletin K1 ≝ (H2 y1 y2);
+ ncases (f2 y1 y2) in K1:(%) ⊢ %;
+ nnormalize;
+ ##[ ##2: #H4; #H5; napply (bool_destruct … H5) ##]
+ #H4; #H5; #H6;
+ nrewrite > (H4 (refl_eq …));
+ nrewrite > (H6 (refl_eq …));
+ nrewrite > (H3 z1 z2 H5);
+ napply refl_eq.
+nqed.
+
+nlemma quadruple_destruct_1 :
+∀T1,T2,T3,T4.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.∀v1,v2:T4.
+ quadruple T1 T2 T3 T4 x1 y1 z1 v1 = quadruple T1 T2 T3 T4 x2 y2 z2 v2 → x1 = x2.
+ #T1; #T2; #T3; #T4; #x1; #x2; #y1; #y2; #z1; #z2; #v1; #v2; #H;
+ nchange with (match quadruple T1 T2 T3 T4 x2 y2 z2 v2 with [ quadruple a _ _ _ ⇒ x1 = a ]);
+ nrewrite < H;
+ nnormalize;
+ napply refl_eq.
+nqed.
+
+nlemma quadruple_destruct_2 :
+∀T1,T2,T3,T4.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.∀v1,v2:T4.
+ quadruple T1 T2 T3 T4 x1 y1 z1 v1 = quadruple T1 T2 T3 T4 x2 y2 z2 v2 → y1 = y2.
+ #T1; #T2; #T3; #T4; #x1; #x2; #y1; #y2; #z1; #z2; #v1; #v2; #H;
+ nchange with (match quadruple T1 T2 T3 T4 x2 y2 z2 v2 with [ quadruple _ b _ _ ⇒ y1 = b ]);
+ nrewrite < H;
+ nnormalize;
+ napply refl_eq.
+nqed.
+
+nlemma quadruple_destruct_3 :
+∀T1,T2,T3,T4.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.∀v1,v2:T4.
+ quadruple T1 T2 T3 T4 x1 y1 z1 v1 = quadruple T1 T2 T3 T4 x2 y2 z2 v2 → z1 = z2.
+ #T1; #T2; #T3; #T4; #x1; #x2; #y1; #y2; #z1; #z2; #v1; #v2; #H;
+ nchange with (match quadruple T1 T2 T3 T4 x2 y2 z2 v2 with [ quadruple _ _ c _ ⇒ z1 = c ]);
+ nrewrite < H;
+ nnormalize;
+ napply refl_eq.
+nqed.
+
+nlemma quadruple_destruct_4 :
+∀T1,T2,T3,T4.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.∀v1,v2:T4.
+ quadruple T1 T2 T3 T4 x1 y1 z1 v1 = quadruple T1 T2 T3 T4 x2 y2 z2 v2 → v1 = v2.
+ #T1; #T2; #T3; #T4; #x1; #x2; #y1; #y2; #z1; #z2; #v1; #v2; #H;
+ nchange with (match quadruple T1 T2 T3 T4 x2 y2 z2 v2 with [ quadruple _ _ _ d ⇒ v1 = d ]);
+ nrewrite < H;
+ nnormalize;
+ napply refl_eq.
+nqed.
+
+nlemma symmetric_eqquadruple :
+∀T1,T2,T3,T4:Type.∀p1,p2:Prod4T T1 T2 T3 T4.
+∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool.
+ (symmetricT T1 bool f1) →
+ (symmetricT T2 bool f2) →
+ (symmetricT T3 bool f3) →
+ (symmetricT T4 bool f4) →
+ (eq_quadruple T1 T2 T3 T4 p1 p2 f1 f2 f3 f4 = eq_quadruple T1 T2 T3 T4 p2 p1 f1 f2 f3 f4).
+ #T1; #T2; #T3; #T4; #p1; #p2; #f1; #f2; #f3; #f4; #H; #H1; #H2; #H3;
+ nelim p1;
+ #x1; #y1; #z1; #v1;
+ nelim p2;
+ #x2; #y2; #z2; #v2;
+ nnormalize;
+ nrewrite > (H x1 x2);
+ ncases (f1 x2 x1);
+ nnormalize;
+ ##[ ##1: nrewrite > (H1 y1 y2);
+ ncases (f2 y2 y1);
+ nnormalize;
+ ##[ ##1: nrewrite > (H2 z1 z2);
+ ncases (f3 z2 z1);
+ nnormalize;
+ ##[ ##1: nrewrite > (H3 v1 v2); napply refl_eq
+ ##| ##2: napply refl_eq
+ ##]
+ ##| ##2: napply refl_eq
+ ##]
+ ##| ##2: napply refl_eq
+ ##]
+nqed.
+
+nlemma eq_to_eqquadruple :
+∀T1,T2,T3,T4.∀p1,p2:Prod4T T1 T2 T3 T4.
+∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool.
+ (∀x1,x2:T1.x1 = x2 → f1 x1 x2 = true) →
+ (∀y1,y2:T2.y1 = y2 → f2 y1 y2 = true) →
+ (∀z1,z2:T3.z1 = z2 → f3 z1 z2 = true) →
+ (∀v1,v2:T4.v1 = v2 → f4 v1 v2 = true) →
+ (p1 = p2 → eq_quadruple T1 T2 T3 T4 p1 p2 f1 f2 f3 f4 = true).
+ #T1; #T2; #T3; #T4; #p1; #p2; #f1; #f2; #f3; #f4; #H1; #H2; #H3; #H4;
+ nelim p1;
+ #x1; #y1; #z1; #v1;
+ nelim p2;
+ #x2; #y2; #z2; #v2; #H;
+ nnormalize;
+ nrewrite > (H1 … (quadruple_destruct_1 … H));
+ nnormalize;
+ nrewrite > (H2 … (quadruple_destruct_2 … H));
+ nnormalize;
+ nrewrite > (H3 … (quadruple_destruct_3 … H));
+ nnormalize;
+ nrewrite > (H4 … (quadruple_destruct_4 … H));
+ napply refl_eq.
+nqed.
+
+nlemma eqquadruple_to_eq :
+∀T1,T2,T3,T4.∀p1,p2:Prod4T T1 T2 T3 T4.
+∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool.
+ (∀x1,x2:T1.f1 x1 x2 = true → x1 = x2) →
+ (∀y1,y2:T2.f2 y1 y2 = true → y1 = y2) →
+ (∀z1,z2:T3.f3 z1 z2 = true → z1 = z2) →
+ (∀v1,v2:T4.f4 v1 v2 = true → v1 = v2) →
+ (eq_quadruple T1 T2 T3 T4 p1 p2 f1 f2 f3 f4 = true → p1 = p2).
+ #T1; #T2; #T3; #T4; #p1; #p2; #f1; #f2; #f3; #f4; #H1; #H2; #H3; #H4;
+ nelim p1;
+ #x1; #y1; #z1; #v1;
+ nelim p2;
+ #x2; #y2; #z2; #v2; #H;
+ nnormalize in H:(%);
+ nletin K ≝ (H1 x1 x2);
+ ncases (f1 x1 x2) in H:(%) K:(%);
+ nnormalize;
+ ##[ ##2: #H5; napply (bool_destruct … H5) ##]
+ nletin K1 ≝ (H2 y1 y2);
+ ncases (f2 y1 y2) in K1:(%) ⊢ %;
+ nnormalize;
+ ##[ ##2: #H5; #H6; napply (bool_destruct … H6) ##]
+ nletin K2 ≝ (H3 z1 z2);
+ ncases (f3 z1 z2) in K2:(%) ⊢ %;
+ nnormalize;
+ ##[ ##2: #H5; #H6; #H7; napply (bool_destruct … H7) ##]
+ #H5; #H6; #H7; #H8;
+ nrewrite > (H5 (refl_eq …));
+ nrewrite > (H6 (refl_eq …));
+ nrewrite > (H8 (refl_eq …));
+ nrewrite > (H4 v1 v2 H7);
+ napply refl_eq.
+nqed.
+
+nlemma quintuple_destruct_1 :
+∀T1,T2,T3,T4,T5.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.∀v1,v2:T4.∀w1,w2:T5.
+ quintuple T1 T2 T3 T4 T5 x1 y1 z1 v1 w1 = quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2 → x1 = x2.
+ #T1; #T2; #T3; #T4; #T5; #x1; #x2; #y1; #y2; #z1; #z2; #v1; #v2; #w1; #w2; #H;
+ nchange with (match quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2 with [ quintuple a _ _ _ _ ⇒ x1 = a ]);
+ nrewrite < H;
+ nnormalize;
+ napply refl_eq.
+nqed.
+
+nlemma quintuple_destruct_2 :
+∀T1,T2,T3,T4,T5.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.∀v1,v2:T4.∀w1,w2:T5.
+ quintuple T1 T2 T3 T4 T5 x1 y1 z1 v1 w1 = quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2 → y1 = y2.
+ #T1; #T2; #T3; #T4; #T5; #x1; #x2; #y1; #y2; #z1; #z2; #v1; #v2; #w1; #w2; #H;
+ nchange with (match quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2 with [ quintuple _ b _ _ _ ⇒ y1 = b ]);
+ nrewrite < H;
+ nnormalize;
+ napply refl_eq.
+nqed.
+
+nlemma quintuple_destruct_3 :
+∀T1,T2,T3,T4,T5.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.∀v1,v2:T4.∀w1,w2:T5.
+ quintuple T1 T2 T3 T4 T5 x1 y1 z1 v1 w1 = quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2 → z1 = z2.
+ #T1; #T2; #T3; #T4; #T5; #x1; #x2; #y1; #y2; #z1; #z2; #v1; #v2; #w1; #w2; #H;
+ nchange with (match quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2 with [ quintuple _ _ c _ _ ⇒ z1 = c ]);
+ nrewrite < H;
+ nnormalize;
+ napply refl_eq.
+nqed.
+
+nlemma quintuple_destruct_4 :
+∀T1,T2,T3,T4,T5.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.∀v1,v2:T4.∀w1,w2:T5.
+ quintuple T1 T2 T3 T4 T5 x1 y1 z1 v1 w1 = quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2 → v1 = v2.
+ #T1; #T2; #T3; #T4; #T5; #x1; #x2; #y1; #y2; #z1; #z2; #v1; #v2; #w1; #w2; #H;
+ nchange with (match quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2 with [ quintuple _ _ _ d _ ⇒ v1 = d ]);
+ nrewrite < H;
+ nnormalize;
+ napply refl_eq.
+nqed.
+
+nlemma quintuple_destruct_5 :
+∀T1,T2,T3,T4,T5.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.∀v1,v2:T4.∀w1,w2:T5.
+ quintuple T1 T2 T3 T4 T5 x1 y1 z1 v1 w1 = quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2 → w1 = w2.
+ #T1; #T2; #T3; #T4; #T5; #x1; #x2; #y1; #y2; #z1; #z2; #v1; #v2; #w1; #w2; #H;
+ nchange with (match quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2 with [ quintuple _ _ _ _ e ⇒ w1 = e ]);
+ nrewrite < H;
+ nnormalize;
+ napply refl_eq.
+nqed.
+
+nlemma symmetric_eqquintuple :
+∀T1,T2,T3,T4,T5:Type.∀p1,p2:Prod5T T1 T2 T3 T4 T5.
+∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool.∀f5:T5 → T5 → bool.
+ (symmetricT T1 bool f1) →
+ (symmetricT T2 bool f2) →
+ (symmetricT T3 bool f3) →
+ (symmetricT T4 bool f4) →
+ (symmetricT T5 bool f5) →
+ (eq_quintuple T1 T2 T3 T4 T5 p1 p2 f1 f2 f3 f4 f5 = eq_quintuple T1 T2 T3 T4 T5 p2 p1 f1 f2 f3 f4 f5).
+ #T1; #T2; #T3; #T4; #T5; #p1; #p2; #f1; #f2; #f3; #f4; #f5; #H; #H1; #H2; #H3; #H4;
+ nelim p1;
+ #x1; #y1; #z1; #v1; #w1;
+ nelim p2;
+ #x2; #y2; #z2; #v2; #w2;
+ nnormalize;
+ nrewrite > (H x1 x2);
+ ncases (f1 x2 x1);
+ nnormalize;
+ ##[ ##1: nrewrite > (H1 y1 y2);
+ ncases (f2 y2 y1);
+ nnormalize;
+ ##[ ##1: nrewrite > (H2 z1 z2);
+ ncases (f3 z2 z1);
+ nnormalize;
+ ##[ ##1: nrewrite > (H3 v1 v2);
+ ncases (f4 v2 v1);
+ nnormalize;
+ ##[ ##1: nrewrite > (H4 w1 w2); napply refl_eq
+ ##| ##2: napply refl_eq
+ ##]
+ ##| ##2: napply refl_eq
+ ##]
+ ##| ##2: napply refl_eq
+ ##]
+ ##| ##2: napply refl_eq
+ ##]
+nqed.
+
+nlemma eq_to_eqquintuple :
+∀T1,T2,T3,T4,T5.∀p1,p2:Prod5T T1 T2 T3 T4 T5.
+∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool.∀f5:T5 → T5 → bool.
+ (∀x1,x2:T1.x1 = x2 → f1 x1 x2 = true) →
+ (∀y1,y2:T2.y1 = y2 → f2 y1 y2 = true) →
+ (∀z1,z2:T3.z1 = z2 → f3 z1 z2 = true) →
+ (∀v1,v2:T4.v1 = v2 → f4 v1 v2 = true) →
+ (∀w1,w2:T5.w1 = w2 → f5 w1 w2 = true) →
+ (p1 = p2 → eq_quintuple T1 T2 T3 T4 T5 p1 p2 f1 f2 f3 f4 f5 = true).
+ #T1; #T2; #T3; #T4; #T5; #p1; #p2; #f1; #f2; #f3; #f4; #f5; #H1; #H2; #H3; #H4; #H5;
+ nelim p1;
+ #x1; #y1; #z1; #v1; #w1;
+ nelim p2;
+ #x2; #y2; #z2; #v2; #w2; #H;
+ nnormalize;
+ nrewrite > (H1 … (quintuple_destruct_1 … H));
+ nnormalize;
+ nrewrite > (H2 … (quintuple_destruct_2 … H));
+ nnormalize;
+ nrewrite > (H3 … (quintuple_destruct_3 … H));
+ nnormalize;
+ nrewrite > (H4 … (quintuple_destruct_4 … H));
+ nnormalize;
+ nrewrite > (H5 … (quintuple_destruct_5 … H));
+ napply refl_eq.
+nqed.
+
+nlemma eqquintuple_to_eq :
+∀T1,T2,T3,T4,T5.∀p1,p2:Prod5T T1 T2 T3 T4 T5.
+∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool.∀f5:T5 → T5 → bool.
+ (∀x1,x2:T1.f1 x1 x2 = true → x1 = x2) →
+ (∀y1,y2:T2.f2 y1 y2 = true → y1 = y2) →
+ (∀z1,z2:T3.f3 z1 z2 = true → z1 = z2) →
+ (∀v1,v2:T4.f4 v1 v2 = true → v1 = v2) →
+ (∀w1,w2:T5.f5 w1 w2 = true → w1 = w2) →
+ (eq_quintuple T1 T2 T3 T4 T5 p1 p2 f1 f2 f3 f4 f5 = true → p1 = p2).
+ #T1; #T2; #T3; #T4; #T5; #p1; #p2; #f1; #f2; #f3; #f4; #f5; #H1; #H2; #H3; #H4; #H5;
+ nelim p1;
+ #x1; #y1; #z1; #v1; #w1;
+ nelim p2;
+ #x2; #y2; #z2; #v2; #w2; #H;
+ nnormalize in H:(%);
+ nletin K ≝ (H1 x1 x2);
+ ncases (f1 x1 x2) in H:(%) K:(%);
+ nnormalize;
+ ##[ ##2: #H6; napply (bool_destruct … H6) ##]
+ nletin K1 ≝ (H2 y1 y2);
+ ncases (f2 y1 y2) in K1:(%) ⊢ %;
+ nnormalize;
+ ##[ ##2: #H6; #H7; napply (bool_destruct … H7) ##]
+ nletin K2 ≝ (H3 z1 z2);
+ ncases (f3 z1 z2) in K2:(%) ⊢ %;
+ nnormalize;
+ ##[ ##2: #H6; #H7; #H8; napply (bool_destruct … H8) ##]
+ nletin K3 ≝ (H4 v1 v2);
+ ncases (f4 v1 v2) in K3:(%) ⊢ %;
+ nnormalize;
+ ##[ ##2: #H6; #H7; #H8; #H9; napply (bool_destruct … H9) ##]
+ #H6; #H7; #H8; #H9; #H10;
+ nrewrite > (H6 (refl_eq …));
+ nrewrite > (H7 (refl_eq …));
+ nrewrite > (H8 (refl_eq …));
+ nrewrite > (H10 (refl_eq …));
+ nrewrite > (H5 w1 w2 H9);
+ napply refl_eq.
+nqed.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| A.Asperti, C.Sacerdoti Coen, *)
+(* ||A|| E.Tassi, S.Zacchiroli *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU Lesser General Public License Version 2.1 *)
+(* *)
+(**************************************************************************)
+
+(* ********************************************************************** *)
+(* Progetto FreeScale *)
+(* *)
+(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* *)
+(* ********************************************************************** *)
+
+universe constraint Type[0] < Type[1].
+
+(* ********************************** *)
+(* SOTTOINSIEME MINIMALE DELLA TEORIA *)
+(* ********************************** *)
+
+(* logic/connectives.ma *)
+
+ninductive True: Prop ≝
+ I : True.
+
+ninductive False: Prop ≝.
+
+ndefinition Not: Prop → Prop ≝
+λA.(A → False).
+
+interpretation "logical not" 'not x = (Not x).
+
+nlemma absurd : ∀A,C:Prop.A → ¬A → C.
+ #A; #C; #H;
+ nnormalize;
+ #H1;
+ nelim (H1 H);
+nqed.
+
+nlemma not_to_not : ∀A,B:Prop. (A → B) → ¬B →¬A.
+ #A; #B; #H;
+ nnormalize;
+ #H1; #H2;
+ nelim (H1 (H H2)).
+nqed.
+
+nlemma prop_to_nnprop : ∀P.P → ¬¬P.
+ #P; nnormalize; #H; #H1;
+ napply (H1 H).
+nqed.
+
+(*
+naxiom RAA : ∀P:Prop.∀f:(¬P) → False.P.
+
+nlemma nnprop_to_prop : ∀P.(¬¬P) → P.
+ #P; nchange with (((¬P) → False) → P);
+ #H; napply (RAA P H).
+nqed.
+*)
+
+ninductive And (A,B:Prop) : Prop ≝
+ conj : A → B → (And A B).
+
+interpretation "logical and" 'and x y = (And x y).
+
+nlemma proj1: ∀A,B:Prop.A ∧ B → A.
+ #A; #B; #H;
+ (* \ldots al posto di ??? *)
+ napply (And_ind A B … H);
+ #H1; #H2;
+ napply H1.
+nqed.
+
+nlemma proj2: ∀A,B:Prop.A ∧ B → B.
+ #A; #B; #H;
+ napply (And_ind A B … H);
+ #H1; #H2;
+ napply H2.
+nqed.
+
+ninductive Or (A,B:Prop) : Prop ≝
+ or_introl : A → (Or A B)
+| or_intror : B → (Or A B).
+
+interpretation "logical or" 'or x y = (Or x y).
+
+ndefinition decidable : Prop → Prop ≝ λA:Prop.A ∨ ¬A.
+
+(*
+nlemma decidable_prop : ∀P:Prop.decidable P.
+ #P; nnormalize;
+ napply RAA;
+ #H;
+ napply (absurd (P ∨ (¬P)) …);
+ ##[ ##2: napply H
+ ##| ##1: napply (or_intror P (¬P));
+ napply RAA;
+ #H1;
+ napply (absurd (P ∨ (¬P)) …);
+ ##[ ##2: napply H
+ ##| ##1: napply (or_introl P (¬P));
+ napply (nnprop_to_prop P H1)
+ ##]
+ ##]
+nqed.
+
+nlemma terzo_escluso : ∀P,G:Prop.∀ft:P → G.∀ff:(¬P) → G.G.
+ #P; #G; nnormalize;
+ #H; #H1;
+ napply (Or_ind P (P → False) ? H H1 ?);
+ napply (decidable_prop P).
+nqed.
+*)
+
+nlemma or_elim : ∀P,Q,G:Prop.Or P Q → ∀fp:P → G.∀fq:Q → G.G.
+ #P; #Q; #G; #H; #H1; #H2;
+ napply (Or_ind P Q ? H1 H2 ?);
+ napply H.
+nqed.
+
+ninductive ex (A:Type) (Q:A → Prop) : Prop ≝
+ ex_intro: ∀x:A.Q x → ex A Q.
+
+interpretation "exists" 'exists x = (ex ? x).
+
+ninductive ex2 (A:Type) (Q,R:A → Prop) : Prop ≝
+ ex_intro2: ∀x:A.Q x → R x → ex2 A Q R.
+
+ndefinition iff ≝
+λA,B.(A → B) ∧ (B → A).
+
+(* higher_order_defs/relations *)
+
+ndefinition relation : Type → Type ≝
+λA:Type.A → A → Prop.
+
+ndefinition reflexive : ∀A:Type.∀R:relation A.Prop ≝
+λA.λR.∀x:A.R x x.
+
+ndefinition symmetric : ∀A:Type.∀R:relation A.Prop ≝
+λA.λR.∀x,y:A.R x y → R y x.
+
+ndefinition transitive : ∀A:Type.∀R:relation A.Prop ≝
+λA.λR.∀x,y,z:A.R x y → R y z → R x z.
+
+ndefinition irreflexive : ∀A:Type.∀R:relation A.Prop ≝
+λA.λR.∀x:A.¬ (R x x).
+
+ndefinition cotransitive : ∀A:Type.∀R:relation A.Prop ≝
+λA.λR.∀x,y:A.R x y → ∀z:A. R x z ∨ R z y.
+
+ndefinition tight_apart : ∀A:Type.∀eq,ap:relation A.Prop ≝
+λA.λeq,ap.∀x,y:A. (¬ (ap x y) → eq x y) ∧ (eq x y → ¬ (ap x y)).
+
+ndefinition antisymmetric : ∀A:Type.∀R:relation A.Prop ≝
+λA.λR.∀x,y:A.R x y → ¬ (R y x).
+
+(* logic/equality.ma *)
+
+ninductive eq (A:Type) (x:A) : A → Prop ≝
+ refl_eq : eq A x x.
+
+interpretation "leibnitz's equality" 'eq t x y = (eq t x y).
+
+interpretation "leibnitz's non-equality" 'neq t x y = (Not (eq t x y)).
+
+nlemma eq_f : ∀T1,T2:Type.∀x,y:T1.∀f:T1 → T2.x = y → (f x) = (f y).
+ #T1; #T2; #x; #y; #f; #H;
+ nrewrite < H;
+ napply refl_eq.
+nqed.
+
+nlemma eq_f2 : ∀T1,T2,T3:Type.∀x1,y1:T1.∀x2,y2:T2.∀f:T1 → T2 → T3.x1 = y1 → x2 = y2 → f x1 x2 = f y1 y2.
+ #T1; #T2; #T3; #x1; #y1; #x2; #y2; #f; #H1; #H2;
+ nrewrite < H1;
+ nrewrite < H2;
+ napply refl_eq.
+nqed.
+
+nlemma neqf_to_neq : ∀T1,T2:Type.∀x,y:T1.∀f:T1 → T2.((f x) ≠ (f y)) → x ≠ y.
+ #T1; #T2; #x; #y; #f;
+ nnormalize; #H; #H1;
+ napply (H (eq_f … H1)).
+nqed.
+
+(*
+nlemma neqf2_to_neq : ∀T1,T2,T3:Type.∀x1,y1:T1.∀x2,y2:T2.∀f:T1 → T2 → T3.f x1 x2 ≠ f y1 y2 → (x1 ≠ y1) ∨ (x2 ≠ y2).
+ #T1; #T2; #T3; #x1; #y1; #x2; #y2; #f; nnormalize; #H;
+ napply (terzo_escluso (x1 = y1) …);
+ ##[ ##2: #H1; napply (or_introl … H1)
+ ##| ##1: #H1; napply (terzo_escluso (x2 = y2) …)
+ ##[ ##2: #H2; napply (or_intror … H2)
+ ##| ##1: #H2; nrewrite < H1 in H:(%);
+ nrewrite < H2; #H;
+ nelim (H (refl_eq …))
+ ##]
+ ##]
+nqed.
+*)
+
+nlemma symmetric_eq: ∀A:Type. symmetric A (eq A).
+ #A;
+ nnormalize;
+ #x; #y; #H;
+ nrewrite < H;
+ napply refl_eq.
+nqed.
+
+nlemma eq_elim_r: ∀A:Type.∀x:A.∀P:A → Prop.P x → ∀y:A.y=x → P y.
+ #A; #x; #P; #H; #y; #H1;
+ nrewrite < (symmetric_eq … H1);
+ napply H.
+nqed.
+
+ndefinition relationT : Type → Type → Type ≝
+λA,T:Type.A → A → T.
+
+ndefinition symmetricT: ∀A,T:Type.∀R:relationT A T.Prop ≝
+λA,T.λR.∀x,y:A.R x y = R y x.
+
+ndefinition associative : ∀A:Type.∀R:relationT A A.Prop ≝
+λA.λR.∀x,y,z:A.R (R x y) z = R x (R y z).
-freescale/byte8.ma freescale/bitrigesim.ma freescale/exadecim.ma
-freescale/status.ma freescale/memory_abs.ma freescale/opcode_base.ma freescale/prod.ma
-freescale/memory_bits.ma freescale/memory_trees.ma
-utility/ascii_lemmas1.ma freescale/theory.ma utility/ascii.ma
-freescale/byte8_lemmas.ma freescale/byte8.ma freescale/exadecim_lemmas.ma
-utility/string_lemmas.ma utility/ascii_lemmas2.ma utility/string.ma utility/utility_lemmas.ma
-freescale/table_HCS08_tests.ma freescale/table_HCS08.ma
-freescale/multivm.ma freescale/load_write.ma
-freescale/opcode_base_lemmas.ma freescale/bool_lemmas.ma freescale/opcode_base.ma
-compiler/ast_type_lemmas.ma compiler/ast_type.ma utility/utility_lemmas.ma
-freescale/table_HC05_tests.ma freescale/table_HC05.ma
-freescale/option.ma freescale/bool.ma
-freescale/bool.ma freescale/pts.ma
-freescale/bool_lemmas.ma freescale/bool.ma freescale/theory.ma
-freescale/opcode_base_lemmas_opcode1.ma freescale/bool_lemmas.ma freescale/opcode_base.ma
-freescale/memory_func.ma freescale/memory_struct.ma freescale/option.ma freescale/theory.ma freescale/word16.ma
-freescale/load_write.ma freescale/model.ma freescale/translation.ma
-freescale/bitrigesim.ma freescale/bool.ma
-freescale/table_RS08.ma freescale/opcode.ma
-freescale/oct.ma freescale/bool.ma
-freescale/option_lemmas.ma freescale/bool_lemmas.ma freescale/option.ma
-freescale/table_RS08_tests.ma freescale/table_RS08.ma
-freescale/translation.ma freescale/option.ma freescale/table_HC05.ma freescale/table_HC08.ma freescale/table_HCS08.ma freescale/table_RS08.ma
-freescale/medium_tests_tools.ma freescale/multivm.ma
-utility/utility_lemmas.ma utility/utility.ma
-freescale/memory_abs.ma freescale/memory_bits.ma freescale/memory_func.ma freescale/memory_trees.ma
-freescale/bitrigesim_lemmas.ma freescale/bitrigesim.ma freescale/bool_lemmas.ma
-test_errori.ma compiler/ast_type_lemmas.ma freescale/byte8_lemmas.ma utility/utility.ma
-freescale/memory_struct.ma freescale/byte8.ma freescale/oct.ma
-freescale/model.ma freescale/status.ma
-freescale/table_HC05.ma freescale/opcode.ma
-freescale/quatern_lemmas.ma freescale/bool_lemmas.ma freescale/quatern.ma
-freescale/exadecim_lemmas.ma freescale/bool_lemmas.ma freescale/exadecim.ma
-compiler/ast_type.ma utility/utility.ma
-freescale/word16.ma freescale/byte8.ma
-utility/ascii.ma freescale/bool.ma
-freescale/memory_trees.ma freescale/memory_struct.ma freescale/option.ma freescale/theory.ma freescale/word16.ma
-freescale/pts.ma
-freescale/opcode_base_lemmas_instrmode2.ma freescale/opcode_base_lemmas_instrmode1.ma
-freescale/opcode_base_lemmas1.ma freescale/opcode_base_lemmas_instrmode2.ma freescale/opcode_base_lemmas_opcode2.ma freescale/word16_lemmas.ma
-freescale/table_HC08.ma freescale/opcode.ma
-freescale/prod.ma freescale/bool.ma
-utility/string.ma freescale/theory.ma utility/ascii.ma utility/utility.ma
-freescale/table_HCS08.ma freescale/opcode.ma
-freescale/word32.ma freescale/word16.ma
-freescale/prod_lemmas.ma freescale/bool_lemmas.ma freescale/prod.ma
-freescale/opcode_base.ma freescale/bitrigesim.ma freescale/oct.ma freescale/theory.ma freescale/word16.ma
-freescale/word32_lemmas.ma freescale/word16_lemmas.ma freescale/word32.ma
-freescale/status_lemmas.ma freescale/opcode_base_lemmas1.ma freescale/option_lemmas.ma freescale/prod_lemmas.ma freescale/status.ma freescale/word16_lemmas.ma
-utility/ascii_lemmas2.ma freescale/bool_lemmas.ma utility/ascii_lemmas1.ma
-freescale/micro_tests.ma freescale/multivm.ma freescale/status_lemmas.ma
-freescale/table_HC08_tests.ma freescale/table_HC08.ma
-utility/utility.ma freescale/option.ma freescale/theory.ma
-freescale/quatern.ma freescale/bool.ma
-freescale/opcode_base_lemmas_instrmode1.ma freescale/bitrigesim_lemmas.ma freescale/exadecim_lemmas.ma freescale/oct_lemmas.ma freescale/opcode_base.ma
-freescale/word16_lemmas.ma freescale/byte8_lemmas.ma freescale/word16.ma
-freescale/exadecim.ma freescale/bool.ma freescale/oct.ma freescale/prod.ma freescale/quatern.ma
-freescale/theory.ma freescale/pts.ma
-freescale/opcode_base_lemmas_opcode2.ma freescale/opcode_base_lemmas_opcode1.ma
-freescale/medium_tests.ma freescale/medium_tests_tools.ma utility/utility.ma
-freescale/opcode.ma freescale/opcode_base.ma
-freescale/oct_lemmas.ma freescale/bool_lemmas.ma freescale/oct.ma
+num/exadecim.ma common/prod.ma num/bool.ma num/oct.ma num/quatern.ma
+common/option.ma num/bool.ma
+test_errori.ma
+common/theory.ma
+num/quatern.ma num/bool.ma
+common/prod.ma num/bool.ma
+num/bool.ma common/theory.ma
+num/quatern_lemmas.ma num/bool_lemmas.ma num/quatern.ma
+common/option_lemmas.ma common/option.ma num/bool_lemmas.ma
+common/prod_lemmas.ma common/prod.ma num/bool_lemmas.ma
+num/oct_lemmas.ma num/bool_lemmas.ma num/oct.ma
+num/bool_lemmas.ma num/bool.ma
+num/exadecim_lemmas.ma num/bool_lemmas.ma num/exadecim.ma
+num/oct.ma num/bool.ma
--- /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 *)
+(* Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* *)
+(* ********************************************************************** *)
+
+include "common/theory.ma".
+
+(* ******** *)
+(* BOOLEANI *)
+(* ******** *)
+
+ninductive bool : Type ≝
+ true : bool
+| false : bool.
+
+(* operatori booleani *)
+
+ndefinition eq_bool ≝
+λb1,b2:bool.match b1 with
+ [ true ⇒ match b2 with [ true ⇒ true | false ⇒ false ]
+ | false ⇒ match b2 with [ true ⇒ false | false ⇒ true ]
+ ].
+
+ndefinition not_bool ≝
+λb:bool.match b with [ true ⇒ false | false ⇒ true ].
+
+ndefinition and_bool ≝
+λb1,b2:bool.match b1 with
+ [ true ⇒ b2 | false ⇒ false ].
+
+ndefinition or_bool ≝
+λb1,b2:bool.match b1 with
+ [ true ⇒ true | false ⇒ b2 ].
+
+ndefinition xor_bool ≝
+λb1,b2:bool.match b1 with
+ [ true ⇒ not_bool b2
+ | false ⇒ b2 ].
+
+(* \ominus *)
+notation "hvbox(⊖ a)" non associative with precedence 36
+ for @{ 'not_bool $a }.
+interpretation "not_bool" 'not_bool x = (not_bool x).
+
+(* \otimes *)
+notation "hvbox(a break ⊗ b)" left associative with precedence 35
+ for @{ 'and_bool $a $b }.
+interpretation "and_bool" 'and_bool x y = (and_bool x y).
+
+(* \oplus *)
+notation "hvbox(a break ⊕ b)" left associative with precedence 34
+ for @{ 'or_bool $a $b }.
+interpretation "or_bool" 'or_bool x y = (or_bool x y).
+
+(* \odot *)
+notation "hvbox(a break ⊙ b)" left associative with precedence 33
+ for @{ 'xor_bool $a $b }.
+interpretation "xor_bool" 'xor_bool x y = (xor_bool x y).
+
+ndefinition boolRelation : Type → Type ≝
+λA:Type.A → A → bool.
--- /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 *)
+(* Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* *)
+(* ********************************************************************** *)
+
+include "num/bool.ma".
+
+(* ******** *)
+(* BOOLEANI *)
+(* ******** *)
+
+ndefinition bool_destruct_aux ≝
+Πb1,b2:bool.ΠP:Prop.b1 = b2 →
+ match b1 with
+ [ true ⇒ match b2 with [ true ⇒ P → P | false ⇒ P ]
+ | false ⇒ match b2 with [ true ⇒ P | false ⇒ P → P ]
+ ].
+
+ndefinition bool_destruct : bool_destruct_aux.
+ #b1; #b2; #P;
+ nelim b1;
+ nelim b2;
+ nnormalize;
+ #H;
+ ##[ ##2: napply False_ind;
+ nchange with (match true with [ true ⇒ False | false ⇒ True]);
+ nrewrite > H;
+ nnormalize;
+ napply I
+ ##| ##3: napply False_ind;
+ nchange with (match true with [ true ⇒ False | false ⇒ True]);
+ nrewrite < H;
+ nnormalize;
+ napply I
+ ##| ##1,4: napply (λx:P.x)
+ ##]
+nqed.
+
+nlemma symmetric_eqbool : symmetricT bool bool eq_bool.
+ #b1; #b2;
+ nelim b1;
+ nelim b2;
+ nnormalize;
+ napply refl_eq.
+nqed.
+
+nlemma symmetric_andbool : symmetricT bool bool and_bool.
+ #b1; #b2;
+ nelim b1;
+ nelim b2;
+ nnormalize;
+ napply refl_eq.
+nqed.
+
+nlemma associative_andbool : ∀b1,b2,b3.((b1 ⊗ b2) ⊗ b3) = (b1 ⊗ (b2 ⊗ b3)).
+ #b1; #b2; #b3;
+ nelim b1;
+ nelim b2;
+ nelim b3;
+ nnormalize;
+ napply refl_eq.
+nqed.
+
+nlemma symmetric_orbool : symmetricT bool bool or_bool.
+ #b1; #b2;
+ nelim b1;
+ nelim b2;
+ nnormalize;
+ napply refl_eq.
+nqed.
+
+nlemma associative_orbool : ∀b1,b2,b3.((b1 ⊕ b2) ⊕ b3) = (b1 ⊕ (b2 ⊕ b3)).
+ #b1; #b2; #b3;
+ nelim b1;
+ nelim b2;
+ nelim b3;
+ nnormalize;
+ napply refl_eq.
+nqed.
+
+nlemma symmetric_xorbool : symmetricT bool bool xor_bool.
+ #b1; #b2;
+ nelim b1;
+ nelim b2;
+ nnormalize;
+ napply refl_eq.
+nqed.
+
+nlemma associative_xorbool : ∀b1,b2,b3.((b1 ⊙ b2) ⊙ b3) = (b1 ⊙ (b2 ⊙ b3)).
+ #b1; #b2; #b3;
+ nelim b1;
+ nelim b2;
+ nelim b3;
+ nnormalize;
+ napply refl_eq.
+nqed.
+
+nlemma eqbool_to_eq : ∀b1,b2:bool.(eq_bool b1 b2 = true) → (b1 = b2).
+ #b1; #b2;
+ ncases b1;
+ ncases b2;
+ nnormalize;
+ ##[ ##1,4: #H; napply refl_eq
+ ##| ##*: #H; napply (bool_destruct … H)
+ ##]
+nqed.
+
+nlemma eq_to_eqbool : ∀b1,b2.b1 = b2 → eq_bool b1 b2 = true.
+ #b1; #b2;
+ ncases b1;
+ ncases b2;
+ nnormalize;
+ ##[ ##1,4: #H; napply refl_eq
+ ##| ##*: #H; napply (bool_destruct … H)
+ ##]
+nqed.
+
+nlemma neqbool_to_neq : ∀b1,b2:bool.(eq_bool b1 b2 = false) → (b1 ≠ b2).
+ #b1; #b2;
+ ncases b1;
+ ncases b2;
+ nnormalize;
+ ##[ ##1,4: #H; napply (bool_destruct … H)
+ ##| ##*: #H; #H1; napply (bool_destruct … H1)
+ ##]
+nqed.
+
+nlemma neq_to_neqbool : ∀b1,b2.b1 ≠ b2 → eq_bool b1 b2 = false.
+ #b1; #b2;
+ ncases b1;
+ ncases b2;
+ nnormalize;
+ ##[ ##1,4: #H; napply False_ind; napply (H (refl_eq …))
+ ##| ##*: #H; napply refl_eq
+ ##]
+nqed.
+
+nlemma andb_true_true_l: ∀b1,b2.(b1 ⊗ b2) = true → b1 = true.
+ #b1; #b2;
+ ncases b1;
+ ncases b2;
+ nnormalize;
+ ##[ ##1,2: #H; napply refl_eq
+ ##| ##*: #H; napply (bool_destruct … H)
+ ##]
+nqed.
+
+nlemma andb_true_true_r: ∀b1,b2.(b1 ⊗ b2) = true → b2 = true.
+ #b1; #b2;
+ ncases b1;
+ ncases b2;
+ nnormalize;
+ ##[ ##1,3: #H; napply refl_eq
+ ##| ##*: #H; napply (bool_destruct … H)
+ ##]
+nqed.
+
+nlemma orb_false_false_l : ∀b1,b2:bool.(b1 ⊕ b2) = false → b1 = false.
+ #b1; #b2;
+ ncases b1;
+ ncases b2;
+ nnormalize;
+ ##[ ##4: #H; napply refl_eq
+ ##| ##*: #H; napply (bool_destruct … H)
+ ##]
+nqed.
+
+nlemma orb_false_false_r : ∀b1,b2:bool.(b1 ⊕ b2) = false → b2 = false.
+ #b1; #b2;
+ ncases b1;
+ ncases b2;
+ nnormalize;
+ ##[ ##4: #H; napply refl_eq
+ ##| ##*: #H; napply (bool_destruct … H)
+ ##]
+nqed.
--- /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 *)
+(* Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* *)
+(* ********************************************************************** *)
+
+include "num/bool.ma".
+include "num/quatern.ma".
+include "num/oct.ma".
+include "common/prod.ma".
+
+(* *********** *)
+(* ESADECIMALI *)
+(* *********** *)
+
+ninductive exadecim : Type ≝
+ x0: exadecim
+| x1: exadecim
+| x2: exadecim
+| x3: exadecim
+| x4: exadecim
+| x5: exadecim
+| x6: exadecim
+| x7: exadecim
+| x8: exadecim
+| x9: exadecim
+| xA: exadecim
+| xB: exadecim
+| xC: exadecim
+| xD: exadecim
+| xE: exadecim
+| xF: exadecim.
+
+(* operatore = *)
+ndefinition eq_ex ≝
+λe1,e2:exadecim.
+ match e1 with
+ [ x0 ⇒ match e2 with [ x0 ⇒ true | _ ⇒ false ]
+ | x1 ⇒ match e2 with [ x1 ⇒ true | _ ⇒ false ]
+ | x2 ⇒ match e2 with [ x2 ⇒ true | _ ⇒ false ]
+ | x3 ⇒ match e2 with [ x3 ⇒ true | _ ⇒ false ]
+ | x4 ⇒ match e2 with [ x4 ⇒ true | _ ⇒ false ]
+ | x5 ⇒ match e2 with [ x5 ⇒ true | _ ⇒ false ]
+ | x6 ⇒ match e2 with [ x6 ⇒ true | _ ⇒ false ]
+ | x7 ⇒ match e2 with [ x7 ⇒ true | _ ⇒ false ]
+ | x8 ⇒ match e2 with [ x8 ⇒ true | _ ⇒ false ]
+ | x9 ⇒ match e2 with [ x9 ⇒ true | _ ⇒ false ]
+ | xA ⇒ match e2 with [ xA ⇒ true | _ ⇒ false ]
+ | xB ⇒ match e2 with [ xB ⇒ true | _ ⇒ false ]
+ | xC ⇒ match e2 with [ xC ⇒ true | _ ⇒ false ]
+ | xD ⇒ match e2 with [ xD ⇒ true | _ ⇒ false ]
+ | xE ⇒ match e2 with [ xE ⇒ true | _ ⇒ false ]
+ | xF ⇒ match e2 with [ xF ⇒ true | _ ⇒ false ]
+ ].
+
+(* operatore < *)
+ndefinition lt_ex ≝
+λe1,e2:exadecim.
+ match e1 with
+ [ x0 ⇒ match e2 with
+ [ x0 ⇒ false | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
+ | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
+ | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
+ | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
+ | x1 ⇒ match e2 with
+ [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ true | x3 ⇒ true
+ | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
+ | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
+ | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
+ | x2 ⇒ match e2 with
+ [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ true
+ | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
+ | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
+ | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
+ | x3 ⇒ match e2 with
+ [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
+ | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
+ | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
+ | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
+ | x4 ⇒ match e2 with
+ [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
+ | x4 ⇒ false | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
+ | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
+ | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
+ | x5 ⇒ match e2 with
+ [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
+ | x4 ⇒ false | x5 ⇒ false | x6 ⇒ true | x7 ⇒ true
+ | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
+ | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
+ | x6 ⇒ match e2 with
+ [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
+ | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ true
+ | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
+ | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
+ | x7 ⇒ match e2 with
+ [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
+ | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+ | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
+ | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
+ | x8 ⇒ match e2 with
+ [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
+ | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+ | x8 ⇒ false | x9 ⇒ true | xA ⇒ true | xB ⇒ true
+ | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
+ | x9 ⇒ match e2 with
+ [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
+ | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+ | x8 ⇒ false | x9 ⇒ false | xA ⇒ true | xB ⇒ true
+ | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
+ | xA ⇒ match e2 with
+ [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
+ | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+ | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ true
+ | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
+ | xB ⇒ match e2 with
+ [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
+ | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+ | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
+ | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
+ | xC ⇒ match e2 with
+ [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
+ | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+ | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
+ | xC ⇒ false | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
+ | xD ⇒ match e2 with
+ [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
+ | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+ | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
+ | xC ⇒ false | xD ⇒ false | xE ⇒ true | xF ⇒ true ]
+ | xE ⇒ match e2 with
+ [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
+ | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+ | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
+ | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ true ]
+ | xF ⇒ match e2 with
+ [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
+ | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+ | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
+ | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
+ ].
+
+(* operatore ≤ *)
+ndefinition le_ex ≝
+λe1,e2:exadecim.
+ match e1 with
+ [ x0 ⇒ match e2 with
+ [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
+ | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
+ | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
+ | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
+ | x1 ⇒ match e2 with
+ [ x0 ⇒ false | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
+ | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
+ | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
+ | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
+ | x2 ⇒ match e2 with
+ [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ true | x3 ⇒ true
+ | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
+ | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
+ | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
+ | x3 ⇒ match e2 with
+ [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ true
+ | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
+ | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
+ | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
+ | x4 ⇒ match e2 with
+ [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
+ | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
+ | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
+ | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
+ | x5 ⇒ match e2 with
+ [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
+ | x4 ⇒ false | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
+ | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
+ | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
+ | x6 ⇒ match e2 with
+ [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
+ | x4 ⇒ false | x5 ⇒ false | x6 ⇒ true | x7 ⇒ true
+ | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
+ | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
+ | x7 ⇒ match e2 with
+ [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
+ | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ true
+ | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
+ | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
+ | x8 ⇒ match e2 with
+ [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
+ | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+ | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
+ | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
+ | x9 ⇒ match e2 with
+ [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
+ | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+ | x8 ⇒ false | x9 ⇒ true | xA ⇒ true | xB ⇒ true
+ | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
+ | xA ⇒ match e2 with
+ [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
+ | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+ | x8 ⇒ false | x9 ⇒ false | xA ⇒ true | xB ⇒ true
+ | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
+ | xB ⇒ match e2 with
+ [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
+ | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+ | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ true
+ | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
+ | xC ⇒ match e2 with
+ [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
+ | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+ | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
+ | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
+ | xD ⇒ match e2 with
+ [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
+ | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+ | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
+ | xC ⇒ false | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
+ | xE ⇒ match e2 with
+ [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
+ | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+ | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
+ | xC ⇒ false | xD ⇒ false | xE ⇒ true | xF ⇒ true ]
+ | xF ⇒ match e2 with
+ [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
+ | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+ | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
+ | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ true ]
+ ].
+
+(* operatore > *)
+ndefinition gt_ex ≝
+λe1,e2:exadecim.
+ match e1 with
+ [ x0 ⇒ match e2 with
+ [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
+ | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+ | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
+ | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
+ | x1 ⇒ match e2 with
+ [ x0 ⇒ true | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
+ | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+ | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
+ | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
+ | x2 ⇒ match e2 with
+ [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ false | x3 ⇒ false
+ | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+ | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
+ | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
+ | x3 ⇒ match e2 with
+ [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ false
+ | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+ | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
+ | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
+ | x4 ⇒ match e2 with
+ [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
+ | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+ | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
+ | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
+ | x5 ⇒ match e2 with
+ [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
+ | x4 ⇒ true | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+ | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
+ | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
+ | x6 ⇒ match e2 with
+ [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
+ | x4 ⇒ true | x5 ⇒ true | x6 ⇒ false | x7 ⇒ false
+ | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
+ | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
+ | x7 ⇒ match e2 with
+ [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
+ | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ false
+ | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
+ | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
+ | x8 ⇒ match e2 with
+ [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
+ | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
+ | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
+ | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
+ | x9 ⇒ match e2 with
+ [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
+ | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
+ | x8 ⇒ true | x9 ⇒ false | xA ⇒ false | xB ⇒ false
+ | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
+ | xA ⇒ match e2 with
+ [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
+ | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
+ | x8 ⇒ true | x9 ⇒ true | xA ⇒ false | xB ⇒ false
+ | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
+ | xB ⇒ match e2 with
+ [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
+ | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
+ | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ false
+ | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
+ | xC ⇒ match e2 with
+ [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
+ | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
+ | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
+ | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
+ | xD ⇒ match e2 with
+ [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
+ | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
+ | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
+ | xC ⇒ true | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
+ | xE ⇒ match e2 with
+ [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
+ | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
+ | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
+ | xC ⇒ true | xD ⇒ true | xE ⇒ false | xF ⇒ false ]
+ | xF ⇒ match e2 with
+ [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
+ | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
+ | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
+ | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ false ]
+ ].
+
+(* operatore ≥ *)
+ndefinition ge_ex ≝
+λe1,e2:exadecim.
+ match e1 with
+ [ x0 ⇒ match e2 with
+ [ x0 ⇒ true | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
+ | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+ | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
+ | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
+ | x1 ⇒ match e2 with
+ [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ false | x3 ⇒ false
+ | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+ | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
+ | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
+ | x2 ⇒ match e2 with
+ [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ false
+ | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+ | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
+ | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
+ | x3 ⇒ match e2 with
+ [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
+ | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+ | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
+ | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
+ | x4 ⇒ match e2 with
+ [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
+ | x4 ⇒ true | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+ | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
+ | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
+ | x5 ⇒ match e2 with
+ [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
+ | x4 ⇒ true | x5 ⇒ true | x6 ⇒ false | x7 ⇒ false
+ | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
+ | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
+ | x6 ⇒ match e2 with
+ [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
+ | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ false
+ | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
+ | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
+ | x7 ⇒ match e2 with
+ [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
+ | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
+ | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false
+ | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
+ | x8 ⇒ match e2 with
+ [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
+ | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
+ | x8 ⇒ true | x9 ⇒ false | xA ⇒ false | xB ⇒ false
+ | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
+ | x9 ⇒ match e2 with
+ [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
+ | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
+ | x8 ⇒ true | x9 ⇒ true | xA ⇒ false | xB ⇒ false
+ | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
+ | xA ⇒ match e2 with
+ [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
+ | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
+ | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ false
+ | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
+ | xB ⇒ match e2 with
+ [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
+ | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
+ | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
+ | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
+ | xC ⇒ match e2 with
+ [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
+ | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
+ | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
+ | xC ⇒ true | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
+ | xD ⇒ match e2 with
+ [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
+ | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
+ | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
+ | xC ⇒ true | xD ⇒ true | xE ⇒ false | xF ⇒ false ]
+ | xE ⇒ match e2 with
+ [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
+ | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
+ | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
+ | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ false ]
+ | xF ⇒ match e2 with
+ [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true
+ | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
+ | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
+ | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
+ ].
+
+(* operatore and *)
+ndefinition and_ex ≝
+λe1,e2:exadecim.match e1 with
+ [ x0 ⇒ match e2 with
+ [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x0 | x3 ⇒ x0
+ | x4 ⇒ x0 | x5 ⇒ x0 | x6 ⇒ x0 | x7 ⇒ x0
+ | x8 ⇒ x0 | x9 ⇒ x0 | xA ⇒ x0 | xB ⇒ x0
+ | xC ⇒ x0 | xD ⇒ x0 | xE ⇒ x0 | xF ⇒ x0 ]
+ | x1 ⇒ match e2 with
+ [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x0 | x3 ⇒ x1
+ | x4 ⇒ x0 | x5 ⇒ x1 | x6 ⇒ x0 | x7 ⇒ x1
+ | x8 ⇒ x0 | x9 ⇒ x1 | xA ⇒ x0 | xB ⇒ x1
+ | xC ⇒ x0 | xD ⇒ x1 | xE ⇒ x0 | xF ⇒ x1 ]
+ | x2 ⇒ match e2 with
+ [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x2 | x3 ⇒ x2
+ | x4 ⇒ x0 | x5 ⇒ x0 | x6 ⇒ x2 | x7 ⇒ x2
+ | x8 ⇒ x0 | x9 ⇒ x0 | xA ⇒ x2 | xB ⇒ x2
+ | xC ⇒ x0 | xD ⇒ x0 | xE ⇒ x2 | xF ⇒ x2 ]
+ | x3 ⇒ match e2 with
+ [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3
+ | x4 ⇒ x0 | x5 ⇒ x1 | x6 ⇒ x2 | x7 ⇒ x3
+ | x8 ⇒ x0 | x9 ⇒ x1 | xA ⇒ x2 | xB ⇒ x3
+ | xC ⇒ x0 | xD ⇒ x1 | xE ⇒ x2 | xF ⇒ x3 ]
+ | x4 ⇒ match e2 with
+ [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x0 | x3 ⇒ x0
+ | x4 ⇒ x4 | x5 ⇒ x4 | x6 ⇒ x4 | x7 ⇒ x4
+ | x8 ⇒ x0 | x9 ⇒ x0 | xA ⇒ x0 | xB ⇒ x0
+ | xC ⇒ x4 | xD ⇒ x4 | xE ⇒ x4 | xF ⇒ x4 ]
+ | x5 ⇒ match e2 with
+ [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x0 | x3 ⇒ x1
+ | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x4 | x7 ⇒ x5
+ | x8 ⇒ x0 | x9 ⇒ x1 | xA ⇒ x0 | xB ⇒ x1
+ | xC ⇒ x4 | xD ⇒ x5 | xE ⇒ x4 | xF ⇒ x5 ]
+ | x6 ⇒ match e2 with
+ [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x2 | x3 ⇒ x2
+ | x4 ⇒ x4 | x5 ⇒ x4 | x6 ⇒ x6 | x7 ⇒ x6
+ | x8 ⇒ x0 | x9 ⇒ x0 | xA ⇒ x2 | xB ⇒ x2
+ | xC ⇒ x4 | xD ⇒ x4 | xE ⇒ x6 | xF ⇒ x6 ]
+ | x7 ⇒ match e2 with
+ [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3
+ | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x6 | x7 ⇒ x7
+ | x8 ⇒ x0 | x9 ⇒ x1 | xA ⇒ x2 | xB ⇒ x3
+ | xC ⇒ x4 | xD ⇒ x5 | xE ⇒ x6 | xF ⇒ x7 ]
+ | x8 ⇒ match e2 with
+ [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x0 | x3 ⇒ x0
+ | x4 ⇒ x0 | x5 ⇒ x0 | x6 ⇒ x0 | x7 ⇒ x0
+ | x8 ⇒ x8 | x9 ⇒ x8 | xA ⇒ x8 | xB ⇒ x8
+ | xC ⇒ x8 | xD ⇒ x8 | xE ⇒ x8 | xF ⇒ x8 ]
+ | x9 ⇒ match e2 with
+ [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x0 | x3 ⇒ x1
+ | x4 ⇒ x0 | x5 ⇒ x1 | x6 ⇒ x0 | x7 ⇒ x1
+ | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ x8 | xB ⇒ x9
+ | xC ⇒ x8 | xD ⇒ x9 | xE ⇒ x8 | xF ⇒ x9 ]
+ | xA ⇒ match e2 with
+ [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x2 | x3 ⇒ x2
+ | x4 ⇒ x0 | x5 ⇒ x0 | x6 ⇒ x2 | x7 ⇒ x2
+ | x8 ⇒ x8 | x9 ⇒ x8 | xA ⇒ xA | xB ⇒ xA
+ | xC ⇒ x8 | xD ⇒ x8 | xE ⇒ xA | xF ⇒ xA ]
+ | xB ⇒ match e2 with
+ [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3
+ | x4 ⇒ x0 | x5 ⇒ x1 | x6 ⇒ x2 | x7 ⇒ x3
+ | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ xA | xB ⇒ xB
+ | xC ⇒ x8 | xD ⇒ x9 | xE ⇒ xA | xF ⇒ xB ]
+ | xC ⇒ match e2 with
+ [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x0 | x3 ⇒ x0
+ | x4 ⇒ x4 | x5 ⇒ x4 | x6 ⇒ x4 | x7 ⇒ x4
+ | x8 ⇒ x8 | x9 ⇒ x8 | xA ⇒ x8 | xB ⇒ x8
+ | xC ⇒ xC | xD ⇒ xC | xE ⇒ xC | xF ⇒ xC ]
+ | xD ⇒ match e2 with
+ [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x0 | x3 ⇒ x1
+ | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x4 | x7 ⇒ x5
+ | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ x8 | xB ⇒ x9
+ | xC ⇒ xC | xD ⇒ xD | xE ⇒ xC | xF ⇒ xD ]
+ | xE ⇒ match e2 with
+ [ x0 ⇒ x0 | x1 ⇒ x0 | x2 ⇒ x2 | x3 ⇒ x2
+ | x4 ⇒ x4 | x5 ⇒ x4 | x6 ⇒ x6 | x7 ⇒ x6
+ | x8 ⇒ x8 | x9 ⇒ x8 | xA ⇒ xA | xB ⇒ xA
+ | xC ⇒ xC | xD ⇒ xC | xE ⇒ xE | xF ⇒ xE ]
+ | xF ⇒ match e2 with
+ [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3
+ | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x6 | x7 ⇒ x7
+ | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ xA | xB ⇒ xB
+ | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ]
+ ].
+
+(* operatore or *)
+ndefinition or_ex ≝
+λe1,e2:exadecim.match e1 with
+ [ x0 ⇒ match e2 with
+ [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3
+ | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x6 | x7 ⇒ x7
+ | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ xA | xB ⇒ xB
+ | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ]
+ | x1 ⇒ match e2 with
+ [ x0 ⇒ x1 | x1 ⇒ x1 | x2 ⇒ x3 | x3 ⇒ x3
+ | x4 ⇒ x5 | x5 ⇒ x5 | x6 ⇒ x7 | x7 ⇒ x7
+ | x8 ⇒ x9 | x9 ⇒ x9 | xA ⇒ xB | xB ⇒ xB
+ | xC ⇒ xD | xD ⇒ xD | xE ⇒ xF | xF ⇒ xF ]
+ | x2 ⇒ match e2 with
+ [ x0 ⇒ x2 | x1 ⇒ x3 | x2 ⇒ x2 | x3 ⇒ x3
+ | x4 ⇒ x6 | x5 ⇒ x7 | x6 ⇒ x6 | x7 ⇒ x7
+ | x8 ⇒ xA | x9 ⇒ xB | xA ⇒ xA | xB ⇒ xB
+ | xC ⇒ xE | xD ⇒ xF | xE ⇒ xE | xF ⇒ xF ]
+ | x3 ⇒ match e2 with
+ [ x0 ⇒ x3 | x1 ⇒ x3 | x2 ⇒ x3 | x3 ⇒ x3
+ | x4 ⇒ x7 | x5 ⇒ x7 | x6 ⇒ x7 | x7 ⇒ x7
+ | x8 ⇒ xB | x9 ⇒ xB | xA ⇒ xB | xB ⇒ xB
+ | xC ⇒ xF | xD ⇒ xF | xE ⇒ xF | xF ⇒ xF ]
+ | x4 ⇒ match e2 with
+ [ x0 ⇒ x4 | x1 ⇒ x5 | x2 ⇒ x6 | x3 ⇒ x7
+ | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x6 | x7 ⇒ x7
+ | x8 ⇒ xC | x9 ⇒ xD | xA ⇒ xE | xB ⇒ xF
+ | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ]
+ | x5 ⇒ match e2 with
+ [ x0 ⇒ x5 | x1 ⇒ x5 | x2 ⇒ x7 | x3 ⇒ x7
+ | x4 ⇒ x5 | x5 ⇒ x5 | x6 ⇒ x7 | x7 ⇒ x7
+ | x8 ⇒ xD | x9 ⇒ xD | xA ⇒ xF | xB ⇒ xF
+ | xC ⇒ xD | xD ⇒ xD | xE ⇒ xF | xF ⇒ xF ]
+ | x6 ⇒ match e2 with
+ [ x0 ⇒ x6 | x1 ⇒ x7 | x2 ⇒ x6 | x3 ⇒ x7
+ | x4 ⇒ x6 | x5 ⇒ x7 | x6 ⇒ x6 | x7 ⇒ x7
+ | x8 ⇒ xE | x9 ⇒ xF | xA ⇒ xE | xB ⇒ xF
+ | xC ⇒ xE | xD ⇒ xF | xE ⇒ xE | xF ⇒ xF ]
+ | x7 ⇒ match e2 with
+ [ x0 ⇒ x7 | x1 ⇒ x7 | x2 ⇒ x7 | x3 ⇒ x7
+ | x4 ⇒ x7 | x5 ⇒ x7 | x6 ⇒ x7 | x7 ⇒ x7
+ | x8 ⇒ xF | x9 ⇒ xF | xA ⇒ xF | xB ⇒ xF
+ | xC ⇒ xF | xD ⇒ xF | xE ⇒ xF | xF ⇒ xF ]
+ | x8 ⇒ match e2 with
+ [ x0 ⇒ x8 | x1 ⇒ x9 | x2 ⇒ xA | x3 ⇒ xB
+ | x4 ⇒ xC | x5 ⇒ xD | x6 ⇒ xE | x7 ⇒ xF
+ | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ xA | xB ⇒ xB
+ | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ]
+ | x9 ⇒ match e2 with
+ [ x0 ⇒ x9 | x1 ⇒ x9 | x2 ⇒ xB | x3 ⇒ xB
+ | x4 ⇒ xD | x5 ⇒ xD | x6 ⇒ xF | x7 ⇒ xF
+ | x8 ⇒ x9 | x9 ⇒ x9 | xA ⇒ xB | xB ⇒ xB
+ | xC ⇒ xD | xD ⇒ xD | xE ⇒ xF | xF ⇒ xF ]
+ | xA ⇒ match e2 with
+ [ x0 ⇒ xA | x1 ⇒ xB | x2 ⇒ xA | x3 ⇒ xB
+ | x4 ⇒ xE | x5 ⇒ xF | x6 ⇒ xE | x7 ⇒ xF
+ | x8 ⇒ xA | x9 ⇒ xB | xA ⇒ xA | xB ⇒ xB
+ | xC ⇒ xE | xD ⇒ xF | xE ⇒ xE | xF ⇒ xF ]
+ | xB ⇒ match e2 with
+ [ x0 ⇒ xB | x1 ⇒ xB | x2 ⇒ xB | x3 ⇒ xB
+ | x4 ⇒ xF | x5 ⇒ xF | x6 ⇒ xF | x7 ⇒ xF
+ | x8 ⇒ xB | x9 ⇒ xB | xA ⇒ xB | xB ⇒ xB
+ | xC ⇒ xF | xD ⇒ xF | xE ⇒ xF | xF ⇒ xF ]
+ | xC ⇒ match e2 with
+ [ x0 ⇒ xC | x1 ⇒ xD | x2 ⇒ xE | x3 ⇒ xF
+ | x4 ⇒ xC | x5 ⇒ xD | x6 ⇒ xE | x7 ⇒ xF
+ | x8 ⇒ xC | x9 ⇒ xD | xA ⇒ xE | xB ⇒ xF
+ | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ]
+ | xD ⇒ match e2 with
+ [ x0 ⇒ xD | x1 ⇒ xD | x2 ⇒ xF | x3 ⇒ xF
+ | x4 ⇒ xD | x5 ⇒ xD | x6 ⇒ xF | x7 ⇒ xF
+ | x8 ⇒ xD | x9 ⇒ xD | xA ⇒ xF | xB ⇒ xF
+ | xC ⇒ xD | xD ⇒ xD | xE ⇒ xF | xF ⇒ xF ]
+ | xE ⇒ match e2 with
+ [ x0 ⇒ xE | x1 ⇒ xF | x2 ⇒ xE | x3 ⇒ xF
+ | x4 ⇒ xE | x5 ⇒ xF | x6 ⇒ xE | x7 ⇒ xF
+ | x8 ⇒ xE | x9 ⇒ xF | xA ⇒ xE | xB ⇒ xF
+ | xC ⇒ xE | xD ⇒ xF | xE ⇒ xE | xF ⇒ xF ]
+ | xF ⇒ match e2 with
+ [ x0 ⇒ xF | x1 ⇒ xF | x2 ⇒ xF | x3 ⇒ xF
+ | x4 ⇒ xF | x5 ⇒ xF | x6 ⇒ xF | x7 ⇒ xF
+ | x8 ⇒ xF | x9 ⇒ xF | xA ⇒ xF | xB ⇒ xF
+ | xC ⇒ xF | xD ⇒ xF | xE ⇒ xF | xF ⇒ xF ]
+ ].
+
+(* operatore xor *)
+ndefinition xor_ex ≝
+λe1,e2:exadecim.match e1 with
+ [ x0 ⇒ match e2 with
+ [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3
+ | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x6 | x7 ⇒ x7
+ | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ xA | xB ⇒ xB
+ | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ]
+ | x1 ⇒ match e2 with
+ [ x0 ⇒ x1 | x1 ⇒ x0 | x2 ⇒ x3 | x3 ⇒ x2
+ | x4 ⇒ x5 | x5 ⇒ x4 | x6 ⇒ x7 | x7 ⇒ x6
+ | x8 ⇒ x9 | x9 ⇒ x8 | xA ⇒ xB | xB ⇒ xA
+ | xC ⇒ xD | xD ⇒ xC | xE ⇒ xF | xF ⇒ xE ]
+ | x2 ⇒ match e2 with
+ [ x0 ⇒ x2 | x1 ⇒ x3 | x2 ⇒ x0 | x3 ⇒ x1
+ | x4 ⇒ x6 | x5 ⇒ x7 | x6 ⇒ x4 | x7 ⇒ x5
+ | x8 ⇒ xA | x9 ⇒ xB | xA ⇒ x8 | xB ⇒ x9
+ | xC ⇒ xE | xD ⇒ xF | xE ⇒ xC | xF ⇒ xD ]
+ | x3 ⇒ match e2 with
+ [ x0 ⇒ x3 | x1 ⇒ x2 | x2 ⇒ x1 | x3 ⇒ x0
+ | x4 ⇒ x7 | x5 ⇒ x6 | x6 ⇒ x5 | x7 ⇒ x4
+ | x8 ⇒ xB | x9 ⇒ xA | xA ⇒ x9 | xB ⇒ x8
+ | xC ⇒ xF | xD ⇒ xE | xE ⇒ xD | xF ⇒ xC ]
+ | x4 ⇒ match e2 with
+ [ x0 ⇒ x4 | x1 ⇒ x5 | x2 ⇒ x6 | x3 ⇒ x7
+ | x4 ⇒ x0 | x5 ⇒ x1 | x6 ⇒ x2 | x7 ⇒ x3
+ | x8 ⇒ xC | x9 ⇒ xD | xA ⇒ xE | xB ⇒ xF
+ | xC ⇒ x8 | xD ⇒ x9 | xE ⇒ xA | xF ⇒ xB ]
+ | x5 ⇒ match e2 with
+ [ x0 ⇒ x5 | x1 ⇒ x4 | x2 ⇒ x7 | x3 ⇒ x6
+ | x4 ⇒ x1 | x5 ⇒ x0 | x6 ⇒ x3 | x7 ⇒ x2
+ | x8 ⇒ xD | x9 ⇒ xC | xA ⇒ xF | xB ⇒ xE
+ | xC ⇒ x9 | xD ⇒ x8 | xE ⇒ xB | xF ⇒ xA ]
+ | x6 ⇒ match e2 with
+ [ x0 ⇒ x6 | x1 ⇒ x7 | x2 ⇒ x4 | x3 ⇒ x5
+ | x4 ⇒ x2 | x5 ⇒ x3 | x6 ⇒ x0 | x7 ⇒ x1
+ | x8 ⇒ xE | x9 ⇒ xF | xA ⇒ xC | xB ⇒ xD
+ | xC ⇒ xA | xD ⇒ xB | xE ⇒ x8 | xF ⇒ x9 ]
+ | x7 ⇒ match e2 with
+ [ x0 ⇒ x7 | x1 ⇒ x6 | x2 ⇒ x5 | x3 ⇒ x4
+ | x4 ⇒ x3 | x5 ⇒ x2 | x6 ⇒ x1 | x7 ⇒ x0
+ | x8 ⇒ xF | x9 ⇒ xE | xA ⇒ xD | xB ⇒ xC
+ | xC ⇒ xB | xD ⇒ xA | xE ⇒ x9 | xF ⇒ x8 ]
+ | x8 ⇒ match e2 with
+ [ x0 ⇒ x8 | x1 ⇒ x9 | x2 ⇒ xA | x3 ⇒ xB
+ | x4 ⇒ xC | x5 ⇒ xD | x6 ⇒ xE | x7 ⇒ xF
+ | x8 ⇒ x0 | x9 ⇒ x1 | xA ⇒ x2 | xB ⇒ x3
+ | xC ⇒ x4 | xD ⇒ x5 | xE ⇒ x6 | xF ⇒ x7 ]
+ | x9 ⇒ match e2 with
+ [ x0 ⇒ x9 | x1 ⇒ x8 | x2 ⇒ xB | x3 ⇒ xA
+ | x4 ⇒ xD | x5 ⇒ xC | x6 ⇒ xF | x7 ⇒ xE
+ | x8 ⇒ x1 | x9 ⇒ x0 | xA ⇒ x3 | xB ⇒ x2
+ | xC ⇒ x5 | xD ⇒ x4 | xE ⇒ x7 | xF ⇒ x6 ]
+ | xA ⇒ match e2 with
+ [ x0 ⇒ xA | x1 ⇒ xB | x2 ⇒ x8 | x3 ⇒ x9
+ | x4 ⇒ xE | x5 ⇒ xF | x6 ⇒ xC | x7 ⇒ xD
+ | x8 ⇒ x2 | x9 ⇒ x3 | xA ⇒ x0 | xB ⇒ x1
+ | xC ⇒ x6 | xD ⇒ x7 | xE ⇒ x4 | xF ⇒ x5 ]
+ | xB ⇒ match e2 with
+ [ x0 ⇒ xB | x1 ⇒ xA | x2 ⇒ x9 | x3 ⇒ x8
+ | x4 ⇒ xF | x5 ⇒ xE | x6 ⇒ xD | x7 ⇒ xC
+ | x8 ⇒ x3 | x9 ⇒ x2 | xA ⇒ x1 | xB ⇒ x0
+ | xC ⇒ x7 | xD ⇒ x6 | xE ⇒ x5 | xF ⇒ x4 ]
+ | xC ⇒ match e2 with
+ [ x0 ⇒ xC | x1 ⇒ xD | x2 ⇒ xE | x3 ⇒ xF
+ | x4 ⇒ x8 | x5 ⇒ x9 | x6 ⇒ xA | x7 ⇒ xB
+ | x8 ⇒ x4 | x9 ⇒ x5 | xA ⇒ x6 | xB ⇒ x7
+ | xC ⇒ x0 | xD ⇒ x1 | xE ⇒ x2 | xF ⇒ x3 ]
+ | xD ⇒ match e2 with
+ [ x0 ⇒ xD | x1 ⇒ xC | x2 ⇒ xF | x3 ⇒ xE
+ | x4 ⇒ x9 | x5 ⇒ x8 | x6 ⇒ xB | x7 ⇒ xA
+ | x8 ⇒ x5 | x9 ⇒ x4 | xA ⇒ x7 | xB ⇒ x6
+ | xC ⇒ x1 | xD ⇒ x0 | xE ⇒ x3 | xF ⇒ x2 ]
+ | xE ⇒ match e2 with
+ [ x0 ⇒ xE | x1 ⇒ xF | x2 ⇒ xC | x3 ⇒ xD
+ | x4 ⇒ xA | x5 ⇒ xB | x6 ⇒ x8 | x7 ⇒ x9
+ | x8 ⇒ x6 | x9 ⇒ x7 | xA ⇒ x4 | xB ⇒ x5
+ | xC ⇒ x2 | xD ⇒ x3 | xE ⇒ x0 | xF ⇒ x1 ]
+ | xF ⇒ match e2 with
+ [ x0 ⇒ xF | x1 ⇒ xE | x2 ⇒ xD | x3 ⇒ xC
+ | x4 ⇒ xB | x5 ⇒ xA | x6 ⇒ x9 | x7 ⇒ x8
+ | x8 ⇒ x7 | x9 ⇒ x6 | xA ⇒ x5 | xB ⇒ x4
+ | xC ⇒ x3 | xD ⇒ x2 | xE ⇒ x1 | xF ⇒ x0 ]
+ ].
+
+(* operatore rotazione destra con carry *)
+ndefinition rcr_ex ≝
+λe:exadecim.λc:bool.match c with
+ [ true ⇒ match e with
+ [ x0 ⇒ pair exadecim bool x8 false | x1 ⇒ pair exadecim bool x8 true
+ | x2 ⇒ pair exadecim bool x9 false | x3 ⇒ pair exadecim bool x9 true
+ | x4 ⇒ pair exadecim bool xA false | x5 ⇒ pair exadecim bool xA true
+ | x6 ⇒ pair exadecim bool xB false | x7 ⇒ pair exadecim bool xB true
+ | x8 ⇒ pair exadecim bool xC false | x9 ⇒ pair exadecim bool xC true
+ | xA ⇒ pair exadecim bool xD false | xB ⇒ pair exadecim bool xD true
+ | xC ⇒ pair exadecim bool xE false | xD ⇒ pair exadecim bool xE true
+ | xE ⇒ pair exadecim bool xF false | xF ⇒ pair exadecim bool xF true ]
+ | false ⇒ match e with
+ [ x0 ⇒ pair exadecim bool x0 false | x1 ⇒ pair exadecim bool x0 true
+ | x2 ⇒ pair exadecim bool x1 false | x3 ⇒ pair exadecim bool x1 true
+ | x4 ⇒ pair exadecim bool x2 false | x5 ⇒ pair exadecim bool x2 true
+ | x6 ⇒ pair exadecim bool x3 false | x7 ⇒ pair exadecim bool x3 true
+ | x8 ⇒ pair exadecim bool x4 false | x9 ⇒ pair exadecim bool x4 true
+ | xA ⇒ pair exadecim bool x5 false | xB ⇒ pair exadecim bool x5 true
+ | xC ⇒ pair exadecim bool x6 false | xD ⇒ pair exadecim bool x6 true
+ | xE ⇒ pair exadecim bool x7 false | xF ⇒ pair exadecim bool x7 true ]
+ ].
+
+(* operatore shift destro *)
+ndefinition shr_ex ≝
+λe:exadecim.match e with
+ [ x0 ⇒ pair exadecim bool x0 false | x1 ⇒ pair exadecim bool x0 true
+ | x2 ⇒ pair exadecim bool x1 false | x3 ⇒ pair exadecim bool x1 true
+ | x4 ⇒ pair exadecim bool x2 false | x5 ⇒ pair exadecim bool x2 true
+ | x6 ⇒ pair exadecim bool x3 false | x7 ⇒ pair exadecim bool x3 true
+ | x8 ⇒ pair exadecim bool x4 false | x9 ⇒ pair exadecim bool x4 true
+ | xA ⇒ pair exadecim bool x5 false | xB ⇒ pair exadecim bool x5 true
+ | xC ⇒ pair exadecim bool x6 false | xD ⇒ pair exadecim bool x6 true
+ | xE ⇒ pair exadecim bool x7 false | xF ⇒ pair exadecim bool x7 true ].
+
+(* operatore rotazione destra *)
+ndefinition ror_ex ≝
+λe:exadecim.match e with
+ [ x0 ⇒ x0 | x1 ⇒ x8 | x2 ⇒ x1 | x3 ⇒ x9
+ | x4 ⇒ x2 | x5 ⇒ xA | x6 ⇒ x3 | x7 ⇒ xB
+ | x8 ⇒ x4 | x9 ⇒ xC | xA ⇒ x5 | xB ⇒ xD
+ | xC ⇒ x6 | xD ⇒ xE | xE ⇒ x7 | xF ⇒ xF ].
+
+(* operatore rotazione destra n-volte *)
+nlet rec ror_ex_n (e:exadecim) (n:quatern) (r:rec_quatern n) on r ≝
+ match r with
+ [ qu_O ⇒ e
+ | qu_S t n' ⇒ ror_ex_n (ror_ex e) t n' ].
+
+(* operatore rotazione sinistra con carry *)
+ndefinition rcl_ex ≝
+λe:exadecim.λc:bool.match c with
+ [ true ⇒ match e with
+ [ x0 ⇒ pair exadecim bool x1 false | x1 ⇒ pair exadecim bool x3 false
+ | x2 ⇒ pair exadecim bool x5 false | x3 ⇒ pair exadecim bool x7 false
+ | x4 ⇒ pair exadecim bool x9 false | x5 ⇒ pair exadecim bool xB false
+ | x6 ⇒ pair exadecim bool xD false | x7 ⇒ pair exadecim bool xF false
+ | x8 ⇒ pair exadecim bool x1 true | x9 ⇒ pair exadecim bool x3 true
+ | xA ⇒ pair exadecim bool x5 true | xB ⇒ pair exadecim bool x7 true
+ | xC ⇒ pair exadecim bool x9 true | xD ⇒ pair exadecim bool xB true
+ | xE ⇒ pair exadecim bool xD true | xF ⇒ pair exadecim bool xF true ]
+ | false ⇒ match e with
+ [ x0 ⇒ pair exadecim bool x0 false | x1 ⇒ pair exadecim bool x2 false
+ | x2 ⇒ pair exadecim bool x4 false | x3 ⇒ pair exadecim bool x6 false
+ | x4 ⇒ pair exadecim bool x8 false | x5 ⇒ pair exadecim bool xA false
+ | x6 ⇒ pair exadecim bool xC false | x7 ⇒ pair exadecim bool xE false
+ | x8 ⇒ pair exadecim bool x0 true | x9 ⇒ pair exadecim bool x2 true
+ | xA ⇒ pair exadecim bool x4 true | xB ⇒ pair exadecim bool x6 true
+ | xC ⇒ pair exadecim bool x8 true | xD ⇒ pair exadecim bool xA true
+ | xE ⇒ pair exadecim bool xC true | xF ⇒ pair exadecim bool xE true ]
+ ].
+
+(* operatore shift sinistro *)
+ndefinition shl_ex ≝
+λe:exadecim.match e with
+ [ x0 ⇒ pair exadecim bool x0 false | x1 ⇒ pair exadecim bool x2 false
+ | x2 ⇒ pair exadecim bool x4 false | x3 ⇒ pair exadecim bool x6 false
+ | x4 ⇒ pair exadecim bool x8 false | x5 ⇒ pair exadecim bool xA false
+ | x6 ⇒ pair exadecim bool xC false | x7 ⇒ pair exadecim bool xE false
+ | x8 ⇒ pair exadecim bool x0 true | x9 ⇒ pair exadecim bool x2 true
+ | xA ⇒ pair exadecim bool x4 true | xB ⇒ pair exadecim bool x6 true
+ | xC ⇒ pair exadecim bool x8 true | xD ⇒ pair exadecim bool xA true
+ | xE ⇒ pair exadecim bool xC true | xF ⇒ pair exadecim bool xE true ].
+
+(* operatore rotazione sinistra *)
+ndefinition rol_ex ≝
+λe:exadecim.match e with
+ [ x0 ⇒ x0 | x1 ⇒ x2 | x2 ⇒ x4 | x3 ⇒ x6
+ | x4 ⇒ x8 | x5 ⇒ xA | x6 ⇒ xC | x7 ⇒ xE
+ | x8 ⇒ x1 | x9 ⇒ x3 | xA ⇒ x5 | xB ⇒ x7
+ | xC ⇒ x9 | xD ⇒ xB | xE ⇒ xD | xF ⇒ xF ].
+
+(* operatore rotazione sinistra n-volte *)
+nlet rec rol_ex_n (e:exadecim) (n:quatern) (r:rec_quatern n) on r ≝
+ match r with
+ [ qu_O ⇒ e
+ | qu_S t n' ⇒ rol_ex_n (rol_ex e) t n' ].
+
+(* operatore not/complemento a 1 *)
+ndefinition not_ex ≝
+λe:exadecim.match e with
+ [ x0 ⇒ xF | x1 ⇒ xE | x2 ⇒ xD | x3 ⇒ xC
+ | x4 ⇒ xB | x5 ⇒ xA | x6 ⇒ x9 | x7 ⇒ x8
+ | x8 ⇒ x7 | x9 ⇒ x6 | xA ⇒ x5 | xB ⇒ x4
+ | xC ⇒ x3 | xD ⇒ x2 | xE ⇒ x1 | xF ⇒ x0 ].
+
+(* operatore somma con data+carry → data+carry *)
+ndefinition plus_ex_dc_dc ≝
+λe1,e2:exadecim.λc:bool.
+ match c with
+ [ true ⇒ match e1 with
+ [ x0 ⇒ match e2 with
+ [ x0 ⇒ pair … x1 false | x1 ⇒ pair … x2 false | x2 ⇒ pair … x3 false | x3 ⇒ pair … x4 false
+ | x4 ⇒ pair … x5 false | x5 ⇒ pair … x6 false | x6 ⇒ pair … x7 false | x7 ⇒ pair … x8 false
+ | x8 ⇒ pair … x9 false | x9 ⇒ pair … xA false | xA ⇒ pair … xB false | xB ⇒ pair … xC false
+ | xC ⇒ pair … xD false | xD ⇒ pair … xE false | xE ⇒ pair … xF false | xF ⇒ pair … x0 true ]
+ | x1 ⇒ match e2 with
+ [ x0 ⇒ pair … x2 false | x1 ⇒ pair … x3 false | x2 ⇒ pair … x4 false | x3 ⇒ pair … x5 false
+ | x4 ⇒ pair … x6 false | x5 ⇒ pair … x7 false | x6 ⇒ pair … x8 false | x7 ⇒ pair … x9 false
+ | x8 ⇒ pair … xA false | x9 ⇒ pair … xB false | xA ⇒ pair … xC false | xB ⇒ pair … xD false
+ | xC ⇒ pair … xE false | xD ⇒ pair … xF false | xE ⇒ pair … x0 true | xF ⇒ pair … x1 true ]
+ | x2 ⇒ match e2 with
+ [ x0 ⇒ pair … x3 false | x1 ⇒ pair … x4 false | x2 ⇒ pair … x5 false | x3 ⇒ pair … x6 false
+ | x4 ⇒ pair … x7 false | x5 ⇒ pair … x8 false | x6 ⇒ pair … x9 false | x7 ⇒ pair … xA false
+ | x8 ⇒ pair … xB false | x9 ⇒ pair … xC false | xA ⇒ pair … xD false | xB ⇒ pair … xE false
+ | xC ⇒ pair … xF false | xD ⇒ pair … x0 true | xE ⇒ pair … x1 true | xF ⇒ pair … x2 true ]
+ | x3 ⇒ match e2 with
+ [ x0 ⇒ pair … x4 false | x1 ⇒ pair … x5 false | x2 ⇒ pair … x6 false | x3 ⇒ pair … x7 false
+ | x4 ⇒ pair … x8 false | x5 ⇒ pair … x9 false | x6 ⇒ pair … xA false | x7 ⇒ pair … xB false
+ | x8 ⇒ pair … xC false | x9 ⇒ pair … xD false | xA ⇒ pair … xE false | xB ⇒ pair … xF false
+ | xC ⇒ pair … x0 true | xD ⇒ pair … x1 true | xE ⇒ pair … x2 true | xF ⇒ pair … x3 true ]
+ | x4 ⇒ match e2 with
+ [ x0 ⇒ pair … x5 false | x1 ⇒ pair … x6 false | x2 ⇒ pair … x7 false | x3 ⇒ pair … x8 false
+ | x4 ⇒ pair … x9 false | x5 ⇒ pair … xA false | x6 ⇒ pair … xB false | x7 ⇒ pair … xC false
+ | x8 ⇒ pair … xD false | x9 ⇒ pair … xE false | xA ⇒ pair … xF false | xB ⇒ pair … x0 true
+ | xC ⇒ pair … x1 true | xD ⇒ pair … x2 true | xE ⇒ pair … x3 true | xF ⇒ pair … x4 true ]
+ | x5 ⇒ match e2 with
+ [ x0 ⇒ pair … x6 false | x1 ⇒ pair … x7 false | x2 ⇒ pair … x8 false | x3 ⇒ pair … x9 false
+ | x4 ⇒ pair … xA false | x5 ⇒ pair … xB false | x6 ⇒ pair … xC false | x7 ⇒ pair … xD false
+ | x8 ⇒ pair … xE false | x9 ⇒ pair … xF false | xA ⇒ pair … x0 true | xB ⇒ pair … x1 true
+ | xC ⇒ pair … x2 true | xD ⇒ pair … x3 true | xE ⇒ pair … x4 true | xF ⇒ pair … x5 true ]
+ | x6 ⇒ match e2 with
+ [ x0 ⇒ pair … x7 false | x1 ⇒ pair … x8 false | x2 ⇒ pair … x9 false | x3 ⇒ pair … xA false
+ | x4 ⇒ pair … xB false | x5 ⇒ pair … xC false | x6 ⇒ pair … xD false | x7 ⇒ pair … xE false
+ | x8 ⇒ pair … xF false | x9 ⇒ pair … x0 true | xA ⇒ pair … x1 true | xB ⇒ pair … x2 true
+ | xC ⇒ pair … x3 true | xD ⇒ pair … x4 true | xE ⇒ pair … x5 true | xF ⇒ pair … x6 true ]
+ | x7 ⇒ match e2 with
+ [ x0 ⇒ pair … x8 false | x1 ⇒ pair … x9 false | x2 ⇒ pair … xA false | x3 ⇒ pair … xB false
+ | x4 ⇒ pair … xC false | x5 ⇒ pair … xD false | x6 ⇒ pair … xE false | x7 ⇒ pair … xF false
+ | x8 ⇒ pair … x0 true | x9 ⇒ pair … x1 true | xA ⇒ pair … x2 true | xB ⇒ pair … x3 true
+ | xC ⇒ pair … x4 true | xD ⇒ pair … x5 true | xE ⇒ pair … x6 true | xF ⇒ pair … x7 true ]
+ | x8 ⇒ match e2 with
+ [ x0 ⇒ pair … x9 false | x1 ⇒ pair … xA false | x2 ⇒ pair … xB false | x3 ⇒ pair … xC false
+ | x4 ⇒ pair … xD false | x5 ⇒ pair … xE false | x6 ⇒ pair … xF false | x7 ⇒ pair … x0 true
+ | x8 ⇒ pair … x1 true | x9 ⇒ pair … x2 true | xA ⇒ pair … x3 true | xB ⇒ pair … x4 true
+ | xC ⇒ pair … x5 true | xD ⇒ pair … x6 true | xE ⇒ pair … x7 true | xF ⇒ pair … x8 true ]
+ | x9 ⇒ match e2 with
+ [ x0 ⇒ pair … xA false | x1 ⇒ pair … xB false | x2 ⇒ pair … xC false | x3 ⇒ pair … xD false
+ | x4 ⇒ pair … xE false | x5 ⇒ pair … xF false | x6 ⇒ pair … x0 true | x7 ⇒ pair … x1 true
+ | x8 ⇒ pair … x2 true | x9 ⇒ pair … x3 true | xA ⇒ pair … x4 true | xB ⇒ pair … x5 true
+ | xC ⇒ pair … x6 true | xD ⇒ pair … x7 true | xE ⇒ pair … x8 true | xF ⇒ pair … x9 true ]
+ | xA ⇒ match e2 with
+ [ x0 ⇒ pair … xB false | x1 ⇒ pair … xC false | x2 ⇒ pair … xD false | x3 ⇒ pair … xE false
+ | x4 ⇒ pair … xF false | x5 ⇒ pair … x0 true | x6 ⇒ pair … x1 true | x7 ⇒ pair … x2 true
+ | x8 ⇒ pair … x3 true | x9 ⇒ pair … x4 true | xA ⇒ pair … x5 true | xB ⇒ pair … x6 true
+ | xC ⇒ pair … x7 true | xD ⇒ pair … x8 true | xE ⇒ pair … x9 true | xF ⇒ pair … xA true ]
+ | xB ⇒ match e2 with
+ [ x0 ⇒ pair … xC false | x1 ⇒ pair … xD false | x2 ⇒ pair … xE false | x3 ⇒ pair … xF false
+ | x4 ⇒ pair … x0 true | x5 ⇒ pair … x1 true | x6 ⇒ pair … x2 true | x7 ⇒ pair … x3 true
+ | x8 ⇒ pair … x4 true | x9 ⇒ pair … x5 true | xA ⇒ pair … x6 true | xB ⇒ pair … x7 true
+ | xC ⇒ pair … x8 true | xD ⇒ pair … x9 true | xE ⇒ pair … xA true | xF ⇒ pair … xB true ]
+ | xC ⇒ match e2 with
+ [ x0 ⇒ pair … xD false | x1 ⇒ pair … xE false | x2 ⇒ pair … xF false | x3 ⇒ pair … x0 true
+ | x4 ⇒ pair … x1 true | x5 ⇒ pair … x2 true | x6 ⇒ pair … x3 true | x7 ⇒ pair … x4 true
+ | x8 ⇒ pair … x5 true | x9 ⇒ pair … x6 true | xA ⇒ pair … x7 true | xB ⇒ pair … x8 true
+ | xC ⇒ pair … x9 true | xD ⇒ pair … xA true | xE ⇒ pair … xB true | xF ⇒ pair … xC true ]
+ | xD ⇒ match e2 with
+ [ x0 ⇒ pair … xE false | x1 ⇒ pair … xF false | x2 ⇒ pair … x0 true | x3 ⇒ pair … x1 true
+ | x4 ⇒ pair … x2 true | x5 ⇒ pair … x3 true | x6 ⇒ pair … x4 true | x7 ⇒ pair … x5 true
+ | x8 ⇒ pair … x6 true | x9 ⇒ pair … x7 true | xA ⇒ pair … x8 true | xB ⇒ pair … x9 true
+ | xC ⇒ pair … xA true | xD ⇒ pair … xB true | xE ⇒ pair … xC true | xF ⇒ pair … xD true ]
+ | xE ⇒ match e2 with
+ [ x0 ⇒ pair … xF false | x1 ⇒ pair … x0 true | x2 ⇒ pair … x1 true | x3 ⇒ pair … x2 true
+ | x4 ⇒ pair … x3 true | x5 ⇒ pair … x4 true | x6 ⇒ pair … x5 true | x7 ⇒ pair … x6 true
+ | x8 ⇒ pair … x7 true | x9 ⇒ pair … x8 true | xA ⇒ pair … x9 true | xB ⇒ pair … xA true
+ | xC ⇒ pair … xB true | xD ⇒ pair … xC true | xE ⇒ pair … xD true | xF ⇒ pair … xE true ]
+ | xF ⇒ match e2 with
+ [ x0 ⇒ pair … x0 true | x1 ⇒ pair … x1 true | x2 ⇒ pair … x2 true | x3 ⇒ pair … x3 true
+ | x4 ⇒ pair … x4 true | x5 ⇒ pair … x5 true | x6 ⇒ pair … x6 true | x7 ⇒ pair … x7 true
+ | x8 ⇒ pair … x8 true | x9 ⇒ pair … x9 true | xA ⇒ pair … xA true | xB ⇒ pair … xB true
+ | xC ⇒ pair … xC true | xD ⇒ pair … xD true | xE ⇒ pair … xE true | xF ⇒ pair … xF true ]
+ ]
+ | false ⇒ match e1 with
+ [ x0 ⇒ match e2 with
+ [ x0 ⇒ pair … x0 false | x1 ⇒ pair … x1 false | x2 ⇒ pair … x2 false | x3 ⇒ pair … x3 false
+ | x4 ⇒ pair … x4 false | x5 ⇒ pair … x5 false | x6 ⇒ pair … x6 false | x7 ⇒ pair … x7 false
+ | x8 ⇒ pair … x8 false | x9 ⇒ pair … x9 false | xA ⇒ pair … xA false | xB ⇒ pair … xB false
+ | xC ⇒ pair … xC false | xD ⇒ pair … xD false | xE ⇒ pair … xE false | xF ⇒ pair … xF false ]
+ | x1 ⇒ match e2 with
+ [ x0 ⇒ pair … x1 false | x1 ⇒ pair … x2 false | x2 ⇒ pair … x3 false | x3 ⇒ pair … x4 false
+ | x4 ⇒ pair … x5 false | x5 ⇒ pair … x6 false | x6 ⇒ pair … x7 false | x7 ⇒ pair … x8 false
+ | x8 ⇒ pair … x9 false | x9 ⇒ pair … xA false | xA ⇒ pair … xB false | xB ⇒ pair … xC false
+ | xC ⇒ pair … xD false | xD ⇒ pair … xE false | xE ⇒ pair … xF false | xF ⇒ pair … x0 true ]
+ | x2 ⇒ match e2 with
+ [ x0 ⇒ pair … x2 false | x1 ⇒ pair … x3 false | x2 ⇒ pair … x4 false | x3 ⇒ pair … x5 false
+ | x4 ⇒ pair … x6 false | x5 ⇒ pair … x7 false | x6 ⇒ pair … x8 false | x7 ⇒ pair … x9 false
+ | x8 ⇒ pair … xA false | x9 ⇒ pair … xB false | xA ⇒ pair … xC false | xB ⇒ pair … xD false
+ | xC ⇒ pair … xE false | xD ⇒ pair … xF false | xE ⇒ pair … x0 true | xF ⇒ pair … x1 true ]
+ | x3 ⇒ match e2 with
+ [ x0 ⇒ pair … x3 false | x1 ⇒ pair … x4 false | x2 ⇒ pair … x5 false | x3 ⇒ pair … x6 false
+ | x4 ⇒ pair … x7 false | x5 ⇒ pair … x8 false | x6 ⇒ pair … x9 false | x7 ⇒ pair … xA false
+ | x8 ⇒ pair … xB false | x9 ⇒ pair … xC false | xA ⇒ pair … xD false | xB ⇒ pair … xE false
+ | xC ⇒ pair … xF false | xD ⇒ pair … x0 true | xE ⇒ pair … x1 true | xF ⇒ pair … x2 true ]
+ | x4 ⇒ match e2 with
+ [ x0 ⇒ pair … x4 false | x1 ⇒ pair … x5 false | x2 ⇒ pair … x6 false | x3 ⇒ pair … x7 false
+ | x4 ⇒ pair … x8 false | x5 ⇒ pair … x9 false | x6 ⇒ pair … xA false | x7 ⇒ pair … xB false
+ | x8 ⇒ pair … xC false | x9 ⇒ pair … xD false | xA ⇒ pair … xE false | xB ⇒ pair … xF false
+ | xC ⇒ pair … x0 true | xD ⇒ pair … x1 true | xE ⇒ pair … x2 true | xF ⇒ pair … x3 true ]
+ | x5 ⇒ match e2 with
+ [ x0 ⇒ pair … x5 false | x1 ⇒ pair … x6 false | x2 ⇒ pair … x7 false | x3 ⇒ pair … x8 false
+ | x4 ⇒ pair … x9 false | x5 ⇒ pair … xA false | x6 ⇒ pair … xB false | x7 ⇒ pair … xC false
+ | x8 ⇒ pair … xD false | x9 ⇒ pair … xE false | xA ⇒ pair … xF false | xB ⇒ pair … x0 true
+ | xC ⇒ pair … x1 true | xD ⇒ pair … x2 true | xE ⇒ pair … x3 true | xF ⇒ pair … x4 true ]
+ | x6 ⇒ match e2 with
+ [ x0 ⇒ pair … x6 false | x1 ⇒ pair … x7 false | x2 ⇒ pair … x8 false | x3 ⇒ pair … x9 false
+ | x4 ⇒ pair … xA false | x5 ⇒ pair … xB false | x6 ⇒ pair … xC false | x7 ⇒ pair … xD false
+ | x8 ⇒ pair … xE false | x9 ⇒ pair … xF false | xA ⇒ pair … x0 true | xB ⇒ pair … x1 true
+ | xC ⇒ pair … x2 true | xD ⇒ pair … x3 true | xE ⇒ pair … x4 true | xF ⇒ pair … x5 true ]
+ | x7 ⇒ match e2 with
+ [ x0 ⇒ pair … x7 false | x1 ⇒ pair … x8 false | x2 ⇒ pair … x9 false | x3 ⇒ pair … xA false
+ | x4 ⇒ pair … xB false | x5 ⇒ pair … xC false | x6 ⇒ pair … xD false | x7 ⇒ pair … xE false
+ | x8 ⇒ pair … xF false | x9 ⇒ pair … x0 true | xA ⇒ pair … x1 true | xB ⇒ pair … x2 true
+ | xC ⇒ pair … x3 true | xD ⇒ pair … x4 true | xE ⇒ pair … x5 true | xF ⇒ pair … x6 true ]
+ | x8 ⇒ match e2 with
+ [ x0 ⇒ pair … x8 false | x1 ⇒ pair … x9 false | x2 ⇒ pair … xA false | x3 ⇒ pair … xB false
+ | x4 ⇒ pair … xC false | x5 ⇒ pair … xD false | x6 ⇒ pair … xE false | x7 ⇒ pair … xF false
+ | x8 ⇒ pair … x0 true | x9 ⇒ pair … x1 true | xA ⇒ pair … x2 true | xB ⇒ pair … x3 true
+ | xC ⇒ pair … x4 true | xD ⇒ pair … x5 true | xE ⇒ pair … x6 true | xF ⇒ pair … x7 true ]
+ | x9 ⇒ match e2 with
+ [ x0 ⇒ pair … x9 false | x1 ⇒ pair … xA false | x2 ⇒ pair … xB false | x3 ⇒ pair … xC false
+ | x4 ⇒ pair … xD false | x5 ⇒ pair … xE false | x6 ⇒ pair … xF false | x7 ⇒ pair … x0 true
+ | x8 ⇒ pair … x1 true | x9 ⇒ pair … x2 true | xA ⇒ pair … x3 true | xB ⇒ pair … x4 true
+ | xC ⇒ pair … x5 true | xD ⇒ pair … x6 true | xE ⇒ pair … x7 true | xF ⇒ pair … x8 true ]
+ | xA ⇒ match e2 with
+ [ x0 ⇒ pair … xA false | x1 ⇒ pair … xB false | x2 ⇒ pair … xC false | x3 ⇒ pair … xD false
+ | x4 ⇒ pair … xE false | x5 ⇒ pair … xF false | x6 ⇒ pair … x0 true | x7 ⇒ pair … x1 true
+ | x8 ⇒ pair … x2 true | x9 ⇒ pair … x3 true | xA ⇒ pair … x4 true | xB ⇒ pair … x5 true
+ | xC ⇒ pair … x6 true | xD ⇒ pair … x7 true | xE ⇒ pair … x8 true | xF ⇒ pair … x9 true ]
+ | xB ⇒ match e2 with
+ [ x0 ⇒ pair … xB false | x1 ⇒ pair … xC false | x2 ⇒ pair … xD false | x3 ⇒ pair … xE false
+ | x4 ⇒ pair … xF false | x5 ⇒ pair … x0 true | x6 ⇒ pair … x1 true | x7 ⇒ pair … x2 true
+ | x8 ⇒ pair … x3 true | x9 ⇒ pair … x4 true | xA ⇒ pair … x5 true | xB ⇒ pair … x6 true
+ | xC ⇒ pair … x7 true | xD ⇒ pair … x8 true | xE ⇒ pair … x9 true | xF ⇒ pair … xA true ]
+ | xC ⇒ match e2 with
+ [ x0 ⇒ pair … xC false | x1 ⇒ pair … xD false | x2 ⇒ pair … xE false | x3 ⇒ pair … xF false
+ | x4 ⇒ pair … x0 true | x5 ⇒ pair … x1 true | x6 ⇒ pair … x2 true | x7 ⇒ pair … x3 true
+ | x8 ⇒ pair … x4 true | x9 ⇒ pair … x5 true | xA ⇒ pair … x6 true | xB ⇒ pair … x7 true
+ | xC ⇒ pair … x8 true | xD ⇒ pair … x9 true | xE ⇒ pair … xA true | xF ⇒ pair … xB true ]
+ | xD ⇒ match e2 with
+ [ x0 ⇒ pair … xD false | x1 ⇒ pair … xE false | x2 ⇒ pair … xF false | x3 ⇒ pair … x0 true
+ | x4 ⇒ pair … x1 true | x5 ⇒ pair … x2 true | x6 ⇒ pair … x3 true | x7 ⇒ pair … x4 true
+ | x8 ⇒ pair … x5 true | x9 ⇒ pair … x6 true | xA ⇒ pair … x7 true | xB ⇒ pair … x8 true
+ | xC ⇒ pair … x9 true | xD ⇒ pair … xA true | xE ⇒ pair … xB true | xF ⇒ pair … xC true ]
+ | xE ⇒ match e2 with
+ [ x0 ⇒ pair … xE false | x1 ⇒ pair … xF false | x2 ⇒ pair … x0 true | x3 ⇒ pair … x1 true
+ | x4 ⇒ pair … x2 true | x5 ⇒ pair … x3 true | x6 ⇒ pair … x4 true | x7 ⇒ pair … x5 true
+ | x8 ⇒ pair … x6 true | x9 ⇒ pair … x7 true | xA ⇒ pair … x8 true | xB ⇒ pair … x9 true
+ | xC ⇒ pair … xA true | xD ⇒ pair … xB true | xE ⇒ pair … xC true | xF ⇒ pair … xD true ]
+ | xF ⇒ match e2 with
+ [ x0 ⇒ pair … xF false | x1 ⇒ pair … x0 true | x2 ⇒ pair … x1 true | x3 ⇒ pair … x2 true
+ | x4 ⇒ pair … x3 true | x5 ⇒ pair … x4 true | x6 ⇒ pair … x5 true | x7 ⇒ pair … x6 true
+ | x8 ⇒ pair … x7 true | x9 ⇒ pair … x8 true | xA ⇒ pair … x9 true | xB ⇒ pair … xA true
+ | xC ⇒ pair … xB true | xD ⇒ pair … xC true | xE ⇒ pair … xD true | xF ⇒ pair … xE true ]
+ ]].
+
+(* operatore somma con data → data+carry *)
+ndefinition plus_ex_d_dc ≝
+λe1,e2:exadecim.
+ match e1 with
+ [ x0 ⇒ match e2 with
+ [ x0 ⇒ pair … x0 false | x1 ⇒ pair … x1 false | x2 ⇒ pair … x2 false | x3 ⇒ pair … x3 false
+ | x4 ⇒ pair … x4 false | x5 ⇒ pair … x5 false | x6 ⇒ pair … x6 false | x7 ⇒ pair … x7 false
+ | x8 ⇒ pair … x8 false | x9 ⇒ pair … x9 false | xA ⇒ pair … xA false | xB ⇒ pair … xB false
+ | xC ⇒ pair … xC false | xD ⇒ pair … xD false | xE ⇒ pair … xE false | xF ⇒ pair … xF false ]
+ | x1 ⇒ match e2 with
+ [ x0 ⇒ pair … x1 false | x1 ⇒ pair … x2 false | x2 ⇒ pair … x3 false | x3 ⇒ pair … x4 false
+ | x4 ⇒ pair … x5 false | x5 ⇒ pair … x6 false | x6 ⇒ pair … x7 false | x7 ⇒ pair … x8 false
+ | x8 ⇒ pair … x9 false | x9 ⇒ pair … xA false | xA ⇒ pair … xB false | xB ⇒ pair … xC false
+ | xC ⇒ pair … xD false | xD ⇒ pair … xE false | xE ⇒ pair … xF false | xF ⇒ pair … x0 true ]
+ | x2 ⇒ match e2 with
+ [ x0 ⇒ pair … x2 false | x1 ⇒ pair … x3 false | x2 ⇒ pair … x4 false | x3 ⇒ pair … x5 false
+ | x4 ⇒ pair … x6 false | x5 ⇒ pair … x7 false | x6 ⇒ pair … x8 false | x7 ⇒ pair … x9 false
+ | x8 ⇒ pair … xA false | x9 ⇒ pair … xB false | xA ⇒ pair … xC false | xB ⇒ pair … xD false
+ | xC ⇒ pair … xE false | xD ⇒ pair … xF false | xE ⇒ pair … x0 true | xF ⇒ pair … x1 true ]
+ | x3 ⇒ match e2 with
+ [ x0 ⇒ pair … x3 false | x1 ⇒ pair … x4 false | x2 ⇒ pair … x5 false | x3 ⇒ pair … x6 false
+ | x4 ⇒ pair … x7 false | x5 ⇒ pair … x8 false | x6 ⇒ pair … x9 false | x7 ⇒ pair … xA false
+ | x8 ⇒ pair … xB false | x9 ⇒ pair … xC false | xA ⇒ pair … xD false | xB ⇒ pair … xE false
+ | xC ⇒ pair … xF false | xD ⇒ pair … x0 true | xE ⇒ pair … x1 true | xF ⇒ pair … x2 true ]
+ | x4 ⇒ match e2 with
+ [ x0 ⇒ pair … x4 false | x1 ⇒ pair … x5 false | x2 ⇒ pair … x6 false | x3 ⇒ pair … x7 false
+ | x4 ⇒ pair … x8 false | x5 ⇒ pair … x9 false | x6 ⇒ pair … xA false | x7 ⇒ pair … xB false
+ | x8 ⇒ pair … xC false | x9 ⇒ pair … xD false | xA ⇒ pair … xE false | xB ⇒ pair … xF false
+ | xC ⇒ pair … x0 true | xD ⇒ pair … x1 true | xE ⇒ pair … x2 true | xF ⇒ pair … x3 true ]
+ | x5 ⇒ match e2 with
+ [ x0 ⇒ pair … x5 false | x1 ⇒ pair … x6 false | x2 ⇒ pair … x7 false | x3 ⇒ pair … x8 false
+ | x4 ⇒ pair … x9 false | x5 ⇒ pair … xA false | x6 ⇒ pair … xB false | x7 ⇒ pair … xC false
+ | x8 ⇒ pair … xD false | x9 ⇒ pair … xE false | xA ⇒ pair … xF false | xB ⇒ pair … x0 true
+ | xC ⇒ pair … x1 true | xD ⇒ pair … x2 true | xE ⇒ pair … x3 true | xF ⇒ pair … x4 true ]
+ | x6 ⇒ match e2 with
+ [ x0 ⇒ pair … x6 false | x1 ⇒ pair … x7 false | x2 ⇒ pair … x8 false | x3 ⇒ pair … x9 false
+ | x4 ⇒ pair … xA false | x5 ⇒ pair … xB false | x6 ⇒ pair … xC false | x7 ⇒ pair … xD false
+ | x8 ⇒ pair … xE false | x9 ⇒ pair … xF false | xA ⇒ pair … x0 true | xB ⇒ pair … x1 true
+ | xC ⇒ pair … x2 true | xD ⇒ pair … x3 true | xE ⇒ pair … x4 true | xF ⇒ pair … x5 true ]
+ | x7 ⇒ match e2 with
+ [ x0 ⇒ pair … x7 false | x1 ⇒ pair … x8 false | x2 ⇒ pair … x9 false | x3 ⇒ pair … xA false
+ | x4 ⇒ pair … xB false | x5 ⇒ pair … xC false | x6 ⇒ pair … xD false | x7 ⇒ pair … xE false
+ | x8 ⇒ pair … xF false | x9 ⇒ pair … x0 true | xA ⇒ pair … x1 true | xB ⇒ pair … x2 true
+ | xC ⇒ pair … x3 true | xD ⇒ pair … x4 true | xE ⇒ pair … x5 true | xF ⇒ pair … x6 true ]
+ | x8 ⇒ match e2 with
+ [ x0 ⇒ pair … x8 false | x1 ⇒ pair … x9 false | x2 ⇒ pair … xA false | x3 ⇒ pair … xB false
+ | x4 ⇒ pair … xC false | x5 ⇒ pair … xD false | x6 ⇒ pair … xE false | x7 ⇒ pair … xF false
+ | x8 ⇒ pair … x0 true | x9 ⇒ pair … x1 true | xA ⇒ pair … x2 true | xB ⇒ pair … x3 true
+ | xC ⇒ pair … x4 true | xD ⇒ pair … x5 true | xE ⇒ pair … x6 true | xF ⇒ pair … x7 true ]
+ | x9 ⇒ match e2 with
+ [ x0 ⇒ pair … x9 false | x1 ⇒ pair … xA false | x2 ⇒ pair … xB false | x3 ⇒ pair … xC false
+ | x4 ⇒ pair … xD false | x5 ⇒ pair … xE false | x6 ⇒ pair … xF false | x7 ⇒ pair … x0 true
+ | x8 ⇒ pair … x1 true | x9 ⇒ pair … x2 true | xA ⇒ pair … x3 true | xB ⇒ pair … x4 true
+ | xC ⇒ pair … x5 true | xD ⇒ pair … x6 true | xE ⇒ pair … x7 true | xF ⇒ pair … x8 true ]
+ | xA ⇒ match e2 with
+ [ x0 ⇒ pair … xA false | x1 ⇒ pair … xB false | x2 ⇒ pair … xC false | x3 ⇒ pair … xD false
+ | x4 ⇒ pair … xE false | x5 ⇒ pair … xF false | x6 ⇒ pair … x0 true | x7 ⇒ pair … x1 true
+ | x8 ⇒ pair … x2 true | x9 ⇒ pair … x3 true | xA ⇒ pair … x4 true | xB ⇒ pair … x5 true
+ | xC ⇒ pair … x6 true | xD ⇒ pair … x7 true | xE ⇒ pair … x8 true | xF ⇒ pair … x9 true ]
+ | xB ⇒ match e2 with
+ [ x0 ⇒ pair … xB false | x1 ⇒ pair … xC false | x2 ⇒ pair … xD false | x3 ⇒ pair … xE false
+ | x4 ⇒ pair … xF false | x5 ⇒ pair … x0 true | x6 ⇒ pair … x1 true | x7 ⇒ pair … x2 true
+ | x8 ⇒ pair … x3 true | x9 ⇒ pair … x4 true | xA ⇒ pair … x5 true | xB ⇒ pair … x6 true
+ | xC ⇒ pair … x7 true | xD ⇒ pair … x8 true | xE ⇒ pair … x9 true | xF ⇒ pair … xA true ]
+ | xC ⇒ match e2 with
+ [ x0 ⇒ pair … xC false | x1 ⇒ pair … xD false | x2 ⇒ pair … xE false | x3 ⇒ pair … xF false
+ | x4 ⇒ pair … x0 true | x5 ⇒ pair … x1 true | x6 ⇒ pair … x2 true | x7 ⇒ pair … x3 true
+ | x8 ⇒ pair … x4 true | x9 ⇒ pair … x5 true | xA ⇒ pair … x6 true | xB ⇒ pair … x7 true
+ | xC ⇒ pair … x8 true | xD ⇒ pair … x9 true | xE ⇒ pair … xA true | xF ⇒ pair … xB true ]
+ | xD ⇒ match e2 with
+ [ x0 ⇒ pair … xD false | x1 ⇒ pair … xE false | x2 ⇒ pair … xF false | x3 ⇒ pair … x0 true
+ | x4 ⇒ pair … x1 true | x5 ⇒ pair … x2 true | x6 ⇒ pair … x3 true | x7 ⇒ pair … x4 true
+ | x8 ⇒ pair … x5 true | x9 ⇒ pair … x6 true | xA ⇒ pair … x7 true | xB ⇒ pair … x8 true
+ | xC ⇒ pair … x9 true | xD ⇒ pair … xA true | xE ⇒ pair … xB true | xF ⇒ pair … xC true ]
+ | xE ⇒ match e2 with
+ [ x0 ⇒ pair … xE false | x1 ⇒ pair … xF false | x2 ⇒ pair … x0 true | x3 ⇒ pair … x1 true
+ | x4 ⇒ pair … x2 true | x5 ⇒ pair … x3 true | x6 ⇒ pair … x4 true | x7 ⇒ pair … x5 true
+ | x8 ⇒ pair … x6 true | x9 ⇒ pair … x7 true | xA ⇒ pair … x8 true | xB ⇒ pair … x9 true
+ | xC ⇒ pair … xA true | xD ⇒ pair … xB true | xE ⇒ pair … xC true | xF ⇒ pair … xD true ]
+ | xF ⇒ match e2 with
+ [ x0 ⇒ pair … xF false | x1 ⇒ pair … x0 true | x2 ⇒ pair … x1 true | x3 ⇒ pair … x2 true
+ | x4 ⇒ pair … x3 true | x5 ⇒ pair … x4 true | x6 ⇒ pair … x5 true | x7 ⇒ pair … x6 true
+ | x8 ⇒ pair … x7 true | x9 ⇒ pair … x8 true | xA ⇒ pair … x9 true | xB ⇒ pair … xA true
+ | xC ⇒ pair … xB true | xD ⇒ pair … xC true | xE ⇒ pair … xD true | xF ⇒ pair … xE true ]
+ ].
+
+(* operatore somma con data+carry → data *)
+ndefinition plus_ex_dc_d ≝
+λe1,e2:exadecim.λc:bool.
+ match c with
+ [ true ⇒ match e1 with
+ [ x0 ⇒ match e2 with
+ [ x0 ⇒ x1 | x1 ⇒ x2 | x2 ⇒ x3 | x3 ⇒ x4 | x4 ⇒ x5 | x5 ⇒ x6 | x6 ⇒ x7 | x7 ⇒ x8
+ | x8 ⇒ x9 | x9 ⇒ xA | xA ⇒ xB | xB ⇒ xC | xC ⇒ xD | xD ⇒ xE | xE ⇒ xF | xF ⇒ x0 ]
+ | x1 ⇒ match e2 with
+ [ x0 ⇒ x2 | x1 ⇒ x3 | x2 ⇒ x4 | x3 ⇒ x5 | x4 ⇒ x6 | x5 ⇒ x7 | x6 ⇒ x8 | x7 ⇒ x9
+ | x8 ⇒ xA | x9 ⇒ xB | xA ⇒ xC | xB ⇒ xD | xC ⇒ xE | xD ⇒ xF | xE ⇒ x0 | xF ⇒ x1 ]
+ | x2 ⇒ match e2 with
+ [ x0 ⇒ x3 | x1 ⇒ x4 | x2 ⇒ x5 | x3 ⇒ x6 | x4 ⇒ x7 | x5 ⇒ x8 | x6 ⇒ x9 | x7 ⇒ xA
+ | x8 ⇒ xB | x9 ⇒ xC | xA ⇒ xD | xB ⇒ xE | xC ⇒ xF | xD ⇒ x0 | xE ⇒ x1 | xF ⇒ x2 ]
+ | x3 ⇒ match e2 with
+ [ x0 ⇒ x4 | x1 ⇒ x5 | x2 ⇒ x6 | x3 ⇒ x7 | x4 ⇒ x8 | x5 ⇒ x9 | x6 ⇒ xA | x7 ⇒ xB
+ | x8 ⇒ xC | x9 ⇒ xD | xA ⇒ xE | xB ⇒ xF | xC ⇒ x0 | xD ⇒ x1 | xE ⇒ x2 | xF ⇒ x3 ]
+ | x4 ⇒ match e2 with
+ [ x0 ⇒ x5 | x1 ⇒ x6 | x2 ⇒ x7 | x3 ⇒ x8 | x4 ⇒ x9 | x5 ⇒ xA | x6 ⇒ xB | x7 ⇒ xC
+ | x8 ⇒ xD | x9 ⇒ xE | xA ⇒ xF | xB ⇒ x0 | xC ⇒ x1 | xD ⇒ x2 | xE ⇒ x3 | xF ⇒ x4 ]
+ | x5 ⇒ match e2 with
+ [ x0 ⇒ x6 | x1 ⇒ x7 | x2 ⇒ x8 | x3 ⇒ x9 | x4 ⇒ xA | x5 ⇒ xB | x6 ⇒ xC | x7 ⇒ xD
+ | x8 ⇒ xE | x9 ⇒ xF | xA ⇒ x0 | xB ⇒ x1 | xC ⇒ x2 | xD ⇒ x3 | xE ⇒ x4 | xF ⇒ x5 ]
+ | x6 ⇒ match e2 with
+ [ x0 ⇒ x7 | x1 ⇒ x8 | x2 ⇒ x9 | x3 ⇒ xA | x4 ⇒ xB | x5 ⇒ xC | x6 ⇒ xD | x7 ⇒ xE
+ | x8 ⇒ xF | x9 ⇒ x0 | xA ⇒ x1 | xB ⇒ x2 | xC ⇒ x3 | xD ⇒ x4 | xE ⇒ x5 | xF ⇒ x6 ]
+ | x7 ⇒ match e2 with
+ [ x0 ⇒ x8 | x1 ⇒ x9 | x2 ⇒ xA | x3 ⇒ xB | x4 ⇒ xC | x5 ⇒ xD | x6 ⇒ xE | x7 ⇒ xF
+ | x8 ⇒ x0 | x9 ⇒ x1 | xA ⇒ x2 | xB ⇒ x3 | xC ⇒ x4 | xD ⇒ x5 | xE ⇒ x6 | xF ⇒ x7 ]
+ | x8 ⇒ match e2 with
+ [ x0 ⇒ x9 | x1 ⇒ xA | x2 ⇒ xB | x3 ⇒ xC | x4 ⇒ xD | x5 ⇒ xE | x6 ⇒ xF | x7 ⇒ x0
+ | x8 ⇒ x1 | x9 ⇒ x2 | xA ⇒ x3 | xB ⇒ x4 | xC ⇒ x5 | xD ⇒ x6 | xE ⇒ x7 | xF ⇒ x8 ]
+ | x9 ⇒ match e2 with
+ [ x0 ⇒ xA | x1 ⇒ xB | x2 ⇒ xC | x3 ⇒ xD | x4 ⇒ xE | x5 ⇒ xF | x6 ⇒ x0 | x7 ⇒ x1
+ | x8 ⇒ x2 | x9 ⇒ x3 | xA ⇒ x4 | xB ⇒ x5 | xC ⇒ x6 | xD ⇒ x7 | xE ⇒ x8 | xF ⇒ x9 ]
+ | xA ⇒ match e2 with
+ [ x0 ⇒ xB | x1 ⇒ xC | x2 ⇒ xD | x3 ⇒ xE | x4 ⇒ xF | x5 ⇒ x0 | x6 ⇒ x1 | x7 ⇒ x2
+ | x8 ⇒ x3 | x9 ⇒ x4 | xA ⇒ x5 | xB ⇒ x6 | xC ⇒ x7 | xD ⇒ x8 | xE ⇒ x9 | xF ⇒ xA ]
+ | xB ⇒ match e2 with
+ [ x0 ⇒ xC | x1 ⇒ xD | x2 ⇒ xE | x3 ⇒ xF | x4 ⇒ x0 | x5 ⇒ x1 | x6 ⇒ x2 | x7 ⇒ x3
+ | x8 ⇒ x4 | x9 ⇒ x5 | xA ⇒ x6 | xB ⇒ x7 | xC ⇒ x8 | xD ⇒ x9 | xE ⇒ xA | xF ⇒ xB ]
+ | xC ⇒ match e2 with
+ [ x0 ⇒ xD | x1 ⇒ xE | x2 ⇒ xF | x3 ⇒ x0 | x4 ⇒ x1 | x5 ⇒ x2 | x6 ⇒ x3 | x7 ⇒ x4
+ | x8 ⇒ x5 | x9 ⇒ x6 | xA ⇒ x7 | xB ⇒ x8 | xC ⇒ x9 | xD ⇒ xA | xE ⇒ xB | xF ⇒ xC ]
+ | xD ⇒ match e2 with
+ [ x0 ⇒ xE | x1 ⇒ xF | x2 ⇒ x0 | x3 ⇒ x1 | x4 ⇒ x2 | x5 ⇒ x3 | x6 ⇒ x4 | x7 ⇒ x5
+ | x8 ⇒ x6 | x9 ⇒ x7 | xA ⇒ x8 | xB ⇒ x9 | xC ⇒ xA | xD ⇒ xB | xE ⇒ xC | xF ⇒ xD ]
+ | xE ⇒ match e2 with
+ [ x0 ⇒ xF | x1 ⇒ x0 | x2 ⇒ x1 | x3 ⇒ x2 | x4 ⇒ x3 | x5 ⇒ x4 | x6 ⇒ x5 | x7 ⇒ x6
+ | x8 ⇒ x7 | x9 ⇒ x8 | xA ⇒ x9 | xB ⇒ xA | xC ⇒ xB | xD ⇒ xC | xE ⇒ xD | xF ⇒ xE ]
+ | xF ⇒ match e2 with
+ [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3 | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x6 | x7 ⇒ x7
+ | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ xA | xB ⇒ xB | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ]
+ ]
+ | false ⇒ match e1 with
+ [ x0 ⇒ match e2 with
+ [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3 | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x6 | x7 ⇒ x7
+ | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ xA | xB ⇒ xB | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ]
+ | x1 ⇒ match e2 with
+ [ x0 ⇒ x1 | x1 ⇒ x2 | x2 ⇒ x3 | x3 ⇒ x4 | x4 ⇒ x5 | x5 ⇒ x6 | x6 ⇒ x7 | x7 ⇒ x8
+ | x8 ⇒ x9 | x9 ⇒ xA | xA ⇒ xB | xB ⇒ xC | xC ⇒ xD | xD ⇒ xE | xE ⇒ xF | xF ⇒ x0 ]
+ | x2 ⇒ match e2 with
+ [ x0 ⇒ x2 | x1 ⇒ x3 | x2 ⇒ x4 | x3 ⇒ x5 | x4 ⇒ x6 | x5 ⇒ x7 | x6 ⇒ x8 | x7 ⇒ x9
+ | x8 ⇒ xA | x9 ⇒ xB | xA ⇒ xC | xB ⇒ xD | xC ⇒ xE | xD ⇒ xF | xE ⇒ x0 | xF ⇒ x1 ]
+ | x3 ⇒ match e2 with
+ [ x0 ⇒ x3 | x1 ⇒ x4 | x2 ⇒ x5 | x3 ⇒ x6 | x4 ⇒ x7 | x5 ⇒ x8 | x6 ⇒ x9 | x7 ⇒ xA
+ | x8 ⇒ xB | x9 ⇒ xC | xA ⇒ xD | xB ⇒ xE | xC ⇒ xF | xD ⇒ x0 | xE ⇒ x1 | xF ⇒ x2 ]
+ | x4 ⇒ match e2 with
+ [ x0 ⇒ x4 | x1 ⇒ x5 | x2 ⇒ x6 | x3 ⇒ x7 | x4 ⇒ x8 | x5 ⇒ x9 | x6 ⇒ xA | x7 ⇒ xB
+ | x8 ⇒ xC | x9 ⇒ xD | xA ⇒ xE | xB ⇒ xF | xC ⇒ x0 | xD ⇒ x1 | xE ⇒ x2 | xF ⇒ x3 ]
+ | x5 ⇒ match e2 with
+ [ x0 ⇒ x5 | x1 ⇒ x6 | x2 ⇒ x7 | x3 ⇒ x8 | x4 ⇒ x9 | x5 ⇒ xA | x6 ⇒ xB | x7 ⇒ xC
+ | x8 ⇒ xD | x9 ⇒ xE | xA ⇒ xF | xB ⇒ x0 | xC ⇒ x1 | xD ⇒ x2 | xE ⇒ x3 | xF ⇒ x4 ]
+ | x6 ⇒ match e2 with
+ [ x0 ⇒ x6 | x1 ⇒ x7 | x2 ⇒ x8 | x3 ⇒ x9 | x4 ⇒ xA | x5 ⇒ xB | x6 ⇒ xC | x7 ⇒ xD
+ | x8 ⇒ xE | x9 ⇒ xF | xA ⇒ x0 | xB ⇒ x1 | xC ⇒ x2 | xD ⇒ x3 | xE ⇒ x4 | xF ⇒ x5 ]
+ | x7 ⇒ match e2 with
+ [ x0 ⇒ x7 | x1 ⇒ x8 | x2 ⇒ x9 | x3 ⇒ xA | x4 ⇒ xB | x5 ⇒ xC | x6 ⇒ xD | x7 ⇒ xE
+ | x8 ⇒ xF | x9 ⇒ x0 | xA ⇒ x1 | xB ⇒ x2 | xC ⇒ x3 | xD ⇒ x4 | xE ⇒ x5 | xF ⇒ x6 ]
+ | x8 ⇒ match e2 with
+ [ x0 ⇒ x8 | x1 ⇒ x9 | x2 ⇒ xA | x3 ⇒ xB | x4 ⇒ xC | x5 ⇒ xD | x6 ⇒ xE | x7 ⇒ xF
+ | x8 ⇒ x0 | x9 ⇒ x1 | xA ⇒ x2 | xB ⇒ x3 | xC ⇒ x4 | xD ⇒ x5 | xE ⇒ x6 | xF ⇒ x7 ]
+ | x9 ⇒ match e2 with
+ [ x0 ⇒ x9 | x1 ⇒ xA | x2 ⇒ xB | x3 ⇒ xC | x4 ⇒ xD | x5 ⇒ xE | x6 ⇒ xF | x7 ⇒ x0
+ | x8 ⇒ x1 | x9 ⇒ x2 | xA ⇒ x3 | xB ⇒ x4 | xC ⇒ x5 | xD ⇒ x6 | xE ⇒ x7 | xF ⇒ x8 ]
+ | xA ⇒ match e2 with
+ [ x0 ⇒ xA | x1 ⇒ xB | x2 ⇒ xC | x3 ⇒ xD | x4 ⇒ xE | x5 ⇒ xF | x6 ⇒ x0 | x7 ⇒ x1
+ | x8 ⇒ x2 | x9 ⇒ x3 | xA ⇒ x4 | xB ⇒ x5 | xC ⇒ x6 | xD ⇒ x7 | xE ⇒ x8 | xF ⇒ x9 ]
+ | xB ⇒ match e2 with
+ [ x0 ⇒ xB | x1 ⇒ xC | x2 ⇒ xD | x3 ⇒ xE | x4 ⇒ xF | x5 ⇒ x0 | x6 ⇒ x1 | x7 ⇒ x2
+ | x8 ⇒ x3 | x9 ⇒ x4 | xA ⇒ x5 | xB ⇒ x6 | xC ⇒ x7 | xD ⇒ x8 | xE ⇒ x9 | xF ⇒ xA ]
+ | xC ⇒ match e2 with
+ [ x0 ⇒ xC | x1 ⇒ xD | x2 ⇒ xE | x3 ⇒ xF | x4 ⇒ x0 | x5 ⇒ x1 | x6 ⇒ x2 | x7 ⇒ x3
+ | x8 ⇒ x4 | x9 ⇒ x5 | xA ⇒ x6 | xB ⇒ x7 | xC ⇒ x8 | xD ⇒ x9 | xE ⇒ xA | xF ⇒ xB ]
+ | xD ⇒ match e2 with
+ [ x0 ⇒ xD | x1 ⇒ xE | x2 ⇒ xF | x3 ⇒ x0 | x4 ⇒ x1 | x5 ⇒ x2 | x6 ⇒ x3 | x7 ⇒ x4
+ | x8 ⇒ x5 | x9 ⇒ x6 | xA ⇒ x7 | xB ⇒ x8 | xC ⇒ x9 | xD ⇒ xA | xE ⇒ xB | xF ⇒ xC ]
+ | xE ⇒ match e2 with
+ [ x0 ⇒ xE | x1 ⇒ xF | x2 ⇒ x0 | x3 ⇒ x1 | x4 ⇒ x2 | x5 ⇒ x3 | x6 ⇒ x4 | x7 ⇒ x5
+ | x8 ⇒ x6 | x9 ⇒ x7 | xA ⇒ x8 | xB ⇒ x9 | xC ⇒ xA | xD ⇒ xB | xE ⇒ xC | xF ⇒ xD ]
+ | xF ⇒ match e2 with
+ [ x0 ⇒ xF | x1 ⇒ x0 | x2 ⇒ x1 | x3 ⇒ x2 | x4 ⇒ x3 | x5 ⇒ x4 | x6 ⇒ x5 | x7 ⇒ x6
+ | x8 ⇒ x7 | x9 ⇒ x8 | xA ⇒ x9 | xB ⇒ xA | xC ⇒ xB | xD ⇒ xC | xE ⇒ xD | xF ⇒ xE ]
+ ]].
+
+(* operatore somma con data → data *)
+ndefinition plus_ex_d_d ≝
+λe1,e2:exadecim.
+ match e1 with
+ [ x0 ⇒ match e2 with
+ [ x0 ⇒ x0 | x1 ⇒ x1 | x2 ⇒ x2 | x3 ⇒ x3 | x4 ⇒ x4 | x5 ⇒ x5 | x6 ⇒ x6 | x7 ⇒ x7
+ | x8 ⇒ x8 | x9 ⇒ x9 | xA ⇒ xA | xB ⇒ xB | xC ⇒ xC | xD ⇒ xD | xE ⇒ xE | xF ⇒ xF ]
+ | x1 ⇒ match e2 with
+ [ x0 ⇒ x1 | x1 ⇒ x2 | x2 ⇒ x3 | x3 ⇒ x4 | x4 ⇒ x5 | x5 ⇒ x6 | x6 ⇒ x7 | x7 ⇒ x8
+ | x8 ⇒ x9 | x9 ⇒ xA | xA ⇒ xB | xB ⇒ xC | xC ⇒ xD | xD ⇒ xE | xE ⇒ xF | xF ⇒ x0 ]
+ | x2 ⇒ match e2 with
+ [ x0 ⇒ x2 | x1 ⇒ x3 | x2 ⇒ x4 | x3 ⇒ x5 | x4 ⇒ x6 | x5 ⇒ x7 | x6 ⇒ x8 | x7 ⇒ x9
+ | x8 ⇒ xA | x9 ⇒ xB | xA ⇒ xC | xB ⇒ xD | xC ⇒ xE | xD ⇒ xF | xE ⇒ x0 | xF ⇒ x1 ]
+ | x3 ⇒ match e2 with
+ [ x0 ⇒ x3 | x1 ⇒ x4 | x2 ⇒ x5 | x3 ⇒ x6 | x4 ⇒ x7 | x5 ⇒ x8 | x6 ⇒ x9 | x7 ⇒ xA
+ | x8 ⇒ xB | x9 ⇒ xC | xA ⇒ xD | xB ⇒ xE | xC ⇒ xF | xD ⇒ x0 | xE ⇒ x1 | xF ⇒ x2 ]
+ | x4 ⇒ match e2 with
+ [ x0 ⇒ x4 | x1 ⇒ x5 | x2 ⇒ x6 | x3 ⇒ x7 | x4 ⇒ x8 | x5 ⇒ x9 | x6 ⇒ xA | x7 ⇒ xB
+ | x8 ⇒ xC | x9 ⇒ xD | xA ⇒ xE | xB ⇒ xF | xC ⇒ x0 | xD ⇒ x1 | xE ⇒ x2 | xF ⇒ x3 ]
+ | x5 ⇒ match e2 with
+ [ x0 ⇒ x5 | x1 ⇒ x6 | x2 ⇒ x7 | x3 ⇒ x8 | x4 ⇒ x9 | x5 ⇒ xA | x6 ⇒ xB | x7 ⇒ xC
+ | x8 ⇒ xD | x9 ⇒ xE | xA ⇒ xF | xB ⇒ x0 | xC ⇒ x1 | xD ⇒ x2 | xE ⇒ x3 | xF ⇒ x4 ]
+ | x6 ⇒ match e2 with
+ [ x0 ⇒ x6 | x1 ⇒ x7 | x2 ⇒ x8 | x3 ⇒ x9 | x4 ⇒ xA | x5 ⇒ xB | x6 ⇒ xC | x7 ⇒ xD
+ | x8 ⇒ xE | x9 ⇒ xF | xA ⇒ x0 | xB ⇒ x1 | xC ⇒ x2 | xD ⇒ x3 | xE ⇒ x4 | xF ⇒ x5 ]
+ | x7 ⇒ match e2 with
+ [ x0 ⇒ x7 | x1 ⇒ x8 | x2 ⇒ x9 | x3 ⇒ xA | x4 ⇒ xB | x5 ⇒ xC | x6 ⇒ xD | x7 ⇒ xE
+ | x8 ⇒ xF | x9 ⇒ x0 | xA ⇒ x1 | xB ⇒ x2 | xC ⇒ x3 | xD ⇒ x4 | xE ⇒ x5 | xF ⇒ x6 ]
+ | x8 ⇒ match e2 with
+ [ x0 ⇒ x8 | x1 ⇒ x9 | x2 ⇒ xA | x3 ⇒ xB | x4 ⇒ xC | x5 ⇒ xD | x6 ⇒ xE | x7 ⇒ xF
+ | x8 ⇒ x0 | x9 ⇒ x1 | xA ⇒ x2 | xB ⇒ x3 | xC ⇒ x4 | xD ⇒ x5 | xE ⇒ x6 | xF ⇒ x7 ]
+ | x9 ⇒ match e2 with
+ [ x0 ⇒ x9 | x1 ⇒ xA | x2 ⇒ xB | x3 ⇒ xC | x4 ⇒ xD | x5 ⇒ xE | x6 ⇒ xF | x7 ⇒ x0
+ | x8 ⇒ x1 | x9 ⇒ x2 | xA ⇒ x3 | xB ⇒ x4 | xC ⇒ x5 | xD ⇒ x6 | xE ⇒ x7 | xF ⇒ x8 ]
+ | xA ⇒ match e2 with
+ [ x0 ⇒ xA | x1 ⇒ xB | x2 ⇒ xC | x3 ⇒ xD | x4 ⇒ xE | x5 ⇒ xF | x6 ⇒ x0 | x7 ⇒ x1
+ | x8 ⇒ x2 | x9 ⇒ x3 | xA ⇒ x4 | xB ⇒ x5 | xC ⇒ x6 | xD ⇒ x7 | xE ⇒ x8 | xF ⇒ x9 ]
+ | xB ⇒ match e2 with
+ [ x0 ⇒ xB | x1 ⇒ xC | x2 ⇒ xD | x3 ⇒ xE | x4 ⇒ xF | x5 ⇒ x0 | x6 ⇒ x1 | x7 ⇒ x2
+ | x8 ⇒ x3 | x9 ⇒ x4 | xA ⇒ x5 | xB ⇒ x6 | xC ⇒ x7 | xD ⇒ x8 | xE ⇒ x9 | xF ⇒ xA ]
+ | xC ⇒ match e2 with
+ [ x0 ⇒ xC | x1 ⇒ xD | x2 ⇒ xE | x3 ⇒ xF | x4 ⇒ x0 | x5 ⇒ x1 | x6 ⇒ x2 | x7 ⇒ x3
+ | x8 ⇒ x4 | x9 ⇒ x5 | xA ⇒ x6 | xB ⇒ x7 | xC ⇒ x8 | xD ⇒ x9 | xE ⇒ xA | xF ⇒ xB ]
+ | xD ⇒ match e2 with
+ [ x0 ⇒ xD | x1 ⇒ xE | x2 ⇒ xF | x3 ⇒ x0 | x4 ⇒ x1 | x5 ⇒ x2 | x6 ⇒ x3 | x7 ⇒ x4
+ | x8 ⇒ x5 | x9 ⇒ x6 | xA ⇒ x7 | xB ⇒ x8 | xC ⇒ x9 | xD ⇒ xA | xE ⇒ xB | xF ⇒ xC ]
+ | xE ⇒ match e2 with
+ [ x0 ⇒ xE | x1 ⇒ xF | x2 ⇒ x0 | x3 ⇒ x1 | x4 ⇒ x2 | x5 ⇒ x3 | x6 ⇒ x4 | x7 ⇒ x5
+ | x8 ⇒ x6 | x9 ⇒ x7 | xA ⇒ x8 | xB ⇒ x9 | xC ⇒ xA | xD ⇒ xB | xE ⇒ xC | xF ⇒ xD ]
+ | xF ⇒ match e2 with
+ [ x0 ⇒ xF | x1 ⇒ x0 | x2 ⇒ x1 | x3 ⇒ x2 | x4 ⇒ x3 | x5 ⇒ x4 | x6 ⇒ x5 | x7 ⇒ x6
+ | x8 ⇒ x7 | x9 ⇒ x8 | xA ⇒ x9 | xB ⇒ xA | xC ⇒ xB | xD ⇒ xC | xE ⇒ xD | xF ⇒ xE ]
+ ].
+
+(* operatore somma con data+carry → carry *)
+ndefinition plus_ex_dc_c ≝
+λe1,e2:exadecim.λc:bool.
+ match c with
+ [ true ⇒ match e1 with
+ [ x0 ⇒ match e2 with
+ [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+ | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ true ]
+ | x1 ⇒ match e2 with
+ [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+ | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ false | xD ⇒ false | xE ⇒ true | xF ⇒ true ]
+ | x2 ⇒ match e2 with
+ [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+ | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ false | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
+ | x3 ⇒ match e2 with
+ [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+ | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
+ | x4 ⇒ match e2 with
+ [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+ | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
+ | x5 ⇒ match e2 with
+ [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+ | x8 ⇒ false | x9 ⇒ false | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
+ | x6 ⇒ match e2 with
+ [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+ | x8 ⇒ false | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
+ | x7 ⇒ match e2 with
+ [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+ | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
+ | x8 ⇒ match e2 with
+ [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ true
+ | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
+ | x9 ⇒ match e2 with
+ [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ true | x7 ⇒ true
+ | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
+ | xA ⇒ match e2 with
+ [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
+ | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
+ | xB ⇒ match e2 with
+ [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
+ | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
+ | xC ⇒ match e2 with
+ [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ true | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
+ | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
+ | xD ⇒ match e2 with
+ [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ true | x3 ⇒ true | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
+ | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
+ | xE ⇒ match e2 with
+ [ x0 ⇒ false | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
+ | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
+ | xF ⇒ match e2 with
+ [ x0 ⇒ true | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
+ | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
+ ]
+ | false ⇒ match e1 with
+ [ x0 ⇒ match e2 with
+ [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+ | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
+ | x1 ⇒ match e2 with
+ [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+ | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ true ]
+ | x2 ⇒ match e2 with
+ [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+ | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ false | xD ⇒ false | xE ⇒ true | xF ⇒ true ]
+ | x3 ⇒ match e2 with
+ [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+ | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ false | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
+ | x4 ⇒ match e2 with
+ [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+ | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
+ | x5 ⇒ match e2 with
+ [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+ | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
+ | x6 ⇒ match e2 with
+ [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+ | x8 ⇒ false | x9 ⇒ false | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
+ | x7 ⇒ match e2 with
+ [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+ | x8 ⇒ false | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
+ | x8 ⇒ match e2 with
+ [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+ | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
+ | x9 ⇒ match e2 with
+ [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ true
+ | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
+ | xA ⇒ match e2 with
+ [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ true | x7 ⇒ true
+ | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
+ | xB ⇒ match e2 with
+ [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
+ | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
+ | xC ⇒ match e2 with
+ [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
+ | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
+ | xD ⇒ match e2 with
+ [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ true | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
+ | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
+ | xE ⇒ match e2 with
+ [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ true | x3 ⇒ true | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
+ | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
+ | xF ⇒ match e2 with
+ [ x0 ⇒ false | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
+ | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
+ ]].
+
+(* operatore somma con data → carry *)
+ndefinition plus_ex_d_c ≝
+λe1,e2:exadecim.
+ match e1 with
+ [ x0 ⇒ match e2 with
+ [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+ | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ false ]
+ | x1 ⇒ match e2 with
+ [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+ | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ false | xD ⇒ false | xE ⇒ false | xF ⇒ true ]
+ | x2 ⇒ match e2 with
+ [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+ | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ false | xD ⇒ false | xE ⇒ true | xF ⇒ true ]
+ | x3 ⇒ match e2 with
+ [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+ | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ false | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
+ | x4 ⇒ match e2 with
+ [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+ | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ false | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
+ | x5 ⇒ match e2 with
+ [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+ | x8 ⇒ false | x9 ⇒ false | xA ⇒ false | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
+ | x6 ⇒ match e2 with
+ [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+ | x8 ⇒ false | x9 ⇒ false | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
+ | x7 ⇒ match e2 with
+ [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+ | x8 ⇒ false | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
+ | x8 ⇒ match e2 with
+ [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+ | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
+ | x9 ⇒ match e2 with
+ [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ true
+ | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
+ | xA ⇒ match e2 with
+ [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ false | x6 ⇒ true | x7 ⇒ true
+ | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
+ | xB ⇒ match e2 with
+ [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ false | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
+ | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
+ | xC ⇒ match e2 with
+ [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
+ | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
+ | xD ⇒ match e2 with
+ [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ true | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
+ | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
+ | xE ⇒ match e2 with
+ [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ true | x3 ⇒ true | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
+ | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
+ | xF ⇒ match e2 with
+ [ x0 ⇒ false | x1 ⇒ true | x2 ⇒ true | x3 ⇒ true | x4 ⇒ true | x5 ⇒ true | x6 ⇒ true | x7 ⇒ true
+ | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ]
+ ].
+
+(* operatore Most Significant Bit *)
+ndefinition MSB_ex ≝
+λe:exadecim.match e with
+ [ x0 ⇒ false | x1 ⇒ false | x2 ⇒ false | x3 ⇒ false
+ | x4 ⇒ false | x5 ⇒ false | x6 ⇒ false | x7 ⇒ false
+ | x8 ⇒ true | x9 ⇒ true | xA ⇒ true | xB ⇒ true
+ | xC ⇒ true | xD ⇒ true | xE ⇒ true | xF ⇒ true ].
+
+(* operatore predecessore *)
+ndefinition pred_ex ≝
+λe:exadecim.
+ match e with
+ [ x0 ⇒ xF | x1 ⇒ x0 | x2 ⇒ x1 | x3 ⇒ x2 | x4 ⇒ x3 | x5 ⇒ x4 | x6 ⇒ x5 | x7 ⇒ x6
+ | x8 ⇒ x7 | x9 ⇒ x8 | xA ⇒ x9 | xB ⇒ xA | xC ⇒ xB | xD ⇒ xC | xE ⇒ xD | xF ⇒ xE ].
+
+(* operatore successore *)
+ndefinition succ_ex ≝
+λe:exadecim.
+ match e with
+ [ x0 ⇒ x1 | x1 ⇒ x2 | x2 ⇒ x3 | x3 ⇒ x4 | x4 ⇒ x5 | x5 ⇒ x6 | x6 ⇒ x7 | x7 ⇒ x8
+ | x8 ⇒ x9 | x9 ⇒ xA | xA ⇒ xB | xB ⇒ xC | xC ⇒ xD | xD ⇒ xE | xE ⇒ xF | xF ⇒ x0 ].
+
+(* operatore neg/complemento a 2 *)
+ndefinition compl_ex ≝
+λe:exadecim.match e with
+ [ x0 ⇒ x0 | x1 ⇒ xF | x2 ⇒ xE | x3 ⇒ xD
+ | x4 ⇒ xC | x5 ⇒ xB | x6 ⇒ xA | x7 ⇒ x9
+ | x8 ⇒ x8 | x9 ⇒ x7 | xA ⇒ x6 | xB ⇒ x5
+ | xC ⇒ x4 | xD ⇒ x3 | xE ⇒ x2 | xF ⇒ x1 ].
+
+(* iteratore sugli esadecimali *)
+ndefinition forall_ex ≝ λP.
+ P x0 ⊗ P x1 ⊗ P x2 ⊗ P x3 ⊗ P x4 ⊗ P x5 ⊗ P x6 ⊗ P x7 ⊗
+ P x8 ⊗ P x9 ⊗ P xA ⊗ P xB ⊗ P xC ⊗ P xD ⊗ P xE ⊗ P xF.
+
+(* esadecimali ricorsivi *)
+ninductive rec_exadecim : exadecim → Type ≝
+ ex_O : rec_exadecim x0
+| ex_S : ∀n.rec_exadecim n → rec_exadecim (succ_ex n).
+
+(* esadecimali → esadecimali ricorsivi *)
+ndefinition ex_to_recex ≝
+λn.match n return λx.rec_exadecim x with
+ [ x0 ⇒ ex_O
+ | x1 ⇒ ex_S ? ex_O
+ | x2 ⇒ ex_S ? (ex_S ? ex_O)
+ | x3 ⇒ ex_S ? (ex_S ? (ex_S ? ex_O))
+ | x4 ⇒ ex_S ? (ex_S ? (ex_S ? (ex_S ? ex_O)))
+ | x5 ⇒ ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? ex_O))))
+ | x6 ⇒ ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? ex_O)))))
+ | x7 ⇒ ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? ex_O))))))
+ | x8 ⇒ ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? ex_O)))))))
+ | x9 ⇒ ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? ex_O))))))))
+ | xA ⇒ ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? ex_O)))))))))
+ | xB ⇒ ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? ex_O))))))))))
+ | xC ⇒ ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? ex_O)))))))))))
+ | xD ⇒ ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? ex_O))))))))))))
+ | xE ⇒ ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? ex_O)))))))))))))
+ | xF ⇒ ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? (ex_S ? ex_O))))))))))))))
+ ].
+
+(* quaternari → esadecimali *)
+ndefinition ex_of_qu ≝
+λn.match n with
+ [ q0 ⇒ x0 | q1 ⇒ x1 | q2 ⇒ x2 | q3 ⇒ x3 ].
+
+(* ottali → esadecimali *)
+ndefinition ex_of_oct ≝
+λn.match n with
+ [ o0 ⇒ x0 | o1 ⇒ x1 | o2 ⇒ x2 | o3 ⇒ x3 | o4 ⇒ x4 | o5 ⇒ x5 | o6 ⇒ x6 | o7 ⇒ x7 ].
--- /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 *)
+(* Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* *)
+(* ********************************************************************** *)
+
+include "num/exadecim.ma".
+include "num/bool_lemmas.ma".
+
+(* *********** *)
+(* ESADECIMALI *)
+(* *********** *)
+
+ndefinition exadecim_destruct1 : Πe2.ΠP:Prop.ΠH:x0 = e2.match e2 with [ x0 ⇒ P → P | _ ⇒ P ].
+ #e2; #P; ncases e2; nnormalize; #H;
+ ##[ ##1: napply (λx:P.x)
+ ##| ##*: napply False_ind;
+ nchange with (match x0 with [ x0 ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition exadecim_destruct2 : Πe2.ΠP:Prop.ΠH:x1 = e2.match e2 with [ x1 ⇒ P → P | _ ⇒ P ].
+ #e2; #P; ncases e2; nnormalize; #H;
+ ##[ ##2: napply (λx:P.x)
+ ##| ##*: napply False_ind;
+ nchange with (match x1 with [ x1 ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition exadecim_destruct3 : Πe2.ΠP:Prop.ΠH:x2 = e2.match e2 with [ x2 ⇒ P → P | _ ⇒ P ].
+ #e2; #P; ncases e2; nnormalize; #H;
+ ##[ ##3: napply (λx:P.x)
+ ##| ##*: napply False_ind;
+ nchange with (match x2 with [ x2 ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition exadecim_destruct4 : Πe2.ΠP:Prop.ΠH:x3 = e2.match e2 with [ x3 ⇒ P → P | _ ⇒ P ].
+ #e2; #P; ncases e2; nnormalize; #H;
+ ##[ ##4: napply (λx:P.x)
+ ##| ##*: napply False_ind;
+ nchange with (match x3 with [ x3 ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition exadecim_destruct5 : Πe2.ΠP:Prop.ΠH:x4 = e2.match e2 with [ x4 ⇒ P → P | _ ⇒ P ].
+ #e2; #P; ncases e2; nnormalize; #H;
+ ##[ ##5: napply (λx:P.x)
+ ##| ##*: napply False_ind;
+ nchange with (match x4 with [ x4 ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition exadecim_destruct6 : Πe2.ΠP:Prop.ΠH:x5 = e2.match e2 with [ x5 ⇒ P → P | _ ⇒ P ].
+ #e2; #P; ncases e2; nnormalize; #H;
+ ##[ ##6: napply (λx:P.x)
+ ##| ##*: napply False_ind;
+ nchange with (match x5 with [ x5 ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition exadecim_destruct7 : Πe2.ΠP:Prop.ΠH:x6 = e2.match e2 with [ x6 ⇒ P → P | _ ⇒ P ].
+ #e2; #P; ncases e2; nnormalize; #H;
+ ##[ ##7: napply (λx:P.x)
+ ##| ##*: napply False_ind;
+ nchange with (match x6 with [ x6 ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition exadecim_destruct8 : Πe2.ΠP:Prop.ΠH:x7 = e2.match e2 with [ x7 ⇒ P → P | _ ⇒ P ].
+ #e2; #P; ncases e2; nnormalize; #H;
+ ##[ ##8: napply (λx:P.x)
+ ##| ##*: napply False_ind;
+ nchange with (match x7 with [ x7 ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition exadecim_destruct9 : Πe2.ΠP:Prop.ΠH:x8 = e2.match e2 with [ x8 ⇒ P → P | _ ⇒ P ].
+ #e2; #P; ncases e2; nnormalize; #H;
+ ##[ ##9: napply (λx:P.x)
+ ##| ##*: napply False_ind;
+ nchange with (match x8 with [ x8 ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition exadecim_destruct10 : Πe2.ΠP:Prop.ΠH:x9 = e2.match e2 with [ x9 ⇒ P → P | _ ⇒ P ].
+ #e2; #P; ncases e2; nnormalize; #H;
+ ##[ ##10: napply (λx:P.x)
+ ##| ##*: napply False_ind;
+ nchange with (match x9 with [ x9 ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition exadecim_destruct11 : Πe2.ΠP:Prop.ΠH:xA = e2.match e2 with [ xA ⇒ P → P | _ ⇒ P ].
+ #e2; #P; ncases e2; nnormalize; #H;
+ ##[ ##11: napply (λx:P.x)
+ ##| ##*: napply False_ind;
+ nchange with (match xA with [ xA ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition exadecim_destruct12 : Πe2.ΠP:Prop.ΠH:xB = e2.match e2 with [ xB ⇒ P → P | _ ⇒ P ].
+ #e2; #P; ncases e2; nnormalize; #H;
+ ##[ ##12: napply (λx:P.x)
+ ##| ##*: napply False_ind;
+ nchange with (match xB with [ xB ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition exadecim_destruct13 : Πe2.ΠP:Prop.ΠH:xC = e2.match e2 with [ xC ⇒ P → P | _ ⇒ P ].
+ #e2; #P; ncases e2; nnormalize; #H;
+ ##[ ##13: napply (λx:P.x)
+ ##| ##*: napply False_ind;
+ nchange with (match xC with [ xC ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition exadecim_destruct14 : Πe2.ΠP:Prop.ΠH:xD = e2.match e2 with [ xD ⇒ P → P | _ ⇒ P ].
+ #e2; #P; ncases e2; nnormalize; #H;
+ ##[ ##14: napply (λx:P.x)
+ ##| ##*: napply False_ind;
+ nchange with (match xD with [ xD ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition exadecim_destruct15 : Πe2.ΠP:Prop.ΠH:xE = e2.match e2 with [ xE ⇒ P → P | _ ⇒ P ].
+ #e2; #P; ncases e2; nnormalize; #H;
+ ##[ ##15: napply (λx:P.x)
+ ##| ##*: napply False_ind;
+ nchange with (match xE with [ xE ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition exadecim_destruct16 : Πe2.ΠP:Prop.ΠH:xF = e2.match e2 with [ xF ⇒ P → P | _ ⇒ P ].
+ #e2; #P; ncases e2; nnormalize; #H;
+ ##[ ##16: napply (λx:P.x)
+ ##| ##*: napply False_ind;
+ nchange with (match xF with [ xF ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition exadecim_destruct_aux ≝
+Πe1,e2.ΠP:Prop.ΠH:e1 = e2.
+ match e1 with
+ [ x0 ⇒ match e2 with [ x0 ⇒ P → P | _ ⇒ P ]
+ | x1 ⇒ match e2 with [ x1 ⇒ P → P | _ ⇒ P ]
+ | x2 ⇒ match e2 with [ x2 ⇒ P → P | _ ⇒ P ]
+ | x3 ⇒ match e2 with [ x3 ⇒ P → P | _ ⇒ P ]
+ | x4 ⇒ match e2 with [ x4 ⇒ P → P | _ ⇒ P ]
+ | x5 ⇒ match e2 with [ x5 ⇒ P → P | _ ⇒ P ]
+ | x6 ⇒ match e2 with [ x6 ⇒ P → P | _ ⇒ P ]
+ | x7 ⇒ match e2 with [ x7 ⇒ P → P | _ ⇒ P ]
+ | x8 ⇒ match e2 with [ x8 ⇒ P → P | _ ⇒ P ]
+ | x9 ⇒ match e2 with [ x9 ⇒ P → P | _ ⇒ P ]
+ | xA ⇒ match e2 with [ xA ⇒ P → P | _ ⇒ P ]
+ | xB ⇒ match e2 with [ xB ⇒ P → P | _ ⇒ P ]
+ | xC ⇒ match e2 with [ xC ⇒ P → P | _ ⇒ P ]
+ | xD ⇒ match e2 with [ xD ⇒ P → P | _ ⇒ P ]
+ | xE ⇒ match e2 with [ xE ⇒ P → P | _ ⇒ P ]
+ | xF ⇒ match e2 with [ xF ⇒ P → P | _ ⇒ P ]
+ ].
+
+ndefinition exadecim_destruct : exadecim_destruct_aux.
+ #e1; ncases e1;
+ ##[ ##1: napply exadecim_destruct1
+ ##| ##2: napply exadecim_destruct2
+ ##| ##3: napply exadecim_destruct3
+ ##| ##4: napply exadecim_destruct4
+ ##| ##5: napply exadecim_destruct5
+ ##| ##6: napply exadecim_destruct6
+ ##| ##7: napply exadecim_destruct7
+ ##| ##8: napply exadecim_destruct8
+ ##| ##9: napply exadecim_destruct9
+ ##| ##10: napply exadecim_destruct10
+ ##| ##11: napply exadecim_destruct11
+ ##| ##12: napply exadecim_destruct12
+ ##| ##13: napply exadecim_destruct13
+ ##| ##14: napply exadecim_destruct14
+ ##| ##15: napply exadecim_destruct15
+ ##| ##16: napply exadecim_destruct16
+ ##]
+nqed.
+
+nlemma symmetric_eqex : symmetricT exadecim bool eq_ex.
+ #e1; #e2;
+ nelim e1;
+ nelim e2;
+ nnormalize;
+ napply refl_eq.
+nqed.
+
+nlemma symmetric_andex : symmetricT exadecim exadecim and_ex.
+ #e1; #e2;
+ nelim e1;
+ nelim e2;
+ nnormalize;
+ napply refl_eq.
+nqed.
+
+nlemma associative_andex : ∀e1,e2,e3.(and_ex (and_ex e1 e2) e3) = (and_ex e1 (and_ex e2 e3)).
+ #e1; #e2; #e3;
+ nelim e1;
+ ##[ ##1: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##| ##2: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##| ##3: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##| ##4: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##| ##5: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##| ##6: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##| ##7: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##| ##8: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##| ##9: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##| ##10: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##| ##11: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##| ##12: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##| ##13: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##| ##14: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##| ##15: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##| ##16: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##]
+nqed.
+
+nlemma symmetric_orex : symmetricT exadecim exadecim or_ex.
+ #e1; #e2;
+ nelim e1;
+ nelim e2;
+ nnormalize;
+ napply refl_eq.
+nqed.
+
+nlemma associative_orex : ∀e1,e2,e3.(or_ex (or_ex e1 e2) e3) = (or_ex e1 (or_ex e2 e3)).
+ #e1; #e2; #e3;
+ nelim e1;
+ ##[ ##1: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##| ##2: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##| ##3: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##| ##4: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##| ##5: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##| ##6: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##| ##7: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##| ##8: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##| ##9: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##| ##10: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##| ##11: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##| ##12: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##| ##13: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##| ##14: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##| ##15: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##| ##16: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##]
+nqed.
+
+nlemma symmetric_xorex : symmetricT exadecim exadecim xor_ex.
+ #e1; #e2;
+ nelim e1;
+ nelim e2;
+ nnormalize;
+ napply refl_eq.
+nqed.
+
+nlemma associative_xorex : ∀e1,e2,e3.(xor_ex (xor_ex e1 e2) e3) = (xor_ex e1 (xor_ex e2 e3)).
+ #e1; #e2; #e3;
+ nelim e1;
+ ##[ ##1: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##| ##2: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##| ##3: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##| ##4: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##| ##5: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##| ##6: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##| ##7: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##| ##8: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##| ##9: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##| ##10: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##| ##11: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##| ##12: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##| ##13: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##| ##14: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##| ##15: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##| ##16: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##]
+nqed.
+
+nlemma symmetric_plusex_dc_dc : ∀e1,e2,c.plus_ex_dc_dc e1 e2 c = plus_ex_dc_dc e2 e1 c.
+ #e1; #e2; #c;
+ nelim e1;
+ nelim e2;
+ nelim c;
+ nnormalize;
+ napply refl_eq.
+nqed.
+
+nlemma plusex_dc_dc_to_dc_d : ∀e1,e2,c.fst … (plus_ex_dc_dc e1 e2 c) = plus_ex_dc_d e1 e2 c.
+ #e1; #e2; #c;
+ nelim e1;
+ nelim e2;
+ nelim c;
+ nnormalize;
+ napply refl_eq.
+nqed.
+
+nlemma plusex_dc_dc_to_dc_c : ∀e1,e2,c.snd … (plus_ex_dc_dc e1 e2 c) = plus_ex_dc_c e1 e2 c.
+ #e1; #e2; #c;
+ nelim e1;
+ nelim e2;
+ nelim c;
+ nnormalize;
+ napply refl_eq.
+nqed.
+
+nlemma plusex_dc_dc_to_d_dc : ∀e1,e2.plus_ex_dc_dc e1 e2 false = plus_ex_d_dc e1 e2.
+ #e1; #e2;
+ nelim e1;
+ nelim e2;
+ nnormalize;
+ napply refl_eq.
+nqed.
+
+nlemma plusex_dc_dc_to_d_d : ∀e1,e2.fst … (plus_ex_dc_dc e1 e2 false) = plus_ex_d_d e1 e2.
+ #e1; #e2;
+ nelim e1;
+ nelim e2;
+ nnormalize;
+ napply refl_eq.
+nqed.
+
+nlemma plusex_dc_dc_to_d_c : ∀e1,e2.snd … (plus_ex_dc_dc e1 e2 false) = plus_ex_d_c e1 e2.
+ #e1; #e2;
+ nelim e1;
+ nelim e2;
+ nnormalize;
+ napply refl_eq.
+nqed.
+
+nlemma symmetric_plusex_dc_d : ∀e1,e2,c.plus_ex_dc_d e1 e2 c = plus_ex_dc_d e2 e1 c.
+ #e1; #e2; #c;
+ nelim e1;
+ nelim e2;
+ nelim c;
+ nnormalize;
+ napply refl_eq.
+nqed.
+
+nlemma symmetric_plusex_dc_c : ∀e1,e2,c.plus_ex_dc_c e1 e2 c = plus_ex_dc_c e2 e1 c.
+ #e1; #e2; #c;
+ nelim e1;
+ nelim e2;
+ nelim c;
+ nnormalize;
+ napply refl_eq.
+nqed.
+
+nlemma symmetric_plusex_d_dc : ∀e1,e2.plus_ex_d_dc e1 e2 = plus_ex_d_dc e2 e1.
+ #e1; #e2;
+ nelim e1;
+ nelim e2;
+ nnormalize;
+ napply refl_eq.
+nqed.
+
+nlemma plusex_d_dc_to_d_d : ∀e1,e2.fst … (plus_ex_d_dc e1 e2) = plus_ex_d_d e1 e2.
+ #e1; #e2;
+ nelim e1;
+ nelim e2;
+ nnormalize;
+ napply refl_eq.
+nqed.
+
+nlemma plusex_d_dc_to_d_c : ∀e1,e2.snd … (plus_ex_d_dc e1 e2) = plus_ex_d_c e1 e2.
+ #e1; #e2;
+ nelim e1;
+ nelim e2;
+ nnormalize;
+ napply refl_eq.
+nqed.
+
+nlemma symmetric_plusex_d_d : ∀e1,e2.plus_ex_d_d e1 e2 = plus_ex_d_d e2 e1.
+ #e1; #e2;
+ nelim e1;
+ nelim e2;
+ nnormalize;
+ napply refl_eq.
+nqed.
+
+nlemma associative_plusex_d_d : ∀e1,e2,e3.(plus_ex_d_d (plus_ex_d_d e1 e2) e3) = (plus_ex_d_d e1 (plus_ex_d_d e2 e3)).
+ #e1; #e2; #e3;
+ nelim e1;
+ ##[ ##1: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##| ##2: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##| ##3: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##| ##4: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##| ##5: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##| ##6: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##| ##7: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##| ##8: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##| ##9: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##| ##10: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##| ##11: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##| ##12: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##| ##13: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##| ##14: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##| ##15: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##| ##16: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##]
+nqed.
+
+nlemma symmetric_plusex_d_c : ∀e1,e2.plus_ex_d_c e1 e2 = plus_ex_d_c e2 e1.
+ #e1; #e2;
+ nelim e1;
+ nelim e2;
+ nnormalize;
+ napply refl_eq.
+nqed.
+
+nlemma eqex_to_eq : ∀e1,e2:exadecim.(eq_ex e1 e2 = true) → (e1 = e2).
+ #e1; #e2;
+ ncases e1;
+ ncases e2;
+ nnormalize;
+ ##[ ##1,18,35,52,69,86,103,120,137,154,171,188,205,222,239,256: #H; napply refl_eq
+ ##| ##*: #H; napply (bool_destruct … H)
+ ##]
+nqed.
+
+nlemma eq_to_eqex : ∀e1,e2.e1 = e2 → eq_ex e1 e2 = true.
+ #m1; #m2;
+ ncases m1;
+ ncases m2;
+ nnormalize;
+ ##[ ##1,18,35,52,69,86,103,120,137,154,171,188,205,222,239,256: #H; napply refl_eq
+ ##| ##*: #H; napply (exadecim_destruct … H)
+ ##]
+nqed.
+
+nlemma neqex_to_neq : ∀e1,e2:exadecim.(eq_ex e1 e2 = false) → (e1 ≠ e2).
+ #e1; #e2;
+ ncases e1;
+ ncases e2;
+ nnormalize;
+ ##[ ##1,18,35,52,69,86,103,120,137,154,171,188,205,222,239,256: #H; napply (bool_destruct … H)
+ ##| ##*: #H; #H1; napply (exadecim_destruct … H1)
+ ##]
+nqed.
+
+nlemma neq_to_neqex : ∀e1,e2.e1 ≠ e2 → eq_ex e1 e2 = false.
+ #e1; #e2;
+ ncases e1;
+ ncases e2;
+ nnormalize;
+ ##[ ##1,18,35,52,69,86,103,120,137,154,171,188,205,222,239,256: #H; napply False_ind; napply (H (refl_eq …))
+ ##| ##*: #H; napply refl_eq
+ ##]
+nqed.
--- /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 *)
+(* Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* *)
+(* ********************************************************************** *)
+
+include "num/bool.ma".
+
+(* ****** *)
+(* OTTALI *)
+(* ****** *)
+
+ninductive oct : Type ≝
+ o0: oct
+| o1: oct
+| o2: oct
+| o3: oct
+| o4: oct
+| o5: oct
+| o6: oct
+| o7: oct.
+
+(* operatore = *)
+ndefinition eq_oct ≝
+λn1,n2:oct.
+ match n1 with
+ [ o0 ⇒ match n2 with [ o0 ⇒ true | _ ⇒ false ]
+ | o1 ⇒ match n2 with [ o1 ⇒ true | _ ⇒ false ]
+ | o2 ⇒ match n2 with [ o2 ⇒ true | _ ⇒ false ]
+ | o3 ⇒ match n2 with [ o3 ⇒ true | _ ⇒ false ]
+ | o4 ⇒ match n2 with [ o4 ⇒ true | _ ⇒ false ]
+ | o5 ⇒ match n2 with [ o5 ⇒ true | _ ⇒ false ]
+ | o6 ⇒ match n2 with [ o6 ⇒ true | _ ⇒ false ]
+ | o7 ⇒ match n2 with [ o7 ⇒ true | _ ⇒ false ]
+ ].
+
+(* iteratore sugli ottali *)
+ndefinition forall_oct ≝ λP.
+ P o0 ⊗ P o1 ⊗ P o2 ⊗ P o3 ⊗ P o4 ⊗ P o5 ⊗ P o6 ⊗ P o7.
+
+(* operatore successore *)
+ndefinition succ_oct ≝
+λn.match n with
+ [ o0 ⇒ o1 | o1 ⇒ o2 | o2 ⇒ o3 | o3 ⇒ o4 | o4 ⇒ o5 | o5 ⇒ o6 | o6 ⇒ o7 | o7 ⇒ o0 ].
+
+(* ottali ricorsivi *)
+ninductive rec_oct : oct → Type ≝
+ oc_O : rec_oct o0
+| oc_S : ∀n.rec_oct n → rec_oct (succ_oct n).
+
+(* ottali → ottali ricorsivi *)
+ndefinition oct_to_recoct ≝
+λn.match n return λx.rec_oct x with
+ [ o0 ⇒ oc_O
+ | o1 ⇒ oc_S ? oc_O
+ | o2 ⇒ oc_S ? (oc_S ? oc_O)
+ | o3 ⇒ oc_S ? (oc_S ? (oc_S ? oc_O))
+ | o4 ⇒ oc_S ? (oc_S ? (oc_S ? (oc_S ? oc_O)))
+ | o5 ⇒ oc_S ? (oc_S ? (oc_S ? (oc_S ? (oc_S ? oc_O))))
+ | o6 ⇒ oc_S ? (oc_S ? (oc_S ? (oc_S ? (oc_S ? (oc_S ? oc_O)))))
+ | o7 ⇒ oc_S ? (oc_S ? (oc_S ? (oc_S ? (oc_S ? (oc_S ? (oc_S ? oc_O))))))
+ ].
--- /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 *)
+(* Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* *)
+(* ********************************************************************** *)
+
+include "num/oct.ma".
+include "num/bool_lemmas.ma".
+
+(* ****** *)
+(* OTTALI *)
+(* ****** *)
+
+ndefinition oct_destruct_aux ≝
+Πn1,n2:oct.ΠP:Prop.n1 = n2 →
+ match n1 with
+ [ o0 ⇒ match n2 with [ o0 ⇒ P → P | _ ⇒ P ]
+ | o1 ⇒ match n2 with [ o1 ⇒ P → P | _ ⇒ P ]
+ | o2 ⇒ match n2 with [ o2 ⇒ P → P | _ ⇒ P ]
+ | o3 ⇒ match n2 with [ o3 ⇒ P → P | _ ⇒ P ]
+ | o4 ⇒ match n2 with [ o4 ⇒ P → P | _ ⇒ P ]
+ | o5 ⇒ match n2 with [ o5 ⇒ P → P | _ ⇒ P ]
+ | o6 ⇒ match n2 with [ o6 ⇒ P → P | _ ⇒ P ]
+ | o7 ⇒ match n2 with [ o7 ⇒ P → P | _ ⇒ P ]
+ ].
+
+ndefinition oct_destruct : oct_destruct_aux.
+ #n1; #n2; #P;
+ nelim n1;
+ ##[ ##1: nelim n2; nnormalize; #H;
+ ##[ ##1: napply (λx:P.x)
+ ##| ##*: napply False_ind;
+ nchange with (match o0 with [ o0 ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+ ##| ##2: nelim n2; nnormalize; #H;
+ ##[ ##2: napply (λx:P.x)
+ ##| ##*: napply False_ind;
+ nchange with (match o1 with [ o1 ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+ ##| ##3: nelim n2; nnormalize; #H;
+ ##[ ##3: napply (λx:P.x)
+ ##| ##*: napply False_ind;
+ nchange with (match o2 with [ o2 ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+ ##| ##4: nelim n2; nnormalize; #H;
+ ##[ ##4: napply (λx:P.x)
+ ##| ##*: napply False_ind;
+ nchange with (match o3 with [ o3 ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+ ##| ##5: nelim n2; nnormalize; #H;
+ ##[ ##5: napply (λx:P.x)
+ ##| ##*: napply False_ind;
+ nchange with (match o4 with [ o4 ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+ ##| ##6: nelim n2; nnormalize; #H;
+ ##[ ##6: napply (λx:P.x)
+ ##| ##*: napply False_ind;
+ nchange with (match o5 with [ o5 ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+ ##| ##7: nelim n2; nnormalize; #H;
+ ##[ ##7: napply (λx:P.x)
+ ##| ##*: napply False_ind;
+ nchange with (match o6 with [ o6 ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+ ##| ##8: nelim n2; nnormalize; #H;
+ ##[ ##8: napply (λx:P.x)
+ ##| ##*: napply False_ind;
+ nchange with (match o7 with [ o7 ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+ ##]
+nqed.
+
+nlemma symmetric_eqoct : symmetricT oct bool eq_oct.
+ #n1; #n2;
+ nelim n1;
+ nelim n2;
+ nnormalize;
+ napply refl_eq.
+nqed.
+
+nlemma eqoct_to_eq : ∀n1,n2.eq_oct n1 n2 = true → n1 = n2.
+ #n1; #n2;
+ ncases n1;
+ ncases n2;
+ nnormalize;
+ ##[ ##1,10,19,28,37,46,55,64: #H; napply refl_eq
+ ##| ##*: #H; napply (bool_destruct … H)
+ ##]
+nqed.
+
+nlemma eq_to_eqoct : ∀n1,n2.n1 = n2 → eq_oct n1 n2 = true.
+ #n1; #n2;
+ ncases n1;
+ ncases n2;
+ nnormalize;
+ ##[ ##1,10,19,28,37,46,55,64: #H; napply refl_eq
+ ##| ##*: #H; napply (oct_destruct … H)
+ ##]
+nqed.
+
+nlemma neqoct_to_neq : ∀n1,n2.eq_oct n1 n2 = false → n1 ≠ n2.
+ #n1; #n2;
+ ncases n1;
+ ncases n2;
+ nnormalize;
+ ##[ ##1,10,19,28,37,46,55,64: #H; napply (bool_destruct … H)
+ ##| ##*: #H; #H1; napply (oct_destruct … H1)
+ ##]
+nqed.
+
+nlemma neq_to_neqoct : ∀n1,n2.n1 ≠ n2 → eq_oct n1 n2 = false.
+ #n1; #n2;
+ ncases n1;
+ ncases n2;
+ nnormalize;
+ ##[ ##1,10,19,28,37,46,55,64: #H; napply False_ind; napply (H (refl_eq …))
+ ##| ##*: #H; napply refl_eq
+ ##]
+nqed.
--- /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 *)
+(* Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* *)
+(* ********************************************************************** *)
+
+include "num/bool.ma".
+
+(* ********** *)
+(* QUATERNARI *)
+(* ********** *)
+
+ninductive quatern : Type ≝
+ q0 : quatern
+| q1 : quatern
+| q2 : quatern
+| q3 : quatern.
+
+(* operatore = *)
+ndefinition eq_qu ≝
+λn1,n2:quatern.
+ match n1 with
+ [ q0 ⇒ match n2 with [ q0 ⇒ true | _ ⇒ false ]
+ | q1 ⇒ match n2 with [ q1 ⇒ true | _ ⇒ false ]
+ | q2 ⇒ match n2 with [ q2 ⇒ true | _ ⇒ false ]
+ | q3 ⇒ match n2 with [ q3 ⇒ true | _ ⇒ false ]
+ ].
+
+(* iteratore sui quaternari *)
+ndefinition forall_qu ≝ λP.
+ P q0 ⊗ P q1 ⊗ P q2 ⊗ P q3.
+
+(* operatore successorre *)
+ndefinition succ_qu ≝
+λn.match n with
+ [ q0 ⇒ q1 | q1 ⇒ q2 | q2 ⇒ q3 | q3 ⇒ q0 ].
+
+(* quaternari ricorsivi *)
+ninductive rec_quatern : quatern → Type ≝
+ qu_O : rec_quatern q0
+| qu_S : ∀n.rec_quatern n → rec_quatern (succ_qu n).
+
+(* quaternari → quaternari ricorsivi *)
+ndefinition qu_to_recqu ≝
+λn.match n return λx.rec_quatern x with
+ [ q0 ⇒ qu_O
+ | q1 ⇒ qu_S ? qu_O
+ | q2 ⇒ qu_S ? (qu_S ? qu_O)
+ | q3 ⇒ qu_S ? (qu_S ? (qu_S ? qu_O))
+ ].
--- /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 *)
+(* Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* *)
+(* ********************************************************************** *)
+
+include "num/quatern.ma".
+include "num/bool_lemmas.ma".
+
+(* ********** *)
+(* QUATERNARI *)
+(* ********** *)
+
+ndefinition quatern_destruct_aux ≝
+Πn1,n2:quatern.ΠP:Prop.n1 = n2 →
+ match n1 with
+ [ q0 ⇒ match n2 with [ q0 ⇒ P → P | _ ⇒ P ]
+ | q1 ⇒ match n2 with [ q1 ⇒ P → P | _ ⇒ P ]
+ | q2 ⇒ match n2 with [ q2 ⇒ P → P | _ ⇒ P ]
+ | q3 ⇒ match n2 with [ q3 ⇒ P → P | _ ⇒ P ]
+ ].
+
+ndefinition quatern_destruct : quatern_destruct_aux.
+ #n1; #n2; #P;
+ nelim n1;
+ ##[ ##1: nelim n2; nnormalize; #H;
+ ##[ ##1: napply (λx:P.x)
+ ##| ##*: napply False_ind;
+ nchange with (match q0 with [ q0 ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+ ##| ##2: nelim n2; nnormalize; #H;
+ ##[ ##2: napply (λx:P.x)
+ ##| ##*: napply False_ind;
+ nchange with (match q1 with [ q1 ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+ ##| ##3: nelim n2; nnormalize; #H;
+ ##[ ##3: napply (λx:P.x)
+ ##| ##*: napply False_ind;
+ nchange with (match q2 with [ q2 ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+ ##| ##4: nelim n2; nnormalize; #H;
+ ##[ ##4: napply (λx:P.x)
+ ##| ##*: napply False_ind;
+ nchange with (match q3 with [ q3 ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+ ##]
+nqed.
+
+nlemma symmetric_eqqu : symmetricT quatern bool eq_qu.
+ #n1; #n2;
+ nelim n1;
+ nelim n2;
+ nnormalize;
+ napply refl_eq.
+nqed.
+
+nlemma eqqu_to_eq : ∀n1,n2.eq_qu n1 n2 = true → n1 = n2.
+ #n1; #n2;
+ ncases n1;
+ ncases n2;
+ nnormalize;
+ ##[ ##1,6,11,16: #H; napply refl_eq
+ ##| ##*: #H; napply (bool_destruct … H)
+ ##]
+nqed.
+
+nlemma eq_to_eqqu : ∀n1,n2.n1 = n2 → eq_qu n1 n2 = true.
+ #n1; #n2;
+ ncases n1;
+ ncases n2;
+ nnormalize;
+ ##[ ##1,6,11,16: #H; napply refl_eq
+ ##| ##*: #H; napply (quatern_destruct … H)
+ ##]
+nqed.
+
+nlemma neqqu_to_neq : ∀n1,n2.eq_qu n1 n2 = false → n1 ≠ n2.
+ #n1; #n2;
+ ncases n1;
+ ncases n2;
+ nnormalize;
+ ##[ ##1,6,11,16: #H; napply (bool_destruct … H)
+ ##| ##*: #H; #H1; napply (quatern_destruct … H1)
+ ##]
+nqed.
+
+nlemma neq_to_neqqu : ∀n1,n2.n1 ≠ n2 → eq_qu n1 n2 = false.
+ #n1; #n2;
+ ncases n1;
+ ncases n2;
+ nnormalize;
+ ##[ ##1,6,11,16: #H; napply False_ind; napply (H (refl_eq …))
+ ##| ##*: #H; napply refl_eq
+ ##]
+nqed.
-include "utility/utility.ma".
+(*include "utility/utility.ma".
-(*
nlemma fold_right_neList2_aux3 :
\forall T. \forall h,h',t,t'.len_neList T (h§§t) = len_neList T (h'§§t') → len_neList T t = len_neList T t'.
#T; #h; #h'; #t; #t';
nchange in H2:(%) with ((S (len_neList T (a§§l1))) = (S (len_neList T (a§§l))));
*)
-include "freescale/byte8_lemmas.ma".
+(*include "freescale/byte8_lemmas.ma".
-(*
nlemma associative_plusb8_aux
: \forall e1,e2,e3,e4.
match plus_ex_d_dc e2 e4 with
(*...*)
*)
-include "compiler/ast_type_lemmas.ma".
+(*include "compiler/ast_type_lemmas.ma".
-(*
nlemma symmetric_eqasttype_aux1
: ∀x1,x2,y2.eq_nat (len_neList ast_type («£x1»)) (len_neList ast_type (x2§§y2)) = false.
#x1; #x2; #y2; ncases y2; nnormalize;
projects / helm.git / commitdiff