X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FBasic-1%2Fsn3%2Fprops.ma;h=ea72c8869168a58a755fbd7d1a00f134b09b6abe;hb=d3c72253769956a8af10e6ea990ed34c92999e58;hp=cf432cbfc2434f56f7c57d7a7fc51ffbdfbf5e11;hpb=3531d88e2a19cba027b4b882f8dd74bf37283b9c;p=helm.git

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/sn3/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/sn3/props.ma
index cf432cbfc..ea72c8869 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/sn3/props.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/sn3/props.ma
@@ -14,13 +14,13 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "LambdaDelta-1/sn3/nf2.ma".
+include "Basic-1/sn3/nf2.ma".
 
-include "LambdaDelta-1/sn3/fwd.ma".
+include "Basic-1/sn3/fwd.ma".
 
-include "LambdaDelta-1/nf2/iso.ma".
+include "Basic-1/nf2/iso.ma".
 
-include "LambdaDelta-1/pr3/iso.ma".
+include "Basic-1/pr3/iso.ma".
 
 theorem sn3_pr3_trans:
  \forall (c: C).(\forall (t1: T).((sn3 c t1) \to (\forall (t2: T).((pr3 c t1 
@@ -41,6 +41,9 @@ H7 \def (eq_ind_r T t3 (\lambda (t: T).(pr3 c t t0)) H4 t2 H6) in (let H8
 H3 t2 H6) in (let H9 \def (eq_ind_r T t3 (\lambda (t: T).(pr3 c t2 t)) H2 t2 
 H6) in (H0 t0 H8 H7))))) (\lambda (H6: (((eq T t2 t3) \to (\forall (P: 
 Prop).P)))).(H1 t3 H6 H2 t0 H4)) H5)))))))))))) t1 H))).
+(* COMMENTS
+Initial nodes: 289
+END *)
 
 theorem sn3_pr2_intro:
  \forall (c: C).(\forall (t1: T).(((\forall (t2: T).((((eq T t1 t2) \to 
@@ -71,6 +74,9 @@ t6) \to (sn3 c t6))))) H7 t3 H10) in (let H13 \def (eq_ind T t4 (\lambda (t:
 T).(pr2 c t t3)) H4 t3 H10) in (H6 H12 H11))))) (\lambda (H10: (((eq T t4 t3) 
 \to (\forall (P: Prop).P)))).(sn3_pr3_trans c t3 (H7 t3 H10 H4) t5 H5)) 
 H9))))))))))) t1 t2 H1 H3)) H2)))))))).
+(* COMMENTS
+Initial nodes: 467
+END *)
 
 theorem sn3_cast:
  \forall (c: C).(\forall (u: T).((sn3 c u) \to (\forall (t: T).((sn3 c t) \to 
@@ -136,6 +142,9 @@ Cast) x0 t3)) \to (\forall (P: Prop).P))) H12 t0 H16) in (let H18 \def
 H11))) H15))))) H13))) t2 H9))))))) H8)) (\lambda (H8: (pr2 c t0 
 t2)).(sn3_pr3_trans c t0 (sn3_sing c t0 H3) t2 (pr3_pr2 c t0 t2 H8))) 
 H7))))))))) t H2)))))) u H))).
+(* COMMENTS
+Initial nodes: 1239
+END *)
 
 theorem sn3_cflat:
  \forall (c: C).(\forall (t: T).((sn3 c t) \to (\forall (f: F).(\forall (u: 
@@ -150,6 +159,9 @@ F).(\lambda (u: T).(sn3_ind c (\lambda (t0: T).(sn3 (CHead c (Flat f) u) t0))
 (\lambda (t2: T).(\lambda (H2: (((eq T t1 t2) \to (\forall (P: 
 Prop).P)))).(\lambda (H3: (pr2 (CHead c (Flat f) u) t1 t2)).(H1 t2 H2 
 (pr3_pr2 c t1 t2 (pr2_gen_cflat f c u t1 t2 H3)))))))))) t H))))).
+(* COMMENTS
+Initial nodes: 175
+END *)
 
 theorem sn3_shift:
  \forall (b: B).(\forall (c: C).(\forall (v: T).(\forall (t: T).((sn3 c 
@@ -160,6 +172,9 @@ theorem sn3_shift:
 H0 \def H_x in (land_ind (sn3 c v) (sn3 (CHead c (Bind b) v) t) (sn3 (CHead c 
 (Bind b) v) t) (\lambda (_: (sn3 c v)).(\lambda (H2: (sn3 (CHead c (Bind b) 
 v) t)).H2)) H0))))))).
