X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FBasic-1%2Fpr0%2Fpr0.ma;fp=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FBasic-1%2Fpr0%2Fpr0.ma;h=9a3b397fe9f10f9dfd52c60c7bfb989a059d84c1;hb=de77f79d60ee3c1d30fe03469172950b557441f3;hp=c95e41331b5d9a75e83fcb9ec119844ebed43714;hpb=3531d88e2a19cba027b4b882f8dd74bf37283b9c;p=helm.git

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/pr0/pr0.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/pr0/pr0.ma
index c95e41331..9a3b397fe 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/pr0/pr0.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/pr0/pr0.ma
@@ -14,9 +14,9 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "LambdaDelta-1/pr0/fwd.ma".
+include "Basic-1/pr0/fwd.ma".
 
-include "LambdaDelta-1/lift/tlt.ma".
+include "Basic-1/lift/tlt.ma".
 
 theorem pr0_confluence__pr0_cong_upsilon_refl:
  \forall (b: B).((not (eq B b Abst)) \to (\forall (u0: T).(\forall (u3: 
@@ -37,6 +37,9 @@ t5 H1) (pr0_comp u3 u3 (pr0_refl u3) (THead (Flat Appl) (lift (S O) O v2) t5)
 (THead (Flat Appl) (lift (S O) O x) t5) (pr0_comp (lift (S O) O v2) (lift (S 
 O) O x) (pr0_lift v2 x H3 (S O) O) t5 t5 (pr0_refl t5) (Flat Appl)) (Bind 
 b))))))))))))))).
+(* COMMENTS
+Initial nodes: 257
+END *)
 
 theorem pr0_confluence__pr0_cong_upsilon_cong:
  \forall (b: B).((not (eq B b Abst)) \to (\forall (u2: T).(\forall (v2: 
@@ -59,6 +62,9 @@ t5)) t)) (THead (Bind b) x1 (THead (Flat Appl) (lift (S O) O x) x0))
 Appl) (lift (S O) O v2) t5) (THead (Flat Appl) (lift (S O) O x) x0) (pr0_comp 
 (lift (S O) O v2) (lift (S O) O x) (pr0_lift v2 x H1 (S O) O) t5 x0 H3 (Flat 
 Appl)) (Bind b))))))))))))))))))).
+(* COMMENTS
+Initial nodes: 269
+END *)
 
 theorem pr0_confluence__pr0_cong_upsilon_delta:
  (not (eq B Abbr Abst)) \to (\forall (u5: T).(\forall (t2: T).(\forall (w: 
@@ -100,6 +106,9 @@ O v2) (lift (S O) O x) (pr0_lift v2 x H2 (S O) O) t5 x0 H4 (Flat Appl))
 (THead (Flat Appl) (lift (S O) O x) x2) (subst0_snd (Flat Appl) x1 x2 x0 O H9 
 (lift (S O) O x))))))) H7)) (pr0_subst0 t2 x0 H3 u5 w O H0 x1 
 H5))))))))))))))))))).
+(* COMMENTS
+Initial nodes: 769
+END *)
 
 theorem pr0_confluence__pr0_cong_upsilon_zeta:
  \forall (b: B).((not (eq B b Abst)) \to (\forall (u0: T).(\forall (u3: 
@@ -122,6 +131,9 @@ t3 x1 H4 (Flat Appl)) (pr0_zeta b H (THead (Flat Appl) v2 x) (THead (Flat
 Appl) x0 x1) (pr0_comp v2 x0 H2 x x1 H3 (Flat Appl)) u3)) (THead (Flat Appl) 
 (lift (S O) O v2) (lift (S O) O x)) (lift_flat Appl v2 x (S O) 
 O)))))))))))))))).
+(* COMMENTS
+Initial nodes: 283
+END *)
 
 theorem pr0_confluence__pr0_cong_delta:
  \forall (u3: T).(\forall (t5: T).(\forall (w: T).((subst0 O u3 t5 w) \to 
@@ -148,6 +160,9 @@ x1)).(ex_intro2 T (\lambda (t: T).(pr0 (THead (Bind Abbr) u2 t3) t)) (\lambda
 (t: T).(pr0 (THead (Bind Abbr) u3 w) t)) (THead (Bind Abbr) x x1) (pr0_delta 
 u2 x H0 t3 x0 H2 x1 H6) (pr0_comp u3 x H1 w x1 H5 (Bind Abbr)))))) H4)) 
 (pr0_subst0 t5 x0 H3 u3 w O H x H1))))))))))))).
+(* COMMENTS
+Initial nodes: 409
+END *)
 
 theorem pr0_confluence__pr0_upsilon_upsilon:
  \forall (b: B).((not (eq B b Abst)) \to (\forall (v1: T).(\forall (v2: 
@@ -172,6 +187,9 @@ Appl) (lift (S O) O x0) x2) (pr0_comp (lift (S O) O v1) (lift (S O) O x0)
 H3 (THead (Flat Appl) (lift (S O) O v2) t2) (THead (Flat Appl) (lift (S O) O 
 x0) x2) (pr0_comp (lift (S O) O v2) (lift (S O) O x0) (pr0_lift v2 x0 H1 (S 
 O) O) t2 x2 H5 (Flat Appl)) (Bind b))))))))))))))))))).
+(* COMMENTS
+Initial nodes: 347
+END *)
 
 theorem pr0_confluence__pr0_delta_delta:
  \forall (u2: T).(\forall (t3: T).(\forall (w: T).((subst0 O u2 t3 w) \to 
@@ -241,6 +259,9 @@ w0 x1 H6 (Bind Abbr)))) (\lambda (H11: (subst0 O x x1 x2)).(ex_intro2 T
 (Bind Abbr)) (pr0_delta u3 x H2 w0 x1 H6 x2 H11))) (subst0_confluence_eq x0 
 x2 x O H10 x1 H7))))) H8)) (pr0_subst0 t3 x0 H3 u2 w O H x H1))))) H5)) 
 (pr0_subst0 t5 x0 H4 u3 w0 O H0 x H2))))))))))))))).
+(* COMMENTS
+Initial nodes: 1501
+END *)
 
 theorem pr0_confluence__pr0_delta_tau:
  \forall (u2: T).(\forall (t3: T).(\forall (w: T).((subst0 O u2 t3 w) \to 
@@ -259,6 +280,9 @@ T).(subst0 O u2 t w)) H (lift (S O) O x) H1) in (subst0_gen_lift_false x u2 w
 (le_n (plus (S O) O)) (plus O (S O)) (plus_sym O (S O))) H3 (ex2 T (\lambda 
 (t: T).(pr0 (THead (Bind Abbr) u2 w) t)) (\lambda (t: T).(pr0 t2 t)))))))) 
 (pr0_gen_lift t4 t3 (S O) O H0)))))))).
+(* COMMENTS
+Initial nodes: 257
+END *)
 
 theorem pr0_confluence:
  \forall (t0: T).(\forall (t1: T).((pr0 t0 t1) \to (\forall (t2: T).((pr0 t0 
@@ -2477,4 +2501,7 @@ x H18 H19)))) (H16 t5 (tlt_head_dx (Flat Cast) u0 t5) t1 H17 t2 H11))))))
 H13)))) t6 (sym_eq T t6 t2 H10))) t H8 H9 H7)))]) in (H7 (refl_equal T t) 
 (refl_equal T t2)))) t4 (sym_eq T t4 t1 H5))) t H3 H4 H2)))]) in (H2 
 (refl_equal T t) (refl_equal T t1))))))))) t0).
+(* COMMENTS
+Initial nodes: 46103
+END *)