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

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/pc3/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/pc3/props.ma
index 159e6d5e7..b0a9a2f50 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/pc3/props.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/pc3/props.ma
@@ -14,9 +14,9 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "LambdaDelta-1/pc3/defs.ma".
+include "Basic-1/pc3/defs.ma".
 
-include "LambdaDelta-1/pr3/pr3.ma".
+include "Basic-1/pr3/pr3.ma".
 
 theorem clear_pc3_trans:
  \forall (c2: C).(\forall (t1: T).(\forall (t2: T).((pc3 c2 t1 t2) \to 
@@ -29,6 +29,9 @@ t2) (\lambda (x: T).(\lambda (H2: (pr3 c2 t1 x)).(\lambda (H3: (pr3 c2 t2
 x)).(ex_intro2 T (\lambda (t: T).(pr3 c1 t1 t)) (\lambda (t: T).(pr3 c1 t2 
 t)) x (clear_pr3_trans c2 t1 x H2 c1 H0) (clear_pr3_trans c2 t2 x H3 c1 
 H0))))) H1))))))).
+(* COMMENTS
+Initial nodes: 129
+END *)
 
 theorem pc3_pr2_r:
  \forall (c: C).(\forall (t1: T).(\forall (t2: T).((pr2 c t1 t2) \to (pc3 c 
@@ -37,6 +40,9 @@ t1 t2))))
  \lambda (c: C).(\lambda (t1: T).(\lambda (t2: T).(\lambda (H: (pr2 c t1 
 t2)).(ex_intro2 T (\lambda (t: T).(pr3 c t1 t)) (\lambda (t: T).(pr3 c t2 t)) 
 t2 (pr3_pr2 c t1 t2 H) (pr3_refl c t2))))).
+(* COMMENTS
+Initial nodes: 55
+END *)
 
 theorem pc3_pr2_x:
  \forall (c: C).(\forall (t1: T).(\forall (t2: T).((pr2 c t2 t1) \to (pc3 c 
@@ -45,6 +51,9 @@ t1 t2))))
  \lambda (c: C).(\lambda (t1: T).(\lambda (t2: T).(\lambda (H: (pr2 c t2 
 t1)).(ex_intro2 T (\lambda (t: T).(pr3 c t1 t)) (\lambda (t: T).(pr3 c t2 t)) 
 t1 (pr3_refl c t1) (pr3_pr2 c t2 t1 H))))).
+(* COMMENTS
+Initial nodes: 55
+END *)
 
 theorem pc3_pr3_r:
  \forall (c: C).(\forall (t1: T).(\forall (t2: T).((pr3 c t1 t2) \to (pc3 c 
@@ -53,6 +62,9 @@ t1 t2))))
  \lambda (c: C).(\lambda (t1: T).(\lambda (t2: T).(\lambda (H: (pr3 c t1 
 t2)).(ex_intro2 T (\lambda (t: T).(pr3 c t1 t)) (\lambda (t: T).(pr3 c t2 t)) 
 t2 H (pr3_refl c t2))))).
+(* COMMENTS
+Initial nodes: 47
+END *)
 
 theorem pc3_pr3_x:
  \forall (c: C).(\forall (t1: T).(\forall (t2: T).((pr3 c t2 t1) \to (pc3 c 
@@ -61,6 +73,9 @@ t1 t2))))
  \lambda (c: C).(\lambda (t1: T).(\lambda (t2: T).(\lambda (H: (pr3 c t2 
 t1)).(ex_intro2 T (\lambda (t: T).(pr3 c t1 t)) (\lambda (t: T).(pr3 c t2 t)) 
 t1 (pr3_refl c t1) H)))).
