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

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/pc1/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/pc1/props.ma
index a156a65b4..0da1a5aca 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/pc1/props.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/pc1/props.ma
@@ -14,9 +14,9 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "LambdaDelta-1/pc1/defs.ma".
+include "Basic-1/pc1/defs.ma".
 
-include "LambdaDelta-1/pr1/pr1.ma".
+include "Basic-1/pr1/pr1.ma".
 
 theorem pc1_pr0_r:
  \forall (t1: T).(\forall (t2: T).((pr0 t1 t2) \to (pc1 t1 t2)))
@@ -24,6 +24,9 @@ theorem pc1_pr0_r:
  \lambda (t1: T).(\lambda (t2: T).(\lambda (H: (pr0 t1 t2)).(ex_intro2 T 
 (\lambda (t: T).(pr1 t1 t)) (\lambda (t: T).(pr1 t2 t)) t2 (pr1_pr0 t1 t2 H) 
 (pr1_refl t2)))).
+(* COMMENTS
+Initial nodes: 43
+END *)
 
 theorem pc1_pr0_x:
  \forall (t1: T).(\forall (t2: T).((pr0 t2 t1) \to (pc1 t1 t2)))
@@ -31,12 +34,18 @@ theorem pc1_pr0_x:
  \lambda (t1: T).(\lambda (t2: T).(\lambda (H: (pr0 t2 t1)).(ex_intro2 T 
 (\lambda (t: T).(pr1 t1 t)) (\lambda (t: T).(pr1 t2 t)) t1 (pr1_refl t1) 
 (pr1_pr0 t2 t1 H)))).
+(* COMMENTS
+Initial nodes: 43
+END *)
 
 theorem pc1_refl:
  \forall (t: T).(pc1 t t)
 \def
  \lambda (t: T).(ex_intro2 T (\lambda (t0: T).(pr1 t t0)) (\lambda (t0: 
 T).(pr1 t t0)) t (pr1_refl t) (pr1_refl t)).
+(* COMMENTS
+Initial nodes: 31
+END *)
 
 theorem pc1_pr0_u:
  \forall (t2: T).(\forall (t1: T).((pr0 t1 t2) \to (\forall (t3: T).((pc1 t2 
@@ -48,6 +57,9 @@ T).(pr1 t2 t)) (\lambda (t: T).(pr1 t3 t)) (pc1 t1 t3) (\lambda (x:
 T).(\lambda (H2: (pr1 t2 x)).(\lambda (H3: (pr1 t3 x)).(ex_intro2 T (\lambda 
 (t: T).(pr1 t1 t)) (\lambda (t: T).(pr1 t3 t)) x (pr1_sing t2 t1 H x H2) 
 H3)))) H1)))))).
+(* COMMENTS
+Initial nodes: 97
+END *)
 
 theorem pc1_s:
  \forall (t2: T).(\forall (t1: T).((pc1 t1 t2) \to (pc1 t2 t1)))
@@ -57,6 +69,9 @@ theorem pc1_s:
 t1) (\lambda (x: T).(\lambda (H1: (pr1 t1 x)).(\lambda (H2: (pr1 t2 
 x)).(ex_intro2 T (\lambda (t: T).(pr1 t2 t)) (\lambda (t: T).(pr1 t1 t)) x H2 
 H1)))) H0)))).
+(* COMMENTS
+Initial nodes: 79
+END *)
 
 theorem pc1_head_1:
  \forall (u1: T).(\forall (u2: T).((pc1 u1 u2) \to (\forall (t: T).(\forall 
@@ -69,6 +84,9 @@ T).(\lambda (k: K).(let H0 \def H in (ex2_ind T (\lambda (t0: T).(pr1 u1 t0))
 (\lambda (t0: T).(pr1 (THead k u1 t) t0)) (\lambda (t0: T).(pr1 (THead k u2 
 t) t0)) (THead k x t) (pr1_head_1 u1 x H1 t k) (pr1_head_1 u2 x H2 t k))))) 
 H0)))))).
+(* COMMENTS
+Initial nodes: 133
+END *)
 
 theorem pc1_head_2:
  \forall (t1: T).(\forall (t2: T).((pc1 t1 t2) \to (\forall (u: T).(\forall 
@@ -80,6 +98,9 @@ T).(\lambda (k: K).(let H0 \def H in (ex2_ind T (\lambda (t: T).(pr1 t1 t))
 T).(\lambda (H1: (pr1 t1 x)).(\lambda (H2: (pr1 t2 x)).(ex_intro2 T (\lambda 
 (t: T).(pr1 (THead k u t1) t)) (\lambda (t: T).(pr1 (THead k u t2) t)) (THead 
 k u x) (pr1_head_2 t1 x H1 u k) (pr1_head_2 t2 x H2 u k))))) H0)))))).
+(* COMMENTS
+Initial nodes: 133
+END *)
 
 theorem pc1_t:
  \forall (t2: T).(\forall (t1: T).((pc1 t1 t2) \to (\forall (t3: T).((pc1 t2 
@@ -96,6 +117,9 @@ t1 t3) (\lambda (x1: T).(\lambda (H7: (pr1 x0 x1)).(\lambda (H8: (pr1 x
 x1)).(ex_intro2 T (\lambda (t: T).(pr1 t1 t)) (\lambda (t: T).(pr1 t3 t)) x1 
 (pr1_t x0 t1 H5 x1 H7) (pr1_t x t3 H3 x1 H8))))) (pr1_confluence t2 x0 H6 x 
 H2))))) H4))))) H1)))))).
+(* COMMENTS
+Initial nodes: 203
+END *)
 
 theorem pc1_pr0_u2:
  \forall (t0: T).(\forall (t1: T).((pr0 t0 t1) \to (\forall (t2: T).((pc1 t0 
@@ -103,6 +127,9 @@ t2) \to (pc1 t1 t2)))))
 \def
  \lambda (t0: T).(\lambda (t1: T).(\lambda (H: (pr0 t0 t1)).(\lambda (t2: 
 T).(\lambda (H0: (pc1 t0 t2)).(pc1_t t0 t1 (pc1_pr0_x t1 t0 H) t2 H0))))).
+(* COMMENTS
+Initial nodes: 35
+END *)
 
 theorem pc1_head:
  \forall (u1: T).(\forall (u2: T).((pc1 u1 u2) \to (\forall (t1: T).(\forall 
@@ -113,4 +140,7 @@ t2))))))))
 T).(\lambda (t2: T).(\lambda (H0: (pc1 t1 t2)).(\lambda (k: K).(pc1_t (THead 
 k u2 t1) (THead k u1 t1) (pc1_head_1 u1 u2 H t1 k) (THead k u2 t2) 
 (pc1_head_2 t1 t2 H0 u2 k)))))))).
+(* COMMENTS
+Initial nodes: 71
+END *)