+(* COMMENTS
+Initial nodes: 95
+END *)
 
 theorem sn3_change:
  \forall (b: B).((not (eq B b Abbr)) \to (\forall (c: C).(\forall (v1: 
@@ -178,6 +193,9 @@ t2) \to (\forall (P: Prop).P))) \to ((pr3 (CHead c (Bind b) v1) t1 t2) \to
 Prop).P)))).(\lambda (H4: (pr2 (CHead c (Bind b) v2) t1 t2)).(H2 t2 H3 
 (pr3_pr2 (CHead c (Bind b) v1) t1 t2 (pr2_change b H c v2 t1 t2 H4 
 v1)))))))))) t H0))))))).
+(* COMMENTS
+Initial nodes: 239
+END *)
 
 theorem sn3_gen_def:
  \forall (c: C).(\forall (d: C).(\forall (v: T).(\forall (i: nat).((getl i c 
@@ -189,6 +207,9 @@ i))).(sn3_gen_lift c v (S i) O (sn3_pr3_trans c (TLRef i) H0 (lift (S i) O v)
 (pr3_pr2 c (TLRef i) (lift (S i) O v) (pr2_delta c d v i H (TLRef i) (TLRef 
 i) (pr0_refl (TLRef i)) (lift (S i) O v) (subst0_lref v i)))) d (getl_drop 
 Abbr c d v i H))))))).
+(* COMMENTS
+Initial nodes: 139
+END *)
 
 theorem sn3_cdelta:
  \forall (v: T).(\forall (t: T).(\forall (i: nat).(((\forall (w: T).(ex T 
@@ -243,6 +264,9 @@ v0))))))).(\lambda (c: C).(\lambda (d: C).(\lambda (H6: (getl i0 c (CHead d
 (Bind Abbr) v0))).(\lambda (H7: (sn3 c (THead k u1 t1))).(let H_y \def 
 (sn3_gen_head k c u1 t1 H7) in (H3 c d H6 H_y))))))))))))))))) i v t x H1))) 
 H0)))))).
+(* COMMENTS
+Initial nodes: 949
+END *)
 
 theorem sn3_cpr3_trans:
  \forall (c: C).(\forall (u1: T).(\forall (u2: T).((pr3 c u1 u2) \to (\forall 
@@ -259,6 +283,9 @@ Prop).P))) \to ((pr3 (CHead c k u1) t1 t2) \to (sn3 (CHead c k u2)
 t2)))))).(sn3_sing (CHead c k u2) t1 (\lambda (t2: T).(\lambda (H3: (((eq T 
 t1 t2) \to (\forall (P: Prop).P)))).(\lambda (H4: (pr3 (CHead c k u2) t1 
 t2)).(H2 t2 H3 (pr3_pr3_pr3_t c u1 u2 H t1 t2 k H4))))))))) t H0))))))).
+(* COMMENTS
+Initial nodes: 203
+END *)
 
 theorem sn3_bind:
  \forall (b: B).(\forall (c: C).(\forall (u: T).((sn3 c u) \to (\forall (t: 
@@ -373,6 +400,9 @@ t3))).(sn3_gen_lift (CHead c (Bind b) t1) t3 (S O) O (sn3_pr3_trans (CHead c
 (Bind b) t1) t2 (sn3_sing (CHead c (Bind b) t1) t2 H3) (lift (S O) O t3) H10) 
 c (drop_drop (Bind b) O c c (drop_refl c) t1))) H9)))) H7)))))))))) t 
 H2)))))) u H)))).
+(* COMMENTS
+Initial nodes: 2401
+END *)
 
 theorem sn3_beta:
  \forall (c: C).(\forall (v: T).(\forall (t: T).((sn3 c (THead (Bind Abbr) v 
@@ -670,6 +700,9 @@ c (THead (Bind b) x6 (THead (Flat Appl) (lift (S O) O x5) x4)))) (let H29
 False).(sn3 c (THead (Bind Abst) x6 (THead (Flat Appl) (lift (S O) O x5) 
 x4)))) with []) in H29) x1 H24)))))))) H21)) H20)) t3 H15)))))))))))))) H12)) 
 H11))))))))) w H4))))))))))) y H0))))) H)))).
+(* COMMENTS
+Initial nodes: 5699
+END *)
 
 theorem sn3_appl_lref:
  \forall (c: C).(\forall (i: nat).((nf2 c (TLRef i)) \to (\forall (v: 
@@ -790,6 +823,9 @@ O) O x4) x3)) (\lambda (t: T).(sn3 c t)) (let H14 \def (eq_ind T (TLRef i)
 False])) I (THead (Bind x0) x1 x2) H8) in (False_ind (sn3 c (THead (Bind x0) 
 x5 (THead (Flat Appl) (lift (S O) O x4) x3))) H14)) t2 H9)))))))))))))) H6)) 
 H5))))))))) v H0))))).