+(* COMMENTS
+Initial nodes: 47
+END *)
 
 theorem pc3_pr3_t:
  \forall (c: C).(\forall (t1: T).(\forall (t0: T).((pr3 c t1 t0) \to (\forall 
@@ -69,12 +84,18 @@ theorem pc3_pr3_t:
  \lambda (c: C).(\lambda (t1: T).(\lambda (t0: T).(\lambda (H: (pr3 c t1 
 t0)).(\lambda (t2: T).(\lambda (H0: (pr3 c t2 t0)).(ex_intro2 T (\lambda (t: 
 T).(pr3 c t1 t)) (\lambda (t: T).(pr3 c t2 t)) t0 H H0)))))).
+(* COMMENTS
+Initial nodes: 53
+END *)
 
 theorem pc3_refl:
  \forall (c: C).(\forall (t: T).(pc3 c t t))
 \def
  \lambda (c: C).(\lambda (t: T).(ex_intro2 T (\lambda (t0: T).(pr3 c t t0)) 
 (\lambda (t0: T).(pr3 c t t0)) t (pr3_refl c t) (pr3_refl c t))).
+(* COMMENTS
+Initial nodes: 41
+END *)
 
 theorem pc3_s:
  \forall (c: C).(\forall (t2: T).(\forall (t1: T).((pc3 c t1 t2) \to (pc3 c 
@@ -85,6 +106,9 @@ t2)).(let H0 \def H in (ex2_ind T (\lambda (t: T).(pr3 c t1 t)) (\lambda (t:
 T).(pr3 c t2 t)) (pc3 c t2 t1) (\lambda (x: T).(\lambda (H1: (pr3 c t1 
 x)).(\lambda (H2: (pr3 c t2 x)).(ex_intro2 T (\lambda (t: T).(pr3 c t2 t)) 
 (\lambda (t: T).(pr3 c t1 t)) x H2 H1)))) H0))))).
+(* COMMENTS
+Initial nodes: 97
+END *)
 
 theorem pc3_thin_dx:
  \forall (c: C).(\forall (t1: T).(\forall (t2: T).((pc3 c t1 t2) \to (\forall 
@@ -99,6 +123,9 @@ x)).(\lambda (H2: (pr3 c t2 x)).(ex_intro2 T (\lambda (t: T).(pr3 c (THead
 (Flat f) u t1) t)) (\lambda (t: T).(pr3 c (THead (Flat f) u t2) t)) (THead 
 (Flat f) u x) (pr3_thin_dx c t1 x H1 u f) (pr3_thin_dx c t2 x H2 u f))))) 
 H0))))))).
+(* COMMENTS
+Initial nodes: 165
+END *)
 
 theorem pc3_head_1:
  \forall (c: C).(\forall (u1: T).(\forall (u2: T).((pc3 c u1 u2) \to (\forall 
@@ -112,6 +139,9 @@ u2)).(\lambda (k: K).(\lambda (t: T).(let H0 \def H in (ex2_ind T (\lambda
 (\lambda (t0: T).(pr3 c (THead k u2 t) t0)) (THead k x t) (pr3_head_12 c u1 x 
 H1 k t t (pr3_refl (CHead c k x) t)) (pr3_head_12 c u2 x H2 k t t (pr3_refl 
 (CHead c k x) t)))))) H0))))))).
+(* COMMENTS
+Initial nodes: 183
+END *)
 
 theorem pc3_head_2:
  \forall (c: C).(\forall (u: T).(\forall (t1: T).(\forall (t2: T).(\forall 
@@ -126,6 +156,9 @@ t2 t)) (pc3 c (THead k u t1) (THead k u t2)) (\lambda (x: T).(\lambda (H1:
 T (\lambda (t: T).(pr3 c (THead k u t1) t)) (\lambda (t: T).(pr3 c (THead k u 
 t2) t)) (THead k u x) (pr3_head_12 c u u (pr3_refl c u) k t1 x H1) 
 (pr3_head_12 c u u (pr3_refl c u) k t2 x H2))))) H0))))))).
+(* COMMENTS
+Initial nodes: 201
+END *)
 
 theorem pc3_pr2_u:
  \forall (c: C).(\forall (t2: T).(\forall (t1: T).((pr2 c t1 t2) \to (\forall 
@@ -137,6 +170,9 @@ t2)).(\lambda (t3: T).(\lambda (H0: (pc3 c t2 t3)).(let H1 \def H0 in
 t1 t3) (\lambda (x: T).(\lambda (H2: (pr3 c t2 x)).(\lambda (H3: (pr3 c t3 
 x)).(ex_intro2 T (\lambda (t: T).(pr3 c t1 t)) (\lambda (t: T).(pr3 c t3 t)) 
 x (pr3_sing c t2 t1 H x H2) H3)))) H1))))))).
