Release 0.5.9.

[helm.git] / helm / software / matita / contribs / ng_assembly / common / list_utility.ma

diff --git a/helm/software/matita/contribs/ng_assembly/common/list_utility.ma b/helm/software/matita/contribs/ng_assembly/common/list_utility.ma
index 154d85d36f2794c7984c9d07b0aa8f9dff33eae8..1c062a91297894d71284e594a553aa880a0c82e7 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/common/list_utility.ma
+++ b/helm/software/matita/contribs/ng_assembly/common/list_utility.ma
@@ -16,7 +16,7 @@
 (*                          Progetto FreeScale                            *)
 (*                                                                        *)
 (*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
-(*   Sviluppo: 2008-2010                                                  *)
+(*   Ultima modifica: 05/08/2009                                          *)
 (*                                                                        *)
 (* ********************************************************************** *)
 
@@ -95,7 +95,7 @@ nlemma fold_right_list2_aux1 :
  #T; #h; #t;
  nnormalize;
  #H;
- ndestruct (*napply (nat_destruct_0_S ? H)*).
+ napply (nat_destruct_0_S ? H).
 nqed.
 
 nlemma fold_right_list2_aux2 :
@@ -103,7 +103,7 @@ nlemma fold_right_list2_aux2 :
  #T; #h; #t;
  nnormalize;
  #H;
- ndestruct (*napply (nat_destruct_S_0 ? H)*).
+ napply (nat_destruct_S_0 ? H).
 nqed.
 
 nlemma fold_right_list2_aux3 :
@@ -114,10 +114,10 @@ nlemma fold_right_list2_aux3 :
  ##[ ##1: nnormalize; #H; napply refl_eq
  ##| ##2: #a; #l'; #H; #H1;
           nchange in H1:(%) with ((S O) = (S (S (len_list T l'))));
-          ndestruct (*nelim (nat_destruct_0_S ? (nat_destruct_S_S … H1))*)
+          nelim (nat_destruct_0_S ? (nat_destruct_S_S … H1))
  ##| ##3: #a; #l'; #H; #H1;
           nchange in H1:(%) with ((S (S (len_list T l'))) = (S O));
-          ndestruct (*nelim (nat_destruct_S_0 ? (nat_destruct_S_S … H1))*)
+          nelim (nat_destruct_S_0 ? (nat_destruct_S_S … H1))
  ##| ##4: #a; #l; #H; #a1; #l1; #H1; #H2;
           nchange in H2:(%) with ((S (S (len_list T l1))) = (S (S (len_list T l))));
           nchange with ((S (len_list T l1)) = (S (len_list T l)));
@@ -162,7 +162,7 @@ nlet rec nth_list (T:Type) (l:list T) (n:nat) on l ≝
 
 (* abs elem *)
 ndefinition abs_list_aux1 : ∀T:Type.∀n.((len_list T []) > n) = true → False.
- #T; nnormalize; #n; #H; ndestruct (*napply (bool_destruct … H)*). nqed.
+ #T; nnormalize; #n; #H; napply (bool_destruct … H). nqed.
 
 ndefinition abs_list_aux2 : ∀T:Type.∀h:T.∀t:list T.∀n.((len_list T (h::t)) > (S n) = true) → ((len_list T t) > n) = true.
  #T; #h; #t; #n; nnormalize; #H; napply H. nqed.
@@ -241,8 +241,8 @@ nlemma fold_right_neList2_aux1 :
  nnormalize;
  ncases t';
  nnormalize;
- ##[ ##1: #x; #H; ndestruct (*nelim (nat_destruct_0_S ? (nat_destruct_S_S … H))*)
- ##| ##2: #x; #l; #H; ndestruct (*nelim (nat_destruct_0_S ? (nat_destruct_S_S … H))*)
+ ##[ ##1: #x; #H; nelim (nat_destruct_0_S ? (nat_destruct_S_S … H))
+ ##| ##2: #x; #l; #H; nelim (nat_destruct_0_S ? (nat_destruct_S_S … H))
  ##]
 nqed.
 
@@ -252,8 +252,8 @@ nlemma fold_right_neList2_aux2 :
  nnormalize;
  ncases t;
  nnormalize;
- ##[ ##1: #x; #H; ndestruct (*nelim (nat_destruct_S_0 ? (nat_destruct_S_S … H))*)
- ##| ##2: #x; #l; #H; ndestruct (*nelim (nat_destruct_S_0 ? (nat_destruct_S_S … H))*)
+ ##[ ##1: #x; #H; nelim (nat_destruct_S_0 ? (nat_destruct_S_S … H))
+ ##| ##2: #x; #l; #H; nelim (nat_destruct_S_0 ? (nat_destruct_S_S … H))
  ##]
 nqed.
 
@@ -316,7 +316,7 @@ nlet rec nth_neList (T:Type) (nl:ne_list T) (n:nat) on nl ≝
 
 (* abs elem *)
 ndefinition abs_neList_aux1 : ∀T:Type.∀h:T.∀n.((len_neList T («£h»)) > (S n)) = true → False.
- #T; #h; #n; nnormalize; #H; ndestruct (*napply (bool_destruct … H)*). nqed.
+ #T; #h; #n; nnormalize; #H; napply (bool_destruct … H). nqed.
 
 ndefinition abs_neList_aux2 : ∀T:Type.∀h:T.∀t:ne_list T.∀n.((len_neList T (h§§t)) > (S n) = true) → ((len_neList T t) > n) = true.
  #T; #h; #t; #n; nnormalize; #H; napply H. nqed.