(* ********************************************************************** *)
(* Progetto FreeScale *)
(* *)
-(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *)
-(* Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* Ultima modifica: 05/08/2009 *)
(* *)
(* ********************************************************************** *)
##]
nqed.
+nlemma decidable_ex : ∀x,y:exadecim.decidable (x = y).
+ #x; #y;
+ nnormalize;
+ nelim x;
+ nelim y;
+ ##[ ##1,18,35,52,69,86,103,120,137,154,171,188,205,222,239,256: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; 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;
+ #n1; #n2;
+ ncases n1;
+ ncases n2;
nnormalize;
##[ ##1,18,35,52,69,86,103,120,137,154,171,188,205,222,239,256: #H; napply (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;
+ #n1; #n2;
+ ncases n1;
+ ncases n2;
nnormalize;
- ##[ ##1,18,35,52,69,86,103,120,137,154,171,188,205,222,239,256: #H; napply False_ind; napply (H (refl_eq …))
+ ##[ ##1,18,35,52,69,86,103,120,137,154,171,188,205,222,239,256: #H; nelim (H (refl_eq …))
##| ##*: #H; napply refl_eq
##]
nqed.