X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda-delta%2FBasic-2%2Freduction%2Ftpr_tpr.ma;h=ac09a41ef078185263ca586b77a7dcdf5fe2b494;hb=55dc00c1c44cc21c7ae179cb9df03e7446002c46;hp=43c48d0f2cc756fcefdf99eb9eaacc8fdbbef1e8;hpb=cd0870e2572a77bd69bda4b8c403c30b569c58b9;p=helm.git

diff --git a/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr_tpr.ma b/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr_tpr.ma
index 43c48d0f2..ac09a41ef 100644
--- a/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr_tpr.ma
+++ b/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr_tpr.ma
@@ -49,6 +49,10 @@ elim (IH … HV01 … HV02) -HV01 HV02 // #V #HV1 #HV2
 elim (IH … HT02 … HU01) -HT02 HU01 IH /3 width=5/
 qed.
 
+(* basic-1: was:
+            pr0_cong_upsilon_refl pr0_cong_upsilon_zeta
+            pr0_cong_upsilon_cong pr0_cong_upsilon_delta
+*)
 fact tpr_conf_flat_theta:
    ∀V0,V1,T1,V2,V,W0,W2,U0,U2. (
       ∀X0:term. #[X0] < #[V0] + (#[W0] + #[U0] + 1) + 1 →
@@ -111,6 +115,7 @@ elim (IH … HV01 … HV02) -HV01 HV02 //
 elim (IH … HT01 … HT02) -HT01 HT02 IH /3 width=5/
 qed.
 
+(* Basic-1: was: pr0_cong_delta pr0_delta_delta *)
 fact tpr_conf_delta_delta:
    ∀I1,V0,V1,T0,T1,TT1,V2,T2,TT2. (
       ∀X0:term. #[X0] < #[V0] + #[T0] + 1 →
@@ -146,6 +151,7 @@ lapply (tw_lift … HTT20) -HTT20 #HTT20
 elim (IH … HTX2 … HTT2) -HTX2 HTT2 IH /3/
 qed.
 
+(* Basic-1: was: pr0_upsilon_upsilon *)
 fact tpr_conf_theta_theta:
    ∀VV1,V0,V1,W0,W1,T0,T1,V2,VV2,W2,T2. (
       ∀X0:term. #[X0] < #[V0] + (#[W0] + #[T0] + 1) + 1 →
@@ -274,6 +280,7 @@ fact tpr_conf_aux:
 ]
 qed.
 
+(* Basic-1: was: pr0_confluence *)
 theorem tpr_conf: ∀T0:term. ∀T1,T2. T0 ⇒ T1 → T0 ⇒ T2 →
                   ∃∃T. T1 ⇒ T & T2 ⇒ T.
 #T @(tw_wf_ind … T) -T /3 width=6 by tpr_conf_aux/