freescale porting, work in progress

[helm.git] / helm / software / matita / contribs / ng_assembly / test_errori.ma

diff --git a/helm/software/matita/contribs/ng_assembly/test_errori.ma b/helm/software/matita/contribs/ng_assembly/test_errori.ma
index 155b6073fe79eb1019284f7f5ba2e0531ad0597f..921c1b505a26636a662551ab407f055db1d3c22a 100644 (file)
--- a/helm/software/matita/contribs/ng_assembly/test_errori.ma
+++ b/helm/software/matita/contribs/ng_assembly/test_errori.ma
@@ -1,7 +1,30 @@
 
-include "utility/utility.ma".
+(* congettura, come si fa? *)
+include "num/exadecim.ma".
+include "num/exadecim_lemmas.ma".
+
+nlemma decidable_ex_aux1 : ∀x.∀H:x0 = x.(x0 = x) ∨ (x0 ≠ x).
+ #x; nelim x;
+ ##[ ##1: #H; napply (or_introl … H)
+ ##| ##*: #H; nelim (exadecim_destruct … H)
+ ##]. nqed.
+
+nlemma decidable_ex0 : ∀x:exadecim.decidable (x0 = x).
+ #x;
+ nelim x;
+ nnormalize;
+ napply (Or_ind (x0=x) (x0≠x) ? ? …);
+ ##[ ##1: napply (or_introl (x0 = x0) (x0 ≠ x0) (refl_eq …))
+ ##| ##*:
+ 
+ nnormalize;
+ nelim x;
+ ##[ ##1: nelim y;
+          ##[ ##1: napply (or_introl (? = ?) (? ≠ ?) (refl_eq …))
+          ##| ##*:
+
+(*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';
@@ -22,9 +45,8 @@ nlemma fold_right_neList2_aux3 :
           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
@@ -70,9 +92,8 @@ nlemma associative_plusb8
  (*...*)
 *)
 
-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;