1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "basic_2/rt_computation/lprs_tc.ma".
17 (* PARALLEL R-COMPUTATION FOR FULL LOCAL ENVIRONMENTS ***********************)
19 (* Eliminators with r-transition for full local environments ****************)
21 (* Basic_2A1: was: lprs_ind_dx *)
22 lemma lprs_ind_sn (h) (G) (L2):
23 ∀Q:predicate lenv. Q L2 →
24 (∀L1,L. ❪G,L1❫ ⊢ ➡[h,0] L → ❪G,L❫ ⊢ ➡*[h,0] L2 → Q L → Q L1) →
25 ∀L1. ❪G,L1❫ ⊢ ➡*[h,0] L2 → Q L1.
26 /4 width=8 by lprs_inv_CTC, lprs_CTC, lpr_cprs_trans, cpr_refl, lex_CTC_ind_sn/ qed-.
28 (* Basic_2A1: was: lprs_ind *)
29 lemma lprs_ind_dx (h) (G) (L1):
30 ∀Q:predicate lenv. Q L1 →
31 (∀L,L2. ❪G,L1❫ ⊢ ➡*[h,0] L → ❪G,L❫ ⊢ ➡[h,0] L2 → Q L → Q L2) →
32 ∀L2. ❪G,L1❫ ⊢ ➡*[h,0] L2 → Q L2.
33 /4 width=8 by lprs_inv_CTC, lprs_CTC, lpr_cprs_trans, cpr_refl, lex_CTC_ind_dx/ qed-.
35 (* Properties with extended rt-transition for full local environments *******)
37 lemma lpr_lprs (h) (G):
38 ∀L1,L2. ❪G,L1❫ ⊢ ➡[h,0] L2 → ❪G,L1❫ ⊢ ➡*[h,0] L2.
39 /4 width=3 by lprs_CTC, lpr_cprs_trans, lex_CTC_inj/ qed.
41 (* Basic_2A1: was: lprs_strap2 *)
42 lemma lprs_step_sn (h) (G):
43 ∀L1,L. ❪G,L1❫ ⊢ ➡[h,0] L →
44 ∀L2.❪G,L❫ ⊢ ➡*[h,0] L2 → ❪G,L1❫ ⊢ ➡*[h,0] L2.
45 /4 width=3 by lprs_inv_CTC, lprs_CTC, lpr_cprs_trans, lex_CTC_step_sn/ qed-.
47 (* Basic_2A1: was: lpxs_strap1 *)
48 lemma lprs_step_dx (h) (G):
49 ∀L1,L. ❪G,L1❫ ⊢ ➡*[h,0] L →
50 ∀L2. ❪G,L❫ ⊢ ➡[h,0] L2 → ❪G,L1❫ ⊢ ➡*[h,0] L2.
51 /4 width=3 by lprs_inv_CTC, lprs_CTC, lpr_cprs_trans, lex_CTC_step_dx/ qed-.
53 lemma lprs_strip (h) (G):
54 confluent2 … (lprs h 0 G) (lpr h 0 G).
55 #h #G #L0 #L1 #HL01 #L2 #HL02
56 elim (TC_strip1 … L1 ?? HL02) -HL02
57 [ /3 width=3 by lprs_TC, ex2_intro/ | skip
58 | /2 width=1 by lprs_inv_TC/
59 | /2 width=3 by lpr_conf/