+(* COMMENTS
+Initial nodes: 119
+END *)
 
 theorem pc3_t:
  \forall (t2: T).(\forall (c: C).(\forall (t1: T).((pc3 c t1 t2) \to (\forall 
@@ -153,6 +189,9 @@ x0)).(\lambda (H6: (pr3 c t2 x0)).(ex2_ind T (\lambda (t: T).(pr3 c x0 t))
 (pr3 c x0 x1)).(\lambda (H8: (pr3 c x x1)).(pc3_pr3_t c t1 x1 (pr3_t x0 t1 c 
 H5 x1 H7) t3 (pr3_t x t3 c H3 x1 H8))))) (pr3_confluence c t2 x0 H6 x H2))))) 
 H4))))) H1))))))).
+(* COMMENTS
+Initial nodes: 233
+END *)
 
 theorem pc3_pr2_u2:
  \forall (c: C).(\forall (t0: T).(\forall (t1: T).((pr2 c t0 t1) \to (\forall 
@@ -161,6 +200,9 @@ theorem pc3_pr2_u2:
  \lambda (c: C).(\lambda (t0: T).(\lambda (t1: T).(\lambda (H: (pr2 c t0 
 t1)).(\lambda (t2: T).(\lambda (H0: (pc3 c t0 t2)).(pc3_t t0 c t1 (pc3_pr2_x 
 c t1 t0 H) t2 H0)))))).
+(* COMMENTS
+Initial nodes: 45
+END *)
 
 theorem pc3_pr3_conf:
  \forall (c: C).(\forall (t: T).(\forall (t1: T).((pc3 c t t1) \to (\forall 
@@ -169,6 +211,9 @@ theorem pc3_pr3_conf:
  \lambda (c: C).(\lambda (t: T).(\lambda (t1: T).(\lambda (H: (pc3 c t 
 t1)).(\lambda (t2: T).(\lambda (H0: (pr3 c t t2)).(pc3_t t c t2 (pc3_pr3_x c 
 t2 t H0) t1 H)))))).
+(* COMMENTS
+Initial nodes: 45
+END *)
 
 theorem pc3_head_12:
  \forall (c: C).(\forall (u1: T).(\forall (u2: T).((pc3 c u1 u2) \to (\forall 
@@ -179,6 +224,9 @@ c (THead k u1 t1) (THead k u2 t2)))))))))
 u2)).(\lambda (k: K).(\lambda (t1: T).(\lambda (t2: T).(\lambda (H0: (pc3 
 (CHead c k u2) t1 t2)).(pc3_t (THead k u2 t1) c (THead k u1 t1) (pc3_head_1 c 
 u1 u2 H k t1) (THead k u2 t2) (pc3_head_2 c u2 t1 t2 k H0))))))))).
+(* COMMENTS
+Initial nodes: 89
+END *)
 
 theorem pc3_head_21:
  \forall (c: C).(\forall (u1: T).(\forall (u2: T).((pc3 c u1 u2) \to (\forall 
@@ -189,6 +237,9 @@ c (THead k u1 t1) (THead k u2 t2)))))))))
 u2)).(\lambda (k: K).(\lambda (t1: T).(\lambda (t2: T).(\lambda (H0: (pc3 
 (CHead c k u1) t1 t2)).(pc3_t (THead k u1 t2) c (THead k u1 t1) (pc3_head_2 c 
 u1 t1 t2 k H0) (THead k u2 t2) (pc3_head_1 c u1 u2 H k t2))))))))).
+(* COMMENTS
+Initial nodes: 89
+END *)
 
 theorem pc3_pr0_pr2_t:
  \forall (u1: T).(\forall (u2: T).((pr0 u2 u1) \to (\forall (c: C).(\forall 
@@ -260,6 +311,9 @@ f) i0) c (CHead d (Bind Abbr) u))).(pc3_pr2_r (CHead c (Flat f) u1) t3 t
 (pr2_cflat c t3 t (pr2_delta c d u (r (Flat f) i0) H10 t3 t4 H3 t H9) f 
 u1))))) k IHi (getl_gen_S k c (CHead d (Bind Abbr) u) u2 i0 H8)))))) i H7 
 H4)))))))))))))) y t1 t2 H1))) H0)))))))).
+(* COMMENTS
+Initial nodes: 1533
+END *)
 
 theorem pc3_pr2_pr2_t:
  \forall (c: C).(\forall (u1: T).(\forall (u2: T).((pr2 c u2 u1) \to (\forall 
@@ -341,6 +395,9 @@ c0 (Flat f) t) t4 t6 (pr2_cflat c0 t4 t6 (pr2_delta c0 d0 u0 (r (Flat f) i1)
 H12 t4 t5 H6 t6 H11) f t)))) k (getl_gen_S k c0 (CHead d0 (Bind Abbr) u0) t1 
 i1 H10)))))) i0 H9 H7))))))))))))) y t0 t3 H4))) H3))))))))))))))) c u2 u1 
 H)))).
+(* COMMENTS
+Initial nodes: 1671
+END *)
 
 theorem pc3_pr2_pr3_t:
  \forall (c: C).(\forall (u2: T).(\forall (t1: T).(\forall (t2: T).(\forall 
@@ -357,6 +414,9 @@ T).(\lambda (H0: (pr2 (CHead c k u2) t3 t0)).(\lambda (t4: T).(\lambda (_:
 \to (pc3 (CHead c k u1) t0 t4))))).(\lambda (u1: T).(\lambda (H3: (pr2 c u2 
 u1)).(pc3_t t0 (CHead c k u1) t3 (pc3_pr2_pr2_t c u1 u2 H3 t3 t0 k H0) t4 (H2 
 u1 H3)))))))))) t1 t2 H)))))).
+(* COMMENTS
+Initial nodes: 199
+END *)
 
 theorem pc3_pr3_pc3_t:
  \forall (c: C).(\forall (u1: T).(\forall (u2: T).((pr3 c u2 u1) \to (\forall 
@@ -378,6 +438,9 @@ t0 t4) (\lambda (x: T).(\lambda (H5: (pr3 (CHead c k t1) t0 x)).(\lambda (H6:
 (pr3 (CHead c k t1) t4 x)).(pc3_t x (CHead c k t2) t0 (pc3_pr2_pr3_t c t1 t0 
 x k H5 t2 H0) t4 (pc3_s (CHead c k t2) x t4 (pc3_pr2_pr3_t c t1 t4 x k H6 t2 
 H0)))))) H4))))))))))))) u2 u1 H)))).
+(* COMMENTS
+Initial nodes: 319
+END *)
 
 theorem pc3_lift:
  \forall (c: C).(\forall (e: C).(\forall (h: nat).(\forall (d: nat).((drop h 
@@ -391,6 +454,9 @@ T).(pr3 e t2 t)) (pc3 c (lift h d t1) (lift h d t2)) (\lambda (x: T).(\lambda
 (H2: (pr3 e t1 x)).(\lambda (H3: (pr3 e t2 x)).(pc3_pr3_t c (lift h d t1) 
 (lift h d x) (pr3_lift c e h d H t1 x H2) (lift h d t2) (pr3_lift c e h d H 
 t2 x H3))))) H1))))))))).
+(* COMMENTS
+Initial nodes: 159
+END *)
 
 theorem pc3_eta:
  \forall (c: C).(\forall (t: T).(\forall (w: T).(\forall (u: T).((pc3 c t 
@@ -411,4 +477,7 @@ H) (TLRef O) Appl)) t (pc3_t (THead (Bind Abst) w u) c (THead (Bind Abst) w
 (pc3_pr3_r c (THead (Bind Abst) w (THead (Flat Appl) (TLRef O) (lift (S O) O 
 (THead (Bind Abst) w u)))) (THead (Bind Abst) w u) (pr3_eta c w u w (pr3_refl 
 c w))) t (pc3_s c (THead (Bind Abst) w u) t H))))))))).
+(* COMMENTS
+Initial nodes: 399
+END *)