+(* COMMENTS
+Initial nodes: 2125
+END *)
 
 theorem sn3_appl_abbr:
  \forall (c: C).(\forall (d: C).(\forall (w: T).(\forall (i: nat).((getl i c 
@@ -979,6 +1015,9 @@ False | (TLRef _) \Rightarrow True | (THead _ _ _) \Rightarrow False])) I
 (THead (Bind x0) x1 x2) H12) in (False_ind (sn3 c (THead (Bind x0) x5 (THead 
 (Flat Appl) (lift (S O) O x4) x3))) H18)) t2 H13)))))))))))))) H10)) 
 H9))))))))))))) y H1)))) H0))))))).
+(* COMMENTS
+Initial nodes: 3727
+END *)
 
 theorem sn3_appl_cast:
  \forall (c: C).(\forall (v: T).(\forall (u: T).((sn3 c (THead (Flat Appl) v 
@@ -1242,6 +1281,9 @@ x0 x1) (\lambda (ee: T).(match ee in T return (\lambda (_: T).Prop) with
 H18) in (False_ind (sn3 c (THead (Bind x2) x7 (THead (Flat Appl) (lift (S O) 
 O x6) x5))) H24)) t2 H19)))))))))))))) H16)) H15))))))))))))))) y0 H5)))) 
 H4))))))))) y H0))))) H)))).
+(* COMMENTS
+Initial nodes: 5149
+END *)
 
 theorem sn3_appl_bind:
  \forall (b: B).((not (eq B b Abst)) \to (\forall (c: C).(\forall (u: 
@@ -1687,6 +1729,9 @@ Appl) (lift (S O) O x5) x4)) (pr3_pr2 c (THead (Bind b) t1 (THead (Flat Appl)
 x5) x4)) (pr2_head_1 c t1 x6 H27 (Bind b) (THead (Flat Appl) (lift (S O) O 
 x5) x4)))) x1 H25))))))) H22)) H21)) t3 H16)))))))))))))) H13)) 
 H12)))))))))))))) y H4))))) H3))))))) u H0))))).
+(* COMMENTS
+Initial nodes: 9191
+END *)
 
 theorem sn3_appl_appl:
  \forall (v1: T).(\forall (t1: T).(let u1 \def (THead (Flat Appl) v1 t1) in 
@@ -2155,6 +2200,9 @@ _) \Rightarrow False | (TLRef _) \Rightarrow False | (THead k _ _)
 H17) in (False_ind (sn3 c (THead (Bind x1) x6 (THead (Flat Appl) (lift (S O) 
 O x5) x4))) H23)) t3 H18)))))))))))))) H15)) H14)))))) t2 H3))))))))) v2 
 H4))))))))) y H0))))) H))))).
+(* COMMENTS
+Initial nodes: 9317
+END *)
 
 theorem sn3_appl_beta:
  \forall (c: C).(\forall (u: T).(\forall (v: T).(\forall (t: T).((sn3 c 
@@ -2175,6 +2223,9 @@ Abst) w t)) u2) \to (\forall (P: Prop).P)))).(sn3_pr3_trans c (THead (Flat
 Appl) u (THead (Bind Abbr) v t)) H (THead (Flat Appl) u u2) (pr3_thin_dx c 
 (THead (Bind Abbr) v t) u2 (pr3_iso_beta v w t c u2 H4 H5) u Appl)))))))) 
 H1))))))))).
+(* COMMENTS
+Initial nodes: 289
+END *)
 
 theorem sn3_appl_appls:
  \forall (v1: T).(\forall (t1: T).(\forall (vs: TList).(let u1 \def (THeads 
@@ -2191,6 +2242,9 @@ theorem sn3_appl_appls:
 (Flat Appl) vs t1)) u2) \to (\forall (P: Prop).P))) \to (sn3 c (THead (Flat 
 Appl) v2 u2))))))).(sn3_appl_appl v1 (THeads (Flat Appl) vs t1) c H v2 H0 
 H1))))))))).
+(* COMMENTS
+Initial nodes: 141
+END *)
 
 theorem sn3_appls_lref:
  \forall (c: C).(\forall (i: nat).((nf2 c (TLRef i)) \to (\forall (us: 
@@ -2222,6 +2276,9 @@ Appl) (TCons t1 t2) (TLRef i)) u2)).(\lambda (H9: (((iso (THeads (Flat Appl)
 (TCons t1 t2) (TLRef i)) u2) \to (\forall (P: Prop).P)))).(H9 
 (nf2_iso_appls_lref c i H (TCons t1 t2) u2 H8) (sn3 c (THead (Flat Appl) t 
 u2))))))))) H5))) H3))))))) t0))) us)))).
