λR. ∀L,U. R L U → ∀b,f,K. ⬇*[b, f] L ≡ K →
∀T. ⬆*[f] T ≡ U → R K T.
-definition d_liftable2: predicate (lenv → relation term) ≝
- λR. ∀K,T1,T2. R K T1 T2 → ∀b,f,L. ⬇*[b, f] L ≡ K →
- ∀U1. ⬆*[f] T1 ≡ U1 →
- ∃∃U2. ⬆*[f] T2 ≡ U2 & R L U1 U2.
+definition d_liftable2_sn: predicate (lenv → relation term) ≝
+ λR. ∀K,T1,T2. R K T1 T2 → ∀b,f,L. ⬇*[b, f] L ≡ K →
+ ∀U1. ⬆*[f] T1 ≡ U1 →
+ ∃∃U2. ⬆*[f] T2 ≡ U2 & R L U1 U2.
definition d_deliftable2_sn: predicate (lenv → relation term) ≝
λR. ∀L,U1,U2. R L U1 U2 → ∀b,f,K. ⬇*[b, f] L ≡ K →
∀T1. ⬆*[f] T1 ≡ U1 →
∃∃T2. ⬆*[f] T2 ≡ U2 & R K T1 T2.
+definition d_liftable2_bi: predicate (lenv → relation term) ≝
+ λR. ∀K,T1,T2. R K T1 T2 → ∀b,f,L. ⬇*[b, f] L ≡ K →
+ ∀U1. ⬆*[f] T1 ≡ U1 →
+ ∀U2. ⬆*[f] T2 ≡ U2 → R L U1 U2.
+
+definition d_deliftable2_bi: predicate (lenv → relation term) ≝
+ λR. ∀L,U1,U2. R L U1 U2 → ∀b,f,K. ⬇*[b, f] L ≡ K →
+ ∀T1. ⬆*[f] T1 ≡ U1 →
+ ∀T2. ⬆*[f] T2 ≡ U2 → R K T1 T2.
+
definition co_dropable_sn: predicate (rtmap → relation lenv) ≝
λR. ∀b,f,L1,K1. ⬇*[b, f] L1 ≡ K1 → 𝐔⦃f⦄ →
∀f2,L2. R f2 L1 L2 → ∀f1. f ~⊚ f1 ≡ f2 →
∃∃K2. R f1 K1 K2 & ⬇*[b, f] L2 ≡ K2.
-
definition co_dropable_dx: predicate (rtmap → relation lenv) ≝
λR. ∀f2,L1,L2. R f2 L1 L2 →
∀b,f,K2. ⬇*[b, f] L2 ≡ K2 → 𝐔⦃f⦄ →
(* Properties with context-sensitive equivalence for terms ******************)
-lemma ceq_lift: d_liftable2 ceq.
+lemma ceq_lift_sn: d_liftable2_sn ceq.
/2 width=3 by ex2_intro/ qed-.
-lemma ceq_inv_lift: d_deliftable2_sn ceq.
+lemma ceq_inv_lift_sn: d_deliftable2_sn ceq.
/2 width=3 by ex2_intro/ qed-.
(* Note: d_deliftable2_sn cfull does not hold *)
-lemma cfull_lift: d_liftable2 cfull.
+lemma cfull_lift_sn: d_liftable2_sn cfull.
#K #T1 #T2 #_ #b #f #L #_ #U1 #_ -K -T1 -b
elim (lifts_total T2 f) /2 width=3 by ex2_intro/
qed-.
(* GENERIC SLICING FOR LOCAL ENVIRONMENTS ***********************************)
+(* Main properties on generic relocation ************************************)
+
+lemma d_liftable2_sn_bi: ∀R. d_liftable2_sn R → d_liftable2_bi R.
+#R #HR #K #T1 #T2 #HT12 #b #f #L #HLK #U1 #HTU1 #U2 #HTU2
+elim (HR … HT12 … HLK … HTU1) -HR -K -T1 #X #HTX #HUX
+<(lifts_mono … HTX … HTU2) -T2 -U2 -b -f //
+qed-.
+
+lemma d_deliftable2_sn_bi: ∀R. d_deliftable2_sn R → d_deliftable2_bi R.
+#R #HR #L #U1 #U2 #HU12 #b #f #K #HLK #T1 #HTU1 #T2 #HTU2
+elim (HR … HU12 … HLK … HTU1) -HR -L -U1 #X #HUX #HTX
+<(lifts_inj … HUX … HTU2) -U2 -T2 -b -f //
+qed-.
+
(* Main properties **********************************************************)
(* Basic_2A1: includes: drop_conf_ge drop_conf_be drop_conf_le *)
qed-.
(* Basic_2A1: includes: lpx_sn_liftable_dedropable *)
-lemma lexs_liftable_co_dedropable: ∀RN,RP. (∀L. reflexive ? (RN L)) → (∀L. reflexive ? (RP L)) →
- d_liftable2 RN → d_liftable2 RP → co_dedropable_sn (lexs RN RP).
+lemma lexs_liftable_co_dedropable_sn: ∀RN,RP. (∀L. reflexive ? (RN L)) → (∀L. reflexive ? (RP L)) →
+ d_liftable2_sn RN → d_liftable2_sn RP → co_dedropable_sn (lexs 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 >(lexs_inv_atom1 … H) -X
/4 width=4 by drops_atom, lexs_atom, ex3_intro/
qed-.
lemma drops_lexs_trans_next: ∀RN,RP. (∀L. reflexive ? (RN L)) → (∀L. reflexive ? (RP L)) →
- d_liftable2 RN → d_liftable2 RP →
+ d_liftable2_sn RN → d_liftable2_sn RP →
∀f1,K1,K2. K1 ⦻*[RN, RP, f1] K2 →
∀b,f,I,L1,V1. ⬇*[b,f] L1.ⓑ{I}V1 ≡ K1 →
∀f2. f ~⊚ f1 ≡ ⫯f2 →
∃∃L2,V2. ⬇*[b,f] L2.ⓑ{I}V2 ≡ K2 & L1 ⦻*[RN, RP, f2] L2 & RN L1 V1 V2 & L1.ⓑ{I}V1≡[f]L2.ⓑ{I}V2.
#RN #RP #H1RN #H1RP #H2RN #H2RP #f1 #K1 #K2 #HK12 #b #f #I #L1 #V1 #HLK1 #f2 #Hf2
-elim (lexs_liftable_co_dedropable … H1RN H1RP H2RN H2RP … HLK1 … HK12 … Hf2) -K1 -f1 -H1RN -H1RP -H2RN -H2RP
+elim (lexs_liftable_co_dedropable_sn … H1RN H1RP H2RN H2RP … HLK1 … HK12 … Hf2) -K1 -f1 -H1RN -H1RP -H2RN -H2RP
#X #HX #HLK2 #H1L12 elim (lexs_inv_next1 … HX) -HX
#L2 #V2 #H2L12 #HV12 #H destruct /2 width=6 by ex4_2_intro/
qed-.
lemma drops_lexs_trans_push: ∀RN,RP. (∀L. reflexive ? (RN L)) → (∀L. reflexive ? (RP L)) →
- d_liftable2 RN → d_liftable2 RP →
+ d_liftable2_sn RN → d_liftable2_sn RP →
∀f1,K1,K2. K1 ⦻*[RN, RP, f1] K2 →
∀b,f,I,L1,V1. ⬇*[b,f] L1.ⓑ{I}V1 ≡ K1 →
∀f2. f ~⊚ f1 ≡ ↑f2 →
∃∃L2,V2. ⬇*[b,f] L2.ⓑ{I}V2 ≡ K2 & L1 ⦻*[RN, RP, f2] L2 & RP L1 V1 V2 & L1.ⓑ{I}V1≡[f]L2.ⓑ{I}V2.
#RN #RP #H1RN #H1RP #H2RN #H2RP #f1 #K1 #K2 #HK12 #b #f #I #L1 #V1 #HLK1 #f2 #Hf2
-elim (lexs_liftable_co_dedropable … H1RN H1RP H2RN H2RP … HLK1 … HK12 … Hf2) -K1 -f1 -H1RN -H1RP -H2RN -H2RP
+elim (lexs_liftable_co_dedropable_sn … H1RN H1RP H2RN H2RP … HLK1 … HK12 … Hf2) -K1 -f1 -H1RN -H1RP -H2RN -H2RP
#X #HX #HLK2 #H1L12 elim (lexs_inv_push1 … HX) -HX
#L2 #V2 #H2L12 #HV12 #H destruct /2 width=6 by ex4_2_intro/
qed-.
(* Properties with ranged equivalence for local environments ****************)
-lemma lreq_co_dedropable: co_dedropable_sn lreq.
-@lexs_liftable_co_dedropable
-/2 width=6 by cfull_lift, ceq_lift/ qed-.
+lemma lreq_co_dedropable_sn: co_dedropable_sn lreq.
+@lexs_liftable_co_dedropable_sn
+/2 width=6 by cfull_lift_sn, ceq_lift_sn/ qed-.
lemma lreq_co_dropable_sn: co_dropable_sn lreq.
@lexs_co_dropable_sn qed-.
∃∃L2. ⬇*[b,f] L2.ⓑ{I}V ≡ K2 & L1 ≡[f2] L2 & L1.ⓑ{I}V ≡[f] L2.ⓑ{I}V.
#f1 #K1 #K2 #HK12 #b #f #I #L1 #V #HLK1 #f2 #Hf2
elim (drops_lexs_trans_next … HK12 … HLK1 … Hf2) -f1 -K1
-/2 width=6 by cfull_lift, ceq_lift, ex3_intro/ qed-.
+/2 width=6 by cfull_lift_sn, ceq_lift_sn, ex3_intro/ qed-.
(* Properties with reflexive and transitive closure *************************)
(* Basic_2A1: was: d_liftable_LTC *)
-lemma d2_liftable_LTC: ∀R. d_liftable2 R → d_liftable2 (LTC … R).
+lemma d2_liftable_sn_LTC: ∀R. d_liftable2_sn R → d_liftable2_sn (LTC … R).
#R #HR #K #T1 #T2 #H elim H -T2
[ #T2 #HT12 #b #f #L #HLK #U1 #HTU1
elim (HR … HT12 … HLK … HTU1) /3 width=3 by inj, ex2_intro/
qed-.
(* Basic_2A1: was: d_liftable_llstar *)
-lemma d2_liftable_llstar: ∀R. d_liftable2 R → ∀d. d_liftable2 (llstar … R d).
+lemma d2_liftable_sn_llstar: ∀R. d_liftable2_sn R → ∀d. d_liftable2_sn (llstar … R d).
#R #HR #d #K #T1 #T2 #H @(lstar_ind_r … d T2 H) -d -T2
[ #b #f #L #_ #U1 #HTU1 -HR -b -K /2 width=3 by ex2_intro/
| #l #T #T2 #_ #HT2 #IHT1 #b #f #L #HLK #U1 #HTU1
interpretation "generic relocation (term)"
'RLiftStar f T1 T2 = (lifts f T1 T2).
-definition liftable2: predicate (relation term) ≝
- λR. ∀T1,T2. R T1 T2 → ∀f,U1. ⬆*[f] T1 ≡ U1 →
- ∃∃U2. ⬆*[f] T2 ≡ U2 & R U1 U2.
+definition liftable2_sn: predicate (relation term) ≝
+ λR. ∀T1,T2. R T1 T2 → ∀f,U1. ⬆*[f] T1 ≡ U1 →
+ ∃∃U2. ⬆*[f] T2 ≡ U2 & R U1 U2.
definition deliftable2_sn: predicate (relation term) ≝
λR. ∀U1,U2. R U1 U2 → ∀f,T1. ⬆*[f] T1 ≡ U1 →
/3 width=6 by lifts_conf, lifts_fwd_isid/
qed-.
-lemma liftable2_sn_bi: ∀R. liftable2 R → liftable2_bi R.
+lemma liftable2_sn_bi: ∀R. liftable2_sn R → liftable2_bi R.
#R #HR #T1 #T2 #HT12 #f #U1 #HTU1 #U2 #HTU2
elim (HR … HT12 … HTU1) -HR -T1 #X #HTX #HUX
<(lifts_mono … HTX … HTU2) -T2 -U2 -f //
(* Properties with degree-based equivalence for terms ***********************)
-lemma tdeq_lifts: ∀h,o. liftable2 (tdeq h o).
+lemma tdeq_lifts_sn: ∀h,o. liftable2_sn (tdeq h o).
#h #o #T1 #T2 #H elim H -T1 -T2 [||| * ]
[ #s1 #s2 #d #Hs1 #Hs2 #f #X #H >(lifts_inv_sort1 … H) -H
/3 width=5 by lifts_sort, tdeq_sort, ex2_intro/
qed-.
lemma tdeq_lifts_bi: ∀h,o. liftable2_bi (tdeq h o).
-/3 width=6 by tdeq_lifts, liftable2_sn_bi/ qed-.
+/3 width=6 by tdeq_lifts_sn, liftable2_sn_bi/ qed-.
(* Inversion lemmas with degree-based equivalence for terms *****************)
-lemma tdeq_inv_lifts: ∀h,o. deliftable2_sn (tdeq h o).
+lemma tdeq_inv_lifts_sn: ∀h,o. deliftable2_sn (tdeq h o).
#h #o #U1 #U2 #H elim H -U1 -U2 [||| * ]
[ #s1 #s2 #d #Hs1 #Hs2 #f #X #H >(lifts_inv_sort2 … H) -H
/3 width=5 by lifts_sort, tdeq_sort, ex2_intro/
qed-.
lemma tdeq_inv_lifts_bi: ∀h,o. deliftable2_bi (tdeq h o).
-/3 width=6 by tdeq_inv_lifts, deliftable2_sn_bi/ qed-.
+/3 width=6 by tdeq_inv_lifts_sn, deliftable2_sn_bi/ qed-.
#h #I #G #K #V1 #V2 #H @(cpxs_ind … H) -V2
[ /3 width=3 by cpx_cpxs, cpx_delta/
| #V #V2 #_ #HV2 #IH #W2 #HVW2
- elim (lifts_total V (𝐔❴1❵)) #W #HVW
- elim (cpx_lifts … HV2 (Ⓣ) … (K.ⓑ{I}V1) … HVW) -HV2
- [ #V0 #HV20 <(lifts_mono … HVW2 … HV20) -V2 -V0 /3 width=3 by cpxs_strap1/
- | /3 width=1 by drops_refl, drops_drop/
- ]
+ elim (lifts_total V (𝐔❴1❵))
+ /5 width=11 by cpxs_strap1, cpx_lifts_bi, drops_refl, drops_drop/
]
qed.
#h #I #G #K #V #T #i #H @(cpxs_ind … H) -T
[ /3 width=3 by cpx_cpxs, cpx_lref/
| #T0 #T #_ #HT2 #IH #U #HTU
- elim (lifts_total T0 (𝐔❴1❵)) #U0 #HTU0
- elim (cpx_lifts … HT2 (Ⓣ) … (K.ⓑ{I}V) … HTU0) -HT2
- [ #X #HTX <(lifts_mono … HTU … HTX) -T -X /3 width=3 by cpxs_strap1/
- | /3 width=1 by drops_refl, drops_drop/
- ]
+ elim (lifts_total T0 (𝐔❴1❵))
+ /5 width=11 by cpxs_strap1, cpx_lifts_bi, drops_refl, drops_drop/
]
qed.
#h #I #G #L #K #V1 #V2 #i #HLK #H @(cpxs_ind … H) -V2
[ /3 width=7 by cpx_cpxs, cpx_delta_drops/
| #V #V2 #_ #HV2 #IH #W2 #HVW2
- elim (lifts_total V (𝐔❴⫯i❵)) #W #HVW
- elim (cpx_lifts … HV2 (Ⓣ) … L … HVW) -HV2
- [ #V0 #HV20 <(lifts_mono … HVW2 … HV20) -V2 -V0 /3 width=3 by cpxs_strap1/
- | /2 width=3 by drops_isuni_fwd_drop2/
- ]
+ elim (lifts_total V (𝐔❴⫯i❵))
+ /4 width=11 by cpxs_strap1, cpx_lifts_bi, drops_isuni_fwd_drop2/
]
qed.
elim (cpx_inv_zero1 … HT2) -HT2 /2 width=1 by or_introl/
* /4 width=7 by cpx_cpxs, ex3_4_intro, or_intror/
| * #I #K #V1 #T1 #HVT1 #HT1 #H destruct
- elim (cpx_inv_lifts … HT2 (Ⓣ) … K … HT1) -T
+ elim (cpx_inv_lifts_sn … HT2 (Ⓣ) … K … HT1) -T
/4 width=7 by cpxs_strap1, drops_refl, drops_drop, ex3_4_intro, or_intror/
]
qed-.
elim (cpx_inv_lref1 … HT2) -HT2 /2 width=1 by or_introl/
* /4 width=7 by cpx_cpxs, ex3_4_intro, or_intror/
| * #I #K #V1 #T1 #Hi #HT1 #H destruct
- elim (cpx_inv_lifts … HT2 (Ⓣ) … K … HT1) -T
+ elim (cpx_inv_lifts_sn … HT2 (Ⓣ) … K … HT1) -T
/4 width=7 by cpxs_strap1, drops_refl, drops_drop, ex3_4_intro, or_intror/
]
qed-.
* /4 width=7 by cpx_cpxs, ex3_4_intro, or_intror/
| * #I #K #V1 #T1 #HLK #HVT1 #HT1
lapply (drops_isuni_fwd_drop2 … HLK) // #H0LK
- elim (cpx_inv_lifts … HT2 … H0LK … HT1) -H0LK -T
+ elim (cpx_inv_lifts_sn … HT2 … H0LK … HT1) -H0LK -T
/4 width=7 by cpxs_strap1, ex3_4_intro, or_intror/
]
qed-.
(* Properties with generic relocation ***************************************)
(* Basic_2A1: includes: cpxs_lift *)
-lemma cpxs_lifts: ∀h,G. d_liftable2 (cpxs h G).
-/3 width=10 by cpx_lifts, cpxs_strap1, d2_liftable_LTC/ qed-.
+lemma cpxs_lifts_sn: ∀h,G. d_liftable2_sn (cpxs h G).
+/3 width=10 by cpx_lifts_sn, cpxs_strap1, d2_liftable_sn_LTC/ qed-.
+
+lemma cpxs_lifts_bi: ∀h,G. d_liftable2_bi (cpxs h G).
+/3 width=9 by cpxs_lifts_sn, d_liftable2_sn_bi/ qed-.
(* Inversion lemmas with generic relocation *********************************)
(* Basic_2A1: includes: cpxs_inv_lift1 *)
-lemma cpxs_inv_lifts: ∀h,G. d_deliftable2_sn (cpxs h G).
-/3 width=6 by d2_deliftable_sn_LTC, cpx_inv_lifts/ qed-.
+lemma cpxs_inv_lifts_sn: ∀h,G. d_deliftable2_sn (cpxs h G).
+/3 width=6 by d2_deliftable_sn_LTC, cpx_inv_lifts_sn/ qed-.
+
+lemma cpxs_inv_lifts_bi: ∀h,G. d_deliftable2_bi (cpxs h G).
+/3 width=9 by cpxs_inv_lifts_sn, d_deliftable2_sn_bi/ qed-.
elim (cpxs_inv_lref1_drops … H) -H /2 width=1 by or_introl/
* #I0 #K0 #V0 #U0 #HLK0 #HVU0 #HU0
lapply (drops_mono … HLK0 … HLK) -HLK0 #H destruct
-elim (cpxs_lifts … HVU0 (Ⓣ) … L … HV12) -HVU0 -HV12 /2 width=3 by drops_isuni_fwd_drop2/ #X #H
-<(lifts_mono … HU0 … H) -U0 -X /2 width=1 by or_intror/
+/4 width=9 by cpxs_lifts_bi, drops_isuni_fwd_drop2, or_intror/
qed-.
(* Basic_1: was just: pr3_iso_beta *)
@or_intror @(cpxs_trans … HU) -U (**) (* explicit constructor *)
elim (cpxs_inv_abbr1 … HT0) -HT0 *
[ #V5 #T5 #HV5 #HT5 #H destruct
- elim (cpxs_lifts … HV13 (Ⓣ) … (L.ⓓV) … HV12) -V1 /3 width=1 by drops_refl, drops_drop/ #X #H
- <(lifts_mono … HV34 … H) -V3 -X /3 width=1 by cpxs_flat, cpxs_bind/
+ /6 width=9 by cpxs_lifts_bi, drops_refl, drops_drop, cpxs_flat, cpxs_bind/
| #X #HT1 #H #H0 destruct
elim (lifts_inv_bind1 … H) -H #V5 #T5 #HV05 #HT05 #H destruct
- elim (cpxs_lifts … HV13 (Ⓣ) … (L.ⓓV0) … HV12) -HV13 /3 width=1 by drops_refl, drops_drop/ #X #H
- <(lifts_mono … HV34 … H) -V3 -X #HV24
+ lapply (cpxs_lifts_bi … HV13 (Ⓣ) … (L.ⓓV0) … HV12 … HV34) -V3 /3 width=1 by drops_refl, drops_drop/ #HV24
@(cpxs_trans … (+ⓓV.ⓐV2.ⓓ{q}V5.T5)) [ /3 width=1 by cpxs_flat_dx, cpxs_bind_dx/ ] -T
@(cpxs_strap2 … (ⓐV1.ⓓ{q}V0.T0)) [ /4 width=7 by cpx_zeta, lifts_bind, lifts_flat/ ] -V -V5 -T5
@(cpxs_strap2 … (ⓓ{q}V0.ⓐV2.T0)) /3 width=3 by cpxs_pair_sn, cpxs_bind_dx, cpx_theta/
@(cpxs_trans … HU) -U
elim (cpxs_inv_abbr1 … HT0) -HT0 *
[ #V1 #T1 #HV1 #HT1 #H destruct
- elim (cpxs_lifts … HV10a (Ⓣ) … (L.ⓓV) … HV12a) -V1a /3 width=1 by drops_refl, drops_drop/ #X #H
- <(lifts_mono … HV0a … H) -V0a -X #HV2a
+ lapply (cpxs_lifts_bi … HV10a (Ⓣ) … (L.ⓓV) … HV12a … HV0a) -V1a -V0a /3 width=1 by drops_refl, drops_drop/ #HV2a
@(cpxs_trans … (ⓓ{p}V.ⓐV2a.T1)) /3 width=1 by cpxs_bind, cpxs_pair_sn, cpxs_flat_dx, cpxs_bind_dx/
| #X #HT1 #H #H0 destruct
elim (lifts_inv_bind1 … H) -H #V1 #T1 #HW01 #HT01 #H destruct
- elim (cpxs_lifts … HV10a (Ⓣ) … (L.ⓓV0) … HV12a) /3 width=1 by drops_refl, drops_drop/ #X #H
- <(lifts_mono … HV0a … H) -V0a -X #HV2a
+ lapply (cpxs_lifts_bi … HV10a (Ⓣ) … (L.ⓓV0) … HV12a … HV0a) -V0a /3 width=1 by drops_refl, drops_drop/ #HV2a
@(cpxs_trans … (+ⓓV.ⓐV2a.ⓓ{q}V1.T1)) [ /3 width=1 by cpxs_flat_dx, cpxs_bind_dx/ ] -T -V2b -V2b
@(cpxs_strap2 … (ⓐV1a.ⓓ{q}V0.T0)) [ /4 width=7 by cpx_zeta, lifts_bind, lifts_flat/ ] -V -V1 -T1
@(cpxs_strap2 … (ⓓ{q}V0.ⓐV2a.T0)) /3 width=3 by cpxs_pair_sn, cpxs_bind_dx, cpx_theta/
]
qed-.
-lemma csx_ind_alt: ∀h,o,G,L. ∀R:predicate term.
- (∀T1. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T1⦄ →
- (∀T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 → (T1 ≡[h, o] T2 → ⊥) → R T2) → R T1
- ) →
- ∀T. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄ → R T.
+(* Basic_2A1: was: csx_ind_alt *)
+lemma csx_ind_cpxs: ∀h,o,G,L. ∀R:predicate term.
+ (∀T1. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T1⦄ →
+ (∀T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 → (T1 ≡[h, o] T2 → ⊥) → R T2) → R T1
+ ) →
+ ∀T. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄ → R T.
#h #o #G #L #R #IH #T #HT
@(csx_ind_cpxs_tdeq … IH … HT) -IH -HT // (**) (* full auto fails *)
qed-.
#h #o #G #K #T #H @(csx_ind … H) -T
#T1 #_ #IH #b #f #L #HLK #U1 #HTU1
@csx_intro #U2 #HU12 #HnU12
-elim (cpx_inv_lifts … HU12 … HLK … HTU1) -HU12
+elim (cpx_inv_lifts_sn … HU12 … HLK … HTU1) -HU12
/4 width=7 by tdeq_lifts_bi/
qed-.
#h #o #G #L #U #H @(csx_ind … H) -U
#U1 #_ #IH #b #f #K #HLK #T1 #HTU1
@csx_intro #T2 #HT12 #HnT12
-elim (cpx_lifts … HT12 … HLK … HTU1) -HT12
+elim (cpx_lifts_sn … HT12 … HLK … HTU1) -HT12
/4 width=7 by tdeq_inv_lifts_bi/
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 "basic_2/rt_computation/cpxs_lfpx.ma".
+include "basic_2/rt_computation/csx_drops.ma".
+include "basic_2/rt_computation/csx_cpxs.ma".
+
+(* STRONGLY NORMALIZING TERMS FOR UNCOUNTED PARALLEL RT-TRANSITION **********)
+
+(* Advanced properties ******************************************************)
+
+(* Basic_2A1: was just: csx_lpx_conf *)
+lemma csx_lfpx_conf: ∀h,o,G,L1,T. ⦃G, L1⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄ →
+ ∀L2. ⦃G, L1⦄ ⊢ ⬈[h, T] L2 → ⦃G, L2⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄.
+#h #o #G #L1 #T #H @(csx_ind_cpxs … H) -T
+/5 width=3 by csx_intro, lfpx_cpx_trans, lfpx_cpxs_conf/
+qed-.
+
+lemma csx_abst: ∀h,o,p,G,L,W. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃W⦄ →
+ ∀T. ⦃G, L.ⓛW⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄ → ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃ⓛ{p}W.T⦄.
+#h #o #p #G #L #W #HW @(csx_ind … HW) -W
+#W #_ #IHW #T #HT @(csx_ind … HT) -T #T #HT #IHT
+@csx_intro #X #H1 #H2
+elim (cpx_inv_abst1 … H1) -H1
+#W0 #T0 #HLW0 #HLT0 #H destruct
+elim (tdneq_inv_pair … H2) -H2
+[ #H elim H -H //
+| -IHT #H lapply (csx_cpx_trans … o … HLT0) // -HT
+ #HT0 lapply (csx_lfpx_conf … HT0 … (L.ⓛW0)) -HT0 /4 width=1 by lfpx_pair/
+| -IHW -HT /4 width=3 by csx_cpx_trans, cpx_pair_sn/
+]
+qed.
+
+lemma csx_abbr: ∀h,o,p,G,L,V. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃V⦄ →
+ ∀T. ⦃G, L.ⓓV⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄ → ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃ⓓ{p}V.T⦄.
+#h #o #p #G #L #V #HV @(csx_ind … HV) -V
+#V #_ #IHV #T #HT @(csx_ind_cpxs … HT) -T #T #HT #IHT
+@csx_intro #X #H1 #H2
+elim (cpx_inv_abbr1 … H1) -H1 *
+[ #V1 #T1 #HLV1 #HLT1 #H destruct
+ elim (tdneq_inv_pair … H2) -H2
+ [ #H elim H -H //
+ | /4 width=3 by csx_cpx_trans, csx_lfpx_conf, lfpx_pair/
+ | -IHV /4 width=3 by csx_cpx_trans, cpx_cpxs, cpx_pair_sn/
+ ]
+| -IHV -IHT -H2
+ /4 width=7 by csx_cpx_trans, csx_inv_lifts, drops_drop, drops_refl/
+]
+qed.
+
+fact csx_appl_theta_aux: ∀h,o,p,G,L,U. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃U⦄ → ∀V1,V2. ⬆*[1] V1 ≡ V2 →
+ ∀V,T. U = ⓓ{p}V.ⓐV2.T → ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃ⓐV1.ⓓ{p}V.T⦄.
+#h #o #p #G #L #X #H @(csx_ind_cpxs … H) -X
+#X #HVT #IHVT #V1 #V2 #HV12 #V #T #H destruct
+lapply (csx_fwd_pair_sn … HVT) #HV
+lapply (csx_fwd_bind_dx … HVT) -HVT #HVT
+@csx_intro #X #HL #H
+elim (cpx_inv_appl1 … HL) -HL *
+[ -HV #V0 #Y #HLV10 #HL #H0 destruct
+ elim (cpx_inv_abbr1 … HL) -HL *
+ [ #V3 #T3 #HV3 #HLT3 #H0 destruct
+ elim (lift_total V0 0 1) #V4 #HV04
+ elim (eq_term_dec (ⓓ{a}V.ⓐV2.T) (ⓓ{a}V3.ⓐV4.T3))
+ [ -IHVT #H0 destruct
+ elim (eq_false_inv_tpair_sn … H) -H
+ [ -HLV10 -HV3 -HLT3 -HVT
+ >(lift_inj … HV12 … HV04) -V4
+ #H elim H //
+ | * #_ #H elim H //
+ ]
+ | -H -HVT #H
+ lapply (cpx_lift … HLV10 (L.ⓓV) (Ⓕ) … HV12 … HV04) -HLV10 -HV12 /2 width=1 by drop_drop/ #HV24
+ @(IHVT … H … HV04) -IHVT /4 width=1 by cpx_cpxs, cpx_bind, cpx_flat/
+ ]
+ | -H -IHVT #T0 #HLT0 #HT0 #H0 destruct
+ lapply (csx_cpx_trans … HVT (ⓐV2.T0) ?) /2 width=1 by cpx_flat/ -T #HVT0
+ lapply (csx_inv_lift … L … (Ⓕ) … 1 HVT0 ? ? ?) -HVT0
+ /3 width=5 by csx_cpx_trans, cpx_pair_sn, drop_drop, lift_flat/
+ ]
+| -HV -HV12 -HVT -IHVT -H #b #V0 #W0 #W1 #T0 #T1 #_ #_ #_ #H destruct
+| -IHVT -H #b #V0 #V3 #W0 #W1 #T0 #T1 #HLV10 #HV03 #HLW01 #HLT01 #H1 #H2 destruct
+ lapply (cpx_lift … HLV10 (L. ⓓW0) … HV12 … HV03) -HLV10 -HV12 -HV03 /2 width=2 by drop_drop/ #HLV23
+ @csx_abbr /2 width=3 by csx_cpx_trans/ -HV
+ @(csx_lpx_conf … (L.ⓓW0)) /2 width=1 by lpx_pair/ -W1
+ /4 width=5 by csx_cpxs_trans, cpx_cpxs, cpx_flat/
+]
+qed-.
+
+lemma csx_appl_theta: ∀h,o,a,V1,V2. ⬆[0, 1] V1 ≡ V2 →
+ ∀G,L,V,T. ⦃G, L⦄ ⊢ ⬈*[h, o] ⓓ{a}V.ⓐV2.T → ⦃G, L⦄ ⊢ ⬈*[h, o] ⓐV1.ⓓ{a}V.T.
+/2 width=5 by csx_appl_theta_aux/ 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 "basic_2/computation/cpxs_cpxs.ma".
-include "basic_2/computation/csx_alt.ma".
-include "basic_2/computation/csx_lift.ma".
-
-(* CONTEXT-SENSITIVE EXTENDED STRONGLY NORMALIZING TERMS ********************)
-
-(* Advanced properties ******************************************************)
-
-lemma csx_lpx_conf: ∀h,o,G,L1,L2. ⦃G, L1⦄ ⊢ ➡[h, o] L2 →
- ∀T. ⦃G, L1⦄ ⊢ ⬊*[h, o] T → ⦃G, L2⦄ ⊢ ⬊*[h, o] T.
-#h #o #G #L1 #L2 #HL12 #T #H @(csx_ind_alt … H) -T
-/4 width=3 by csx_intro, lpx_cpx_trans/
-qed-.
-
-lemma csx_abst: ∀h,o,a,G,L,W. ⦃G, L⦄ ⊢ ⬊*[h, o] W →
- ∀T. ⦃G, L.ⓛW⦄ ⊢ ⬊*[h, o] T → ⦃G, L⦄ ⊢ ⬊*[h, o] ⓛ{a}W.T.
-#h #o #a #G #L #W #HW @(csx_ind … HW) -W #W #_ #IHW #T #HT @(csx_ind … HT) -T #T #HT #IHT
-@csx_intro #X #H1 #H2
-elim (cpx_inv_abst1 … H1) -H1
-#W0 #T0 #HLW0 #HLT0 #H destruct
-elim (eq_false_inv_tpair_sn … H2) -H2
-[ -IHT #H lapply (csx_cpx_trans … HLT0) // -HT
- #HT0 lapply (csx_lpx_conf … (L.ⓛW0) … HT0) -HT0 /3 width=1 by lpx_pair/
-| -IHW -HLW0 -HT * #H destruct /3 width=1 by/
-]
-qed.
-
-lemma csx_abbr: ∀h,o,a,G,L,V. ⦃G, L⦄ ⊢ ⬊*[h, o] V →
- ∀T. ⦃G, L.ⓓV⦄ ⊢ ⬊*[h, o] T → ⦃G, L⦄ ⊢ ⬊*[h, o] ⓓ{a}V. T.
-#h #o #a #G #L #V #HV elim HV -V #V #_ #IHV #T #HT @(csx_ind_alt … HT) -T #T #HT #IHT
-@csx_intro #X #H1 #H2
-elim (cpx_inv_abbr1 … H1) -H1 *
-[ #V1 #T1 #HLV1 #HLT1 #H destruct
- elim (eq_false_inv_tpair_sn … H2) -H2
- [ /4 width=5 by csx_cpx_trans, csx_lpx_conf, lpx_pair/
- | -IHV -HLV1 * #H destruct /3 width=1 by cpx_cpxs/
- ]
-| -IHV -IHT -H2
- /3 width=8 by csx_cpx_trans, csx_inv_lift, drop_drop/
-]
-qed.
-
-fact csx_appl_beta_aux: ∀h,o,a,G,L,U1. ⦃G, L⦄ ⊢ ⬊*[h, o] U1 →
- ∀V,W,T1. U1 = ⓓ{a}ⓝW.V.T1 → ⦃G, L⦄ ⊢ ⬊*[h, o] ⓐV.ⓛ{a}W.T1.
-#h #o #a #G #L #X #H @(csx_ind … H) -X
-#X #HT1 #IHT1 #V #W #T1 #H1 destruct
-@csx_intro #X #H1 #H2
-elim (cpx_inv_appl1 … H1) -H1 *
-[ -HT1 #V0 #Y #HLV0 #H #H0 destruct
- elim (cpx_inv_abst1 … H) -H #W0 #T0 #HLW0 #HLT0 #H destruct
- @IHT1 -IHT1 [4: // | skip |3: #H destruct /2 width=1 by/ ] -H2
- lapply (lsubr_cpx_trans … HLT0 (L.ⓓⓝW.V) ?) -HLT0 /3 width=1 by cpx_bind, cpx_flat, lsubr_beta/
-| -IHT1 -H2 #b #V0 #W0 #W2 #T0 #T2 #HLV0 #HLW02 #HLT02 #H1 #H3 destruct
- lapply (lsubr_cpx_trans … HLT02 (L.ⓓⓝW0.V) ?) -HLT02
- /4 width=5 by csx_cpx_trans, cpx_bind, cpx_flat, lsubr_beta/
-| -HT1 -IHT1 -H2 #b #V0 #V1 #W0 #W1 #T0 #T3 #_ #_ #_ #_ #H destruct
-]
-qed-.
-
-(* Basic_1: was just: sn3_beta *)
-lemma csx_appl_beta: ∀h,o,a,G,L,V,W,T. ⦃G, L⦄ ⊢ ⬊*[h, o] ⓓ{a}ⓝW.V.T → ⦃G, L⦄ ⊢ ⬊*[h, o] ⓐV.ⓛ{a}W.T.
-/2 width=3 by csx_appl_beta_aux/ qed.
-
-fact csx_appl_theta_aux: ∀h,o,a,G,L,U. ⦃G, L⦄ ⊢ ⬊*[h, o] U → ∀V1,V2. ⬆[0, 1] V1 ≡ V2 →
- ∀V,T. U = ⓓ{a}V.ⓐV2.T → ⦃G, L⦄ ⊢ ⬊*[h, o] ⓐV1.ⓓ{a}V.T.
-#h #o #a #G #L #X #H @(csx_ind_alt … H) -X #X #HVT #IHVT #V1 #V2 #HV12 #V #T #H destruct
-lapply (csx_fwd_pair_sn … HVT) #HV
-lapply (csx_fwd_bind_dx … HVT) -HVT #HVT
-@csx_intro #X #HL #H
-elim (cpx_inv_appl1 … HL) -HL *
-[ -HV #V0 #Y #HLV10 #HL #H0 destruct
- elim (cpx_inv_abbr1 … HL) -HL *
- [ #V3 #T3 #HV3 #HLT3 #H0 destruct
- elim (lift_total V0 0 1) #V4 #HV04
- elim (eq_term_dec (ⓓ{a}V.ⓐV2.T) (ⓓ{a}V3.ⓐV4.T3))
- [ -IHVT #H0 destruct
- elim (eq_false_inv_tpair_sn … H) -H
- [ -HLV10 -HV3 -HLT3 -HVT
- >(lift_inj … HV12 … HV04) -V4
- #H elim H //
- | * #_ #H elim H //
- ]
- | -H -HVT #H
- lapply (cpx_lift … HLV10 (L.ⓓV) (Ⓕ) … HV12 … HV04) -HLV10 -HV12 /2 width=1 by drop_drop/ #HV24
- @(IHVT … H … HV04) -IHVT /4 width=1 by cpx_cpxs, cpx_bind, cpx_flat/
- ]
- | -H -IHVT #T0 #HLT0 #HT0 #H0 destruct
- lapply (csx_cpx_trans … HVT (ⓐV2.T0) ?) /2 width=1 by cpx_flat/ -T #HVT0
- lapply (csx_inv_lift … L … (Ⓕ) … 1 HVT0 ? ? ?) -HVT0
- /3 width=5 by csx_cpx_trans, cpx_pair_sn, drop_drop, lift_flat/
- ]
-| -HV -HV12 -HVT -IHVT -H #b #V0 #W0 #W1 #T0 #T1 #_ #_ #_ #H destruct
-| -IHVT -H #b #V0 #V3 #W0 #W1 #T0 #T1 #HLV10 #HV03 #HLW01 #HLT01 #H1 #H2 destruct
- lapply (cpx_lift … HLV10 (L. ⓓW0) … HV12 … HV03) -HLV10 -HV12 -HV03 /2 width=2 by drop_drop/ #HLV23
- @csx_abbr /2 width=3 by csx_cpx_trans/ -HV
- @(csx_lpx_conf … (L.ⓓW0)) /2 width=1 by lpx_pair/ -W1
- /4 width=5 by csx_cpxs_trans, cpx_cpxs, cpx_flat/
-]
-qed-.
-
-lemma csx_appl_theta: ∀h,o,a,V1,V2. ⬆[0, 1] V1 ≡ V2 →
- ∀G,L,V,T. ⦃G, L⦄ ⊢ ⬊*[h, o] ⓓ{a}V.ⓐV2.T → ⦃G, L⦄ ⊢ ⬊*[h, o] ⓐV1.ⓓ{a}V.T.
-/2 width=5 by csx_appl_theta_aux/ 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 "basic_2/rt_transition/cpx_lsubr.ma".
+include "basic_2/rt_computation/csx_csx.ma".
+
+(* STRONGLY NORMALIZING TERMS FOR UNCOUNTED PARALLEL RT-TRANSITION **********)
+
+(* Advanced properties ******************************************************)
+
+fact csx_appl_beta_aux: ∀h,o,p,G,L,U1. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃U1⦄ →
+ ∀V,W,T1. U1 = ⓓ{p}ⓝW.V.T1 → ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃ⓐV.ⓛ{p}W.T1⦄.
+#h #o #p #G #L #X #H @(csx_ind … H) -X
+#X #HT1 #IHT1 #V #W #T1 #H1 destruct
+@csx_intro #X #H1 #H2
+elim (cpx_inv_appl1 … H1) -H1 *
+[ -HT1 #V0 #Y #HLV0 #H #H0 destruct
+ elim (cpx_inv_abst1 … H) -H #W0 #T0 #HLW0 #HLT0 #H destruct
+ @IHT1 -IHT1 [4: // | skip ]
+ [ lapply (lsubr_cpx_trans … HLT0 (L.ⓓⓝW.V) ?) -HLT0 -H2
+ /3 width=1 by cpx_bind, cpx_flat, lsubr_beta/
+ | #H elim (tdeq_inv_pair … H) -H
+ #_ #H elim (tdeq_inv_pair … H) -H
+ #_ /4 width=1 by tdeq_pair/
+ ]
+| -IHT1 -H2 #q #V0 #W0 #W2 #T0 #T2 #HLV0 #HLW02 #HLT02 #H1 #H3 destruct
+ lapply (lsubr_cpx_trans … HLT02 (L.ⓓⓝW0.V) ?) -HLT02
+ /4 width=5 by csx_cpx_trans, cpx_bind, cpx_flat, lsubr_beta/
+| -HT1 -IHT1 -H2 #q #V0 #V1 #W0 #W1 #T0 #T3 #_ #_ #_ #_ #H destruct
+]
+qed-.
+
+(* Basic_1: was just: sn3_beta *)
+lemma csx_appl_beta: ∀h,o,p,G,L,V,W,T. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃ⓓ{p}ⓝW.V.T⦄ → ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃ⓐV.ⓛ{p}W.T⦄.
+/2 width=3 by csx_appl_beta_aux/ qed.
/4 width=3 by lfpxs_pair, cpxs_trans, ex3_intro, or_intror/
]
| #U1 #HTU1 #HU01
- elim (cpx_lifts … HU02 (Ⓣ) … (L.ⓓV1) … HU01)
+ elim (cpx_lifts_sn … HU02 (Ⓣ) … (L.ⓓV1) … HU01)
/4 width=3 by cpxs_strap1, drops_refl, drops_drop, ex3_intro, or_intror/
]
qed-.
cpxs.ma cpxs_tdeq.ma cpxs_theq.ma cpxs_theq_vector.ma cpxs_drops.ma cpxs_lsubr.ma cpxs_lfpx.ma cpxs_cnx.ma cpxs_cpxs.ma
lfpxs.ma lfpxs_fqup.ma lfpxs_cpxs.ma
-csx.ma csx_simple.ma csx_theq.ma csx_drops.ma csx_gcp.ma csx_cnx.ma csx_cpxs.ma csx_csx.ma
+csx.ma csx_simple.ma csx_theq.ma csx_drops.ma csx_lsubr.ma csx_gcp.ma csx_cnx.ma csx_cpxs.ma csx_csx.ma
csx_vector.ma
(* Basic_2A1: includes: cnx_lift *)
lemma cnx_lifts: ∀h,o,G. d_liftable1 … (cnx h o G).
#h #o #G #K #T #HT #b #f #L #HLK #U #HTU #U0 #H
-elim (cpx_inv_lifts … H … HLK … HTU) -b -L #T0 #HTU0 #HT0
-lapply (HT … HT0) -G -K #HT0
-elim (tdeq_lifts … HT0 … HTU) -T #X #HX #HU
-<(lifts_mono … HX … HTU0) -T0 //
+elim (cpx_inv_lifts_sn … H … HLK … HTU) -b -L #T0 #HTU0 #HT0
+lapply (HT … HT0) -G -K /2 width=6 by tdeq_lifts_bi/
qed-.
(* Inversion lemmas with generic slicing ************************************)
(* Basic_2A1: includes: cnx_inv_lift *)
lemma cnx_inv_lifts: ∀h,o,G. d_deliftable1 … (cnx h o G).
#h #o #G #L #U #HU #b #f #K #HLK #T #HTU #T0 #H
-elim (cpx_lifts … H … HLK … HTU) -b -K #U0 #HTU0 #HU0
-lapply (HU … HU0) -G -L #HU0
-elim (tdeq_inv_lifts … HU0 … HTU) -U #X #HX #HT
-<(lifts_inj … HX … HTU0) -U0 //
+elim (cpx_lifts_sn … H … HLK … HTU) -b -K #U0 #HTU0 #HU0
+lapply (HU … HU0) -G -L /2 width=6 by tdeq_inv_lifts_bi/
qed-.
(* Properties with generic slicing for local environments *******************)
(* Note: it should use drops_split_trans_pair2 *)
-lemma cpg_lifts: ∀Rt. reflexive … Rt → ∀c,h,G. d_liftable2 (cpg Rt h c G).
+lemma cpg_lifts_sn: ∀Rt. reflexive … Rt → ∀c,h,G. d_liftable2_sn (cpg Rt h c G).
#Rt #HRt #c #h #G #K #T generalize in match c; -c
@(fqup_wf_ind_eq … G K T) -G -K -T #G0 #K0 #T0 #IH #G #K * *
[ #s #HG #HK #HT #c #X2 #H2 #b #f #L #HLK #X1 #H1 destruct -IH
]
qed-.
+lemma cpg_lifts_bi: ∀Rt. reflexive … Rt → ∀c,h,G. d_liftable2_bi (cpg Rt h c G).
+/3 width=9 by cpg_lifts_sn, d_liftable2_sn_bi/ qed-.
+
(* Inversion lemmas with generic slicing for local environments *************)
-lemma cpg_inv_lifts1: ∀Rt. reflexive … Rt → ∀c,h,G. d_deliftable2_sn (cpg Rt h c G).
+lemma cpg_inv_lifts_sn: ∀Rt. reflexive … Rt → ∀c,h,G. d_deliftable2_sn (cpg Rt h c G).
#Rt #HRt #c #h #G #L #U generalize in match c; -c
@(fqup_wf_ind_eq … G L U) -G -L -U #G0 #L0 #U0 #IH #G #L * *
[ #s #HG #HL #HU #c #X2 #H2 #b #f #K #HLK #X1 #H1 destruct -IH
]
]
qed-.
+
+lemma cpg_inv_lifts_bi: ∀Rt. reflexive … Rt → ∀c,h,G. d_deliftable2_bi (cpg Rt h c G).
+/3 width=9 by cpg_inv_lifts_sn, d_deliftable2_sn_bi/ qed-.
(* Basic_1: includes: pr0_lift pr2_lift *)
(* Basic_2A1: includes: cpr_lift *)
-lemma cpm_lifts: ∀n,h,G. d_liftable2 (cpm n h G).
+lemma cpm_lifts_sn: ∀n,h,G. d_liftable2_sn (cpm n h G).
#n #h #G #K #T1 #T2 * #c #Hc #HT12 #b #f #L #HLK #U1 #HTU1
-elim (cpg_lifts … HT12 … HLK … HTU1) -K -T1
+elim (cpg_lifts_sn … HT12 … HLK … HTU1) -K -T1
/3 width=5 by ex2_intro/
qed-.
+lemma cpm_lifts_bi: ∀n,h,G. d_liftable2_bi (cpm n h G).
+/3 width=9 by cpm_lifts_sn, d_liftable2_sn_bi/ qed-.
+
(* Inversion lemmas with generic slicing for local environments *************)
(* Basic_1: includes: pr0_gen_lift pr2_gen_lift *)
(* Basic_2A1: includes: cpr_inv_lift1 *)
-lemma cpm_inv_lifts1: ∀n,h,G. d_deliftable2_sn (cpm n h G).
+lemma cpm_inv_lifts_sn: ∀n,h,G. d_deliftable2_sn (cpm n h G).
#n #h #G #L #U1 #U2 * #c #Hc #HU12 #b #f #K #HLK #T1 #HTU1
-elim (cpg_inv_lifts1 … HU12 … HLK … HTU1) -L -U1
+elim (cpg_inv_lifts_sn … HU12 … HLK … HTU1) -L -U1
/3 width=5 by ex2_intro/
qed-.
+
+lemma cpm_inv_lifts_bi: ∀n,h,G. d_deliftable2_bi (cpm n h G).
+/3 width=9 by cpm_inv_lifts_sn, d_deliftable2_sn_bi/ qed-.
(* Properties with generic slicing for local environments *******************)
(* Basic_2A1: includes: cpx_lift *)
-lemma cpx_lifts: ∀h,G. d_liftable2 (cpx h G).
+lemma cpx_lifts_sn: ∀h,G. d_liftable2_sn (cpx h G).
#h #G #K #T1 #T2 * #cT #HT12 #b #f #L #HLK #U1 #HTU1
-elim (cpg_lifts … HT12 … HLK … HTU1) -K -T1
+elim (cpg_lifts_sn … HT12 … HLK … HTU1) -K -T1
/3 width=4 by ex2_intro, ex_intro/
qed-.
+lemma cpx_lifts_bi: ∀h,G. d_liftable2_bi (cpx h G).
+/3 width=9 by cpx_lifts_sn, d_liftable2_sn_bi/ qed-.
+
(* Inversion lemmas with generic slicing for local environments *************)
(* Basic_2A1: includes: cpx_inv_lift1 *)
-lemma cpx_inv_lifts: ∀h,G. d_deliftable2_sn (cpx h G).
+lemma cpx_inv_lifts_sn: ∀h,G. d_deliftable2_sn (cpx h G).
#h #G #L #U1 #U2 * #cU #HU12 #b #f #K #HLK #T1 #HTU1
-elim (cpg_inv_lifts1 … HU12 … HLK … HTU1) -L -U1
+elim (cpg_inv_lifts_sn … HU12 … HLK … HTU1) -L -U1
/3 width=4 by ex2_intro, ex_intro/
qed-.
+
+lemma cpx_inv_lifts_bi: ∀h,G. d_deliftable2_bi (cpx h G).
+/3 width=9 by cpx_inv_lifts_sn, d_deliftable2_sn_bi/ qed-.
elim (lifts_total X2 (𝐔❴1❵))
/3 width=3 by fqu_drop, cpx_delta, ex2_intro/
| #I #G #L2 #V #T2 #X2 #HTX2 #U2 #HTU2
- elim (cpx_lifts … HTU2 (Ⓣ) … (L2.ⓑ{I}V) … HTX2)
+ elim (cpx_lifts_sn … HTU2 (Ⓣ) … (L2.ⓑ{I}V) … HTX2)
/3 width=3 by fqu_drop, drops_refl, drops_drop, ex2_intro/
]
qed-.
| #H elim (tdeq_inv_pair … H) -H /2 width=1 by/
]
| #I #G #L #V #T1 #U1 #HTU1 #T2 #HT12 #H0
- elim (cpx_lifts … HT12 (Ⓣ) … (L.ⓑ{I}V) … HTU1) -HT12 /3 width=1 by drops_refl, drops_drop/
- #U2 #HTU2 #HU12 @(ex3_intro … U2)
- [1,3: /3 width=1 by fqu_drop/
- | #H elim (tdeq_inv_lifts … H … HTU1) -U1
- #X2 #H <(lifts_inj … HTU2 … H) -U2 /2 width=1 by/
- ]
+ elim (cpx_lifts_sn … HT12 (Ⓣ) … (L.ⓑ{I}V) … HTU1) -HT12
+ /4 width=6 by fqu_drop, drops_refl, drops_drop, tdeq_inv_lifts_bi, ex3_intro/
]
qed-.
(* Properties with generic slicing for local environments *******************)
lemma drops_lfpr_trans: ∀h,G. dedropable_sn (cpm 0 h G).
-/3 width=6 by lfxs_liftable_dedropable, cpm_lifts/ qed-.
+/3 width=6 by lfxs_liftable_dedropable_sn, cpm_lifts_sn/ qed-.
(* Inversion lemmas with generic slicing for local environments *************)
∃∃L,U1. ⦃G1, L1⦄ ⊢ ➡[h, T1] L & ⦃G1, L⦄ ⊢ T1 ➡[h] U1 & ⦃G1, L, U1⦄ ⊐ ⦃G2, L2, U2⦄.
#h #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2
/3 width=5 by lfpr_pair, cpr_pair_sn, cpr_flat, cpm_bind, fqu_lref_O, fqu_pair_sn, fqu_bind_dx, fqu_flat_dx, ex3_2_intro/
-#I #G #L #V #U #T #HUT #U2 #HU2 elim (cpm_lifts … HU2 (Ⓣ) … HUT) -U
+#I #G #L #V #U #T #HUT #U2 #HU2 elim (cpm_lifts_sn … HU2 (Ⓣ) … HUT) -U
/3 width=9 by fqu_drop, drops_refl, drops_drop, ex3_2_intro/
qed-.
∃∃L,U1. ⦃G1, L1⦄ ⊢ ➡[h, T1] L & ⦃G1, L1⦄ ⊢ T1 ➡[h] U1 & ⦃G1, L, U1⦄ ⊐ ⦃G2, L2, U2⦄.
#h #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2
/3 width=5 by lfpr_pair, cpr_pair_sn, cpr_flat, cpm_bind, fqu_lref_O, fqu_pair_sn, fqu_bind_dx, fqu_flat_dx, ex3_2_intro/
-#I #G #L #V #U #T #HUT #U2 #HU2 elim (cpm_lifts … HU2 (Ⓣ) … HUT) -U
+#I #G #L #V #U #T #HUT #U2 #HU2 elim (cpm_lifts_sn … HU2 (Ⓣ) … HUT) -U
/3 width=9 by fqu_drop, drops_refl, drops_drop, ex3_2_intro/
qed-.
lapply (drops_isuni_fwd_drop2 … HLK2) // -W2 #HLK2
lapply (fqup_lref … G … HLK0) -HLK0 #HLK0
elim (IH … HLK0 … HV01 … HV02 … HK01 … HK02) -L0 -K0 -V0 #V #HV1 #HV2
-elim (cpm_lifts … HV2 … HLK2 … HVT2) -K2 -V2
+elim (cpm_lifts_sn … HV2 … HLK2 … HVT2) -K2 -V2
/3 width=6 by cpm_delta_drops, ex2_intro/
qed-.
+(* Note: we don't use cpm_lifts_bi to preserve visual symmetry *)
fact cpr_conf_lfpr_delta_delta:
∀h,G,L0,i. (
∀L,T. ⦃G, L0, #i⦄ ⊐+ ⦃G, L, T⦄ →
lapply (drops_isuni_fwd_drop2 … HLK2) -W2 // #HLK2
lapply (fqup_lref … G … HLK0) -HLK0 #HLK0
elim (IH … HLK0 … HV01 … HV02 … HK01 … HK02) -L0 -K0 -V0 #V #HV1 #HV2
-elim (cpm_lifts … HV1 … HLK1 … HVT1) -K1 -V1 #T #HVT #HT1
-elim (cpm_lifts … HV2 … HLK2 … HVT2) -K2 -V2 #X #HX #HT2
+elim (cpm_lifts_sn … HV1 … HLK1 … HVT1) -K1 -V1 #T #HVT #HT1
+elim (cpm_lifts_sn … HV2 … HLK2 … HVT2) -K2 -V2 #X #HX #HT2
lapply (lifts_mono … HX … HVT) #H destruct
/2 width=3 by ex2_intro/
qed-.
elim (lfpr_inv_bind … HL01) -HL01 #H1V0 #H1T0
elim (lfpr_inv_bind … HL02) -HL02 #H2V0 #H2T0
elim (IH … HT01 … HT02 (L1.ⓓV1) … (L2.ⓓV1)) -IH -HT01 -HT02 /2 width=4 by lfpr_pair_repl_dx/ -L0 -V0 -T0 #T #HT1 #HT2
-elim (cpm_inv_lifts1 … HT2 … L2 … HXT2) -T2 /3 width=3 by drops_refl, drops_drop, cpm_zeta, ex2_intro/
+elim (cpm_inv_lifts_sn … HT2 … L2 … HXT2) -T2 /3 width=3 by drops_refl, drops_drop, cpm_zeta, ex2_intro/
qed-.
+(* Note: we don't use cpm_inv_lifts_bi to preserve visual symmetry *)
fact cpr_conf_lfpr_zeta_zeta:
∀h,G,L0,V0,T0. (
∀L,T. ⦃G, L0, +ⓓV0.T0⦄ ⊐+ ⦃G, L, T⦄ →
elim (lfpr_inv_bind … HL01) -HL01 #H1V0 #H1T0
elim (lfpr_inv_bind … HL02) -HL02 #H2V0 #H2T0
elim (IH … HT01 … HT02 (L1.ⓓV0) … (L2.ⓓV0)) -IH -HT01 -HT02 /2 width=4 by lfpr_pair_repl_dx/ -L0 -T0 #T #HT1 #HT2
-elim (cpm_inv_lifts1 … HT1 … L1 … HXT1) -T1 /3 width=2 by drops_refl, drops_drop/ #T1 #HT1 #HXT1
-elim (cpm_inv_lifts1 … HT2 … L2 … HXT2) -T2 /3 width=2 by drops_refl, drops_drop/ #T2 #HT2 #HXT2
+elim (cpm_inv_lifts_sn … HT1 … L1 … HXT1) -T1 /3 width=2 by drops_refl, drops_drop/ #T1 #HT1 #HXT1
+elim (cpm_inv_lifts_sn … HT2 … L2 … HXT2) -T2 /3 width=2 by drops_refl, drops_drop/ #T2 #HT2 #HXT2
lapply (lifts_inj … HT2 … HT1) -T #H destruct /2 width=3 by ex2_intro/
qed-.
elim (lfpr_inv_flat … HL02) -HL02 #H2V0 #HL02
elim (lfpr_inv_bind … HL02) -HL02 #H2W0 #H2T0
elim (IH … HV01 … HV02 … H1V0 … H2V0) -HV01 -HV02 /2 width=1 by/ #V #HV1 #HV2
-elim (cpm_lifts … HV2 … (L2.ⓓW2) … HVU2) -HVU2 /3 width=2 by drops_refl, drops_drop/ #U #HVU #HU2
+elim (cpm_lifts_sn … HV2 … (L2.ⓓW2) … HVU2) -HVU2 /3 width=2 by drops_refl, drops_drop/ #U #HVU #HU2
elim (cpm_inv_abbr1 … H) -H *
[ #W1 #T1 #HW01 #HT01 #H destruct
elim (IH … HW01 … HW02 … H1W0 … H2W0) /2 width=1 by/
/4 width=7 by cpm_bind, cpr_flat, cpm_theta, ex2_intro/
| #T1 #HT01 #HXT1 #H destruct
elim (IH … HT01 … HT02 (L1.ⓓW2) … (L2.ⓓW2)) /2 width=4 by lfpr_pair_repl_dx/ -L0 -V0 -W0 -T0 #T #HT1 #HT2
- elim (cpm_inv_lifts1 … HT1 … L1 … HXT1) -HXT1
+ elim (cpm_inv_lifts_sn … HT1 … L1 … HXT1) -HXT1
/4 width=9 by cpr_flat, cpm_zeta, drops_refl, drops_drop, lifts_flat, ex2_intro/
]
qed-.
/4 width=5 by cpm_bind, cpr_flat, ex2_intro/ (**) (* full auto not tried *)
qed-.
+(* Note: we don't use cpm_lifts_bi to preserve visual symmetry *)
fact cpr_conf_lfpr_theta_theta:
∀h,p,G,L0,V0,W0,T0. (
∀L,T. ⦃G, L0, ⓐV0.ⓓ{p}W0.T0⦄ ⊐+ ⦃G, L, T⦄ →
elim (IH … HV01 … HV02 … H1V0 … H2V0) -HV01 -HV02 /2 width=1 by/ #V #HV1 #HV2
elim (IH … HW01 … HW02 … H1W0 … H2W0) /2 width=1 by/
elim (IH … HT01 … HT02 (L1.ⓓW1) … (L2.ⓓW2)) /2 width=4 by lfpr_pair_repl_dx/ -L0 -V0 -W0 -T0
-elim (cpm_lifts … HV1 … (L1.ⓓW1) … HVU1) -HVU1 /3 width=2 by drops_refl, drops_drop/ #U #HVU
-elim (cpm_lifts … HV2 … (L2.ⓓW2) … HVU2) -HVU2 /3 width=2 by drops_refl, drops_drop/ #X #HX
+elim (cpm_lifts_sn … HV1 … (L1.ⓓW1) … HVU1) -HVU1 /3 width=2 by drops_refl, drops_drop/ #U #HVU
+elim (cpm_lifts_sn … HV2 … (L2.ⓓW2) … HVU2) -HVU2 /3 width=2 by drops_refl, drops_drop/ #X #HX
lapply (lifts_mono … HX … HVU) -HX #H destruct
/4 width=7 by cpm_bind, cpr_flat, ex2_intro/ (**) (* full auto not tried *)
qed-.
(* Properties with generic slicing for local environments *******************)
lemma drops_lfpx_trans: ∀h,G. dedropable_sn (cpx h G).
-/3 width=6 by lfxs_liftable_dedropable, cpx_lifts/ qed-.
+/3 width=6 by lfxs_liftable_dedropable_sn, cpx_lifts_sn/ qed-.
(* Inversion lemmas with generic slicing for local environments *************)
elim (lfpx_inv_zero_pair_sn … H1) -H1 #K1 #X1 #HK01 #HX1 #H destruct
elim (lfdeq_inv_zero_pair_sn … H2) -H2 #K2 #X2 #HK02 #HX2 #H destruct
elim (IH X2 … HK01 … HK02) // -K0 -V0 #V #HV1 #HV2
- elim (tdeq_lifts … HV1 … HVW1) -V1 /3 width=5 by cpx_delta, ex2_intro/
+ elim (tdeq_lifts_sn … HV1 … HVW1) -V1 /3 width=5 by cpx_delta, ex2_intro/
| #I #G #K0 #V0 #V1 #W1 #i #_ #IH #HVW1 #T2 #H0 #L1 #H1 #L2 #H2
>(tdeq_inv_lref1 … H0) -H0
elim (lfpx_inv_lref_pair_sn … H1) -H1 #K1 #X1 #HK01 #H destruct
elim (lfdeq_inv_lref_pair_sn … H2) -H2 #K2 #X2 #HK02 #H destruct
elim (IH … HK01 … HK02) [|*: //] -K0 -V0 #V #HV1 #HV2
- elim (tdeq_lifts … HV1 … HVW1) -V1 /3 width=5 by cpx_lref, ex2_intro/
+ elim (tdeq_lifts_sn … HV1 … HVW1) -V1 /3 width=5 by cpx_lref, ex2_intro/
| #p #I #G #L0 #V0 #V1 #T0 #T1 #_ #_ #IHV #IHT #X0 #H0 #L1 #H1 #L2 #H2
elim (tdeq_inv_pair1 … H0) -H0 #V2 #T2 #HV02 #HT02 #H destruct
elim (lfpx_inv_bind … H1) -H1 #HL01 #H1
elim (lfdeq_inv_bind … H2) -H2 #HL02 #H2
lapply (lfdeq_pair_repl_dx … H2 … HV02) -H2 -HV02 #H2
elim (IH … HT02 … H1 … H2) -L0 -T0 #T #HT1
- elim (tdeq_inv_lifts … HT1 … HUT1) -T1
+ elim (tdeq_inv_lifts_sn … HT1 … HUT1) -T1
/3 width=5 by cpx_zeta, ex2_intro/
| #G #L0 #V0 #T0 #T1 #_ #IH #X0 #H0 #L1 #H1 #L2 #H2
elim (tdeq_inv_pair1 … H0) -H0 #V2 #T2 #_ #HT02 #H destruct
elim (IHV … HV02 … H1LV0 … H2LV0) -IHV -HV02 -H1LV0 -H2LV0 #V #HV1
elim (IHW … HW02 … H1LW0 … H2LW0) -IHW -HW02 -H1LW0 -H2LW0
elim (IHT … HT02 … H1LT0 … H2LT0) -L0 -V0 -T0
- elim (tdeq_lifts … HV1 … HVU1) -V1
+ elim (tdeq_lifts_sn … HV1 … HVU1) -V1
/4 width=9 by cpx_theta, tdeq_pair, ex2_intro/ (* note: 2 tdeq_pair *)
]
qed-.
(* Properties with generic slicing for local environments *******************)
(* Basic_2A1: includes: lleq_lift_le lleq_lift_ge *)
-lemma lfdeq_lifts: ∀h,o. dedropable_sn (cdeq h o).
-/3 width=5 by lfxs_liftable_dedropable, tdeq_lifts/ qed-.
+lemma lfdeq_lifts_sn: ∀h,o. dedropable_sn (cdeq h o).
+/3 width=5 by lfxs_liftable_dedropable_sn, tdeq_lifts_sn/ qed-.
(* Inversion lemmas with generic slicing for local environments *************)
(* Basic_2A1: restricts: lleq_inv_lift_le lleq_inv_lift_be lleq_inv_lift_ge *)
-lemma lfdeq_inv_lifts: ∀h,o. dropable_sn (cdeq h o).
+lemma lfdeq_inv_lifts_sn: ∀h,o. dropable_sn (cdeq h o).
/2 width=5 by lfxs_dropable_sn/ qed-.
(* Note: missing in basic_2A1 *)
elim (tdeq_inv_pair1 … H) -H #W2 #U2 #_ #HU12 #H destruct
/2 width=5 by fqu_flat_dx, ex3_2_intro/
| #I #G #L #W #T1 #U1 #HTU1 #U2 #HU12
- elim (tdeq_inv_lifts … HU12 … HTU1) -U1 #T2 #HTU2 #HT12
+ elim (tdeq_inv_lifts_sn … HU12 … HTU1) -U1 #T2 #HTU2 #HT12
/3 width=5 by fqu_drop, ex3_2_intro/
]
qed-.
(* Properties with generic slicing for local environments *******************)
(* Basic_2A1: includes: llpx_sn_lift_le llpx_sn_lift_ge *)
-lemma lfxs_liftable_dedropable: ∀R. (∀L. reflexive ? (R L)) →
- d_liftable2 R → dedropable_sn R.
+lemma lfxs_liftable_dedropable_sn: ∀R. (∀L. reflexive ? (R L)) →
+ d_liftable2_sn R → dedropable_sn R.
#R #H1R #H2R #b #f #L1 #K1 #HLK1 #K2 #T * #f1 #Hf1 #HK12 #U #HTU
elim (frees_total L1 U) #f2 #Hf2
lapply (frees_fwd_coafter … Hf2 … HLK1 … HTU … Hf1) -HTU #Hf
-elim (lexs_liftable_co_dedropable … H1R … H2R … HLK1 … HK12 … Hf) -f1 -K1
-/3 width=6 by cfull_lift, ex3_intro, ex2_intro/
+elim (lexs_liftable_co_dedropable_sn … H1R … H2R … HLK1 … HK12 … Hf) -f1 -K1
+/3 width=6 by cfull_lift_sn, ex3_intro, ex2_intro/
qed-.
(* Inversion lemmas with generic slicing for local environments *************)
[ "cpxs_lreq" + "cpxs_lleq" + "cpxs_aaa" * ]
*)
[ "csx_vector ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" * ]
- [ "csx ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" "csx_simple" + "csx_theq" + "csx_drops" + "csx_gcp" + "csx_cnx" + "csx_cpxs" + "csx_csx" * ]
+ [ "csx ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" "csx_simple" + "csx_theq" + "csx_drops" + "csx_lsubr" + "csx_gcp" + "csx_cnx" + "csx_cpxs" + "csx_csx" * ]
[ "lfpxs ( ⦃?,?⦄ ⊢ ⬈*[?,?] ? )" "lfpxs_length" + "lfpxs_fqup" + "lfpxs_cpxs" * ]
[ "cpxs ( ⦃?,?⦄ ⊢ ? ⬈*[?] ? )" "cpxs_tdeq" + "cpxs_theq" + "cpxs_theq_vector" + "cpxs_drops" + "cpxs_lsubr" + "cpxs_lfpx" + "cpxs_cnx" + "cpxs_cpxs" * ]
}
projects / helm.git / commitdiff