X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FBasic-1%2FT%2Fdec.ma;h=a088c40e3bb410629eb0c8e932c9aca9ecce0b8a;hb=bf8fe5331d6e6d2dfe955efa54b1ffdafaae8429;hp=adb1b8c1bf1898bb56ae7127060b9875f062d558;hpb=3531d88e2a19cba027b4b882f8dd74bf37283b9c;p=helm.git

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/T/dec.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/T/dec.ma
index adb1b8c1b..a088c40e3 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/T/dec.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/T/dec.ma
@@ -14,7 +14,7 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "LambdaDelta-1/T/defs.ma".
+include "Basic-1/T/defs.ma".
 
 theorem terms_props__bind_dec:
  \forall (b1: B).(\forall (b2: B).(or (eq B b1 b2) ((eq B b1 b2) \to (\forall 
@@ -56,6 +56,9 @@ B).(match ee in B return (\lambda (_: B).Prop) with [Abbr \Rightarrow False |
 Abst \Rightarrow False | Void \Rightarrow True])) I Abst H) in (False_ind P 
 H0))))) (or_introl (eq B Void Void) ((eq B Void Void) \to (\forall (P: 
 Prop).P)) (refl_equal B Void)) b2)) b1).
+(* COMMENTS
+Initial nodes: 559
+END *)
 
 theorem bind_dec_not:
  \forall (b1: B).(\forall (b2: B).(or (eq B b1 b2) (not (eq B b1 b2))))
@@ -66,6 +69,9 @@ Prop).P)) (or (eq B b1 b2) ((eq B b1 b2) \to False)) (\lambda (H0: (eq B b1
 b2)).(or_introl (eq B b1 b2) ((eq B b1 b2) \to False) H0)) (\lambda (H0: 
 (((eq B b1 b2) \to (\forall (P: Prop).P)))).(or_intror (eq B b1 b2) ((eq B b1 
 b2) \to False) (\lambda (H1: (eq B b1 b2)).(H0 H1 False)))) H)))).
+(* COMMENTS
+Initial nodes: 131
+END *)
 
 theorem terms_props__flat_dec:
  \forall (f1: F).(\forall (f2: F).(or (eq F f1 f2) ((eq F f1 f2) \to (\forall 
@@ -87,6 +93,9 @@ ee in F return (\lambda (_: F).Prop) with [Appl \Rightarrow False | Cast
 \Rightarrow True])) I Appl H) in (False_ind P H0))))) (or_introl (eq F Cast 
 Cast) ((eq F Cast Cast) \to (\forall (P: Prop).P)) (refl_equal F Cast)) f2)) 
 f1).
+(* COMMENTS
+Initial nodes: 263
+END *)
 
 theorem terms_props__kind_dec:
  \forall (k1: K).(\forall (k2: K).(or (eq K k1 k2) ((eq K k1 k2) \to (\forall 
@@ -133,6 +142,9 @@ f) (Flat f)) \to (\forall (P: Prop).P)) (refl_equal K (Flat f))) f0 H0))
 [(Bind _) \Rightarrow f | (Flat f1) \Rightarrow f1])) (Flat f) (Flat f0) H1) 
 in (let H3 \def (eq_ind_r F f0 (\lambda (f1: F).((eq F f f1) \to (\forall 
 (P0: Prop).P0))) H0 f H2) in (H3 (refl_equal F f) P))))))) H)))) k2))) k1).
+(* COMMENTS
+Initial nodes: 799
+END *)
 
 theorem term_dec:
  \forall (t1: T).(\forall (t2: T).(or (eq T t1 t2) ((eq T t1 t2) \to (\forall 
@@ -281,6 +293,9 @@ T t3 (\lambda (t5: T).((eq T t t5) \to (\forall (P0: Prop).P0))) H4 t H9) in
 (let H13 \def (eq_ind_r T t3 (\lambda (t5: T).(or (eq T (THead k t t0) t5) 
 ((eq T (THead k t t0) t5) \to (\forall (P0: Prop).P0)))) H1 t H9) in (H12 
 (refl_equal T t) P))))))) H7)) H6)))))) H3)))))))) t2))))))) t1).
+(* COMMENTS
+Initial nodes: 2821
+END *)
 
 theorem binder_dec:
  \forall (t: T).(or (ex_3 B T T (\lambda (b: B).(\lambda (w: T).(\lambda (u: 
@@ -347,6 +362,9 @@ _) \Rightarrow False | (TLRef _) \Rightarrow False | (THead k0 _ _)
 \Rightarrow (match k0 in K return (\lambda (_: K).Prop) with [(Bind _) 
 \Rightarrow False | (Flat _) \Rightarrow True])])) I (THead (Bind b) w u) H1) 
 in (False_ind P H2))))))))))))) k)) t).
+(* COMMENTS
+Initial nodes: 1063
+END *)
 
 theorem abst_dec:
  \forall (u: T).(\forall (v: T).(or (ex T (\lambda (t: T).(eq T u (THead 
@@ -422,4 +440,7 @@ with [(TSort _) \Rightarrow t0 | (TLRef _) \Rightarrow t0 | (THead _ _ t2)
 \Rightarrow t2])) (THead k t t0) (THead (Bind Abst) v t1) H3) in (\lambda (_: 
 (eq T t v)).(\lambda (H8: (eq K k (Bind Abst))).(H2 H8 P)))) H5)) H4))))))) 
 H1))))))))) u).
+(* COMMENTS
+Initial nodes: 1305
+END *)