X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_transition%2Flfpr_lfpr.ma;h=7c6c22237058b6f64d9af569300d6e044f9fb72f;hb=981599dd384b3424c60297ea3a64ab0af9788ea2;hp=e8955fd1eca40270d173896be0b676c6c7b99f7f;hpb=984856dbab870ddc3156040df69b1f1846cc3aaf;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_lfpr.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_lfpr.ma
index e8955fd1e..7c6c22237 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_lfpr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_lfpr.ma
@@ -12,11 +12,13 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "basic_2/static/lfxs_lfxs.ma".
 include "basic_2/rt_transition/cpm_lsubr.ma".
 include "basic_2/rt_transition/cpr.ma".
 include "basic_2/rt_transition/cpr_drops.ma".
 include "basic_2/rt_transition/lfpr_drops.ma".
 include "basic_2/rt_transition/lfpr_fqup.ma".
+include "basic_2/rt_transition/lfpr_frees.ma".
 
 (* PARALLEL R-TRANSITION FOR LOCAL ENV.S ON REFERRED ENTRIES ****************)
 
@@ -43,10 +45,11 @@ elim (lfpr_inv_lref_sn … HL02 … HLK0) -HL02 #K2 #W2 #HLK2 #HK02 #_
 lapply (drops_isuni_fwd_drop2 … HLK2) // -W2 #HLK2
 lapply (fqup_lref … G … HLK0) -HLK0 #HLK0
 elim (IH … HLK0 … HV01 … HV02 … HK01 … HK02) -L0 -K0 -V0 #V #HV1 #HV2
-elim (cpm_lifts … HV2 … HLK2 … HVT2) -K2 -V2
+elim (cpm_lifts_sn … HV2 … HLK2 … HVT2) -K2 -V2
 /3 width=6 by cpm_delta_drops, ex2_intro/
 qed-.
 
