X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FBasic-1%2Fsubst0%2Fsubst0.ma;h=66c167d2b117015bdc09de1b10c02c545404c7fd;hb=de77f79d60ee3c1d30fe03469172950b557441f3;hp=43747913fc3f775e726abc76eb3c53f3e55053c8;hpb=3531d88e2a19cba027b4b882f8dd74bf37283b9c;p=helm.git

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/subst0/subst0.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/subst0/subst0.ma
index 43747913f..66c167d2b 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/subst0/subst0.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/subst0/subst0.ma
@@ -14,7 +14,7 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "LambdaDelta-1/subst0/props.ma".
+include "Basic-1/subst0/props.ma".
 
 theorem subst0_subst0:
  \forall (t1: T).(\forall (t2: T).(\forall (u2: T).(\forall (j: nat).((subst0 
@@ -91,6 +91,9 @@ T).(subst0 i u3 (THead k u1 t0) t)) (\lambda (t: T).(subst0 (S (plus i0 i)) u
 t (THead k u0 t3))) (THead k x0 x) (subst0_both u3 u1 x0 i H7 k t0 x H5) 
 (subst0_both u x0 u0 (S (plus i0 i)) H8 k x t3 H10))))))) (H1 u3 u i0 H4))))) 
 (H3 u3 u i0 H4))))))))))))))))) j u2 t1 t2 H))))).
+(* COMMENTS
+Initial nodes: 1613
+END *)
 
 theorem subst0_subst0_back:
  \forall (t1: T).(\forall (t2: T).(\forall (u2: T).(\forall (j: nat).((subst0 
@@ -167,6 +170,9 @@ t)) (\lambda (t: T).(subst0 (S (plus i0 i)) u (THead k u0 t3) t)) (THead k x0
 x) (subst0_both u3 u1 x0 i H7 k t0 x H5) (subst0_both u u0 x0 (S (plus i0 i)) 
 H8 k t3 x H10))))))) (H1 u3 u i0 H4))))) (H3 u3 u i0 H4))))))))))))))))) j u2 
 t1 t2 H))))).
+(* COMMENTS
+Initial nodes: 1613
+END *)
 
 theorem subst0_trans:
  \forall (t2: T).(\forall (t1: T).(\forall (v: T).(\forall (i: nat).((subst0 
@@ -279,6 +285,9 @@ i0 v0 u2 u3))) (\lambda (_: T).(\lambda (t5: T).(subst0 (s k i0) v0 t3 t5)))
 T).(subst0 i0 v0 (THead k u1 t0) t)) (subst0_both v0 u1 x0 i0 (H1 x0 H7) k t0 
 x1 (H3 x1 H8)) t4 H6)))))) H5)) (subst0_gen_head k v0 u2 t3 t4 i0 
 H4))))))))))))))) i v t1 t2 H))))).
+(* COMMENTS
+Initial nodes: 2555
+END *)
 
 theorem subst0_confluence_neq:
  \forall (t0: T).(\forall (t1: T).(\forall (u1: T).(\forall (i1: 
@@ -502,6 +511,9 @@ i2) u3 t3 x2)).(\lambda (_: (subst0 (s k i) v x1 x2)).(\lambda (H14: (eq nat
 (H12: (eq nat (s k i) (s k i2))).(H5 (s_inj k i i2 H12)))))))))) (H1 x0 u3 i2 
 H8 H5)) t4 H7)))))) H6)) (subst0_gen_head k u3 u0 t2 t4 i2 
 H4)))))))))))))))))) i1 u1 t0 t1 H))))).
+(* COMMENTS
+Initial nodes: 5375
+END *)
 
 theorem subst0_confluence_eq:
  \forall (t0: T).(\forall (t1: T).(\forall (u: T).(\forall (i: nat).((subst0 
@@ -1356,6 +1368,9 @@ k x0 x1)) (ex2 T (\lambda (t: T).(subst0 i0 v (THead k u2 t3) t)) (\lambda
 k x0 x1)) (subst0 i0 v (THead k x0 x1) (THead k u2 t3)) (subst0_both v x0 u2 
 i0 H10 k x1 t3 H9))) (H1 x0 H7))) (H3 x1 H8)) t4 H6)))))) H5)) 
 (subst0_gen_head k v u1 t2 t4 i0 H4))))))))))))))) i u t0 t1 H))))).
+(* COMMENTS
+Initial nodes: 25595
+END *)
 
 theorem subst0_confluence_lift:
  \forall (t0: T).(\forall (t1: T).(\forall (u: T).(\forall (i: nat).((subst0 
@@ -1386,4 +1401,7 @@ t2))).(subst0_gen_lift_false t1 u (lift (S O) i t2) (S O) i i (le_n i)
 (eq_ind_r nat (plus (S O) i) (\lambda (n: nat).(lt i n)) (le_n (plus (S O) 
 i)) (plus i (S O)) (plus_sym i (S O))) H1 (eq T t1 t2))) 
 (subst0_confluence_eq t0 (lift (S O) i t2) u i H0 (lift (S O) i t1) H)))))))).
+(* COMMENTS
+Initial nodes: 703
+END *)