milestone update in basic_2

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / rt_computation / lprs_lprs.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs_lprs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs_lprs.ma
index 1bb611012d73bb5e926592527ed06d64ea60a21e..ae645f6aad67c3cee61a5d1ed76ecae4108a2b3e 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs_lprs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs_lprs.ma
@@ -12,20 +12,22 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/reduction/lpr_lpr.ma".
-include "basic_2/computation/lprs.ma".
+include "basic_2/rt_computation/cprs_cprs.ma".
+include "basic_2/rt_computation/lprs_cpms.ma".
 
-(* SN PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS ****************************)
-
-(* Advanced properties ******************************************************)
-
-lemma lprs_strip: ∀G. confluent2 … (lprs G) (lpr G).
-/3 width=3 by TC_strip1, lpr_conf/ qed-.
+(* PARALLEL R-COMPUTATION FOR FULL LOCAL ENVIRONMENTS ***********************)
 
 (* Main properties **********************************************************)
 
-theorem lprs_conf: ∀G. confluent2 … (lprs G) (lprs G).
-/3 width=3 by TC_confluent2, lpr_conf/ qed-.
+theorem lprs_trans (h) (G): Transitive … (lprs h G).
+/4 width=5 by lprs_cpms_trans, cprs_trans, lex_trans/ qed-.
 
-theorem lprs_trans: ∀G. Transitive … (lprs G).
-/2 width=3 by trans_TC/ qed-.
+theorem lprs_conf (h) (G): confluent2 … (lprs h G) (lprs h G).
+#h #G #L0 #L1 #HL01 #L2 #HL02
+elim (TC_confluent2 … L0 L1 … L2)
+[ /3 width=3 by lprs_TC, ex2_intro/ |5,6: skip
+| /2 width=1 by lprs_inv_TC/
+| /2 width=1 by lprs_inv_TC/
+| /2 width=3 by lpr_conf/
+]
+qed-.