+(* Note: we don't use cpm_lifts_bi to preserve visual symmetry *)
 fact cpr_conf_lfpr_delta_delta:
    ∀h,G,L0,i. (
       ∀L,T. ⦃G, L0, #i⦄ ⊐+ ⦃G, L, T⦄ →
@@ -69,8 +72,8 @@ elim (lfpr_inv_lref_sn … HL02 … HLK0) -HL02 #K2 #W2 #HLK2 #HK02 #_
 lapply (drops_isuni_fwd_drop2 … HLK2) -W2 // #HLK2
 lapply (fqup_lref … G … HLK0) -HLK0 #HLK0
 elim (IH … HLK0 … HV01 … HV02 … HK01 … HK02) -L0 -K0 -V0 #V #HV1 #HV2
-elim (cpm_lifts … HV1 … HLK1 … HVT1) -K1 -V1 #T #HVT #HT1
-elim (cpm_lifts … HV2 … HLK2 … HVT2) -K2 -V2 #X #HX #HT2
+elim (cpm_lifts_sn … HV1 … HLK1 … HVT1) -K1 -V1 #T #HVT #HT1
+elim (cpm_lifts_sn … HV2 … HLK2 … HVT2) -K2 -V2 #X #HX #HT2
 lapply (lifts_mono … HX … HVT) #H destruct
 /2 width=3 by ex2_intro/
 qed-.
@@ -111,9 +114,10 @@ fact cpr_conf_lfpr_bind_zeta:
 elim (lfpr_inv_bind … HL01) -HL01 #H1V0 #H1T0
 elim (lfpr_inv_bind … HL02) -HL02 #H2V0 #H2T0
 elim (IH … HT01 … HT02 (L1.ⓓV1) … (L2.ⓓV1)) -IH -HT01 -HT02 /2 width=4 by lfpr_pair_repl_dx/ -L0 -V0 -T0 #T #HT1 #HT2
-elim (cpm_inv_lifts1 … HT2 … L2 … HXT2) -T2 /3 width=3 by drops_refl, drops_drop, cpm_zeta, ex2_intro/
+elim (cpm_inv_lifts_sn … HT2 … L2 … HXT2) -T2 /3 width=3 by drops_refl, drops_drop, cpm_zeta, ex2_intro/
 qed-.
 
+(* Note: we don't use cpm_inv_lifts_bi to preserve visual symmetry *)
 fact cpr_conf_lfpr_zeta_zeta:
    ∀h,G,L0,V0,T0. (
       ∀L,T. ⦃G, L0, +ⓓV0.T0⦄ ⊐+ ⦃G, L, T⦄ →
@@ -130,8 +134,8 @@ fact cpr_conf_lfpr_zeta_zeta:
 elim (lfpr_inv_bind … HL01) -HL01 #H1V0 #H1T0
 elim (lfpr_inv_bind … HL02) -HL02 #H2V0 #H2T0
 elim (IH … HT01 … HT02 (L1.ⓓV0) … (L2.ⓓV0)) -IH -HT01 -HT02 /2 width=4 by lfpr_pair_repl_dx/ -L0 -T0 #T #HT1 #HT2
-elim (cpm_inv_lifts1 … HT1 … L1 … HXT1) -T1 /3 width=2 by drops_refl, drops_drop/ #T1 #HT1 #HXT1
-elim (cpm_inv_lifts1 … HT2 … L2 … HXT2) -T2 /3 width=2 by drops_refl, drops_drop/ #T2 #HT2 #HXT2
+elim (cpm_inv_lifts_sn … HT1 … L1 … HXT1) -T1 /3 width=2 by drops_refl, drops_drop/ #T1 #HT1 #HXT1
+elim (cpm_inv_lifts_sn … HT2 … L2 … HXT2) -T2 /3 width=2 by drops_refl, drops_drop/ #T2 #HT2 #HXT2
 lapply (lifts_inj … HT2 … HT1) -T #H destruct /2 width=3 by ex2_intro/
 qed-.
 
@@ -232,7 +236,7 @@ elim (lfpr_inv_bind … HL01) -HL01 #H1W0 #H1T0
 elim (lfpr_inv_flat … HL02) -HL02 #H2V0 #HL02
 elim (lfpr_inv_bind … HL02) -HL02 #H2W0 #H2T0
 elim (IH … HV01 … HV02 … H1V0 … H2V0) -HV01 -HV02 /2 width=1 by/ #V #HV1 #HV2
-elim (cpm_lifts … HV2 … (L2.ⓓW2) … HVU2) -HVU2 /3 width=2 by drops_refl, drops_drop/ #U #HVU #HU2
+elim (cpm_lifts_sn … HV2 … (L2.ⓓW2) … HVU2) -HVU2 /3 width=2 by drops_refl, drops_drop/ #U #HVU #HU2
 elim (cpm_inv_abbr1 … H) -H *
 [ #W1 #T1 #HW01 #HT01 #H destruct
   elim (IH … HW01 … HW02 … H1W0 … H2W0) /2 width=1 by/
@@ -240,7 +244,7 @@ elim (cpm_inv_abbr1 … H) -H *
   /4 width=7 by cpm_bind, cpr_flat, cpm_theta, ex2_intro/
 | #T1 #HT01 #HXT1 #H destruct
   elim (IH … HT01 … HT02 (L1.ⓓW2) … (L2.ⓓW2)) /2 width=4 by lfpr_pair_repl_dx/ -L0 -V0 -W0 -T0 #T #HT1 #HT2
-  elim (cpm_inv_lifts1 … HT1 … L1 … HXT1) -HXT1
+  elim (cpm_inv_lifts_sn … HT1 … L1 … HXT1) -HXT1
   /4 width=9 by cpr_flat, cpm_zeta, drops_refl, drops_drop, lifts_flat, ex2_intro/
 ]
 qed-.
@@ -270,6 +274,7 @@ lapply (lsubr_cpm_trans … HT2 (L2.ⓓⓝW2.V2) ?) -HT2 /2 width=1 by lsubr_bet
 /4 width=5 by cpm_bind, cpr_flat, ex2_intro/ (**) (* full auto not tried *)
 qed-.
 
+(* Note: we don't use cpm_lifts_bi to preserve visual symmetry *)
 fact cpr_conf_lfpr_theta_theta:
    ∀h,p,G,L0,V0,W0,T0. (
       ∀L,T. ⦃G, L0, ⓐV0.ⓓ{p}W0.T0⦄ ⊐+ ⦃G, L, T⦄ →
@@ -292,13 +297,13 @@ elim (lfpr_inv_bind … HL02) -HL02 #H2W0 #H2T0
 elim (IH … HV01 … HV02 … H1V0 … H2V0) -HV01 -HV02 /2 width=1 by/ #V #HV1 #HV2
 elim (IH … HW01 … HW02 … H1W0 … H2W0) /2 width=1 by/
 elim (IH … HT01 … HT02 (L1.ⓓW1) … (L2.ⓓW2)) /2 width=4 by lfpr_pair_repl_dx/ -L0 -V0 -W0 -T0
-elim (cpm_lifts … HV1 … (L1.ⓓW1) … HVU1) -HVU1 /3 width=2 by drops_refl, drops_drop/ #U #HVU
-elim (cpm_lifts … HV2 … (L2.ⓓW2) … HVU2) -HVU2 /3 width=2 by drops_refl, drops_drop/ #X #HX
+elim (cpm_lifts_sn … HV1 … (L1.ⓓW1) … HVU1) -HVU1 /3 width=2 by drops_refl, drops_drop/ #U #HVU
+elim (cpm_lifts_sn … HV2 … (L2.ⓓW2) … HVU2) -HVU2 /3 width=2 by drops_refl, drops_drop/ #X #HX
 lapply (lifts_mono … HX … HVU) -HX #H destruct
 /4 width=7 by cpm_bind, cpr_flat, ex2_intro/ (**) (* full auto not tried *)
 qed-.
 
-theorem cpr_conf_lfpr: ∀h,G. lfxs_confluent (cpm 0 h G) (cpm 0 h G) (cpm 0 h G) (cpm 0 h G).
+theorem cpr_conf_lfpr: ∀h,G. R_confluent2_lfxs (cpm 0 h G) (cpm 0 h G) (cpm 0 h G) (cpm 0 h G).
 #h #G #L0 #T0 @(fqup_wf_ind_eq … G L0 T0) -G -L0 -T0 #G #L #T #IH #G0 #L0 * [| * ]
 [ #I0 #HG #HL #HT #T1 #H1 #T2 #H2 #L1 #HL01 #L2 #HL02 destruct
   elim (cpr_inv_atom1_drops … H1) -H1
@@ -374,10 +379,5 @@ qed-.
 
 (* Main properties **********************************************************)
 
-(*
-
-theorem lpr_conf: ∀G. confluent … (lpr G).
-/3 width=6 by lpx_sn_conf, cpr_conf_lpr/
-qed-.
-
-*)
+theorem lfpr_conf: ∀h,G,T. confluent … (lfpr h G T).
+/3 width=6 by cpr_conf_lfpr, lfpr_frees_conf, lfxs_conf/ qed-.