+(* COMMENTS
+Initial nodes: 577
+END *)
 
 theorem sn3_appls_cast:
  \forall (c: C).(\forall (vs: TList).(\forall (u: T).((sn3 c (THeads (Flat 
@@ -2275,6 +2332,9 @@ Prop).P)))).(sn3_pr3_trans c (THead (Flat Appl) t (THeads (Flat Appl) (TCons
 t1 t2) t3)) H2 (THead (Flat Appl) t u2) (pr3_thin_dx c (THeads (Flat Appl) 
 (TCons t1 t2) t3) u2 (pr3_iso_appls_cast c u t3 (TCons t1 t2) u2 H11 H12) t 
 Appl))))))))) H7)))))) H3))))))))))) t0))) vs)).
+(* COMMENTS
+Initial nodes: 1025
+END *)
 
 theorem sn3_appls_bind:
  \forall (b: B).((not (eq B b Abst)) \to (\forall (c: C).(\forall (u: 
@@ -2327,6 +2387,9 @@ H (TCons t t0) u t1 c u2 H7 H8) in (sn3_pr3_trans c (THead (Flat Appl) v
 t1) v H3) (THead (Flat Appl) v u2) (pr3_flat c v v (pr3_refl c v) (THead 
 (Bind b) u (THeads (Flat Appl) (lifts (S O) O (TCons t t0)) t1)) u2 H9 
 Appl)))))))))) H4))))))))) vs0))) vs)))))).
+(* COMMENTS
+Initial nodes: 1143
+END *)
 
 theorem sn3_appls_beta:
  \forall (c: C).(\forall (v: T).(\forall (t: T).(\forall (us: TList).((sn3 c 
@@ -2376,6 +2439,9 @@ Appl) v (THead (Bind Abst) w t))) u2) \to (\forall (P: Prop).P)))).(let H8
 (THead (Flat Appl) u (THeads (Flat Appl) (TCons t0 t1) (THead (Bind Abbr) v 
 t))) H1 (THead (Flat Appl) u u2) (pr3_thin_dx c (THeads (Flat Appl) (TCons t0 
 t1) (THead (Bind Abbr) v t)) u2 H8 u Appl))))))))) H3)))))))))) us0))) us)))).
+(* COMMENTS
+Initial nodes: 987
+END *)
 
 theorem sn3_lift:
  \forall (d: C).(\forall (t: T).((sn3 d t) \to (\forall (c: C).(\forall (h: 
@@ -2402,6 +2468,9 @@ x)).(\lambda (P: Prop).(let H10 \def (eq_ind_r T x (\lambda (t0: T).((eq T
 H11 \def (eq_ind_r T x (\lambda (t0: T).(pr2 d t1 t0)) H7 t1 H9) in (H10 
 (refl_equal T (lift h i t1)) P))))) (pr3_pr2 d t1 x H7) c h i H2) t2 H6))))) 
 H5))))))))))))) t H))).
+(* COMMENTS
+Initial nodes: 439
+END *)
 
 theorem sn3_abbr:
  \forall (c: C).(\forall (d: C).(\forall (v: T).(\forall (i: nat).((getl i c 
@@ -2441,6 +2510,9 @@ H10) in (eq_ind T v (\lambda (t: T).(sn3 c (lift (S i) O t))) (let H13 \def
 (eq_ind_r C x0 (\lambda (c0: C).(getl i c (CHead c0 (Bind Abbr) v))) H12 d 
 H11) in (sn3_lift d v H0 c (S i) O (getl_drop Abbr c d v i H13))) x1 H10)))) 
 H9))) t2 H6)))))) H4)) H3))))))))))).
+(* COMMENTS
+Initial nodes: 743
+END *)
 
 theorem sn3_appls_abbr:
  \forall (c: C).(\forall (d: C).(\forall (w: T).(\forall (i: nat).((getl i c 
@@ -2480,6 +2552,9 @@ Appl) (TCons t t0) (lift (S i) O w))) H2 (THead (Flat Appl) v u2)
 (pr3_thin_dx c (THeads (Flat Appl) (TCons t t0) (lift (S i) O w)) u2 
 (pr3_iso_appls_abbr c d w i H (TCons t t0) u2 H6 H7) v Appl)))))))) 
 H3)))))))) vs0))) vs)))))).
+(* COMMENTS
+Initial nodes: 797
+END *)
 
 theorem sns3_lifts:
  \forall (c: C).(\forall (d: C).(\forall (h: nat).(\forall (i: nat).((drop h 
@@ -2494,4 +2569,7 @@ H1 in (land_ind (sn3 d t) (sns3 d t0) (land (sn3 c (lift h i t)) (sns3 c
 (lifts h i t0))) (\lambda (H3: (sn3 d t)).(\lambda (H4: (sns3 d t0)).(conj 
 (sn3 c (lift h i t)) (sns3 c (lifts h i t0)) (sn3_lift d t H3 c h i H) (H0 
 H4)))) H2)))))) ts)))))).
+(* COMMENTS
+Initial nodes: 185
+END *)