--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "static_2/static/reqx_fqup.ma".
+include "basic_2/rt_transition/lpx.ma".
+include "basic_2/rt_transition/rpx.ma".
+
+(* EXAMPLES *****************************************************************)
+
+(* Lemma "rpx_fwd_lpx_reqx" is not an inversion *****************************)
+
+definition L1 (K) (s1) (s0): lenv ≝ K.ⓛ⋆s1.ⓛⓝ#0.⋆s0.
+
+definition L (K) (s1) (s0): lenv ≝ K.ⓛ⋆s1.ⓛ⋆s0.
+
+definition L2 (K) (i1) (s0): lenv ≝ K.ⓛ#i1.ⓛ⋆s0.
+
+definition T: term ≝ #0.
+
+(* Basic properties *********************************************************)
+
+lemma ex_rpx_fwd_1 (G) (K) (s1) (s0):
+ ❪G,L1 K s1 s0❫ ⊢ ⬈ L K s1 s0.
+/3 width=1 by lpx_pair, lpx_bind_refl_dx, cpx_eps/ qed.
+
+lemma ex_rpx_fwd_2 (K) (s1) (s0) (i1) (i0):
+ L K s1 s0 ≛[T] L2 K i1 i0.
+/3 width=1 by reqx_pair, reqx_sort/ qed.
+
+lemma ex_rpx_fwd_3 (G) (K) (s1) (s0) (i1) (i0):
+ ❪G,L1 K s1 s0❫ ⊢ ⬈[T] L2 K i1 i0 → ⊥.
+#G #K #s1 #s0 #i1 #i0 #H
+elim (rpx_inv_zero_pair_sn … H) -H #Y2 #X2 #H #_ normalize #H0 destruct
+elim (rpx_inv_flat … H) -H #H #_
+elim (rpx_inv_zero_pair_sn … H) -H #Y2 #X2 #_ #H #H0 destruct
+elim (cpx_inv_sort1 … H) #s2 #H destruct
+qed-.
+
+(* Main properties **********************************************************)
+
+theorem ex_rpx_fwd (G) (K) (s1) (s0) (i1) (i0):
+ (❪G,L1 K s1 s0❫ ⊢ ⬈ L K s1 s0 → L K s1 s0 ≛[T] L2 K i1 i0 → ❪G,L1 K s1 s0❫ ⊢ ⬈[T] L2 K i1 i0) → ⊥.
+/3 width=7 by ex_rpx_fwd_3, ex_rpx_fwd_2, ex_rpx_fwd_1/ qed-.
class "red"
[ { "examples" * } {
[ { "terms with special features" * } {
- [ "ex_cpr_omega" + "ex_fpbg_refl" + "ex_cnv_eta" * ]
+ [ "ex_cpr_omega" + "ex_rpx_fwd" + "ex_fpbg_refl" + "ex_cnv_eta" * ]
}
]
}
(* Forward lemmas with free variables inclusion for restricted closures *****)
-lemma cpm_fsge_comp: ∀h,n,G. R_fsge_compatible (λL. cpm h G L n).
+lemma cpm_fsge_comp (h) (n) (G):
+ R_fsge_compatible (λL. cpm h G L n).
/3 width=6 by cpm_fwd_cpx, cpx_fsge_comp/ qed-.
-lemma rpr_fsge_comp: ∀h,G. rex_fsge_compatible (λL. cpm h G L 0).
+lemma rpr_fsge_comp (h) (G):
+ rex_fsge_compatible (λL. cpm h G L 0).
/4 width=5 by cpm_fwd_cpx, rpx_fsge_comp, rex_co/ qed-.
(* Properties with generic extension on referred entries ********************)
(* Basic_2A1: was just: cpr_llpx_sn_conf *)
-lemma cpm_rex_conf: ∀R,n,h,G. s_r_confluent1 … (λL. cpm h G L n) (rex R).
-/3 width=5 by cpm_fwd_cpx, cpx_rex_conf/ qed-.
+lemma cpm_rex_conf_sn (R) (h) (n) (G):
+ s_r_confluent1 … (λL. cpm h G L n) (rex R).
+/3 width=5 by cpm_fwd_cpx, cpx_rex_conf_sn/ qed-.
(* *)
(**************************************************************************)
+include "static_2/static/req_length.ma".
include "static_2/static/req_drops.ma".
include "basic_2/rt_transition/rpx_fsle.ma".
(* Properties with syntactic equivalence for lenvs on referred entries ******)
(* Basic_2A1: was: lleq_cpx_trans *)
-lemma req_cpx_trans (G): req_transitive (cpx G).
+lemma req_cpx_trans (G): R_transitive_req (cpx G).
#G #L2 #T1 #T2 #H @(cpx_ind … H) -G -L2 -T1 -T2 /2 width=2 by cpx_qu/
[ #I #G #K2 #V1 #V2 #W2 #_ #IH #HVW2 #L1 #H
elim (req_inv_zero_pair_dx … H) -H #K1 #HK12 #H destruct
]
qed-.
+lemma cpx_req_conf (G): R_confluent1_rex (cpx G) ceq.
+/3 width=3 by req_cpx_trans, req_sym/ qed-.
+
(* Basic_2A1: was: cpx_lleq_conf_sn *)
lemma cpx_req_conf_sn (G): s_r_confluent1 … (cpx G) req.
-/2 width=5 by cpx_rex_conf/ qed-.
+/2 width=5 by cpx_rex_conf_sn/ qed-.
(* Basic_2A1: was just: cpx_lleq_conf_sn *)
lemma cpx_reqx_conf_sn (G):
s_r_confluent1 … (cpx G) reqx.
-/3 width=6 by cpx_rex_conf/ qed-.
+/3 width=6 by cpx_rex_conf_sn/ qed-.
(* Basic_2A1: was just: cpx_lleq_conf_dx *)
lemma cpx_reqx_conf_dx (G) (L2):
elim (teqx_fpb_trans … HT12 … H12) -T2 #K0 #T0 #H #HT0 #HK0
elim (reqx_fpb_trans … HK12 … H) -K2 #L0 #U0 #H #HUT0 #HLK0
@(ex2_3_intro … H) -H (**) (* full auto too slow *)
-/4 width=3 by feqx_intro_dx, reqx_trans, teqx_reqx_conf, teqx_trans/
+/4 width=3 by feqx_intro_dx, reqx_trans, teqx_reqx_conf_sn, teqx_trans/
qed-.
(* Inversion lemmas with degree-based equivalence for closures **************)
| #T1 #HUT1 #HnUT1
lapply (teqx_cpx_trans … HU21 … HUT1) -HUT1
/6 width=5 by fpb_cpx, teqx_canc_sn, teqx_trans, ex3_2_intro/
-| /6 width=5 by fpb_lpx, rpx_teqx_div, teqx_reqx_conf, ex3_2_intro/
+| /6 width=5 by fpb_lpx, rpx_teqx_div, teqx_reqx_conf_sn, ex3_2_intro/
]
qed-.
[ #G #L2 #U #H2 elim (reqx_fqu_trans … H2 … HT) -K2
/3 width=5 by fpb_fqu, ex3_2_intro/
| #U #HTU #HnTU lapply (reqx_cpx_trans … HT … HTU) -HTU
- /5 width=11 by fpb_cpx, cpx_reqx_conf_sn, teqx_trans, teqx_reqx_conf, ex3_2_intro/ (**) (* time: 36s on dev *)
+ /5 width=11 by fpb_cpx, cpx_reqx_conf_sn, teqx_trans, teqx_reqx_conf_sn, ex3_2_intro/ (**) (* time: 36s on dev *)
| #L2 #HKL2 #HnKL2 elim (reqx_lpx_trans … HKL2 … HT) -HKL2
/6 width=5 by fpb_lpx, (* 2x *) reqx_canc_sn, ex3_2_intro/
]
(* Properties with sort-irrelevant equivalence for local environments *******)
-(**) (* to update as reqx_rpx_trans *)
+lemma reqx_lpx_trans_rpx (G) (L) (T:term):
+ ∀L1. L1 ≛[T] L → ∀L2. ❪G,L❫ ⊢ ⬈ L2 → ❪G,L❫ ⊢ ⬈[T] L2.
+/3 width=1 by lpx_rpx, reqx_rpx_trans/ qed.
+
(* Basic_2A1: uses: lleq_lpx_trans *)
lemma reqx_lpx_trans (G):
∀L2,K2. ❪G,L2❫ ⊢ ⬈ K2 → ∀L1. ∀T:term. L1 ≛[T] L2 →
∃∃K1. ❪G,L1❫ ⊢ ⬈ K1 & K1 ≛[T] K2.
#G #L2 #K2 #HLK2 #L1 #T #HL12
-lapply (lpx_rpx … T HLK2) -HLK2 #HLK2
+lapply (lpx_rpx … T … HLK2) -HLK2 #HLK2
lapply (reqx_rpx_trans … HL12 … HLK2) -L2 #H
-elim (rpx_inv_lpx_req … H) -H #K1 #HLK1 #HK12
+elim (rpx_fwd_lpx_req … H) -H #K1 #HLK1 #HK12
+/3 width=3 by req_reqx, ex2_intro/
+qed-.
+
+(* Inversion lemmas with sort-irrelevant equivalence for local environments *)
+
+lemma rpx_inv_reqx_lpx (G) (T):
+ ∀L1,L2. ❪G,L1❫ ⊢ ⬈[T] L2 →
+ ∃∃L. L1 ≛[T] L & ❪G,L❫ ⊢ ⬈ L2.
+#G #T #L1 #L2 #H
+elim (rpx_inv_req_lpx … H) -H #L #HL1 #HL2
+/3 width=3 by req_reqx, ex2_intro/
+qed-.
+
+(* Forward lemmas with sort-irrelevant equivalence for local environments ***)
+
+lemma rpx_fwd_lpx_reqx (G) (T):
+ ∀L1,L2. ❪G,L1❫ ⊢ ⬈[T] L2 →
+ ∃∃L. ❪G,L1❫ ⊢ ⬈ L & L ≛[T] L2.
+#G #T #L1 #L2 #H
+elim (rpx_fwd_lpx_req … H) -H #L #HL1 #HL2
/3 width=3 by req_reqx, ex2_intro/
qed-.
(* Note: lemma 1000 *)
(* Basic_2A1: uses: cpx_llpx_sn_conf *)
-lemma cpx_rex_conf (R) (G): s_r_confluent1 … (cpx G) (rex R).
+lemma cpx_rex_conf_sn (R) (G): s_r_confluent1 … (cpx G) (rex R).
/3 width=3 by fsge_rex_trans, cpx_fsge_comp/ qed-.
(* Advanced properties ******************************************************)
-lemma rpx_cpx_conf (G): s_r_confluent1 … (cpx G) (rpx G).
-/2 width=5 by cpx_rex_conf/ qed-.
+lemma rpx_cpx_conf_sn (G): s_r_confluent1 … (cpx G) (rpx G).
+/2 width=5 by cpx_rex_conf_sn/ qed-.
lemma rpx_cpx_conf_fsge_dx (G):
∀L0,T0,T1. ❪G,L0❫ ⊢ T0 ⬈ T1 →
∀L2. ❪G,L0❫ ⊢⬈[T0] L2 → ❪L2,T1❫ ⊆ ❪L0,T1❫.
-/3 width=5 by rpx_cpx_conf, rpx_fsge_comp/ qed-.
+/3 width=5 by rpx_cpx_conf_sn, rpx_fsge_comp/ qed-.
(**************************************************************************)
include "static_2/static/rex_lex.ma".
-include "basic_2/rt_transition/rpx_fsle.ma".
+include "basic_2/rt_transition/cpx_req.ma".
include "basic_2/rt_transition/lpx.ma".
(* EXTENDED PARALLEL RT-TRANSITION FOR REFERRED LOCAL ENVIRONMENTS **********)
(* Properties with syntactic equivalence for referred local environments ****)
-lemma fleq_rpx (G):
- ∀L1,L2,T. L1 ≡[T] L2 → ❪G,L1❫ ⊢ ⬈[T] L2.
+lemma req_rpx (G) (T):
+ ∀L1,L2. L1 ≡[T] L2 → ❪G,L1❫ ⊢ ⬈[T] L2.
/2 width=1 by req_fwd_rex/ qed.
(* Properties with extended rt-transition for full local envs ***************)
-lemma lpx_rpx (G):
- ∀L1,L2,T. ❪G,L1❫ ⊢ ⬈ L2 → ❪G,L1❫ ⊢ ⬈[T] L2.
+lemma lpx_rpx (G) (T):
+ ∀L1,L2. ❪G,L1❫ ⊢ ⬈ L2 → ❪G,L1❫ ⊢ ⬈[T] L2.
/2 width=1 by rex_lex/ qed.
(* Inversion lemmas with extended rt-transition for full local envs *********)
-lemma rpx_inv_lpx_req (G):
- ∀L1,L2,T. ❪G,L1❫ ⊢ ⬈[T] L2 →
+lemma rpx_inv_req_lpx (G) (T):
+ ∀L1,L2. ❪G,L1❫ ⊢ ⬈[T] L2 →
+ ∃∃L. L1 ≡[T] L & ❪G,L❫ ⊢ ⬈ L2.
+/4 width=13 by cpx_req_conf, rex_inv_req_lex, rex_conf1_next/ qed-.
+
+(* Forward lemmas with extended rt-transition for full local envs ***********)
+
+lemma rpx_fwd_lpx_req (G) (T):
+ ∀L1,L2. ❪G,L1❫ ⊢ ⬈[T] L2 →
∃∃L. ❪G,L1❫ ⊢ ⬈ L & L ≡[T] L2.
-/3 width=3 by rpx_fsge_comp, rex_inv_lex_req/ qed-.
+/3 width=3 by rpx_fsge_comp, rex_fwd_lex_req/ qed-.
∃∃K2. ❪G,K1❫ ⊢ ⬈[ⓑ[p,I]V.T] K2 & K2.ⓧ ≛[T] L2.
/3 width=5 by rpx_fsge_comp, rex_bind_dx_split_void/ qed-.
-lemma rpx_teqx_conf (G): s_r_confluent1 … cdeq (rpx G).
-/2 width=5 by teqx_rex_conf/ qed-.
+lemma rpx_teqx_conf_sn (G): s_r_confluent1 … cdeq (rpx G).
+/2 width=5 by teqx_rex_conf_sn/ qed-.
lemma rpx_teqx_div (G):
∀T1,T2. T1 ≛ T2 → ∀L1,L2. ❪G,L1❫ ⊢ ⬈[T2] L2 → ❪G,L1❫ ⊢ ⬈[T1] L2.
(* Properties with generic extension of a context sensitive relation ********)
-lemma rexs_lex (R): c_reflexive … R →
+lemma rexs_lex (R):
+ c_reflexive … R →
∀L1,L2,T. L1 ⪤[CTC … R] L2 → L1 ⪤*[R,T] L2.
#R #HR #L1 #L2 #T *
/5 width=7 by rexs_tc, sex_inv_tc_dx, sex_co, ext2_inv_tc, ext2_refl/
qed.
-lemma rexs_lex_req (R): c_reflexive … R →
+lemma rexs_lex_req (R):
+ c_reflexive … R →
∀L1,L. L1 ⪤[CTC … R] L → ∀L2,T. L ≡[T] L2 → L1 ⪤*[R,T] L2.
/3 width=3 by rexs_lex, rexs_step_dx, req_fwd_rex/ qed.
(* Note: s_rs_transitive_lex_inv_isid could be invoked in the last auto but makes it too slow *)
lemma rexs_inv_lex_req (R):
c_reflexive … R → rex_fsge_compatible R →
- s_rs_transitive … R (λ_.lex R) → req_transitive R →
+ s_rs_transitive … R (λ_.lex R) → R_transitive_req R →
∀L1,L2,T. L1 ⪤*[R,T] L2 →
∃∃L. L1 ⪤[CTC … R] L & L ≡[T] L2.
#R #H1R #H2R #H3R #H4R #L1 #L2 #T #H
[ /4 width=3 by req_refl, lex_refl, inj, ex2_intro/
| #L0 #L2 #_ #HL02 * #L * #f0 #Hf0 #HL1 #HL0
lapply (req_rex_trans … HL0 … HL02) -L0 // * #f1 #Hf1 #HL2
- elim (sex_sdj_split … ceq_ext … HL2 f0 ?) -HL2
+ elim (sex_sdj_split_sn … ceq_ext … HL2 f0 ?) -HL2
[ #L0 #HL0 #HL02 |*: /2 width=1 by ext2_refl, sdj_isid_dx/ ]
lapply (sex_sdj … HL0 f1 ?) /2 width=1 by sdj_isid_sn/ #H
elim (frees_sex_conf_fsge … Hf1 … H) // -H2R -H #f2 #Hf2 #Hf21
(* Properties with entrywise extension of context-sensitive relations *******)
(**) (* changed after commit 13218 *)
-lemma sex_co_dropable_sn: ∀RN,RP. co_dropable_sn (sex RN RP).
+lemma sex_co_dropable_sn (RN) (RP):
+ co_dropable_sn (sex RN RP).
#RN #RP #b #f #L1 #K1 #H elim H -f -L1 -K1
[ #f #Hf #_ #f2 #X #H #f1 #Hf2 >(sex_inv_atom1 … H) -X
/4 width=3 by sex_atom, drops_atom, ex2_intro/
]
qed-.
-lemma sex_liftable_co_dedropable_bi: ∀RN,RP. d_liftable2_sn … liftsb RN → d_liftable2_sn … liftsb RP →
- ∀f2,L1,L2. L1 ⪤[cfull,RP,f2] L2 → ∀f1,K1,K2. K1 ⪤[RN,RP,f1] K2 →
- ∀b,f. ⇩*[b,f] L1 ≘ K1 → ⇩*[b,f] L2 ≘ K2 →
- f ~⊚ f1 ≘ f2 → L1 ⪤[RN,RP,f2] L2.
+lemma sex_liftable_co_dedropable_bi (RN) (RP):
+ d_liftable2_sn … liftsb RN → d_liftable2_sn … liftsb RP →
+ ∀f2,L1,L2. L1 ⪤[cfull,RP,f2] L2 → ∀f1,K1,K2. K1 ⪤[RN,RP,f1] K2 →
+ ∀b,f. ⇩*[b,f] L1 ≘ K1 → ⇩*[b,f] L2 ≘ K2 →
+ f ~⊚ f1 ≘ f2 → L1 ⪤[RN,RP,f2] L2.
#RN #RP #HRN #HRP #f2 #L1 #L2 #H elim H -f2 -L1 -L2 //
#g2 #I1 #I2 #L1 #L2 #HL12 #HI12 #IH #f1 #Y1 #Y2 #HK12 #b #f #HY1 #HY2 #H
[ elim (coafter_inv_xxn … H) [ |*: // ] -H #g #g1 #Hg2 #H1 #H2 destruct
]
qed-.
-lemma sex_liftable_co_dedropable_sn: ∀RN,RP. (∀L. reflexive … (RN L)) → (∀L. reflexive … (RP L)) →
- d_liftable2_sn … liftsb RN → d_liftable2_sn … liftsb RP →
- co_dedropable_sn (sex RN RP).
+lemma sex_liftable_co_dedropable_sn (RN) (RP):
+ (∀L. reflexive … (RN L)) → (∀L. reflexive … (RP L)) →
+ d_liftable2_sn … liftsb RN → d_liftable2_sn … liftsb RP →
+ co_dedropable_sn (sex RN RP).
#RN #RP #H1RN #H1RP #H2RN #H2RP #b #f #L1 #K1 #H elim H -f -L1 -K1
[ #f #Hf #X #f1 #H #f2 #Hf2 >(sex_inv_atom1 … H) -X
/4 width=4 by drops_atom, sex_atom, ex3_intro/
]
qed-.
-fact sex_dropable_dx_aux: ∀RN,RP,b,f,L2,K2. ⇩*[b,f] L2 ≘ K2 → 𝐔❪f❫ →
- ∀f2,L1. L1 ⪤[RN,RP,f2] L2 → ∀f1. f ~⊚ f1 ≘ f2 →
- ∃∃K1. ⇩*[b,f] L1 ≘ K1 & K1 ⪤[RN,RP,f1] K2.
+fact sex_dropable_dx_aux (RN) (RP):
+ ∀b,f,L2,K2. ⇩*[b,f] L2 ≘ K2 → 𝐔❪f❫ →
+ ∀f2,L1. L1 ⪤[RN,RP,f2] L2 → ∀f1. f ~⊚ f1 ≘ f2 →
+ ∃∃K1. ⇩*[b,f] L1 ≘ K1 & K1 ⪤[RN,RP,f1] K2.
#RN #RP #b #f #L2 #K2 #H elim H -f -L2 -K2
[ #f #Hf #_ #f2 #X #H #f1 #Hf2 lapply (sex_inv_atom2 … H) -H
#H destruct /4 width=3 by sex_atom, drops_atom, ex2_intro/
]
qed-.
-lemma sex_co_dropable_dx: ∀RN,RP. co_dropable_dx (sex RN RP).
+lemma sex_co_dropable_dx (RN) (RP):
+ co_dropable_dx (sex RN RP).
/2 width=5 by sex_dropable_dx_aux/ qed-.
-lemma sex_drops_conf_next: ∀RN,RP.
- ∀f2,L1,L2. L1 ⪤[RN,RP,f2] L2 →
- ∀b,f,I1,K1. ⇩*[b,f] L1 ≘ K1.ⓘ[I1] → 𝐔❪f❫ →
- ∀f1. f ~⊚ ↑f1 ≘ f2 →
- ∃∃I2,K2. ⇩*[b,f] L2 ≘ K2.ⓘ[I2] & K1 ⪤[RN,RP,f1] K2 & RN K1 I1 I2.
+lemma sex_drops_conf_next (RN) (RP):
+ ∀f2,L1,L2. L1 ⪤[RN,RP,f2] L2 →
+ ∀b,f,I1,K1. ⇩*[b,f] L1 ≘ K1.ⓘ[I1] → 𝐔❪f❫ →
+ ∀f1. f ~⊚ ↑f1 ≘ f2 →
+ ∃∃I2,K2. ⇩*[b,f] L2 ≘ K2.ⓘ[I2] & K1 ⪤[RN,RP,f1] K2 & RN K1 I1 I2.
#RN #RP #f2 #L1 #L2 #HL12 #b #f #I1 #K1 #HLK1 #Hf #f1 #Hf2
elim (sex_co_dropable_sn … HLK1 … Hf … HL12 … Hf2) -L1 -f2 -Hf
#X #HX #HLK2 elim (sex_inv_next1 … HX) -HX
#I2 #K2 #HK12 #HI12 #H destruct /2 width=5 by ex3_2_intro/
qed-.
-lemma sex_drops_conf_push: ∀RN,RP.
- ∀f2,L1,L2. L1 ⪤[RN,RP,f2] L2 →
- ∀b,f,I1,K1. ⇩*[b,f] L1 ≘ K1.ⓘ[I1] → 𝐔❪f❫ →
- ∀f1. f ~⊚ ⫯f1 ≘ f2 →
- ∃∃I2,K2. ⇩*[b,f] L2 ≘ K2.ⓘ[I2] & K1 ⪤[RN,RP,f1] K2 & RP K1 I1 I2.
+lemma sex_drops_conf_push (RN) (RP):
+ ∀f2,L1,L2. L1 ⪤[RN,RP,f2] L2 →
+ ∀b,f,I1,K1. ⇩*[b,f] L1 ≘ K1.ⓘ[I1] → 𝐔❪f❫ →
+ ∀f1. f ~⊚ ⫯f1 ≘ f2 →
+ ∃∃I2,K2. ⇩*[b,f] L2 ≘ K2.ⓘ[I2] & K1 ⪤[RN,RP,f1] K2 & RP K1 I1 I2.
#RN #RP #f2 #L1 #L2 #HL12 #b #f #I1 #K1 #HLK1 #Hf #f1 #Hf2
elim (sex_co_dropable_sn … HLK1 … Hf … HL12 … Hf2) -L1 -f2 -Hf
#X #HX #HLK2 elim (sex_inv_push1 … HX) -HX
#I2 #K2 #HK12 #HI12 #H destruct /2 width=5 by ex3_2_intro/
qed-.
-lemma sex_drops_trans_next: ∀RN,RP,f2,L1,L2. L1 ⪤[RN,RP,f2] L2 →
- ∀b,f,I2,K2. ⇩*[b,f] L2 ≘ K2.ⓘ[I2] → 𝐔❪f❫ →
- ∀f1. f ~⊚ ↑f1 ≘ f2 →
- ∃∃I1,K1. ⇩*[b,f] L1 ≘ K1.ⓘ[I1] & K1 ⪤[RN,RP,f1] K2 & RN K1 I1 I2.
+lemma sex_drops_trans_next (RN) (RP):
+ ∀f2,L1,L2. L1 ⪤[RN,RP,f2] L2 →
+ ∀b,f,I2,K2. ⇩*[b,f] L2 ≘ K2.ⓘ[I2] → 𝐔❪f❫ →
+ ∀f1. f ~⊚ ↑f1 ≘ f2 →
+ ∃∃I1,K1. ⇩*[b,f] L1 ≘ K1.ⓘ[I1] & K1 ⪤[RN,RP,f1] K2 & RN K1 I1 I2.
#RN #RP #f2 #L1 #L2 #HL12 #b #f #I2 #K2 #HLK2 #Hf #f1 #Hf2
elim (sex_co_dropable_dx … HL12 … HLK2 … Hf … Hf2) -L2 -f2 -Hf
#X #HLK1 #HX elim (sex_inv_next2 … HX) -HX
#I1 #K1 #HK12 #HI12 #H destruct /2 width=5 by ex3_2_intro/
qed-.
-lemma sex_drops_trans_push: ∀RN,RP,f2,L1,L2. L1 ⪤[RN,RP,f2] L2 →
- ∀b,f,I2,K2. ⇩*[b,f] L2 ≘ K2.ⓘ[I2] → 𝐔❪f❫ →
- ∀f1. f ~⊚ ⫯f1 ≘ f2 →
- ∃∃I1,K1. ⇩*[b,f] L1 ≘ K1.ⓘ[I1] & K1 ⪤[RN,RP,f1] K2 & RP K1 I1 I2.
+lemma sex_drops_trans_push (RN) (RP): ∀f2,L1,L2. L1 ⪤[RN,RP,f2] L2 →
+ ∀b,f,I2,K2. ⇩*[b,f] L2 ≘ K2.ⓘ[I2] → 𝐔❪f❫ →
+ ∀f1. f ~⊚ ⫯f1 ≘ f2 →
+ ∃∃I1,K1. ⇩*[b,f] L1 ≘ K1.ⓘ[I1] & K1 ⪤[RN,RP,f1] K2 & RP K1 I1 I2.
#RN #RP #f2 #L1 #L2 #HL12 #b #f #I2 #K2 #HLK2 #Hf #f1 #Hf2
elim (sex_co_dropable_dx … HL12 … HLK2 … Hf … Hf2) -L2 -f2 -Hf
#X #HLK1 #HX elim (sex_inv_push2 … HX) -HX
#I1 #K1 #HK12 #HI12 #H destruct /2 width=5 by ex3_2_intro/
qed-.
-lemma drops_sex_trans_next: ∀RN,RP. (∀L. reflexive ? (RN L)) → (∀L. reflexive ? (RP L)) →
- d_liftable2_sn … liftsb RN → d_liftable2_sn … liftsb RP →
- ∀f1,K1,K2. K1 ⪤[RN,RP,f1] K2 →
- ∀b,f,I1,L1. ⇩*[b,f] L1.ⓘ[I1] ≘ K1 →
- ∀f2. f ~⊚ f1 ≘ ↑f2 →
- ∃∃I2,L2. ⇩*[b,f] L2.ⓘ[I2] ≘ K2 & L1 ⪤[RN,RP,f2] L2 & RN L1 I1 I2 & L1.ⓘ[I1] ≡[f] L2.ⓘ[I2].
+lemma drops_sex_trans_next (RN) (RP):
+ (∀L. reflexive ? (RN L)) → (∀L. reflexive ? (RP L)) →
+ d_liftable2_sn … liftsb RN → d_liftable2_sn … liftsb RP →
+ ∀f1,K1,K2. K1 ⪤[RN,RP,f1] K2 →
+ ∀b,f,I1,L1. ⇩*[b,f] L1.ⓘ[I1] ≘ K1 →
+ ∀f2. f ~⊚ f1 ≘ ↑f2 →
+ ∃∃I2,L2. ⇩*[b,f] L2.ⓘ[I2] ≘ K2 & L1 ⪤[RN,RP,f2] L2 & RN L1 I1 I2 & L1.ⓘ[I1] ≡[f] L2.ⓘ[I2].
#RN #RP #H1RN #H1RP #H2RN #H2RP #f1 #K1 #K2 #HK12 #b #f #I1 #L1 #HLK1 #f2 #Hf2
elim (sex_liftable_co_dedropable_sn … H1RN H1RP H2RN H2RP … HLK1 … HK12 … Hf2) -K1 -f1 -H1RN -H1RP -H2RN -H2RP
#X #HX #HLK2 #H1L12 elim (sex_inv_next1 … HX) -HX
#I2 #L2 #H2L12 #HI12 #H destruct /2 width=6 by ex4_2_intro/
qed-.
-lemma drops_sex_trans_push: ∀RN,RP. (∀L. reflexive ? (RN L)) → (∀L. reflexive ? (RP L)) →
- d_liftable2_sn … liftsb RN → d_liftable2_sn … liftsb RP →
- ∀f1,K1,K2. K1 ⪤[RN,RP,f1] K2 →
- ∀b,f,I1,L1. ⇩*[b,f] L1.ⓘ[I1] ≘ K1 →
- ∀f2. f ~⊚ f1 ≘ ⫯f2 →
- ∃∃I2,L2. ⇩*[b,f] L2.ⓘ[I2] ≘ K2 & L1 ⪤[RN,RP,f2] L2 & RP L1 I1 I2 & L1.ⓘ[I1] ≡[f] L2.ⓘ[I2].
+lemma drops_sex_trans_push (RN) (RP):
+ (∀L. reflexive ? (RN L)) → (∀L. reflexive ? (RP L)) →
+ d_liftable2_sn … liftsb RN → d_liftable2_sn … liftsb RP →
+ ∀f1,K1,K2. K1 ⪤[RN,RP,f1] K2 →
+ ∀b,f,I1,L1. ⇩*[b,f] L1.ⓘ[I1] ≘ K1 →
+ ∀f2. f ~⊚ f1 ≘ ⫯f2 →
+ ∃∃I2,L2. ⇩*[b,f] L2.ⓘ[I2] ≘ K2 & L1 ⪤[RN,RP,f2] L2 & RP L1 I1 I2 & L1.ⓘ[I1] ≡[f] L2.ⓘ[I2].
#RN #RP #H1RN #H1RP #H2RN #H2RP #f1 #K1 #K2 #HK12 #b #f #I1 #L1 #HLK1 #f2 #Hf2
elim (sex_liftable_co_dedropable_sn … H1RN H1RP H2RN H2RP … HLK1 … HK12 … Hf2) -K1 -f1 -H1RN -H1RP -H2RN -H2RP
#X #HX #HLK2 #H1L12 elim (sex_inv_push1 … HX) -HX
#I2 #L2 #H2L12 #HI12 #H destruct /2 width=6 by ex4_2_intro/
qed-.
-lemma drops_atom2_sex_conf: ∀RN,RP,b,f1,L1. ⇩*[b,f1] L1 ≘ ⋆ → 𝐔❪f1❫ →
- ∀f,L2. L1 ⪤[RN,RP,f] L2 →
- ∀f2. f1 ~⊚ f2 ≘f → ⇩*[b,f1] L2 ≘ ⋆.
+lemma drops_atom2_sex_conf (RN) (RP):
+ ∀b,f1,L1. ⇩*[b,f1] L1 ≘ ⋆ → 𝐔❪f1❫ →
+ ∀f,L2. L1 ⪤[RN,RP,f] L2 →
+ ∀f2. f1 ~⊚ f2 ≘f → ⇩*[b,f1] L2 ≘ ⋆.
#RN #RP #b #f1 #L1 #H1 #Hf1 #f #L2 #H2 #f2 #H3
elim (sex_co_dropable_sn … H1 … H2 … H3) // -H1 -H2 -H3 -Hf1
#L #H #HL2 lapply (sex_inv_atom1 … H) -H //
qed-.
+
+lemma sex_sdj_split_dx (R1) (R2) (RP):
+ c_reflexive … R1 → c_reflexive … R2 → c_reflexive … RP →
+ ∀L1,f1.
+ (∀g,I,K,n. ⇩[n] L1 ≘ K.ⓘ[I] → ↑g = ⫱*[n] f1 → R_pw_confluent1_sex R1 R1 R2 cfull g K I) →
+ ∀L2. L1 ⪤[R1,RP,f1] L2 → ∀f2. f1 ∥ f2 →
+ ∃∃L. L1 ⪤[R2,cfull,f1] L & L ⪤[RP,R1,f2] L2.
+#R1 #R2 #RP #HR1 #HR2 #HRP #L1 elim L1 -L1
+[ #f1 #_ #L2 #H #f2 #_
+ lapply (sex_inv_atom1 … H) -H #H destruct
+ /2 width=3 by sex_atom, ex2_intro/
+| #K1 #I1 #IH #f1 elim (pn_split f1) * #g1 #H destruct
+ #HR #L2 #H #f2 #Hf
+ [ elim (sex_inv_push1 … H) -H #I2 #K2 #HK12 #HI12 #H destruct
+ elim (sdj_inv_px … Hf ??) -Hf [1,3: * |*: // ] #g2 #Hg #H destruct
+ elim (IH … HK12 … Hg) -IH -HK12 -Hg
+ [1,3: /3 width=5 by sex_next, sex_push, ex2_intro/
+ |2,4: /3 width=3 by drops_drop/
+ ]
+ | elim (sex_inv_next1 … H) -H #I2 #K2 #HK12 #HI12 #H destruct
+ elim (sdj_inv_nx … Hf ??) -Hf [|*: // ] #g2 #Hg #H destruct
+ elim (IH … HK12 … Hg) -IH -HK12 -Hg
+ [ /5 width=11 by sex_next, sex_push, drops_refl, ex2_intro/
+ | /3 width=3 by drops_drop/
+ ]
+ ]
+]
+qed-.
sex RN RP (⫯f) (L1.ⓘ[I1]) (L2.ⓘ[I2])
.
-interpretation "generic entrywise extension (local environment)"
- 'Relation RN RP f L1 L2 = (sex RN RP f L1 L2).
-
-definition sex_transitive: relation3 lenv bind bind → relation3 lenv bind bind →
- relation3 lenv bind bind →
- relation3 lenv bind bind → relation3 lenv bind bind →
- relation3 rtmap lenv bind ≝
- λR1,R2,R3,RN,RP,f,L1,I1.
- ∀I. R1 L1 I1 I → ∀L2. L1 ⪤[RN,RP,f] L2 →
- ∀I2. R2 L2 I I2 → R3 L1 I1 I2.
-
-definition R_pw_confluent2_sex: relation3 lenv bind bind → relation3 lenv bind bind →
- relation3 lenv bind bind → relation3 lenv bind bind →
- relation3 lenv bind bind → relation3 lenv bind bind →
- relation3 rtmap lenv bind ≝
- λR1,R2,RN1,RP1,RN2,RP2,f,L0,I0.
- ∀I1. R1 L0 I0 I1 → ∀I2. R2 L0 I0 I2 →
- ∀L1. L0 ⪤[RN1,RP1,f] L1 → ∀L2. L0 ⪤[RN2,RP2,f] L2 →
- ∃∃I. R2 L1 I1 I & R1 L2 I2 I.
-
-definition R_pw_replace3_sex: relation3 lenv bind bind → relation3 lenv bind bind →
- relation3 lenv bind bind → relation3 lenv bind bind →
- relation3 lenv bind bind → relation3 lenv bind bind →
- relation3 rtmap lenv bind ≝
- λR1,R2,RN1,RP1,RN2,RP2,f,L0,I0.
- ∀I1. R1 L0 I0 I1 → ∀I2. R2 L0 I0 I2 →
- ∀L1. L0 ⪤[RN1,RP1,f] L1 → ∀L2. L0 ⪤[RN2,RP2,f] L2 →
- ∀I. R2 L1 I1 I → R1 L2 I2 I.
+interpretation
+ "generic entrywise extension (local environment)"
+ 'Relation RN RP f L1 L2 = (sex RN RP f L1 L2).
+
+definition R_pw_transitive_sex:
+ relation3 lenv bind bind → relation3 lenv bind bind →
+ relation3 lenv bind bind →
+ relation3 lenv bind bind → relation3 lenv bind bind →
+ relation3 rtmap lenv bind ≝
+ λR1,R2,R3,RN,RP,f,L1,I1.
+ ∀I. R1 L1 I1 I → ∀L2. L1 ⪤[RN,RP,f] L2 →
+ ∀I2. R2 L2 I I2 → R3 L1 I1 I2.
+
+definition R_pw_confluent1_sex:
+ relation3 lenv bind bind → relation3 lenv bind bind →
+ relation3 lenv bind bind → relation3 lenv bind bind →
+ relation3 rtmap lenv bind ≝
+ λR1,R2,RN,RP,f,L1,I1.
+ ∀I2. R1 L1 I1 I2 → ∀L2. L1 ⪤[RN,RP,f] L2 → R2 L2 I1 I2.
+
+definition R_pw_confluent2_sex:
+ relation3 lenv bind bind → relation3 lenv bind bind →
+ relation3 lenv bind bind → relation3 lenv bind bind →
+ relation3 lenv bind bind → relation3 lenv bind bind →
+ relation3 rtmap lenv bind ≝
+ λR1,R2,RN1,RP1,RN2,RP2,f,L0,I0.
+ ∀I1. R1 L0 I0 I1 → ∀I2. R2 L0 I0 I2 →
+ ∀L1. L0 ⪤[RN1,RP1,f] L1 → ∀L2. L0 ⪤[RN2,RP2,f] L2 →
+ ∃∃I. R2 L1 I1 I & R1 L2 I2 I.
+
+definition R_pw_replace3_sex:
+ relation3 lenv bind bind → relation3 lenv bind bind →
+ relation3 lenv bind bind → relation3 lenv bind bind →
+ relation3 lenv bind bind → relation3 lenv bind bind →
+ relation3 rtmap lenv bind ≝
+ λR1,R2,RN1,RP1,RN2,RP2,f,L0,I0.
+ ∀I1. R1 L0 I0 I1 → ∀I2. R2 L0 I0 I2 →
+ ∀L1. L0 ⪤[RN1,RP1,f] L1 → ∀L2. L0 ⪤[RN2,RP2,f] L2 →
+ ∀I. R2 L1 I1 I → R1 L2 I2 I.
(* Basic inversion lemmas ***************************************************)
-fact sex_inv_atom1_aux: ∀RN,RP,f,X,Y. X ⪤[RN,RP,f] Y → X = ⋆ → Y = ⋆.
+fact sex_inv_atom1_aux (RN) (RP):
+ ∀f,X,Y. X ⪤[RN,RP,f] Y → X = ⋆ → Y = ⋆.
#RN #RP #f #X #Y * -f -X -Y //
#f #I1 #I2 #L1 #L2 #_ #_ #H destruct
qed-.
(* Basic_2A1: includes lpx_sn_inv_atom1 *)
-lemma sex_inv_atom1: ∀RN,RP,f,Y. ⋆ ⪤[RN,RP,f] Y → Y = ⋆.
+lemma sex_inv_atom1 (RN) (RP):
+ ∀f,Y. ⋆ ⪤[RN,RP,f] Y → Y = ⋆.
/2 width=6 by sex_inv_atom1_aux/ qed-.
-fact sex_inv_next1_aux: ∀RN,RP,f,X,Y. X ⪤[RN,RP,f] Y → ∀g,J1,K1. X = K1.ⓘ[J1] → f = ↑g →
- ∃∃J2,K2. K1 ⪤[RN,RP,g] K2 & RN K1 J1 J2 & Y = K2.ⓘ[J2].
+fact sex_inv_next1_aux (RN) (RP):
+ ∀f,X,Y. X ⪤[RN,RP,f] Y → ∀g,J1,K1. X = K1.ⓘ[J1] → f = ↑g →
+ ∃∃J2,K2. K1 ⪤[RN,RP,g] K2 & RN K1 J1 J2 & Y = K2.ⓘ[J2].
#RN #RP #f #X #Y * -f -X -Y
[ #f #g #J1 #K1 #H destruct
| #f #I1 #I2 #L1 #L2 #HL #HI #g #J1 #K1 #H1 #H2 <(injective_next … H2) -g destruct
qed-.
(* Basic_2A1: includes lpx_sn_inv_pair1 *)
-lemma sex_inv_next1: ∀RN,RP,g,J1,K1,Y. K1.ⓘ[J1] ⪤[RN,RP,↑g] Y →
- ∃∃J2,K2. K1 ⪤[RN,RP,g] K2 & RN K1 J1 J2 & Y = K2.ⓘ[J2].
+lemma sex_inv_next1 (RN) (RP):
+ ∀g,J1,K1,Y. K1.ⓘ[J1] ⪤[RN,RP,↑g] Y →
+ ∃∃J2,K2. K1 ⪤[RN,RP,g] K2 & RN K1 J1 J2 & Y = K2.ⓘ[J2].
/2 width=7 by sex_inv_next1_aux/ qed-.
-fact sex_inv_push1_aux: ∀RN,RP,f,X,Y. X ⪤[RN,RP,f] Y → ∀g,J1,K1. X = K1.ⓘ[J1] → f = ⫯g →
- ∃∃J2,K2. K1 ⪤[RN,RP,g] K2 & RP K1 J1 J2 & Y = K2.ⓘ[J2].
+fact sex_inv_push1_aux (RN) (RP):
+ ∀f,X,Y. X ⪤[RN,RP,f] Y → ∀g,J1,K1. X = K1.ⓘ[J1] → f = ⫯g →
+ ∃∃J2,K2. K1 ⪤[RN,RP,g] K2 & RP K1 J1 J2 & Y = K2.ⓘ[J2].
#RN #RP #f #X #Y * -f -X -Y
[ #f #g #J1 #K1 #H destruct
| #f #I1 #I2 #L1 #L2 #_ #_ #g #J1 #K1 #_ #H elim (discr_next_push … H)
]
qed-.
-lemma sex_inv_push1: ∀RN,RP,g,J1,K1,Y. K1.ⓘ[J1] ⪤[RN,RP,⫯g] Y →
- ∃∃J2,K2. K1 ⪤[RN,RP,g] K2 & RP K1 J1 J2 & Y = K2.ⓘ[J2].
+lemma sex_inv_push1 (RN) (RP):
+ ∀g,J1,K1,Y. K1.ⓘ[J1] ⪤[RN,RP,⫯g] Y →
+ ∃∃J2,K2. K1 ⪤[RN,RP,g] K2 & RP K1 J1 J2 & Y = K2.ⓘ[J2].
/2 width=7 by sex_inv_push1_aux/ qed-.
-fact sex_inv_atom2_aux: ∀RN,RP,f,X,Y. X ⪤[RN,RP,f] Y → Y = ⋆ → X = ⋆.
+fact sex_inv_atom2_aux (RN) (RP):
+ ∀f,X,Y. X ⪤[RN,RP,f] Y → Y = ⋆ → X = ⋆.
#RN #RP #f #X #Y * -f -X -Y //
#f #I1 #I2 #L1 #L2 #_ #_ #H destruct
qed-.
(* Basic_2A1: includes lpx_sn_inv_atom2 *)
-lemma sex_inv_atom2: ∀RN,RP,f,X. X ⪤[RN,RP,f] ⋆ → X = ⋆.
+lemma sex_inv_atom2 (RN) (RP):
+ ∀f,X. X ⪤[RN,RP,f] ⋆ → X = ⋆.
/2 width=6 by sex_inv_atom2_aux/ qed-.
-fact sex_inv_next2_aux: ∀RN,RP,f,X,Y. X ⪤[RN,RP,f] Y → ∀g,J2,K2. Y = K2.ⓘ[J2] → f = ↑g →
- ∃∃J1,K1. K1 ⪤[RN,RP,g] K2 & RN K1 J1 J2 & X = K1.ⓘ[J1].
+fact sex_inv_next2_aux (RN) (RP):
+ ∀f,X,Y. X ⪤[RN,RP,f] Y → ∀g,J2,K2. Y = K2.ⓘ[J2] → f = ↑g →
+ ∃∃J1,K1. K1 ⪤[RN,RP,g] K2 & RN K1 J1 J2 & X = K1.ⓘ[J1].
#RN #RP #f #X #Y * -f -X -Y
[ #f #g #J2 #K2 #H destruct
| #f #I1 #I2 #L1 #L2 #HL #HI #g #J2 #K2 #H1 #H2 <(injective_next … H2) -g destruct
qed-.
(* Basic_2A1: includes lpx_sn_inv_pair2 *)
-lemma sex_inv_next2: ∀RN,RP,g,J2,X,K2. X ⪤[RN,RP,↑g] K2.ⓘ[J2] →
- ∃∃J1,K1. K1 ⪤[RN,RP,g] K2 & RN K1 J1 J2 & X = K1.ⓘ[J1].
+lemma sex_inv_next2 (RN) (RP):
+ ∀g,J2,X,K2. X ⪤[RN,RP,↑g] K2.ⓘ[J2] →
+ ∃∃J1,K1. K1 ⪤[RN,RP,g] K2 & RN K1 J1 J2 & X = K1.ⓘ[J1].
/2 width=7 by sex_inv_next2_aux/ qed-.
-fact sex_inv_push2_aux: ∀RN,RP,f,X,Y. X ⪤[RN,RP,f] Y → ∀g,J2,K2. Y = K2.ⓘ[J2] → f = ⫯g →
- ∃∃J1,K1. K1 ⪤[RN,RP,g] K2 & RP K1 J1 J2 & X = K1.ⓘ[J1].
+fact sex_inv_push2_aux (RN) (RP):
+ ∀f,X,Y. X ⪤[RN,RP,f] Y → ∀g,J2,K2. Y = K2.ⓘ[J2] → f = ⫯g →
+ ∃∃J1,K1. K1 ⪤[RN,RP,g] K2 & RP K1 J1 J2 & X = K1.ⓘ[J1].
#RN #RP #f #X #Y * -f -X -Y
[ #f #J2 #K2 #g #H destruct
| #f #I1 #I2 #L1 #L2 #_ #_ #g #J2 #K2 #_ #H elim (discr_next_push … H)
]
qed-.
-lemma sex_inv_push2: ∀RN,RP,g,J2,X,K2. X ⪤[RN,RP,⫯g] K2.ⓘ[J2] →
- ∃∃J1,K1. K1 ⪤[RN,RP,g] K2 & RP K1 J1 J2 & X = K1.ⓘ[J1].
+lemma sex_inv_push2 (RN) (RP):
+ ∀g,J2,X,K2. X ⪤[RN,RP,⫯g] K2.ⓘ[J2] →
+ ∃∃J1,K1. K1 ⪤[RN,RP,g] K2 & RP K1 J1 J2 & X = K1.ⓘ[J1].
/2 width=7 by sex_inv_push2_aux/ qed-.
(* Basic_2A1: includes lpx_sn_inv_pair *)
-lemma sex_inv_next: ∀RN,RP,f,I1,I2,L1,L2.
- L1.ⓘ[I1] ⪤[RN,RP,↑f] L2.ⓘ[I2] →
- L1 ⪤[RN,RP,f] L2 ∧ RN L1 I1 I2.
+lemma sex_inv_next (RN) (RP):
+ ∀f,I1,I2,L1,L2.
+ L1.ⓘ[I1] ⪤[RN,RP,↑f] L2.ⓘ[I2] →
+ L1 ⪤[RN,RP,f] L2 ∧ RN L1 I1 I2.
#RN #RP #f #I1 #I2 #L1 #L2 #H elim (sex_inv_next1 … H) -H
#I0 #L0 #HL10 #HI10 #H destruct /2 width=1 by conj/
qed-.
-lemma sex_inv_push: ∀RN,RP,f,I1,I2,L1,L2.
- L1.ⓘ[I1] ⪤[RN,RP,⫯f] L2.ⓘ[I2] →
- L1 ⪤[RN,RP,f] L2 ∧ RP L1 I1 I2.
+lemma sex_inv_push (RN) (RP):
+ ∀f,I1,I2,L1,L2.
+ L1.ⓘ[I1] ⪤[RN,RP,⫯f] L2.ⓘ[I2] →
+ L1 ⪤[RN,RP,f] L2 ∧ RP L1 I1 I2.
#RN #RP #f #I1 #I2 #L1 #L2 #H elim (sex_inv_push1 … H) -H
#I0 #L0 #HL10 #HI10 #H destruct /2 width=1 by conj/
qed-.
-lemma sex_inv_tl: ∀RN,RP,f,I1,I2,L1,L2. L1 ⪤[RN,RP,⫱f] L2 →
- RN L1 I1 I2 → RP L1 I1 I2 →
- L1.ⓘ[I1] ⪤[RN,RP,f] L2.ⓘ[I2].
+lemma sex_inv_tl (RN) (RP):
+ ∀f,I1,I2,L1,L2. L1 ⪤[RN,RP,⫱f] L2 →
+ RN L1 I1 I2 → RP L1 I1 I2 →
+ L1.ⓘ[I1] ⪤[RN,RP,f] L2.ⓘ[I2].
#RN #RP #f #I1 #I2 #L2 #L2 elim (pn_split f) *
/2 width=1 by sex_next, sex_push/
qed-.
(* Basic forward lemmas *****************************************************)
-lemma sex_fwd_bind: ∀RN,RP,f,I1,I2,L1,L2.
- L1.ⓘ[I1] ⪤[RN,RP,f] L2.ⓘ[I2] →
- L1 ⪤[RN,RP,⫱f] L2.
+lemma sex_fwd_bind (RN) (RP):
+ ∀f,I1,I2,L1,L2.
+ L1.ⓘ[I1] ⪤[RN,RP,f] L2.ⓘ[I2] → L1 ⪤[RN,RP,⫱f] L2.
#RN #RP #f #I1 #I2 #L1 #L2 #Hf
elim (pn_split f) * #g #H destruct
[ elim (sex_inv_push … Hf) | elim (sex_inv_next … Hf) ] -Hf //
(* Basic properties *********************************************************)
-lemma sex_eq_repl_back: ∀RN,RP,L1,L2. eq_repl_back … (λf. L1 ⪤[RN,RP,f] L2).
+lemma sex_eq_repl_back (RN) (RP):
+ ∀L1,L2. eq_repl_back … (λf. L1 ⪤[RN,RP,f] L2).
#RN #RP #L1 #L2 #f1 #H elim H -f1 -L1 -L2 //
#f1 #I1 #I2 #L1 #L2 #_ #HI #IH #f2 #H
[ elim (eq_inv_nx … H) -H /3 width=3 by sex_next/
]
qed-.
-lemma sex_eq_repl_fwd: ∀RN,RP,L1,L2. eq_repl_fwd … (λf. L1 ⪤[RN,RP,f] L2).
+lemma sex_eq_repl_fwd (RN) (RP):
+ ∀L1,L2. eq_repl_fwd … (λf. L1 ⪤[RN,RP,f] L2).
#RN #RP #L1 #L2 @eq_repl_sym /2 width=3 by sex_eq_repl_back/ (**) (* full auto fails *)
qed-.
-lemma sex_refl: ∀RN,RP. c_reflexive … RN → c_reflexive … RP →
- ∀f.reflexive … (sex RN RP f).
+lemma sex_refl (RN) (RP):
+ c_reflexive … RN → c_reflexive … RP →
+ ∀f.reflexive … (sex RN RP f).
#RN #RP #HRN #HRP #f #L generalize in match f; -f elim L -L //
#L #I #IH #f elim (pn_split f) *
#g #H destruct /2 width=1 by sex_next, sex_push/
qed.
-lemma sex_sym: ∀RN,RP.
- (∀L1,L2,I1,I2. RN L1 I1 I2 → RN L2 I2 I1) →
- (∀L1,L2,I1,I2. RP L1 I1 I2 → RP L2 I2 I1) →
- ∀f. symmetric … (sex RN RP f).
+lemma sex_sym (RN) (RP):
+ (∀L1,L2,I1,I2. RN L1 I1 I2 → RN L2 I2 I1) →
+ (∀L1,L2,I1,I2. RP L1 I1 I2 → RP L2 I2 I1) →
+ ∀f. symmetric … (sex RN RP f).
#RN #RP #HRN #HRP #f #L1 #L2 #H elim H -L1 -L2 -f
/3 width=2 by sex_next, sex_push/
qed-.
-lemma sex_pair_repl: ∀RN,RP,f,I1,I2,L1,L2.
- L1.ⓘ[I1] ⪤[RN,RP,f] L2.ⓘ[I2] →
- ∀J1,J2. RN L1 J1 J2 → RP L1 J1 J2 →
- L1.ⓘ[J1] ⪤[RN,RP,f] L2.ⓘ[J2].
+lemma sex_pair_repl (RN) (RP):
+ ∀f,I1,I2,L1,L2.
+ L1.ⓘ[I1] ⪤[RN,RP,f] L2.ⓘ[I2] →
+ ∀J1,J2. RN L1 J1 J2 → RP L1 J1 J2 →
+ L1.ⓘ[J1] ⪤[RN,RP,f] L2.ⓘ[J2].
/3 width=3 by sex_inv_tl, sex_fwd_bind/ qed-.
-lemma sex_co: ∀RN1,RP1,RN2,RP2. RN1 ⊆ RN2 → RP1 ⊆ RP2 →
- ∀f,L1,L2. L1 ⪤[RN1,RP1,f] L2 → L1 ⪤[RN2,RP2,f] L2.
+lemma sex_co (RN1) (RP1) (RN2) (RP2):
+ RN1 ⊆ RN2 → RP1 ⊆ RP2 →
+ ∀f,L1,L2. L1 ⪤[RN1,RP1,f] L2 → L1 ⪤[RN2,RP2,f] L2.
#RN1 #RP1 #RN2 #RP2 #HRN #HRP #f #L1 #L2 #H elim H -f -L1 -L2
/3 width=1 by sex_atom, sex_next, sex_push/
qed-.
-lemma sex_co_isid: ∀RN1,RP1,RN2,RP2. RP1 ⊆ RP2 →
- ∀f,L1,L2. L1 ⪤[RN1,RP1,f] L2 → 𝐈❪f❫ →
- L1 ⪤[RN2,RP2,f] L2.
+lemma sex_co_isid (RN1) (RP1) (RN2) (RP2):
+ RP1 ⊆ RP2 →
+ ∀f,L1,L2. L1 ⪤[RN1,RP1,f] L2 → 𝐈❪f❫ →
+ L1 ⪤[RN2,RP2,f] L2.
#RN1 #RP1 #RN2 #RP2 #HR #f #L1 #L2 #H elim H -f -L1 -L2 //
#f #I1 #I2 #K1 #K2 #_ #HI12 #IH #H
[ elim (isid_inv_next … H) -H //
]
qed-.
-lemma sex_sdj: ∀RN,RP. RP ⊆ RN →
- ∀f1,L1,L2. L1 ⪤[RN,RP,f1] L2 →
- ∀f2. f1 ∥ f2 → L1 ⪤[RP,RN,f2] L2.
+lemma sex_sdj (RN) (RP):
+ RP ⊆ RN →
+ ∀f1,L1,L2. L1 ⪤[RN,RP,f1] L2 →
+ ∀f2. f1 ∥ f2 → L1 ⪤[RP,RN,f2] L2.
#RN #RP #HR #f1 #L1 #L2 #H elim H -f1 -L1 -L2 //
#f1 #I1 #I2 #L1 #L2 #_ #HI12 #IH #f2 #H12
[ elim (sdj_inv_nx … H12) -H12 [2,3: // ]
]
qed-.
-lemma sle_sex_trans: ∀RN,RP. RN ⊆ RP →
- ∀f2,L1,L2. L1 ⪤[RN,RP,f2] L2 →
- ∀f1. f1 ⊆ f2 → L1 ⪤[RN,RP,f1] L2.
+lemma sle_sex_trans (RN) (RP):
+ RN ⊆ RP →
+ ∀f2,L1,L2. L1 ⪤[RN,RP,f2] L2 →
+ ∀f1. f1 ⊆ f2 → L1 ⪤[RN,RP,f1] L2.
#RN #RP #HR #f2 #L1 #L2 #H elim H -f2 -L1 -L2 //
#f2 #I1 #I2 #L1 #L2 #_ #HI12 #IH #f1 #H12
[ elim (pn_split f1) * ]
]
qed-.
-lemma sle_sex_conf: ∀RN,RP. RP ⊆ RN →
- ∀f1,L1,L2. L1 ⪤[RN,RP,f1] L2 →
- ∀f2. f1 ⊆ f2 → L1 ⪤[RN,RP,f2] L2.
+lemma sle_sex_conf (RN) (RP):
+ RP ⊆ RN →
+ ∀f1,L1,L2. L1 ⪤[RN,RP,f1] L2 →
+ ∀f2. f1 ⊆ f2 → L1 ⪤[RN,RP,f2] L2.
#RN #RP #HR #f1 #L1 #L2 #H elim H -f1 -L1 -L2 //
#f1 #I1 #I2 #L1 #L2 #_ #HI12 #IH #f2 #H12
[2: elim (pn_split f2) * ]
]
qed-.
-lemma sex_sle_split: ∀R1,R2,RP. c_reflexive … R1 → c_reflexive … R2 →
- ∀f,L1,L2. L1 ⪤[R1,RP,f] L2 → ∀g. f ⊆ g →
- ∃∃L. L1 ⪤[R1,RP,g] L & L ⪤[R2,cfull,f] L2.
+lemma sex_sle_split_sn (R1) (R2) (RP):
+ c_reflexive … R1 → c_reflexive … R2 →
+ ∀f,L1,L2. L1 ⪤[R1,RP,f] L2 → ∀g. f ⊆ g →
+ ∃∃L. L1 ⪤[R1,RP,g] L & L ⪤[R2,cfull,f] L2.
#R1 #R2 #RP #HR1 #HR2 #f #L1 #L2 #H elim H -f -L1 -L2
[ /2 width=3 by sex_atom, ex2_intro/ ]
#f #I1 #I2 #L1 #L2 #_ #HI12 #IH #y #H
]
qed-.
-lemma sex_sdj_split: ∀R1,R2,RP. c_reflexive … R1 → c_reflexive … R2 →
- ∀f,L1,L2. L1 ⪤[R1,RP,f] L2 → ∀g. f ∥ g →
- ∃∃L. L1 ⪤[RP,R1,g] L & L ⪤[R2,cfull,f] L2.
+lemma sex_sdj_split_sn (R1) (R2) (RP):
+ c_reflexive … R1 → c_reflexive … R2 →
+ ∀f,L1,L2. L1 ⪤[R1,RP,f] L2 → ∀g. f ∥ g →
+ ∃∃L. L1 ⪤[RP,R1,g] L & L ⪤[R2,cfull,f] L2.
#R1 #R2 #RP #HR1 #HR2 #f #L1 #L2 #H elim H -f -L1 -L2
[ /2 width=3 by sex_atom, ex2_intro/ ]
#f #I1 #I2 #L1 #L2 #_ #HI12 #IH #y #H
]
qed-.
-lemma sex_dec: ∀RN,RP.
- (∀L,I1,I2. Decidable (RN L I1 I2)) →
- (∀L,I1,I2. Decidable (RP L I1 I2)) →
- ∀L1,L2,f. Decidable (L1 ⪤[RN,RP,f] L2).
+lemma sex_dec (RN) (RP):
+ (∀L,I1,I2. Decidable (RN L I1 I2)) →
+ (∀L,I1,I2. Decidable (RP L I1 I2)) →
+ ∀L1,L2,f. Decidable (L1 ⪤[RN,RP,f] L2).
#RN #RP #HRN #HRP #L1 elim L1 -L1 [ * | #L1 #I1 #IH * ]
[ /2 width=1 by sex_atom, or_introl/
| #L2 #I2 #f @or_intror #H
(* Main properties **********************************************************)
theorem sex_trans_gen (RN1) (RP1) (RN2) (RP2) (RN) (RP):
- ∀L1,f.
- (∀g,I,K,n. ⇩[n] L1 ≘ K.ⓘ[I] → ↑g = ⫱*[n] f → sex_transitive RN1 RN2 RN RN1 RP1 g K I) →
- (∀g,I,K,n. ⇩[n] L1 ≘ K.ⓘ[I] → ⫯g = ⫱*[n] f → sex_transitive RP1 RP2 RP RN1 RP1 g K I) →
- ∀L0. L1 ⪤[RN1,RP1,f] L0 →
- ∀L2. L0 ⪤[RN2,RP2,f] L2 →
- L1 ⪤[RN,RP,f] L2.
+ ∀L1,f.
+ (∀g,I,K,n. ⇩[n] L1 ≘ K.ⓘ[I] → ↑g = ⫱*[n] f → R_pw_transitive_sex RN1 RN2 RN RN1 RP1 g K I) →
+ (∀g,I,K,n. ⇩[n] L1 ≘ K.ⓘ[I] → ⫯g = ⫱*[n] f → R_pw_transitive_sex RP1 RP2 RP RN1 RP1 g K I) →
+ ∀L0. L1 ⪤[RN1,RP1,f] L0 →
+ ∀L2. L0 ⪤[RN2,RP2,f] L2 →
+ L1 ⪤[RN,RP,f] L2.
#RN1 #RP1 #RN2 #RP2 #RN #RP #L1 elim L1 -L1
[ #f #_ #_ #L0 #H1 #L2 #H2
lapply (sex_inv_atom1 … H1) -H1 #H destruct
]
qed-.
-theorem sex_trans (RN) (RP) (f): (∀g,I,K. sex_transitive RN RN RN RN RP g K I) →
- (∀g,I,K. sex_transitive RP RP RP RN RP g K I) →
- Transitive … (sex RN RP f).
+theorem sex_trans (RN) (RP) (f):
+ (∀g,I,K. R_pw_transitive_sex RN RN RN RN RP g K I) →
+ (∀g,I,K. R_pw_transitive_sex RP RP RP RN RP g K I) →
+ Transitive … (sex RN RP f).
/2 width=9 by sex_trans_gen/ qed-.
-theorem sex_trans_id_cfull: ∀R1,R2,R3,L1,L,f. L1 ⪤[R1,cfull,f] L → 𝐈❪f❫ →
- ∀L2. L ⪤[R2,cfull,f] L2 → L1 ⪤[R3,cfull,f] L2.
+theorem sex_trans_id_cfull (R1) (R2) (R3):
+ ∀L1,L,f. L1 ⪤[R1,cfull,f] L → 𝐈❪f❫ →
+ ∀L2. L ⪤[R2,cfull,f] L2 → L1 ⪤[R3,cfull,f] L2.
#R1 #R2 #R3 #L1 #L #f #H elim H -L1 -L -f
[ #f #Hf #L2 #H >(sex_inv_atom1 … H) -L2 // ]
#f #I1 #I #K1 #K #HK1 #_ #IH #Hf #L2 #H
qed-.
theorem sex_conf (RN1) (RP1) (RN2) (RP2):
- ∀L,f.
- (∀g,I,K,n. ⇩[n] L ≘ K.ⓘ[I] → ↑g = ⫱*[n] f → R_pw_confluent2_sex RN1 RN2 RN1 RP1 RN2 RP2 g K I) →
- (∀g,I,K,n. ⇩[n] L ≘ K.ⓘ[I] → ⫯g = ⫱*[n] f → R_pw_confluent2_sex RP1 RP2 RN1 RP1 RN2 RP2 g K I) →
- pw_confluent2 … (sex RN1 RP1 f) (sex RN2 RP2 f) L.
+ ∀L,f.
+ (∀g,I,K,n. ⇩[n] L ≘ K.ⓘ[I] → ↑g = ⫱*[n] f → R_pw_confluent2_sex RN1 RN2 RN1 RP1 RN2 RP2 g K I) →
+ (∀g,I,K,n. ⇩[n] L ≘ K.ⓘ[I] → ⫯g = ⫱*[n] f → R_pw_confluent2_sex RP1 RP2 RN1 RP1 RN2 RP2 g K I) →
+ pw_confluent2 … (sex RN1 RP1 f) (sex RN2 RP2 f) L.
#RN1 #RP1 #RN2 #RP2 #L elim L -L
[ #f #_ #_ #L1 #H1 #L2 #H2 >(sex_inv_atom1 … H1) >(sex_inv_atom1 … H2) -H2 -H1
/2 width=3 by sex_atom, ex2_intro/
]
qed-.
-theorem sex_canc_sn: ∀RN,RP,f. Transitive … (sex RN RP f) →
- symmetric … (sex RN RP f) →
- left_cancellable … (sex RN RP f).
+theorem sex_canc_sn (RN) (RP):
+ ∀f. Transitive … (sex RN RP f) → symmetric … (sex RN RP f) →
+ left_cancellable … (sex RN RP f).
/3 width=3 by/ qed-.
-theorem sex_canc_dx: ∀RN,RP,f. Transitive … (sex RN RP f) →
- symmetric … (sex RN RP f) →
- right_cancellable … (sex RN RP f).
+theorem sex_canc_dx (RN) (RP):
+ ∀f. Transitive … (sex RN RP f) → symmetric … (sex RN RP f) →
+ right_cancellable … (sex RN RP f).
/3 width=3 by/ qed-.
-lemma sex_meet: ∀RN,RP,L1,L2.
- ∀f1. L1 ⪤[RN,RP,f1] L2 →
- ∀f2. L1 ⪤[RN,RP,f2] L2 →
- ∀f. f1 ⋒ f2 ≘ f → L1 ⪤[RN,RP,f] L2.
+lemma sex_meet (RN) (RP) (L1) (L2):
+ ∀f1. L1 ⪤[RN,RP,f1] L2 →
+ ∀f2. L1 ⪤[RN,RP,f2] L2 →
+ ∀f. f1 ⋒ f2 ≘ f → L1 ⪤[RN,RP,f] L2.
#RN #RP #L1 #L2 #f1 #H elim H -f1 -L1 -L2 //
#f1 #I1 #I2 #L1 #L2 #_ #HI12 #IH #f2 #H #f #Hf
elim (pn_split f2) * #g2 #H2 destruct
] -Hf /3 width=5 by sex_next, sex_push/
qed-.
-lemma sex_join: ∀RN,RP,L1,L2.
- ∀f1. L1 ⪤[RN,RP,f1] L2 →
- ∀f2. L1 ⪤[RN,RP,f2] L2 →
- ∀f. f1 ⋓ f2 ≘ f → L1 ⪤[RN,RP,f] L2.
+lemma sex_join (RN) (RP) (L1) (L2):
+ ∀f1. L1 ⪤[RN,RP,f1] L2 →
+ ∀f2. L1 ⪤[RN,RP,f2] L2 →
+ ∀f. f1 ⋓ f2 ≘ f → L1 ⪤[RN,RP,f] L2.
#RN #RP #L1 #L2 #f1 #H elim H -f1 -L1 -L2 //
#f1 #I1 #I2 #L1 #L2 #_ #HI12 #IH #f2 #H #f #Hf
elim (pn_split f2) * #g2 #H2 destruct
.
interpretation
- "sort-irrelevant equivalence on referred entries (closure)"
- 'StarEqSn G1 L1 T1 G2 L2 T2 = (feqx G1 L1 T1 G2 L2 T2).
+ "sort-irrelevant equivalence on referred entries (closure)"
+ 'StarEqSn G1 L1 T1 G2 L2 T2 = (feqx G1 L1 T1 G2 L2 T2).
(* Basic_properties *********************************************************)
-lemma feqx_intro_dx (G): ∀L1,L2,T2. L1 ≛[T2] L2 →
- ∀T1. T1 ≛ T2 → ❪G,L1,T1❫ ≛ ❪G,L2,T2❫.
+lemma feqx_intro_dx (G):
+ ∀L1,L2,T2. L1 ≛[T2] L2 →
+ ∀T1. T1 ≛ T2 → ❪G,L1,T1❫ ≛ ❪G,L2,T2❫.
/3 width=3 by feqx_intro_sn, teqx_reqx_div/ qed.
(* Basic inversion lemmas ***************************************************)
-lemma feqx_inv_gen_sn: ∀G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ≛ ❪G2,L2,T2❫ →
- ∧∧ G1 = G2 & L1 ≛[T1] L2 & T1 ≛ T2.
+lemma feqx_inv_gen_sn:
+ ∀G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ≛ ❪G2,L2,T2❫ →
+ ∧∧ G1 = G2 & L1 ≛[T1] L2 & T1 ≛ T2.
#G1 #G2 #L1 #L2 #T1 #T2 * -G2 -L2 -T2 /2 width=1 by and3_intro/
qed-.
-lemma feqx_inv_gen_dx: ∀G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ≛ ❪G2,L2,T2❫ →
- ∧∧ G1 = G2 & L1 ≛[T2] L2 & T1 ≛ T2.
+lemma feqx_inv_gen_dx:
+ ∀G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ≛ ❪G2,L2,T2❫ →
+ ∧∧ G1 = G2 & L1 ≛[T2] L2 & T1 ≛ T2.
#G1 #G2 #L1 #L2 #T1 #T2 * -G2 -L2 -T2
-/3 width=3 by teqx_reqx_conf, and3_intro/
+/3 width=3 by teqx_reqx_conf_sn, and3_intro/
qed-.
(* Basic_2A1: removed theorems 6:
(* Properties with star-iterated structural successor for closures **********)
-lemma feqx_fqus_trans: ∀b,G1,G,L1,L,T1,T. ❪G1,L1,T1❫ ≛ ❪G,L,T❫ →
- ∀G2,L2,T2. ❪G,L,T❫ ⬂*[b] ❪G2,L2,T2❫ →
- ∃∃G,L0,T0. ❪G1,L1,T1❫ ⬂*[b] ❪G,L0,T0❫ & ❪G,L0,T0❫ ≛ ❪G2,L2,T2❫.
+lemma feqx_fqus_trans (b):
+ ∀G1,G,L1,L,T1,T. ❪G1,L1,T1❫ ≛ ❪G,L,T❫ →
+ ∀G2,L2,T2. ❪G,L,T❫ ⬂*[b] ❪G2,L2,T2❫ →
+ ∃∃G,L0,T0. ❪G1,L1,T1❫ ⬂*[b] ❪G,L0,T0❫ & ❪G,L0,T0❫ ≛ ❪G2,L2,T2❫.
#b #G1 #G #L1 #L #T1 #T #H1 #G2 #L2 #T2 #H2
elim(feqx_inv_gen_dx … H1) -H1 #HG #HL1 #HT1 destruct
elim (reqx_fqus_trans … H2 … HL1) -L #L #T0 #H2 #HT02 #HL2
elim (teqx_fqus_trans … H2 … HT1) -T #L0 #T #H2 #HT0 #HL0
-lapply (teqx_reqx_conf … HT02 … HL0) -HL0 #HL0
+lapply (teqx_reqx_conf_sn … HT02 … HL0) -HL0 #HL0
/4 width=7 by feqx_intro_dx, reqx_trans, teqx_trans, ex2_3_intro/
qed-.
(* Basic_2A1: was: lleq *)
definition req: relation3 term lenv lenv ≝
- rex ceq.
+ rex ceq.
interpretation
- "syntactic equivalence on referred entries (local environment)"
- 'IdEqSn T L1 L2 = (req T L1 L2).
+ "syntactic equivalence on referred entries (local environment)"
+ 'IdEqSn T L1 L2 = (req T L1 L2).
-(* Note: "req_transitive R" is equivalent to "rex_transitive ceq R R" *)
+(* Note: "R_transitive_req R" is equivalent to "R_transitive_rex ceq R R" *)
(* Basic_2A1: uses: lleq_transitive *)
-definition req_transitive: predicate (relation3 lenv term term) ≝
+definition R_transitive_req: predicate (relation3 lenv term term) ≝
λR. ∀L2,T1,T2. R L2 T1 T2 → ∀L1. L1 ≡[T1] L2 → R L1 T1 T2.
(* Basic inversion lemmas ***************************************************)
-lemma req_inv_bind: ∀p,I,L1,L2,V,T. L1 ≡[ⓑ[p,I]V.T] L2 →
- ∧∧ L1 ≡[V] L2 & L1.ⓑ[I]V ≡[T] L2.ⓑ[I]V.
+lemma req_inv_bind:
+ ∀p,I,L1,L2,V,T. L1 ≡[ⓑ[p,I]V.T] L2 →
+ ∧∧ L1 ≡[V] L2 & L1.ⓑ[I]V ≡[T] L2.ⓑ[I]V.
/2 width=2 by rex_inv_bind/ qed-.
-lemma req_inv_flat: ∀I,L1,L2,V,T. L1 ≡[ⓕ[I]V.T] L2 →
- ∧∧ L1 ≡[V] L2 & L1 ≡[T] L2.
+lemma req_inv_flat:
+ ∀I,L1,L2,V,T. L1 ≡[ⓕ[I]V.T] L2 →
+ ∧∧ L1 ≡[V] L2 & L1 ≡[T] L2.
/2 width=2 by rex_inv_flat/ qed-.
(* Advanced inversion lemmas ************************************************)
-lemma req_inv_zero_pair_sn: ∀I,L2,K1,V. K1.ⓑ[I]V ≡[#0] L2 →
- ∃∃K2. K1 ≡[V] K2 & L2 = K2.ⓑ[I]V.
+lemma req_inv_zero_pair_sn:
+ ∀I,L2,K1,V. K1.ⓑ[I]V ≡[#0] L2 →
+ ∃∃K2. K1 ≡[V] K2 & L2 = K2.ⓑ[I]V.
#I #L2 #K1 #V #H
elim (rex_inv_zero_pair_sn … H) -H #K2 #X #HK12 #HX #H destruct
/2 width=3 by ex2_intro/
qed-.
-lemma req_inv_zero_pair_dx: ∀I,L1,K2,V. L1 ≡[#0] K2.ⓑ[I]V →
- ∃∃K1. K1 ≡[V] K2 & L1 = K1.ⓑ[I]V.
+lemma req_inv_zero_pair_dx:
+ ∀I,L1,K2,V. L1 ≡[#0] K2.ⓑ[I]V →
+ ∃∃K1. K1 ≡[V] K2 & L1 = K1.ⓑ[I]V.
#I #L1 #K2 #V #H
elim (rex_inv_zero_pair_dx … H) -H #K1 #X #HK12 #HX #H destruct
/2 width=3 by ex2_intro/
qed-.
-lemma req_inv_lref_bind_sn: ∀I1,K1,L2,i. K1.ⓘ[I1] ≡[#↑i] L2 →
- ∃∃I2,K2. K1 ≡[#i] K2 & L2 = K2.ⓘ[I2].
+lemma req_inv_lref_bind_sn:
+ ∀I1,K1,L2,i. K1.ⓘ[I1] ≡[#↑i] L2 →
+ ∃∃I2,K2. K1 ≡[#i] K2 & L2 = K2.ⓘ[I2].
/2 width=2 by rex_inv_lref_bind_sn/ qed-.
-lemma req_inv_lref_bind_dx: ∀I2,K2,L1,i. L1 ≡[#↑i] K2.ⓘ[I2] →
- ∃∃I1,K1. K1 ≡[#i] K2 & L1 = K1.ⓘ[I1].
+lemma req_inv_lref_bind_dx:
+ ∀I2,K2,L1,i. L1 ≡[#↑i] K2.ⓘ[I2] →
+ ∃∃I1,K1. K1 ≡[#i] K2 & L1 = K1.ⓘ[I1].
/2 width=2 by rex_inv_lref_bind_dx/ qed-.
(* Basic forward lemmas *****************************************************)
(* Basic_2A1: was: llpx_sn_lrefl *)
(* Basic_2A1: this should have been lleq_fwd_llpx_sn *)
-lemma req_fwd_rex: ∀R. c_reflexive … R →
- ∀L1,L2,T. L1 ≡[T] L2 → L1 ⪤[R,T] L2.
+lemma req_fwd_rex (R):
+ c_reflexive … R →
+ ∀L1,L2,T. L1 ≡[T] L2 → L1 ⪤[R,T] L2.
#R #HR #L1 #L2 #T * #f #Hf #HL12
/4 width=7 by sex_co, cext2_co, ex2_intro/
qed-.
(* Basic_properties *********************************************************)
-lemma frees_req_conf: ∀f,L1,T. L1 ⊢ 𝐅+❪T❫ ≘ f →
- ∀L2. L1 ≡[T] L2 → L2 ⊢ 𝐅+❪T❫ ≘ f.
+lemma frees_req_conf:
+ ∀f,L1,T. L1 ⊢ 𝐅+❪T❫ ≘ f →
+ ∀L2. L1 ≡[T] L2 → L2 ⊢ 𝐅+❪T❫ ≘ f.
#f #L1 #T #H elim H -f -L1 -T
[ /2 width=3 by frees_sort/
| #f #i #Hf #L2 #H2
(* Properties with free variables inclusion for restricted closures *********)
-lemma req_fsle_comp: rex_fsle_compatible ceq.
+lemma req_fsle_comp:
+ rex_fsle_compatible ceq.
#L1 #L2 #T #HL12
elim (frees_total L1 T)
/4 width=8 by frees_req_conf, rex_fwd_length, lveq_length_eq, sle_refl, ex4_4_intro/
(* Forward lemmas with free variables inclusion for restricted closures *****)
-lemma req_rex_trans: ∀R. req_transitive R →
- ∀L1,L,T. L1 ≡[T] L → ∀L2. L ⪤[R,T] L2 → L1 ⪤[R,T] L2.
+lemma req_rex_trans (R):
+ R_transitive_req R →
+ ∀L1,L,T. L1 ≡[T] L → ∀L2. L ⪤[R,T] L2 → L1 ⪤[R,T] L2.
/4 width=16 by req_fsle_comp, rex_trans_fsle, rex_trans_next/ qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "static_2/static/rex_length.ma".
+include "static_2/static/rex_fsle.ma".
+include "static_2/static/req.ma".
+
+(* SYNTACTIC EQUIVALENCE FOR LOCAL ENVIRONMENTS ON REFERRED ENTRIES *********)
+
+(* Advanved properties with free variables inclusion ************************)
+
+lemma req_fsge_comp:
+ rex_fsge_compatible ceq.
+#L1 #L2 #T #H elim H #f1 #Hf1 #HL12
+lapply (frees_req_conf … Hf1 … H) -H
+lapply (sex_fwd_length … HL12)
+/3 width=8 by lveq_length_eq, ex4_4_intro/ (**) (* full auto fails *)
+qed-.
+
+(* Advanced properties ******************************************************)
+
+(* Basic_2A1: uses: lleq_sym *)
+lemma req_sym (T):
+ symmetric … (req T).
+/3 width=1 by req_fsge_comp, rex_sym/ qed-.
(* SORT-IRRELEVANT EQUIVALENCE FOR LOCAL ENVIRONMENTS ON REFERRED ENTRIES ***)
-definition reqx: relation3 term lenv lenv ≝
- rex cdeq.
+definition reqx: relation3 … ≝
+ rex cdeq.
interpretation
- "sort-irrelevant equivalence on referred entries (local environment)"
- 'StarEqSn T L1 L2 = (reqx T L1 L2).
+ "sort-irrelevant equivalence on referred entries (local environment)"
+ 'StarEqSn T L1 L2 = (reqx T L1 L2).
interpretation
- "sort-irrelevant ranged equivalence (local environment)"
- 'StarEqSn f L1 L2 = (sex cdeq_ext cfull f L1 L2).
+ "sort-irrelevant ranged equivalence (local environment)"
+ 'StarEqSn f L1 L2 = (sex cdeq_ext cfull f L1 L2).
(* Basic properties ***********************************************************)
-lemma frees_teqx_conf_reqx: ∀f,L1,T1. L1 ⊢ 𝐅+❪T1❫ ≘ f → ∀T2. T1 ≛ T2 →
- ∀L2. L1 ≛[f] L2 → L2 ⊢ 𝐅+❪T2❫ ≘ f.
+lemma frees_teqx_conf_reqx:
+ ∀f,L1,T1. L1 ⊢ 𝐅+❪T1❫ ≘ f → ∀T2. T1 ≛ T2 →
+ ∀L2. L1 ≛[f] L2 → L2 ⊢ 𝐅+❪T2❫ ≘ f.
#f #L1 #T1 #H elim H -f -L1 -T1
[ #f #L1 #s1 #Hf #X #H1 #L2 #_
elim (teqx_inv_sort1 … H1) -H1 #s2 #H destruct
]
qed-.
-lemma frees_teqx_conf: ∀f,L,T1. L ⊢ 𝐅+❪T1❫ ≘ f →
- ∀T2. T1 ≛ T2 → L ⊢ 𝐅+❪T2❫ ≘ f.
+lemma frees_teqx_conf:
+ ∀f,L,T1. L ⊢ 𝐅+❪T1❫ ≘ f →
+ ∀T2. T1 ≛ T2 → L ⊢ 𝐅+❪T2❫ ≘ f.
/4 width=7 by frees_teqx_conf_reqx, sex_refl, ext2_refl/ qed-.
-lemma frees_reqx_conf: ∀f,L1,T. L1 ⊢ 𝐅+❪T❫ ≘ f →
- ∀L2. L1 ≛[f] L2 → L2 ⊢ 𝐅+❪T❫ ≘ f.
+lemma frees_reqx_conf:
+ ∀f,L1,T. L1 ⊢ 𝐅+❪T❫ ≘ f →
+ ∀L2. L1 ≛[f] L2 → L2 ⊢ 𝐅+❪T❫ ≘ f.
/2 width=7 by frees_teqx_conf_reqx, teqx_refl/ qed-.
-lemma teqx_rex_conf (R): s_r_confluent1 … cdeq (rex R).
+lemma teqx_rex_conf_sn (R):
+ s_r_confluent1 … cdeq (rex R).
#R #L1 #T1 #T2 #HT12 #L2 *
/3 width=5 by frees_teqx_conf, ex2_intro/
qed-.
-lemma teqx_rex_div (R): ∀T1,T2. T1 ≛ T2 →
- ∀L1,L2. L1 ⪤[R,T2] L2 → L1 ⪤[R,T1] L2.
-/3 width=5 by teqx_rex_conf, teqx_sym/ qed-.
+lemma teqx_rex_div (R):
+ ∀T1,T2. T1 ≛ T2 →
+ ∀L1,L2. L1 ⪤[R,T2] L2 → L1 ⪤[R,T1] L2.
+/3 width=5 by teqx_rex_conf_sn, teqx_sym/ qed-.
-lemma teqx_reqx_conf: s_r_confluent1 … cdeq reqx.
-/2 width=5 by teqx_rex_conf/ qed-.
+lemma teqx_reqx_conf_sn:
+ s_r_confluent1 … cdeq reqx.
+/2 width=5 by teqx_rex_conf_sn/ qed-.
-lemma teqx_reqx_div: ∀T1,T2. T1 ≛ T2 →
- ∀L1,L2. L1 ≛[T2] L2 → L1 ≛[T1] L2.
+lemma teqx_reqx_div:
+ ∀T1,T2. T1 ≛ T2 →
+ ∀L1,L2. L1 ≛[T2] L2 → L1 ≛[T1] L2.
/2 width=5 by teqx_rex_div/ qed-.
lemma reqx_atom: ∀I. ⋆ ≛[⓪[I]] ⋆.
/2 width=1 by rex_atom/ qed.
-lemma reqx_sort: ∀I1,I2,L1,L2,s.
- L1 ≛[⋆s] L2 → L1.ⓘ[I1] ≛[⋆s] L2.ⓘ[I2].
+lemma reqx_sort:
+ ∀I1,I2,L1,L2,s.
+ L1 ≛[⋆s] L2 → L1.ⓘ[I1] ≛[⋆s] L2.ⓘ[I2].
/2 width=1 by rex_sort/ qed.
-lemma reqx_pair: ∀I,L1,L2,V1,V2.
- L1 ≛[V1] L2 → V1 ≛ V2 → L1.ⓑ[I]V1 ≛[#0] L2.ⓑ[I]V2.
+lemma reqx_pair:
+ ∀I,L1,L2,V1,V2.
+ L1 ≛[V1] L2 → V1 ≛ V2 → L1.ⓑ[I]V1 ≛[#0] L2.ⓑ[I]V2.
/2 width=1 by rex_pair/ qed.
-lemma reqx_unit: ∀f,I,L1,L2. 𝐈❪f❫ → L1 ≛[f] L2 →
- L1.ⓤ[I] ≛[#0] L2.ⓤ[I].
+lemma reqx_unit:
+ ∀f,I,L1,L2. 𝐈❪f❫ → L1 ≛[f] L2 →
+ L1.ⓤ[I] ≛[#0] L2.ⓤ[I].
/2 width=3 by rex_unit/ qed.
-lemma reqx_lref: ∀I1,I2,L1,L2,i.
- L1 ≛[#i] L2 → L1.ⓘ[I1] ≛[#↑i] L2.ⓘ[I2].
+lemma reqx_lref:
+ ∀I1,I2,L1,L2,i.
+ L1 ≛[#i] L2 → L1.ⓘ[I1] ≛[#↑i] L2.ⓘ[I2].
/2 width=1 by rex_lref/ qed.
-lemma reqx_gref: ∀I1,I2,L1,L2,l.
- L1 ≛[§l] L2 → L1.ⓘ[I1] ≛[§l] L2.ⓘ[I2].
+lemma reqx_gref:
+ ∀I1,I2,L1,L2,l.
+ L1 ≛[§l] L2 → L1.ⓘ[I1] ≛[§l] L2.ⓘ[I2].
/2 width=1 by rex_gref/ qed.
-lemma reqx_bind_repl_dx: ∀I,I1,L1,L2.∀T:term.
- L1.ⓘ[I] ≛[T] L2.ⓘ[I1] →
- ∀I2. I ≛ I2 →
- L1.ⓘ[I] ≛[T] L2.ⓘ[I2].
+lemma reqx_bind_repl_dx:
+ ∀I,I1,L1,L2.∀T:term. L1.ⓘ[I] ≛[T] L2.ⓘ[I1] →
+ ∀I2. I ≛ I2 → L1.ⓘ[I] ≛[T] L2.ⓘ[I2].
/2 width=2 by rex_bind_repl_dx/ qed-.
(* Basic inversion lemmas ***************************************************)
-lemma reqx_inv_atom_sn: ∀Y2. ∀T:term. ⋆ ≛[T] Y2 → Y2 = ⋆.
+lemma reqx_inv_atom_sn:
+ ∀Y2. ∀T:term. ⋆ ≛[T] Y2 → Y2 = ⋆.
/2 width=3 by rex_inv_atom_sn/ qed-.
-lemma reqx_inv_atom_dx: ∀Y1. ∀T:term. Y1 ≛[T] ⋆ → Y1 = ⋆.
+lemma reqx_inv_atom_dx:
+ ∀Y1. ∀T:term. Y1 ≛[T] ⋆ → Y1 = ⋆.
/2 width=3 by rex_inv_atom_dx/ qed-.
lemma reqx_inv_zero:
/3 width=9 by or3_intro0, or3_intro1, or3_intro2, ex4_5_intro, ex4_4_intro, conj/
qed-.
-lemma reqx_inv_lref: ∀Y1,Y2,i. Y1 ≛[#↑i] Y2 →
- ∨∨ ∧∧ Y1 = ⋆ & Y2 = ⋆
- | ∃∃I1,I2,L1,L2. L1 ≛[#i] L2 &
- Y1 = L1.ⓘ[I1] & Y2 = L2.ⓘ[I2].
+lemma reqx_inv_lref:
+ ∀Y1,Y2,i. Y1 ≛[#↑i] Y2 →
+ ∨∨ ∧∧ Y1 = ⋆ & Y2 = ⋆
+ | ∃∃I1,I2,L1,L2. L1 ≛[#i] L2 & Y1 = L1.ⓘ[I1] & Y2 = L2.ⓘ[I2].
/2 width=1 by rex_inv_lref/ qed-.
(* Basic_2A1: uses: lleq_inv_bind lleq_inv_bind_O *)
-lemma reqx_inv_bind: ∀p,I,L1,L2,V,T. L1 ≛[ⓑ[p,I]V.T] L2 →
- ∧∧ L1 ≛[V] L2 & L1.ⓑ[I]V ≛[T] L2.ⓑ[I]V.
+lemma reqx_inv_bind:
+ ∀p,I,L1,L2,V,T. L1 ≛[ⓑ[p,I]V.T] L2 →
+ ∧∧ L1 ≛[V] L2 & L1.ⓑ[I]V ≛[T] L2.ⓑ[I]V.
/2 width=2 by rex_inv_bind/ qed-.
(* Basic_2A1: uses: lleq_inv_flat *)
-lemma reqx_inv_flat: ∀I,L1,L2,V,T. L1 ≛[ⓕ[I]V.T] L2 →
- ∧∧ L1 ≛[V] L2 & L1 ≛[T] L2.
+lemma reqx_inv_flat:
+ ∀I,L1,L2,V,T. L1 ≛[ⓕ[I]V.T] L2 →
+ ∧∧ L1 ≛[V] L2 & L1 ≛[T] L2.
/2 width=2 by rex_inv_flat/ qed-.
(* Advanced inversion lemmas ************************************************)
-lemma reqx_inv_zero_pair_sn: ∀I,Y2,L1,V1. L1.ⓑ[I]V1 ≛[#0] Y2 →
- ∃∃L2,V2. L1 ≛[V1] L2 & V1 ≛ V2 & Y2 = L2.ⓑ[I]V2.
+lemma reqx_inv_zero_pair_sn:
+ ∀I,Y2,L1,V1. L1.ⓑ[I]V1 ≛[#0] Y2 →
+ ∃∃L2,V2. L1 ≛[V1] L2 & V1 ≛ V2 & Y2 = L2.ⓑ[I]V2.
/2 width=1 by rex_inv_zero_pair_sn/ qed-.
-lemma reqx_inv_zero_pair_dx: ∀I,Y1,L2,V2. Y1 ≛[#0] L2.ⓑ[I]V2 →
- ∃∃L1,V1. L1 ≛[V1] L2 & V1 ≛ V2 & Y1 = L1.ⓑ[I]V1.
+lemma reqx_inv_zero_pair_dx:
+ ∀I,Y1,L2,V2. Y1 ≛[#0] L2.ⓑ[I]V2 →
+ ∃∃L1,V1. L1 ≛[V1] L2 & V1 ≛ V2 & Y1 = L1.ⓑ[I]V1.
/2 width=1 by rex_inv_zero_pair_dx/ qed-.
-lemma reqx_inv_lref_bind_sn: ∀I1,Y2,L1,i. L1.ⓘ[I1] ≛[#↑i] Y2 →
- ∃∃I2,L2. L1 ≛[#i] L2 & Y2 = L2.ⓘ[I2].
+lemma reqx_inv_lref_bind_sn:
+ ∀I1,Y2,L1,i. L1.ⓘ[I1] ≛[#↑i] Y2 →
+ ∃∃I2,L2. L1 ≛[#i] L2 & Y2 = L2.ⓘ[I2].
/2 width=2 by rex_inv_lref_bind_sn/ qed-.
-lemma reqx_inv_lref_bind_dx: ∀I2,Y1,L2,i. Y1 ≛[#↑i] L2.ⓘ[I2] →
- ∃∃I1,L1. L1 ≛[#i] L2 & Y1 = L1.ⓘ[I1].
+lemma reqx_inv_lref_bind_dx:
+ ∀I2,Y1,L2,i. Y1 ≛[#↑i] L2.ⓘ[I2] →
+ ∃∃I1,L1. L1 ≛[#i] L2 & Y1 = L1.ⓘ[I1].
/2 width=2 by rex_inv_lref_bind_dx/ qed-.
(* Basic forward lemmas *****************************************************)
-lemma reqx_fwd_zero_pair: ∀I,K1,K2,V1,V2.
- K1.ⓑ[I]V1 ≛[#0] K2.ⓑ[I]V2 → K1 ≛[V1] K2.
+lemma reqx_fwd_zero_pair:
+ ∀I,K1,K2,V1,V2.
+ K1.ⓑ[I]V1 ≛[#0] K2.ⓑ[I]V2 → K1 ≛[V1] K2.
/2 width=3 by rex_fwd_zero_pair/ qed-.
(* Basic_2A1: uses: lleq_fwd_bind_sn lleq_fwd_flat_sn *)
-lemma reqx_fwd_pair_sn: ∀I,L1,L2,V,T. L1 ≛[②[I]V.T] L2 → L1 ≛[V] L2.
+lemma reqx_fwd_pair_sn:
+ ∀I,L1,L2,V,T. L1 ≛[②[I]V.T] L2 → L1 ≛[V] L2.
/2 width=3 by rex_fwd_pair_sn/ qed-.
(* Basic_2A1: uses: lleq_fwd_bind_dx lleq_fwd_bind_O_dx *)
-lemma reqx_fwd_bind_dx: ∀p,I,L1,L2,V,T.
- L1 ≛[ⓑ[p,I]V.T] L2 → L1.ⓑ[I]V ≛[T] L2.ⓑ[I]V.
+lemma reqx_fwd_bind_dx:
+ ∀p,I,L1,L2,V,T.
+ L1 ≛[ⓑ[p,I]V.T] L2 → L1.ⓑ[I]V ≛[T] L2.ⓑ[I]V.
/2 width=2 by rex_fwd_bind_dx/ qed-.
(* Basic_2A1: uses: lleq_fwd_flat_dx *)
-lemma reqx_fwd_flat_dx: ∀I,L1,L2,V,T. L1 ≛[ⓕ[I]V.T] L2 → L1 ≛[T] L2.
+lemma reqx_fwd_flat_dx:
+ ∀I,L1,L2,V,T. L1 ≛[ⓕ[I]V.T] L2 → L1 ≛[T] L2.
/2 width=3 by rex_fwd_flat_dx/ qed-.
-lemma reqx_fwd_dx: ∀I2,L1,K2. ∀T:term. L1 ≛[T] K2.ⓘ[I2] →
- ∃∃I1,K1. L1 = K1.ⓘ[I1].
+lemma reqx_fwd_dx:
+ ∀I2,L1,K2. ∀T:term. L1 ≛[T] K2.ⓘ[I2] →
+ ∃∃I1,K1. L1 = K1.ⓘ[I1].
/2 width=5 by rex_fwd_dx/ qed-.
(* Properties with extended structural successor for closures ***************)
-lemma fqu_teqx_conf: ∀b,G1,G2,L1,L2,U1,T1. ❪G1,L1,U1❫ ⬂[b] ❪G2,L2,T1❫ →
- ∀U2. U1 ≛ U2 →
- ∃∃L,T2. ❪G1,L1,U2❫ ⬂[b] ❪G2,L,T2❫ & L2 ≛[T1] L & T1 ≛ T2.
+lemma fqu_teqx_conf (b):
+ ∀G1,G2,L1,L2,U1,T1. ❪G1,L1,U1❫ ⬂[b] ❪G2,L2,T1❫ →
+ ∀U2. U1 ≛ U2 →
+ ∃∃L,T2. ❪G1,L1,U2❫ ⬂[b] ❪G2,L,T2❫ & L2 ≛[T1] L & T1 ≛ T2.
#b #G1 #G2 #L1 #L2 #U1 #T1 #H elim H -G1 -G2 -L1 -L2 -U1 -T1
[ #I #G #L #W #X #H >(teqx_inv_lref1 … H) -X
/2 width=5 by fqu_lref_O, ex3_2_intro/
]
qed-.
-lemma teqx_fqu_trans: ∀b,G1,G2,L1,L2,U1,T1. ❪G1,L1,U1❫ ⬂[b] ❪G2,L2,T1❫ →
- ∀U2. U2 ≛ U1 →
- ∃∃L,T2. ❪G1,L1,U2❫ ⬂[b] ❪G2,L,T2❫ & T2 ≛ T1 & L ≛[T1] L2.
+lemma teqx_fqu_trans (b):
+ ∀G1,G2,L1,L2,U1,T1. ❪G1,L1,U1❫ ⬂[b] ❪G2,L2,T1❫ →
+ ∀U2. U2 ≛ U1 →
+ ∃∃L,T2. ❪G1,L1,U2❫ ⬂[b] ❪G2,L,T2❫ & T2 ≛ T1 & L ≛[T1] L2.
#b #G1 #G2 #L1 #L2 #U1 #T1 #H12 #U2 #HU21
elim (fqu_teqx_conf … H12 U2) -H12
/3 width=5 by reqx_sym, teqx_sym, ex3_2_intro/
qed-.
(* Basic_2A1: uses: lleq_fqu_trans *)
-lemma reqx_fqu_trans: ∀b,G1,G2,L2,K2,T,U. ❪G1,L2,T❫ ⬂[b] ❪G2,K2,U❫ →
- ∀L1. L1 ≛[T] L2 →
- ∃∃K1,U0. ❪G1,L1,T❫ ⬂[b] ❪G2,K1,U0❫ & U0 ≛ U & K1 ≛[U] K2.
+lemma reqx_fqu_trans (b):
+ ∀G1,G2,L2,K2,T,U. ❪G1,L2,T❫ ⬂[b] ❪G2,K2,U❫ →
+ ∀L1. L1 ≛[T] L2 →
+ ∃∃K1,U0. ❪G1,L1,T❫ ⬂[b] ❪G2,K1,U0❫ & U0 ≛ U & K1 ≛[U] K2.
#b #G1 #G2 #L2 #K2 #T #U #H elim H -G1 -G2 -L2 -K2 -T -U
[ #I #G #L2 #V2 #L1 #H elim (reqx_inv_zero_pair_dx … H) -H
#K1 #V1 #HV1 #HV12 #H destruct
- /3 width=7 by teqx_reqx_conf, fqu_lref_O, ex3_2_intro/
+ /3 width=7 by teqx_reqx_conf_sn, fqu_lref_O, ex3_2_intro/
| * [ #p ] #I #G #L2 #V #T #L1 #H
[ elim (reqx_inv_bind … H)
| elim (reqx_inv_flat … H)
(* Properties with optional structural successor for closures ***************)
-lemma teqx_fquq_trans: ∀b,G1,G2,L1,L2,U1,T1. ❪G1,L1,U1❫ ⬂⸮[b] ❪G2,L2,T1❫ →
- ∀U2. U2 ≛ U1 →
- ∃∃L,T2. ❪G1,L1,U2❫ ⬂⸮[b] ❪G2,L,T2❫ & T2 ≛ T1 & L ≛[T1] L2.
+lemma teqx_fquq_trans (b):
+ ∀G1,G2,L1,L2,U1,T1. ❪G1,L1,U1❫ ⬂⸮[b] ❪G2,L2,T1❫ →
+ ∀U2. U2 ≛ U1 →
+ ∃∃L,T2. ❪G1,L1,U2❫ ⬂⸮[b] ❪G2,L,T2❫ & T2 ≛ T1 & L ≛[T1] L2.
#b #G1 #G2 #L1 #L2 #U1 #T1 #H elim H -H
[ #H #U2 #HU21 elim (teqx_fqu_trans … H … HU21) -U1
/3 width=5 by fqu_fquq, ex3_2_intro/
qed-.
(* Basic_2A1: was just: lleq_fquq_trans *)
-lemma reqx_fquq_trans: ∀b,G1,G2,L2,K2,T,U. ❪G1,L2,T❫ ⬂⸮[b] ❪G2,K2,U❫ →
- ∀L1. L1 ≛[T] L2 →
- ∃∃K1,U0. ❪G1,L1,T❫ ⬂⸮[b] ❪G2,K1,U0❫ & U0 ≛ U & K1 ≛[U] K2.
+lemma reqx_fquq_trans (b):
+ ∀G1,G2,L2,K2,T,U. ❪G1,L2,T❫ ⬂⸮[b] ❪G2,K2,U❫ →
+ ∀L1. L1 ≛[T] L2 →
+ ∃∃K1,U0. ❪G1,L1,T❫ ⬂⸮[b] ❪G2,K1,U0❫ & U0 ≛ U & K1 ≛[U] K2.
#b #G1 #G2 #L2 #K2 #T #U #H elim H -H
[ #H #L1 #HL12 elim (reqx_fqu_trans … H … HL12) -L2 /3 width=5 by fqu_fquq, ex3_2_intro/
| * #HG #HL #HT destruct /2 width=5 by ex3_2_intro/
(* Properties with plus-iterated structural successor for closures **********)
(* Basic_2A1: was just: lleq_fqup_trans *)
-lemma reqx_fqup_trans: ∀b,G1,G2,L2,K2,T,U. ❪G1,L2,T❫ ⬂+[b] ❪G2,K2,U❫ →
- ∀L1. L1 ≛[T] L2 →
- ∃∃K1,U0. ❪G1,L1,T❫ ⬂+[b] ❪G2,K1,U0❫ & U0 ≛ U & K1 ≛[U] K2.
+lemma reqx_fqup_trans (b):
+ ∀G1,G2,L2,K2,T,U. ❪G1,L2,T❫ ⬂+[b] ❪G2,K2,U❫ →
+ ∀L1. L1 ≛[T] L2 →
+ ∃∃K1,U0. ❪G1,L1,T❫ ⬂+[b] ❪G2,K1,U0❫ & U0 ≛ U & K1 ≛[U] K2.
#b #G1 #G2 #L2 #K2 #T #U #H @(fqup_ind … H) -G2 -K2 -U
[ #G2 #K2 #U #HTU #L1 #HL12 elim (reqx_fqu_trans … HTU … HL12) -L2
/3 width=5 by fqu_fqup, ex3_2_intro/
elim (reqx_fqu_trans … HU2 … HK0) -K #K1 #U1 #HU1 #HU12 #HK12
elim (teqx_fqu_trans … HU1 … HU0) -U #K3 #U3 #HU03 #HU31 #HK31
@(ex3_2_intro … K3 U3) (**) (* full auto too slow *)
- /3 width=5 by reqx_trans, teqx_reqx_conf, fqup_strap1, teqx_trans/
+ /3 width=5 by reqx_trans, teqx_reqx_conf_sn, fqup_strap1, teqx_trans/
]
qed-.
-lemma teqx_fqup_trans: ∀b,G1,G2,L1,L2,U1,T1. ❪G1,L1,U1❫ ⬂+[b] ❪G2,L2,T1❫ →
- ∀U2. U2 ≛ U1 →
- ∃∃L,T2. ❪G1,L1,U2❫ ⬂+[b] ❪G2,L,T2❫ & T2 ≛ T1 & L ≛[T1] L2.
+lemma teqx_fqup_trans (b):
+ ∀G1,G2,L1,L2,U1,T1. ❪G1,L1,U1❫ ⬂+[b] ❪G2,L2,T1❫ →
+ ∀U2. U2 ≛ U1 →
+ ∃∃L,T2. ❪G1,L1,U2❫ ⬂+[b] ❪G2,L,T2❫ & T2 ≛ T1 & L ≛[T1] L2.
#b #G1 #G2 #L1 #L2 #U1 #T1 #H @(fqup_ind_dx … H) -G1 -L1 -U1
[ #G1 #L1 #U1 #H #U2 #HU21 elim (teqx_fqu_trans … H … HU21) -U1
/3 width=5 by fqu_fqup, ex3_2_intro/
lapply (teqx_reqx_div … HTU … HL0) -HL0 #HL0
elim (IH … HTU) -U #K2 #U1 #H2 #HUT1 #HKL2
elim (reqx_fqup_trans … H2 … HL0) -L #K #U #H2 #HU1 #HK2
- lapply (teqx_reqx_conf … HUT1 … HK2) -HK2 #HK2
+ lapply (teqx_reqx_conf_sn … HUT1 … HK2) -HK2 #HK2
/3 width=7 by reqx_trans, fqup_strap2, teqx_trans, ex3_2_intro/
]
qed-.
(* Properties with star-iterated structural successor for closures **********)
-lemma teqx_fqus_trans: ∀b,G1,G2,L1,L2,U1,T1. ❪G1,L1,U1❫ ⬂*[b] ❪G2,L2,T1❫ →
- ∀U2. U2 ≛ U1 →
- ∃∃L,T2. ❪G1,L1,U2❫ ⬂*[b] ❪G2,L,T2❫ & T2 ≛ T1 & L ≛[T1] L2.
+lemma teqx_fqus_trans (b):
+ ∀G1,G2,L1,L2,U1,T1. ❪G1,L1,U1❫ ⬂*[b] ❪G2,L2,T1❫ →
+ ∀U2. U2 ≛ U1 →
+ ∃∃L,T2. ❪G1,L1,U2❫ ⬂*[b] ❪G2,L,T2❫ & T2 ≛ T1 & L ≛[T1] L2.
#b #G1 #G2 #L1 #L2 #U1 #T1 #H #U2 #HU21 elim(fqus_inv_fqup … H) -H
[ #H elim (teqx_fqup_trans … H … HU21) -U1 /3 width=5 by fqup_fqus, ex3_2_intro/
| * #HG #HL #HT destruct /2 width=5 by ex3_2_intro/
qed-.
(* Basic_2A1: was just: lleq_fqus_trans *)
-lemma reqx_fqus_trans: ∀b,G1,G2,L2,K2,T,U. ❪G1,L2,T❫ ⬂*[b] ❪G2,K2,U❫ →
- ∀L1. L1 ≛[T] L2 →
- ∃∃K1,U0. ❪G1,L1,T❫ ⬂*[b] ❪G2,K1,U0❫ & U0 ≛ U & K1 ≛[U] K2.
+lemma reqx_fqus_trans (b):
+ ∀G1,G2,L2,K2,T,U. ❪G1,L2,T❫ ⬂*[b] ❪G2,K2,U❫ →
+ ∀L1. L1 ≛[T] L2 →
+ ∃∃K1,U0. ❪G1,L1,T❫ ⬂*[b] ❪G2,K1,U0❫ & U0 ≛ U & K1 ≛[U] K2.
#b #G1 #G2 #L2 #K2 #T #U #H #L1 #HL12 elim(fqus_inv_fqup … H) -H
[ #H elim (reqx_fqup_trans … H … HL12) -L2 /3 width=5 by fqup_fqus, ex3_2_intro/
| * #HG #HL #HT destruct /2 width=5 by ex3_2_intro/
(* Advanced properties ******************************************************)
-(* Basic_2A1: uses: lleq_sym *)
lemma reqx_sym: ∀T. symmetric … (reqx T).
/3 width=3 by reqx_fsge_comp, rex_sym, teqx_sym/ qed-.
definition rex (R) (T): relation lenv ≝
λL1,L2. ∃∃f. L1 ⊢ 𝐅+❪T❫ ≘ f & L1 ⪤[cext2 R,cfull,f] L2.
-interpretation "generic extension on referred entries (local environment)"
- 'Relation R T L1 L2 = (rex R T L1 L2).
+interpretation
+ "generic extension on referred entries (local environment)"
+ 'Relation R T L1 L2 = (rex R T L1 L2).
definition R_confluent2_rex:
relation4 (relation3 lenv term term)
∀L1. L0 ⪤[RP1,T0] L1 → ∀L2. L0 ⪤[RP2,T0] L2 →
∀T. R2 L1 T1 T → R1 L2 T2 T.
+definition R_transitive_rex: relation3 ? (relation3 ?? term) … ≝
+ λR1,R2,R3.
+ ∀K1,K,V1. K1 ⪤[R1,V1] K →
+ ∀V. R1 K1 V1 V → ∀V2. R2 K V V2 → R3 K1 V1 V2.
+
+definition R_confluent1_rex: relation … ≝
+ λR1,R2.
+ ∀K1,K2,V1. K1 ⪤[R2,V1] K2 → ∀V2. R1 K1 V1 V2 → R1 K2 V1 V2.
+
definition rex_confluent: relation … ≝
λR1,R2.
∀K1,K,V1. K1 ⪤[R1,V1] K → ∀V. R1 K1 V1 V →
∀K2. K ⪤[R2,V] K2 → K ⪤[R2,V1] K2.
-definition rex_transitive: relation3 ? (relation3 ?? term) … ≝
- λR1,R2,R3.
- ∀K1,K,V1. K1 ⪤[R1,V1] K →
- ∀V. R1 K1 V1 V → ∀V2. R2 K V V2 → R3 K1 V1 V2.
-
(* Basic inversion lemmas ***************************************************)
-lemma rex_inv_atom_sn (R): ∀Y2,T. ⋆ ⪤[R,T] Y2 → Y2 = ⋆.
+lemma rex_inv_atom_sn (R):
+ ∀Y2,T. ⋆ ⪤[R,T] Y2 → Y2 = ⋆.
#R #Y2 #T * /2 width=4 by sex_inv_atom1/
qed-.
-lemma rex_inv_atom_dx (R): ∀Y1,T. Y1 ⪤[R,T] ⋆ → Y1 = ⋆.
+lemma rex_inv_atom_dx (R):
+ ∀Y1,T. Y1 ⪤[R,T] ⋆ → Y1 = ⋆.
#R #I #Y1 * /2 width=4 by sex_inv_atom2/
qed-.
lemma rex_inv_zero (R):
∀Y1,Y2. Y1 ⪤[R,#0] Y2 →
- ∨∨ Y1 = ⋆ ∧ Y2 = ⋆
- | ∃∃I,L1,L2,V1,V2. L1 ⪤[R,V1] L2 & R L1 V1 V2 &
- Y1 = L1.ⓑ[I]V1 & Y2 = L2.ⓑ[I]V2
- | ∃∃f,I,L1,L2. 𝐈❪f❫ & L1 ⪤[cext2 R,cfull,f] L2 &
- Y1 = L1.ⓤ[I] & Y2 = L2.ⓤ[I].
+ ∨∨ ∧∧ Y1 = ⋆ & Y2 = ⋆
+ | ∃∃I,L1,L2,V1,V2. L1 ⪤[R,V1] L2 & R L1 V1 V2 & Y1 = L1.ⓑ[I]V1 & Y2 = L2.ⓑ[I]V2
+ | ∃∃f,I,L1,L2. 𝐈❪f❫ & L1 ⪤[cext2 R,cfull,f] L2 & Y1 = L1.ⓤ[I] & Y2 = L2.ⓤ[I].
#R * [ | #Y1 * #I1 [ | #X ] ] #Y2 * #f #H1 #H2
[ lapply (sex_inv_atom1 … H2) -H2 /3 width=1 by or3_intro0, conj/
| elim (frees_inv_unit … H1) -H1 #g #HX #H destruct
qed-.
(* Basic_2A1: uses: llpx_sn_fwd_pair_sn llpx_sn_fwd_bind_sn llpx_sn_fwd_flat_sn *)
-lemma rex_fwd_pair_sn (R): ∀I,L1,L2,V,T. L1 ⪤[R,②[I]V.T] L2 → L1 ⪤[R,V] L2.
+lemma rex_fwd_pair_sn (R):
+ ∀I,L1,L2,V,T. L1 ⪤[R,②[I]V.T] L2 → L1 ⪤[R,V] L2.
#R * [ #p ] #I #L1 #L2 #V #T * #f #Hf #HL
[ elim (frees_inv_bind … Hf) | elim (frees_inv_flat … Hf) ] -Hf
/4 width=6 by sle_sex_trans, sor_inv_sle_sn, ex2_intro/
qed-.
(* Basic_2A1: uses: llpx_sn_fwd_flat_dx *)
-lemma rex_fwd_flat_dx (R): ∀I,L1,L2,V,T. L1 ⪤[R,ⓕ[I]V.T] L2 → L1 ⪤[R,T] L2.
+lemma rex_fwd_flat_dx (R):
+ ∀I,L1,L2,V,T. L1 ⪤[R,ⓕ[I]V.T] L2 → L1 ⪤[R,T] L2.
#R #I #L1 #L2 #V #T #H elim (rex_inv_flat … H) -H //
qed-.
(* Basic properties *********************************************************)
-lemma rex_atom (R): ∀I. ⋆ ⪤[R,⓪[I]] ⋆.
+lemma rex_atom (R):
+ ∀I. ⋆ ⪤[R,⓪[I]] ⋆.
#R * /3 width=3 by frees_sort, frees_atom, frees_gref, sex_atom, ex2_intro/
qed.
(* GENERIC EXTENSION ON REFERRED ENTRIES OF A CONTEXT-SENSITIVE REALTION ****)
-definition f_dedropable_sn: predicate (relation3 lenv term term) ≝
- λR. ∀b,f,L1,K1. ⇩*[b,f] L1 ≘ K1 →
- ∀K2,T. K1 ⪤[R,T] K2 → ∀U. ⇧*[f] T ≘ U →
- ∃∃L2. L1 ⪤[R,U] L2 & ⇩*[b,f] L2 ≘ K2 & L1 ≡[f] L2.
-
-definition f_dropable_sn: predicate (relation3 lenv term term) ≝
- λR. ∀b,f,L1,K1. ⇩*[b,f] L1 ≘ K1 → 𝐔❪f❫ →
- ∀L2,U. L1 ⪤[R,U] L2 → ∀T. ⇧*[f] T ≘ U →
- ∃∃K2. K1 ⪤[R,T] K2 & ⇩*[b,f] L2 ≘ K2.
-
-definition f_dropable_dx: predicate (relation3 lenv term term) ≝
- λR. ∀L1,L2,U. L1 ⪤[R,U] L2 →
- ∀b,f,K2. ⇩*[b,f] L2 ≘ K2 → 𝐔❪f❫ → ∀T. ⇧*[f] T ≘ U →
- ∃∃K1. ⇩*[b,f] L1 ≘ K1 & K1 ⪤[R,T] K2.
-
-definition f_transitive_next: relation3 … ≝ λR1,R2,R3.
- ∀f,L,T. L ⊢ 𝐅+❪T❫ ≘ f →
- ∀g,I,K,i. ⇩[i] L ≘ K.ⓘ[I] → ↑g = ⫱*[i] f →
- sex_transitive (cext2 R1) (cext2 R2) (cext2 R3) (cext2 R1) cfull g K I.
+definition f_dedropable_sn:
+ predicate (relation3 lenv term term) ≝ λR.
+ ∀b,f,L1,K1. ⇩*[b,f] L1 ≘ K1 →
+ ∀K2,T. K1 ⪤[R,T] K2 → ∀U. ⇧*[f] T ≘ U →
+ ∃∃L2. L1 ⪤[R,U] L2 & ⇩*[b,f] L2 ≘ K2 & L1 ≡[f] L2.
+
+definition f_dropable_sn:
+ predicate (relation3 lenv term term) ≝ λR.
+ ∀b,f,L1,K1. ⇩*[b,f] L1 ≘ K1 → 𝐔❪f❫ →
+ ∀L2,U. L1 ⪤[R,U] L2 → ∀T. ⇧*[f] T ≘ U →
+ ∃∃K2. K1 ⪤[R,T] K2 & ⇩*[b,f] L2 ≘ K2.
+
+definition f_dropable_dx:
+ predicate (relation3 lenv term term) ≝ λR.
+ ∀L1,L2,U. L1 ⪤[R,U] L2 →
+ ∀b,f,K2. ⇩*[b,f] L2 ≘ K2 → 𝐔❪f❫ → ∀T. ⇧*[f] T ≘ U →
+ ∃∃K1. ⇩*[b,f] L1 ≘ K1 & K1 ⪤[R,T] K2.
+
+definition f_transitive_next:
+ relation3 … ≝ λR1,R2,R3.
+ ∀f,L,T. L ⊢ 𝐅+❪T❫ ≘ f →
+ ∀g,I,K,i. ⇩[i] L ≘ K.ⓘ[I] → ↑g = ⫱*[i] f →
+ R_pw_transitive_sex (cext2 R1) (cext2 R2) (cext2 R3) (cext2 R1) cfull g K I.
+
+definition f_confluent1_next: relation2 … ≝ λR1,R2.
+ ∀f,L,T. L ⊢ 𝐅+❪T❫ ≘ f →
+ ∀g,I,K,i. ⇩[i] L ≘ K.ⓘ[I] → ↑g = ⫱*[i] f →
+ R_pw_confluent1_sex (cext2 R1) (cext2 R1) (cext2 R2) cfull g K I.
(* Properties with generic slicing for local environments *******************)
qed-.
lemma rex_trans_next (R1) (R2) (R3):
- rex_transitive R1 R2 R3 → f_transitive_next R1 R2 R3.
+ R_transitive_rex R1 R2 R3 → f_transitive_next R1 R2 R3.
#R1 #R2 #R3 #HR #f #L1 #T #Hf #g #I1 #K1 #n #HLK #Hgf #I #H
generalize in match HLK; -HLK elim H -I1 -I
[ #I #_ #L2 #_ #I2 #H
]
qed.
+lemma rex_conf1_next (R1) (R2):
+ R_confluent1_rex R1 R2 → f_confluent1_next R1 R2.
+#R1 #R2 #HR #f #L1 #T #Hf #g #I1 #K1 #n #HLK #Hgf #I #H
+generalize in match HLK; -HLK elim H -I1 -I
+[ /2 width=1 by ext2_unit/
+| #I #V1 #V2 #HV12 #HLK1 #K2 #HK12
+ elim (frees_inv_drops_next … Hf … HLK1 … Hgf) -f -HLK1 #f #Hf #Hfg
+ /5 width=5 by ext2_pair, sle_sex_trans, ex2_intro/
+]
+qed.
+
(* Inversion lemmas with generic slicing for local environments *************)
(* Basic_2A1: uses: llpx_sn_inv_lift_le llpx_sn_inv_lift_be llpx_sn_inv_lift_ge *)
(* Basic_2A1: was: llpx_sn_drop_conf_O *)
-lemma rex_dropable_sn (R): f_dropable_sn R.
+lemma rex_dropable_sn (R):
+ f_dropable_sn R.
#R #b #f #L1 #K1 #HLK1 #H1f #L2 #U * #f2 #Hf2 #HL12 #T #HTU
elim (frees_total K1 T) #f1 #Hf1
lapply (frees_fwd_coafter … Hf2 … HLK1 … HTU … Hf1) -HTU #H2f
(* Basic_2A1: was: llpx_sn_drop_trans_O *)
(* Note: the proof might be simplified *)
-lemma rex_dropable_dx (R): f_dropable_dx R.
+lemma rex_dropable_dx (R):
+ f_dropable_dx R.
#R #L1 #L2 #U * #f2 #Hf2 #HL12 #b #f #K2 #HLK2 #H1f #T #HTU
elim (drops_isuni_ex … H1f L1) #K1 #HLK1
elim (frees_total K1 T) #f1 #Hf1
lapply(frees_mono … H … Hf) -H #H1
lapply (sor_eq_repl_back1 … Hy … H1) -y1 #Hy
lapply (sor_inv_sle_sn … Hy) -y2 #Hfg
-elim (sex_sle_split (cext2 R1) (cext2 R2) … HL12 … Hfg) -HL12 /2 width=1 by ext2_refl/ #L #HL1 #HL2
+elim (sex_sle_split_sn (cext2 R1) (cext2 R2) … HL12 … Hfg) -HL12 /2 width=1 by ext2_refl/ #L #HL1 #HL2
lapply (sle_sex_trans … HL1 … Hfg) // #H
elim (frees_sex_conf_fsge … Hf … H) -Hf -H
/4 width=7 by sle_sex_trans, ex2_intro/
lapply(frees_mono … H … Hf) -H #H2
lapply (sor_eq_repl_back2 … Hy … H2) -y2 #Hy
lapply (sor_inv_sle_dx … Hy) -y1 #Hfg
-elim (sex_sle_split (cext2 R1) (cext2 R2) … HL12 … Hfg) -HL12 /2 width=1 by ext2_refl/ #L #HL1 #HL2
+elim (sex_sle_split_sn (cext2 R1) (cext2 R2) … HL12 … Hfg) -HL12 /2 width=1 by ext2_refl/ #L #HL1 #HL2
lapply (sle_sex_trans … HL1 … Hfg) // #H
elim (frees_sex_conf_fsge … Hf … H) -Hf -H
/4 width=7 by sle_sex_trans, ex2_intro/
lapply (sor_eq_repl_back2 … Hy … H2) -y2 #Hy
lapply (sor_inv_sle_dx … Hy) -y1 #Hfg
lapply (sle_inv_tl_sn … Hfg) -Hfg #Hfg
-elim (sex_sle_split (cext2 R1) (cext2 R2) … HL12 … Hfg) -HL12 /2 width=1 by ext2_refl/ #Y #H #HL2
+elim (sex_sle_split_sn (cext2 R1) (cext2 R2) … HL12 … Hfg) -HL12 /2 width=1 by ext2_refl/ #Y #H #HL2
lapply (sle_sex_trans … H … Hfg) // #H0
elim (sex_inv_next1 … H) -H #Z #L #HL1 #H
elim (ext2_inv_pair_sn … H) -H #V #HV #H1 #H2 destruct
lapply (sor_eq_repl_back2 … Hy … H2) -y2 #Hy
lapply (sor_inv_sle_dx … Hy) -y1 #Hfg
lapply (sle_inv_tl_sn … Hfg) -Hfg #Hfg
-elim (sex_sle_split (cext2 R1) (cext2 R2) … HL12 … Hfg) -HL12 /2 width=1 by ext2_refl/ #Y #H #HL2
+elim (sex_sle_split_sn (cext2 R1) (cext2 R2) … HL12 … Hfg) -HL12 /2 width=1 by ext2_refl/ #Y #H #HL2
lapply (sle_sex_trans … H … Hfg) // #H0
elim (sex_inv_next1 … H) -H #Z #L #HL1 #H
elim (ext2_inv_unit_sn … H) -H #H destruct
(* Inversion lemmas with generic extension of a context sensitive relation **)
-lemma rex_inv_lex_req (R):
+lemma rex_inv_req_lex (R):
+ c_reflexive … R → f_confluent1_next R ceq →
+ ∀L1,L2,T. L1 ⪤[R,T] L2 →
+ ∃∃L. L1 ≡[T] L & L ⪤[R] L2.
+#R #H1R #H2R #L1 #L2 #T * #f1 #Hf1 #HL
+elim (sex_sdj_split_dx … ceq_ext … HL 𝐈𝐝) -HL
+[ #L0 #HL10 #HL02
+ lapply (sex_sdj … HL02 f1 ?) /2 width=1 by sdj_isid_sn/ #H
+ /3 width=5 by (* 2x *) ex2_intro/
+|*: /2 width=1 by ext2_refl, sdj_isid_dx/
+ #g #I #K #n #HLK #Hg @H2R /width=7 by/ (**) (* no auto with H2R *)
+]
+qed-.
+
+(* Forward lemmas with generic extension of a context sensitive relation **)
+
+lemma rex_fwd_lex_req (R):
c_reflexive … R → rex_fsge_compatible R →
∀L1,L2,T. L1 ⪤[R,T] L2 →
∃∃L. L1 ⪤[R] L & L ≡[T] L2.
#R #H1R #H2R #L1 #L2 #T * #f1 #Hf1 #HL
-elim (sex_sdj_split … ceq_ext … HL 𝐈𝐝 ?) -HL
+elim (sex_sdj_split_sn … ceq_ext … HL 𝐈𝐝 ?) -HL
[ #L0 #HL10 #HL02 |*: /2 width=1 by ext2_refl, sdj_isid_dx/ ] -H1R
lapply (sex_sdj … HL10 f1 ?) /2 width=1 by sdj_isid_sn/ #H
elim (frees_sex_conf_fsge … Hf1 … H) // -H2R -H #f0 #Hf0 #Hf01
}
]
[ { "syntactic equivalence" * } {
- [ [ "for lenvs on referred entries" ] "req" + "( ? ≡[?] ? )" "req_drops" + "req_fqup" + "req_fsle" * ]
+ [ [ "for lenvs on referred entries" ] "req" + "( ? ≡[?] ? )" "req_length" + "req_drops" + "req_fqup" + "req_fsle" * ]
}
]
[ { "generic extension of a context-sensitive relation" * } {
projects / helm.git / commitdiff