- partial commit: just the components below "computation"

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / reduction / llpr_ldrop.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/llpr_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/llpr_ldrop.ma
index a19534b4ab1a63e047d68372973bf4d83eb9556a..0ca90bae4de665855ddd799a954cc65f633c1ab3 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/llpr_ldrop.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/llpr_ldrop.ma
@@ -12,9 +12,9 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/relocation/llpx_sn_ldrop.ma".
 include "basic_2/relocation/fquq_alt.ma".
 include "basic_2/reduction/cpr_lift.ma".
+include "basic_2/reduction/cpr_llpx_sn.ma".
 include "basic_2/reduction/llpr.ma".
 
 (* LAZY SN PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS ************************)
@@ -47,6 +47,11 @@ lemma llpr_bind_repl_O: ∀I,G,L1,L2,V1,V2,T. ⦃G, L1.ⓑ{I}V1⦄ ⊢ ➡[T, 0]
                         ∀J,W1,W2. ⦃G, L1⦄ ⊢ ➡[W1, 0] L2 → ⦃G, L1⦄ ⊢ W1 ➡ W2 → ⦃G, L1.ⓑ{J}W1⦄ ⊢ ➡[T, 0] L2.ⓑ{J}W2.
 /2 width=4 by llpx_sn_bind_repl_O/ qed-.
 
+(* Advanced properties ******************************************************)
+
+lemma llpr_cpr_conf: ∀G. s_r_confluent1 … (cpr G) (llpr G 0).
+/3 width=10 by llpx_sn_cpr_conf, cpr_inv_lift1, cpr_lift/ qed-.
+
 (* Properties on context-sensitive parallel reduction for terms *************)
 
 lemma fqu_cpr_trans_dx: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ →