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/static/fsle_drops.ma".
16 include "basic_2/static/lfxs_fsle.ma".
17 include "basic_2/rt_transition/lfpx_length.ma".
18 include "basic_2/rt_transition/lfpx_fqup.ma".
20 (* UNBOUND PARALLEL RT-TRANSITION FOR REFERRED LOCAL ENVIRONMENTS ***********)
22 (* Forward lemmas with free variables inclusion for restricted closures *****)
24 (* Note: "⦃L2, T1⦄ ⊆ ⦃L2, T0⦄" does not hold *)
25 (* Note: Take L0 = K0.ⓓ(ⓝW.V), L2 = K0.ⓓW, T0 = #0, T1 = ⬆*[1]V *)
26 (* Note: This invalidates lfpxs_cpx_conf: "∀h,G. s_r_confluent1 … (cpx h G) (lfpxs h G)" *)
27 lemma lfpx_cpx_conf_fsge (h) (G): ∀L0,T0,T1. ⦃G, L0⦄ ⊢ T0 ⬈[h] T1 →
28 ∀L2. ⦃G, L0⦄ ⊢⬈[h, T0] L2 → ⦃L2, T1⦄ ⊆ ⦃L0, T0⦄.
29 #h #G0 #L0 #T0 @(fqup_wf_ind_eq (Ⓕ) … G0 L0 T0) -G0 -L0 -T0
30 #G #L #T #IH #G0 #L0 * *
31 [ #s #HG #HL #HT #X #HX #Y #HY destruct -IH
32 elim (cpx_inv_sort1 … HX) -HX #H destruct
33 lapply (lfpx_fwd_length … HY) -HY #H0
34 /2 width=1 by fsle_sort_bi/
35 | * [| #i ] #HG #HL #HT #X #HX #Y #HY destruct
36 [ elim (cpx_inv_zero1 … HX) -HX
38 elim (lfpx_inv_zero_length … HY) -HY *
39 [ #H1 #H2 destruct -IH //
40 | #I #K0 #K2 #V0 #V2 #HK02 #HV02 #H1 #H2 destruct
41 lapply (lfpx_fwd_length … HK02) #H0
42 /4 width=4 by fsle_pair_bi, fqu_fqup, fqu_lref_O/
43 | #I #K0 #K2 #HK02 #H1 #H2 destruct -IH
44 /2 width=1 by fsle_unit_bi/
46 | * #I0 #K0 #V0 #V1 #HV01 #HV1X #H destruct
47 elim (lfpx_inv_zero_pair_sn … HY) -HY #K2 #V2 #HK02 #HV02 #H destruct
48 lapply (lfpx_fwd_length … HK02) #H0
49 /4 width=4 by fsle_lifts_SO_sn, fqu_fqup, fqu_lref_O/
51 | elim (cpx_inv_lref1 … HX) -HX
53 elim (lfpx_inv_lref … HY) -HY *
55 | #I0 #I2 #K0 #K2 #HK02 #H1 #H2 destruct
56 lapply (lfpx_fwd_length … HK02) #H0
57 /4 width=5 by fsle_lifts_SO, fqu_fqup/
59 | * #I0 #K0 #V1 #HV1 #HV1X #H0 destruct
60 elim (lfpx_inv_lref_bind_sn … HY) -HY #I2 #K2 #HK02 #H destruct
61 lapply (lfpx_fwd_length … HK02) #H0
62 /4 width=5 by fsle_lifts_SO, fqu_fqup/
65 | #l #HG #HL #HT #X #HX #Y #HY destruct -IH
66 >(cpx_inv_gref1 … HX) -X
67 lapply (lfpx_fwd_length … HY) -HY #H0
68 /2 width=1 by fsle_gref_bi/
69 | #p #I #V0 #T0 #HG #HL #HT #X #HX #Y #HY destruct
70 elim (lfpx_inv_bind … V0 ? HY) -HY #HV0 #HT0
71 elim (cpx_inv_bind1 … HX) -HX *
72 [ #V1 #T1 #HV01 #HT01 #H destruct
73 lapply (lfpx_fwd_length … HV0) #H0
74 /4 width=6 by fsle_bind_eq, fsle_fwd_pair_sn/
75 | #T #HT #HXT #H1 #H2 destruct
76 lapply (lfpx_fwd_length … HV0) #H0
77 /3 width=8 by fsle_inv_lifts_sn/
79 | #I #V0 #X0 #HG #HL #HT #X #HX #Y #HY destruct
80 elim (lfxs_inv_flat … HY) -HY #HV0 #HX0
81 elim (cpx_inv_flat1 … HX) -HX *
82 [ #V1 #T1 #HV01 #HT01 #H destruct
83 /3 width=4 by fsle_flat/
85 /4 width=4 by fsle_flat_dx_dx/
87 /4 width=4 by fsle_flat_dx_sn/
88 | #p #V1 #W0 #W1 #T0 #T1 #HV01 #HW01 #HT01 #H1 #H2 #H3 destruct
89 elim (lfpx_inv_bind … W0 ? HX0) -HX0 #HW0 #HT0
90 lapply (lfpx_fwd_length … HV0) #H0
91 lapply (IH … HV01 … HV0) -HV01 -HV0 // #HV
92 lapply (IH … HW01 … HW0) -HW01 -HW0 // #HW
93 lapply (IH … HT01 … HT0) -HT01 -HT0 -IH // #HT
94 lapply (fsle_fwd_pair_sn … HT) -HT #HT
96 [ /4 width=1 by fsle_flat_sn, fsle_flat_dx_dx, fsle_flat_dx_sn, fsle_bind_dx_sn/
97 | /3 width=1 by fsle_flat_dx_dx, fsle_shift/
99 | #p #V1 #X1 #W0 #W1 #T0 #T1 #HV01 #HVX1 #HW01 #HT01 #H1 #H2 #H3 destruct
100 elim (lfpx_inv_bind … W0 ? HX0) -HX0 #HW0 #HT0
101 lapply (lfpx_fwd_length … HV0) #H0
102 lapply (IH … HV01 … HV0) -HV01 -HV0 // #HV
103 lapply (IH … HW01 … HW0) -HW01 -HW0 // #HW
104 lapply (IH … HT01 … HT0) -HT01 -HT0 -IH // #HT
105 lapply (fsle_fwd_pair_sn … HT) -HT #HT
107 [ /3 width=1 by fsle_flat_dx_dx, fsle_bind_dx_sn/
108 | /4 width=3 by fsle_flat_sn, fsle_flat_dx_sn, fsle_flat_dx_dx, fsle_shift, fsle_lifts_sn/
114 lemma lfpx_fsge_comp (h) (G): lfxs_fsge_compatible (cpx h G).
115 /2 width=4 by lfpx_cpx_conf_fsge/ qed-.
117 (**) (* this section concerns cpx *)
118 (* Properties with generic extension on referred entries ********************)
120 (* Basic_2A1: uses: cpx_frees_trans *)
121 lemma cpx_fsge_comp (h) (G): R_fsge_compatible (cpx h G).
122 /2 width=4 by lfpx_cpx_conf_fsge/ qed-.
124 (* Note: lemma 1000 *)
125 (* Basic_2A1: uses: cpx_llpx_sn_conf *)
126 lemma cpx_lfxs_conf (R) (h) (G): s_r_confluent1 … (cpx h G) (lfxs R).
127 /3 width=3 by fsge_lfxs_trans, cpx_fsge_comp/ qed-.
129 (* Advanced properties ******************************************************)
131 lemma lfpx_cpx_conf (h) (G): s_r_confluent1 … (cpx h G) (lfpx h G).
132 /2 width=5 by cpx_lfxs_conf/ qed-.
134 lemma lfpx_cpx_conf_fsge_dx (h) (G): ∀L0,T0,T1. ⦃G, L0⦄ ⊢ T0 ⬈[h] T1 →
135 ∀L2. ⦃G, L0⦄ ⊢⬈[h, T0] L2 → ⦃L2, T1⦄ ⊆ ⦃L0, T1⦄.
136 /3 width=5 by lfpx_cpx_conf, lfpx_fsge_comp/ qed-.