∀G,L. ∃k. NF … (RR G L) RS (⋆k).
definition CP2 ≝ λRR:relation4 genv lenv term term. λRS:relation term.
- ∀G,L0,L,T,T0,d,e. NF … (RR G L) RS T →
- ⇩[d, e] L0 ≡ L → ⇧[d, e] T ≡ T0 → NF … (RR G L0) RS T0.
+ ∀G,L0,L,T,T0,s,d,e. NF … (RR G L) RS T →
+ ⇩[s, d, e] L0 ≡ L → ⇧[d, e] T ≡ T0 → NF … (RR G L0) RS T0.
definition CP2s ≝ λRR:relation4 genv lenv term term. λRS:relation term.
- ∀G,L0,L,des. ⇩*[des] L0 ≡ L →
+ ∀G,L0,L,s,des. ⇩*[s, des] L0 ≡ L →
∀T,T0. ⇧*[des] T ≡ T0 →
NF … (RR G L) RS T → NF … (RR G L0) RS T0.
(* Basic_1: was: nf2_lift1 *)
lemma acp_lifts: ∀RR,RS. CP2 RR RS → CP2s RR RS.
-#RR #RS #HRR #G #L1 #L2 #des #H elim H -L1 -L2 -des
+#RR #RS #HRR #G #L1 #L2 #s #des #H elim H -L1 -L2 -des
[ #L #T1 #T2 #H #HT1
<(lifts_inv_nil … H) -H //
| #L1 #L #L2 #des #d #e #_ #HL2 #IHL #T2 #T1 #H #HLT2
- elim (lifts_inv_cons … H) -H /3 width=9/
+ elim (lifts_inv_cons … H) -H /3 width=10 by/
]
qed.
(* Basic_1: was: sc3_arity_csubc *)
theorem aacr_aaa_csubc_lifts: ∀RR,RS,RP.
acp RR RS RP → acr RR RS RP (λG,L,T. RP G L T) →
- ∀G,L1,T,A. ⦃G, L1⦄ ⊢ T ⁝ A → ∀L0,des. ⇩*[des] L0 ≡ L1 →
+ ∀G,L1,T,A. ⦃G, L1⦄ ⊢ T ⁝ A → ∀L0,des. ⇩*[Ⓕ, des] L0 ≡ L1 →
∀T0. ⇧*[des] T ≡ T0 → ∀L2. G ⊢ L2 ⊑[RP] L0 →
⦃G, L2, T0⦄ ϵ[RP] 〚A〛.
#RR #RS #RP #H1RP #H2RP #G #L1 #T #A #H elim H -G -L1 -T -A
@(aacr_abst … H1RP H2RP) [ /2 width=5 by/ ]
#L3 #V3 #W3 #T3 #des3 #HL32 #HW03 #HT03 #H1B #H2B
elim (ldrops_lsubc_trans … H1RP H2RP … HL32 … HL02) -L2 #L2 #HL32 #HL20
- lapply (aaa_lifts … L2 W3 … (des @@ des3) … HLWB) -HLWB /2 width=3 by ldrops_trans, lifts_trans/ #HLW2B
- @(IHA (L2. ⓛW3) … (des + 1 @@ des3 + 1)) -IHA /2 width=3/ /3 width=5 by lsubc_abbr, ldrops_trans, ldrops_skip/
+ lapply (aaa_lifts … L2 W3 … (des @@ des3) … HLWB) -HLWB /2 width=4 by ldrops_trans, lifts_trans/ #HLW2B
+ @(IHA (L2. ⓛW3) … (des + 1 @@ des3 + 1)) -IHA
+ /3 width=5 by lsubc_abbr, ldrops_trans, ldrops_skip, lifts_trans/
| #G #L #V #T #B #A #_ #_ #IHB #IHA #L0 #des #HL0 #X #H #L2 #HL20
elim (lifts_inv_flat1 … H) -H #V0 #T0 #HV0 #HT0 #H destruct
/3 width=10 by ldrops_nil, lifts_nil/
∀G,L,Vs. all … (RP G L) Vs → ∀k. C G L (ⒶVs.⋆k).
definition S5 ≝ λC:relation3 genv lenv term. ∀I,G,L,K,Vs,V1,V2,i.
- C G L (ⒶVs.V2) → ⇧[0, i + 1] V1 ≡ V2 →
- ⇩[0, i] L ≡ K.ⓑ{I}V1 → C G L (ⒶVs.#i).
+ C G L (ⒶVs.V2) → ⇧[0, i+1] V1 ≡ V2 →
+ ⇩[i] L ≡ K.ⓑ{I}V1 → C G L (ⒶVs.#i).
definition S6 ≝ λRP,C:relation3 genv lenv term.
∀G,L,V1s,V2s. ⇧[0, 1] V1s ≡ V2s →
∀G,L,Vs,T,W. C G L (ⒶVs.T) → C G L (ⒶVs.W) → C G L (ⒶVs.ⓝW.T).
definition S8 ≝ λC:relation3 genv lenv term. ∀G,L2,L1,T1,d,e.
- C G L1 T1 → ∀T2. ⇩[d, e] L2 ≡ L1 → ⇧[d, e] T1 ≡ T2 → C G L2 T2.
+ C G L1 T1 → ∀T2. ⇩[Ⓕ, d, e] L2 ≡ L1 → ⇧[d, e] T1 ≡ T2 → C G L2 T2.
definition S8s ≝ λC:relation3 genv lenv term.
- ∀G,L1,L2,des. ⇩*[des] L2 ≡ L1 →
+ ∀G,L1,L2,des. ⇩*[Ⓕ, des] L2 ≡ L1 →
∀T1,T2. ⇧*[des] T1 ≡ T2 → C G L1 T1 → C G L2 T2.
(* properties of the abstract candidate of reducibility *)
λT. match A with
[ AAtom ⇒ RP G L T
| APair B A ⇒ ∀L0,V0,T0,des.
- aacr RP B G L0 V0 → ⇩*[des] L0 ≡ L → ⇧*[des] T ≡ T0 →
+ aacr RP B G L0 V0 → ⇩*[Ⓕ, des] L0 ≡ L → ⇧*[des] T ≡ T0 →
aacr RP A G L0 (ⓐV0.T0)
].
(* Basic_1: was: sc3_lift1 *)
lemma acr_lifts: ∀C. S8 C → S8s C.
#C #HC #G #L1 #L2 #des #H elim H -L1 -L2 -des
-[ #L #T1 #T2 #H #HT1
- <(lifts_inv_nil … H) -H //
+[ #L #T1 #T2 #H #HT1 <(lifts_inv_nil … H) -H //
| #L1 #L #L2 #des #d #e #_ #HL2 #IHL #T2 #T1 #H #HLT2
- elim (lifts_inv_cons … H) -H /3 width=9 by/
+ elim (lifts_inv_cons … H) -H /3 width=10 by/
]
qed.
lemma rp_lifts: ∀RR,RS,RP. acr RR RS RP (λG,L,T. RP G L T) →
- ∀des,G,L0,L,V,V0. ⇩*[des] L0 ≡ L → ⇧*[des] V ≡ V0 →
+ ∀des,G,L0,L,V,V0. ⇩*[Ⓕ, des] L0 ≡ L → ⇧*[des] V ≡ V0 →
RP G L V → RP G L0 V0.
#RR #RS #RP #HRP #des #G #L0 #L #V #V0 #HL0 #HV0 #HV
-@acr_lifts /width=6 by/
+@acr_lifts /width=7 by/
@(s8 … HRP)
qed.
(* Basic_1: was only: sns3_lifts1 *)
lemma rp_liftsv_all: ∀RR,RS,RP. acr RR RS RP (λG,L,T. RP G L T) →
- â\88\80des,G,L0,L,Vs,V0s. â\87§*[des] Vs â\89¡ V0s â\86\92 â\87©*[des] L0 â\89¡ L →
+ â\88\80des,G,L0,L,Vs,V0s. â\87©*[â\92», des] L0 â\89¡ L â\86\92 â\87§*[des] Vs â\89¡ V0s →
all … (RP G L) Vs → all … (RP G L0) V0s.
-#RR #RS #RP #HRP #des #G #L0 #L #Vs #V0s #H elim H -Vs -V0s normalize //
-#T1s #T2s #T1 #T2 #HT12 #_ #IHT2s #HL0 * /3 width=6 by rp_lifts, conj/
+#RR #RS #RP #HRP #des #G #L0 #L #Vs #V0s #HL0 #H elim H -Vs -V0s normalize //
+#T1s #T2s #T1 #T2 #HT12 #_ #IHT2s * /3 width=7 by rp_lifts, conj/
qed.
(* Basic_1: was:
elim (lifts_inv_applv1 … H) -H #V0s #T0 #HV0s #HT0 #H destruct
lapply (s1 … IHB … HB) #HV0
@(s2 … IHA … (V0 @ V0s))
- /3 width=13 by rp_liftsv_all, acp_lifts, cp2, lifts_simple_dx, conj/
+ /3 width=14 by rp_liftsv_all, acp_lifts, cp2, lifts_simple_dx, conj/
| #a #G #L #Vs #U #T #W #HA #L0 #V0 #X #des #HB #HL0 #H
elim (lifts_inv_applv1 … H) -H #V0s #Y #HV0s #HY #H destruct
elim (lifts_inv_flat1 … HY) -HY #U0 #X #HU0 #HX #H destruct
elim (lifts_inv_bind1 … HX) -HX #W0 #T0 #HW0 #HT0 #H destruct
- @(s3 … IHA … (V0 @ V0s)) /5 width=5 by lifts_applv, lifts_flat, lifts_bind/
-| #G #L #Vs #HVs #k #L0 #V0 #X #hdes #HB #HL0 #H
+ @(s3 … IHA … (V0 @ V0s)) /5 width=6 by lifts_applv, lifts_flat, lifts_bind/
+| #G #L #Vs #HVs #k #L0 #V0 #X #des #HB #HL0 #H
elim (lifts_inv_applv1 … H) -H #V0s #Y #HV0s #HY #H destruct
>(lifts_inv_sort1 … HY) -Y
lapply (s1 … IHB … HB) #HV0
- @(s4 … IHA … (V0 @ V0s)) /3 width=6 by rp_liftsv_all, conj/
+ @(s4 … IHA … (V0 @ V0s)) /3 width=7 by rp_liftsv_all, conj/
| #I #G #L #K #Vs #V1 #V2 #i #HA #HV12 #HLK #L0 #V0 #X #des #HB #HL0 #H
elim (lifts_inv_applv1 … H) -H #V0s #Y #HV0s #HY #H destruct
elim (lifts_inv_lref1 … HY) -HY #i0 #Hi0 #H destruct
elim (lift_total W1 0 (i0 + 1)) #W2 #HW12
elim (lifts_lift_trans … Hdes0 … HVW1 … HW12) // -Hdes0 -Hi0 #V3 #HV13 #HVW2
>(lift_mono … HV13 … HV12) in HVW2; -V3 #HVW2
- @(s5 … IHA … (V0 @ V0s) … HW12 HL02) /3 width=4 by lifts_applv/
+ @(s5 … IHA … (V0 @ V0s) … HW12 HL02) /3 width=5 by lifts_applv/
| #G #L #V1s #V2s #HV12s #a #V #T #HA #HV #L0 #V10 #X #des #HB #HL0 #H
elim (lifts_inv_applv1 … H) -H #V10s #Y #HV10s #HY #H destruct
elim (lifts_inv_bind1 … HY) -HY #V0 #T0 #HV0 #HT0 #H destruct
elim (lift_total V10 0 1) #V20 #HV120
elim (liftv_total 0 1 V10s) #V20s #HV120s
- @(s6 … IHA … (V10 @ V10s) (V20 @ V20s)) /3 width=6 by rp_lifts, liftv_cons/
- @(HA … (des + 1)) /2 width=1 by ldrops_skip/
- [ @(s8 … IHB … HB … HV120) /2 width=1 by ldrop_ldrop/
+ @(s6 … IHA … (V10 @ V10s) (V20 @ V20s)) /3 width=7 by rp_lifts, liftv_cons/
+ @(HA … (des + 1)) /2 width=2 by ldrops_skip/
+ [ @(s8 … IHB … HB … HV120) /2 width=2 by ldrop_drop/
| @lifts_applv //
elim (liftsv_liftv_trans_le … HV10s … HV120s) -V10s #V10s #HV10s #HV120s
>(liftv_mono … HV12s … HV10s) -V1s //
| #G #L #Vs #T #W #HA #HW #L0 #V0 #X #des #HB #HL0 #H
elim (lifts_inv_applv1 … H) -H #V0s #Y #HV0s #HY #H destruct
elim (lifts_inv_flat1 … HY) -HY #W0 #T0 #HW0 #HT0 #H destruct
- @(s7 … IHA … (V0 @ V0s)) /3 width=4 by lifts_applv/
+ @(s7 … IHA … (V0 @ V0s)) /3 width=5 by lifts_applv/
| /3 width=7 by ldrops_cons, lifts_cons/
]
qed.
lemma aacr_abst: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λG,L,T. RP G L T) →
∀a,G,L,W,T,A,B. ⦃G, L, W⦄ ϵ[RP] 〚B〛 → (
- ∀L0,V0,W0,T0,des. ⇩*[des] L0 ≡ L → ⇧*[des ] W ≡ W0 → ⇧*[des + 1] T ≡ T0 →
+ ∀L0,V0,W0,T0,des. ⇩*[Ⓕ, des] L0 ≡ L → ⇧*[des ] W ≡ W0 → ⇧*[des + 1] T ≡ T0 →
⦃G, L0, V0⦄ ϵ[RP] 〚B〛 → ⦃G, L0, W0⦄ ϵ[RP] 〚B〛 → ⦃G, L0.ⓓⓝW0.V0, T0⦄ ϵ[RP] 〚A〛
) →
⦃G, L, ⓛ{a}W.T⦄ ϵ[RP] 〚②B.A〛.
(* Relocation properties ****************************************************)
lemma cpds_lift: ∀h,g,G. l_liftable (cpds h g G).
-#h #g #G #K #T1 #T2 * #T #l1 #l2 #Hl12 #Hl1 #HT1 #HT2 #L #d #e
+#h #g #G #K #T1 #T2 * #T #l1 #l2 #Hl12 #Hl1 #HT1 #HT2 #L #s #d #e
elim (lift_total T d e)
-/3 width=15 by cprs_lift, da_lift, lsstas_lift, ex4_3_intro/
+/3 width=16 by cprs_lift, da_lift, lsstas_lift, ex4_3_intro/
qed.
lemma cpds_inv_lift1: ∀h,g,G. l_deliftable_sn (cpds h g G).
-#h #g #G #L #U1 #U2 * #U #l1 #l2 #Hl12 #Hl1 #HU1 #HU2 #K #d #e #HLK #T1 #HTU1
+#h #g #G #L #U1 #U2 * #U #l1 #l2 #Hl12 #Hl1 #HU1 #HU2 #K #s #d #e #HLK #T1 #HTU1
lapply (da_inv_lift … Hl1 … HLK … HTU1) -Hl1 #Hl1
elim (lsstas_inv_lift1 … HU1 … HLK … HTU1) -U1 #T #HTU #HT1
-elim (cprs_inv_lift1 … HU2 … HLK … HTU) -U -L /3 width=9/
+elim (cprs_inv_lift1 … HU2 … HLK … HTU) -U -L
+/3 width=9 by ex4_3_intro, ex2_intro/
qed-.
(* Note: apparently this was missing in basic_1 *)
lemma cprs_delta: ∀G,L,K,V,V2,i.
- ⇩[0, i] L ≡ K.ⓓV → ⦃G, K⦄ ⊢ V ➡* V2 →
+ ⇩[i] L ≡ K.ⓓV → ⦃G, K⦄ ⊢ V ➡* V2 →
∀W2. ⇧[0, i + 1] V2 ≡ W2 → ⦃G, L⦄ ⊢ #i ➡* W2.
-#G #L #K #V #V2 #i #HLK #H elim H -V2 [ /3 width=6/ ]
+#G #L #K #V #V2 #i #HLK #H elim H -V2 [ /3 width=6 by cpr_cprs, cpr_delta/ ]
#V1 #V2 #_ #HV12 #IHV1 #W2 #HVW2
lapply (ldrop_fwd_drop2 … HLK) -HLK #HLK
-elim (lift_total V1 0 (i+1)) /4 width=11 by cpr_lift, cprs_strap1/
+elim (lift_total V1 0 (i+1)) /4 width=12 by cpr_lift, cprs_strap1/
qed.
(* Advanced inversion lemmas ************************************************)
(* Basic_1: was: pr3_gen_lref *)
lemma cprs_inv_lref1: ∀G,L,T2,i. ⦃G, L⦄ ⊢ #i ➡* T2 →
T2 = #i ∨
- ∃∃K,V1,T1. ⇩[0, i] L ≡ K. ⓓV1 & ⦃G, K⦄ ⊢ V1 ➡* T1 &
+ ∃∃K,V1,T1. ⇩[i] L ≡ K.ⓓV1 & ⦃G, K⦄ ⊢ V1 ➡* T1 &
⇧[0, i + 1] T1 ≡ T2.
-#G #L #T2 #i #H @(cprs_ind … H) -T2 /2 width=1/
+#G #L #T2 #i #H @(cprs_ind … H) -T2 /2 width=1 by or_introl/
#T #T2 #_ #HT2 *
[ #H destruct
- elim (cpr_inv_lref1 … HT2) -HT2 /2 width=1/
- * /4 width=6/
+ elim (cpr_inv_lref1 … HT2) -HT2 /2 width=1 by or_introl/
+ * /4 width=6 by cpr_cprs, ex3_3_intro, or_intror/
| * #K #V1 #T1 #HLK #HVT1 #HT1
lapply (ldrop_fwd_drop2 … HLK) #H0LK
- elim (cpr_inv_lift1 … HT2 … H0LK … HT1) -H0LK -T /4 width=6/
+ elim (cpr_inv_lift1 … HT2 … H0LK … HT1) -H0LK -T
+ /4 width=6 by cprs_strap1, ex3_3_intro, or_intror/
]
qed-.
(* Basic_1: was: pr3_lift *)
lemma cprs_lift: ∀G. l_liftable (cprs G).
-/3 width=9/ qed.
+/3 width=10 by l_liftable_LTC, cpr_lift/ qed.
(* Basic_1: was: pr3_gen_lift *)
lemma cprs_inv_lift1: ∀G. l_deliftable_sn (cprs G).
-/3 width=5 by l_deliftable_sn_LTC, cpr_inv_lift1/
+/3 width=6 by l_deliftable_sn_LTC, cpr_inv_lift1/
qed-.
]
| #G #L #K #T1 #U1 #e #HLK #HTU1 #T2 #HT12 #H elim (lift_total T2 0 (e+1))
#U2 #HTU2 @(ex3_intro … U2)
- [1,3: /2 width=9 by cpxs_lift, fqu_drop/
+ [1,3: /2 width=10 by cpxs_lift, fqu_drop/
| #H0 destruct /3 width=5 by lift_inj/
]
qed-.
(**************************************************************************)
include "basic_2/substitution/cpys_cpys.ma".
+include "basic_2/reduction/cpx_cpys.ma".
include "basic_2/computation/cpxs_cpxs.ma".
(* SN EXTENDED PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS ********************)
(* Main properties **********************************************************)
-lemma cpx_fwd_cpys_tpxs: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[h, g] T2 →
+axiom cpys_split_down: ∀G,L,T1,T2,d,e. ⦃G, L⦄ ⊢ T1 ▶*×[d, e] T2 →
+ ∀i. d ≤ i → i ≤ d + e →
+ ∃∃T. ⦃G, L⦄ ⊢ T1 ▶*×[i, d+e-i] T & ⦃G, L⦄ ⊢ T ▶*×[d, i-d] T2.
+
+lemma cpys_tpxs_trans: ∀h,g,G,L,T1,T,d,e. ⦃G, L⦄ ⊢ T1 ▶*×[d, e] T →
+ ∀T2. ⦃G, ⋆⦄ ⊢ T ➡*[h, g] T2 → ⦃G, L⦄ ⊢ T1 ➡*[h, g] T2.
+#h #g #G #L #T1 #T #d #e #HT1 #T2 #H @(cpxs_ind … H) -T2
+/3 width=5 by cpxs_strap1, cpys_cpx, lsubr_cpx_trans, cpx_cpxs/
+qed-.
+
+axiom cpx_fwd_cpys_tpxs: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[h, g] T2 →
∃∃T. ⦃G, L⦄ ⊢ T1 ▶*×[0, ∞] T & ⦃G, ⋆⦄ ⊢ T ➡*[h, g] T2.
+(*
#h #g #G #L #T1 #T2 #H elim H -G -L -T1 -T2
[ /2 width=3 by ex2_intro/
| /4 width=3 by cpx_cpxs, cpx_sort, ex2_intro/
| #I #G #L #K #V1 #V2 #W2 #i #HLK #_ #HVW2 * #V #HV1 #HV2
elim (lift_total V 0 (i+1)) #W #HVW
- @(ex2_intro … W) /2 width=7 by cpys_subst_Y2/
+ lapply (cpxs_lift … HV2 (⋆) (Ⓣ) … HVW … HVW2)
+ [ @ldrop_atom #H destruct | /3 width=7 by cpys_subst_Y2, ex2_intro/ ]
| #a #I #G #L #V1 #V2 #T1 #T2 #_ #_ * #V #HV1 #HV2 * #T #HT1 #HT2
- elim (cpys_split_up … HT1 1) -HT1 // #T0 #HT10 #HT0
+ elim (cpys_split_down … HT1 1) -HT1 // #T0 #HT10 #HT0
+(*
@(ex2_intro … (ⓑ{a,I}V.T0))
- [ @(cpys_bind … HV1) -HV1
+ [ @cpys_bind //
| @(cpxs_bind … HV2) -HV2
- ]
+
+ /2 width=5 by cpys_tpxs_trans/
+ ]
+*)*)
\ No newline at end of file
qed.
lemma cpxs_delta: ∀h,g,I,G,L,K,V,V2,i.
- ⇩[0, i] L ≡ K.ⓑ{I}V → ⦃G, K⦄ ⊢ V ➡*[h, g] V2 →
- ∀W2. ⇧[0, i + 1] V2 ≡ W2 → ⦃G, L⦄ ⊢ #i ➡*[h, g] W2.
+ ⇩[i] L ≡ K.ⓑ{I}V → ⦃G, K⦄ ⊢ V ➡*[h, g] V2 →
+ ∀W2. ⇧[0, i+1] V2 ≡ W2 → ⦃G, L⦄ ⊢ #i ➡*[h, g] W2.
#h #g #I #G #L #K #V #V2 #i #HLK #H elim H -V2
[ /3 width=9 by cpx_cpxs, cpx_delta/
| #V1 lapply (ldrop_fwd_drop2 … HLK) -HLK
- elim (lift_total V1 0 (i+1)) /4 width=11 by cpx_lift, cpxs_strap1/
+ elim (lift_total V1 0 (i+1)) /4 width=12 by cpx_lift, cpxs_strap1/
]
qed.
lemma cpxs_inv_lref1: ∀h,g,G,L,T2,i. ⦃G, L⦄ ⊢ #i ➡*[h, g] T2 →
T2 = #i ∨
- ∃∃I,K,V1,T1. ⇩[0, i] L ≡ K.ⓑ{I}V1 & ⦃G, K⦄ ⊢ V1 ➡*[h, g] T1 &
- ⇧[0, i + 1] T1 ≡ T2.
+ ∃∃I,K,V1,T1. ⇩[i] L ≡ K.ⓑ{I}V1 & ⦃G, K⦄ ⊢ V1 ➡*[h, g] T1 &
+ ⇧[0, i+1] T1 ≡ T2.
#h #g #G #L #T2 #i #H @(cpxs_ind … H) -T2 /2 width=1 by or_introl/
#T #T2 #_ #HT2 *
[ #H destruct
(* Relocation properties ****************************************************)
lemma cpxs_lift: ∀h,g,G. l_liftable (cpxs h g G).
-/3 width=9 by cpx_lift, cpxs_strap1, l_liftable_LTC/ qed.
+/3 width=10 by cpx_lift, cpxs_strap1, l_liftable_LTC/ qed.
lemma cpxs_inv_lift1: ∀h,g,G. l_deliftable_sn (cpxs h g G).
-/3 width=5 by l_deliftable_sn_LTC, cpx_inv_lift1/
+/3 width=6 by l_deliftable_sn_LTC, cpx_inv_lift1/
qed-.
(* Properties on supclosure *************************************************)
⋆k ≃ U ∨ ⦃G, L⦄ ⊢ ⋆(next h k) ➡*[h, g] U.
#h #g #G #L #U #k #H
elim (cpxs_inv_sort1 … H) -H #n #l generalize in match k; -k @(nat_ind_plus … n) -n
-[ #k #_ #H -l destruct /2 width=1/
+[ #k #_ #H -l destruct /2 width=1 by or_introl/
| #n #IHn #k >plus_plus_comm_23 #Hnl #H destruct
lapply (deg_next_SO … Hnl) -Hnl #Hnl
elim (IHn … Hnl) -IHn
- [ #H lapply (tstc_inv_atom1 … H) -H #H >H -H /2 width=1/
- | generalize in match Hnl; -Hnl @(nat_ind_plus … n) -n /2 width=1/
- #n #_ /4 width=3/
+ [ #H lapply (tstc_inv_atom1 … H) -H #H >H -H /2 width=1 by or_intror/
+ | generalize in match Hnl; -Hnl @(nat_ind_plus … n) -n
+ /4 width=3 by cpxs_strap2, cpx_sort, or_intror/
| >iter_SO >iter_n_Sm //
]
]
ⓐV.ⓛ{a}W.T ≃ U ∨ ⦃G, L⦄ ⊢ ⓓ{a}ⓝW.V.T ➡*[h, g] U.
#h #g #a #G #L #V #W #T #U #H
elim (cpxs_inv_appl1 … H) -H *
-[ #V0 #T0 #_ #_ #H destruct /2 width=1/
+[ #V0 #T0 #_ #_ #H destruct /2 width=1 by tstc_pair, or_introl/
| #b #W0 #T0 #HT0 #HU
elim (cpxs_inv_abst1 … HT0) -HT0 #W1 #T1 #HW1 #HT1 #H destruct
- lapply (lsubr_cpxs_trans … HT1 (L.ⓓⓝW.V) ?) -HT1 /2 width=1/ #HT1
- @or_intror @(cpxs_trans … HU) -U /3 width=1/ (**) (* explicit constructor *)
+ lapply (lsubr_cpxs_trans … HT1 (L.ⓓⓝW.V) ?) -HT1
+ /5 width=3 by cpxs_trans, cpxs_bind, cpxs_pair_sn, lsubr_abst, or_intror/
| #b #V1 #V2 #V0 #T1 #_ #_ #HT1 #_
elim (cpxs_inv_abst1 … HT1) -HT1 #W2 #T2 #_ #_ #H destruct
]
qed-.
(* Note: probably this is an inversion lemma *)
-lemma cpxs_fwd_delta: ∀h,g,I,G,L,K,V1,i. ⇩[0, i] L ≡ K.ⓑ{I}V1 →
+lemma cpxs_fwd_delta: ∀h,g,I,G,L,K,V1,i. ⇩[i] L ≡ K.ⓑ{I}V1 →
∀V2. ⇧[0, i + 1] V1 ≡ V2 →
∀U. ⦃G, L⦄ ⊢ #i ➡*[h, g] U →
#i ≃ U ∨ ⦃G, L⦄ ⊢ V2 ➡*[h, g] U.
#h #g #I #G #L #K #V1 #i #HLK #V2 #HV12 #U #H
-elim (cpxs_inv_lref1 … H) -H /2 width=1/
+elim (cpxs_inv_lref1 … H) -H /2 width=1 by or_introl/
* #I0 #K0 #V0 #U0 #HLK0 #HVU0 #HU0
lapply (ldrop_mono … HLK0 … HLK) -HLK0 #H destruct
-lapply (ldrop_fwd_drop2 … HLK) -HLK /3 width=9/
+/4 width=10 by cpxs_lift, ldrop_fwd_drop2, or_intror/
qed-.
lemma cpxs_fwd_theta: ∀h,g,a,G,L,V1,V,T,U. ⦃G, L⦄ ⊢ ⓐV1.ⓓ{a}V.T ➡*[h, g] U →
⦃G, L⦄ ⊢ ⓓ{a}V.ⓐV2.T ➡*[h, g] U.
#h #g #a #G #L #V1 #V #T #U #H #V2 #HV12
elim (cpxs_inv_appl1 … H) -H *
-[ -HV12 #V0 #T0 #_ #_ #H destruct /2 width=1/
+[ -HV12 #V0 #T0 #_ #_ #H destruct /2 width=1 by tstc_pair, or_introl/
| #b #W #T0 #HT0 #HU
elim (cpxs_inv_abbr1 … HT0) -HT0 *
[ #V3 #T3 #_ #_ #H destruct
| #X #HT2 #H #H0 destruct
elim (lift_inv_bind1 … H) -H #W2 #T2 #HW2 #HT02 #H destruct
@or_intror @(cpxs_trans … HU) -U (**) (* explicit constructor *)
- @(cpxs_trans … (+ⓓV.ⓐV2.ⓛ{b}W2.T2)) [ /3 width=1/ ] -T
- @(cpxs_strap2 … (ⓐV1.ⓛ{b}W.T0)) [2: /2 width=1/ ]
- /4 width=7 by cpx_zeta, lift_bind, lift_flat/ (**) (* auto too slow without trace *)
+ @(cpxs_trans … (+ⓓV.ⓐV2.ⓛ{b}W2.T2)) [ /3 width=1 by cpxs_flat_dx, cpxs_bind_dx/ ] -T
+ @(cpxs_strap2 … (ⓐV1.ⓛ{b}W.T0)) [2: /2 width=1 by cpxs_beta_dx/ ]
+ /4 width=7 by cpx_zeta, lift_bind, lift_flat/
]
| #b #V3 #V4 #V0 #T0 #HV13 #HV34 #HT0 #HU
@or_intror @(cpxs_trans … HU) -U (**) (* explicit constructor *)
elim (cpxs_inv_abbr1 … HT0) -HT0 *
[ #V5 #T5 #HV5 #HT5 #H destruct
- lapply (cpxs_lift … HV13 (L.ⓓV) … HV12 … HV34) -V1 -V3 /2 width=1/
- /3 width=1/
+ lapply (cpxs_lift … HV13 (L.ⓓV) … HV12 … HV34) -V1 -V3
+ /3 width=2 by cpxs_flat, cpxs_bind, ldrop_drop/
| #X #HT1 #H #H0 destruct
elim (lift_inv_bind1 … H) -H #V5 #T5 #HV05 #HT05 #H destruct
- lapply (cpxs_lift … HV13 (L.ⓓV0) … HV12 … HV34) -V3 /2 width=1/ #HV24
- @(cpxs_trans … (+ⓓV.ⓐV2.ⓓ{b}V5.T5)) [ /3 width=1/ ] -T
- @(cpxs_strap2 … (ⓐV1.ⓓ{b}V0.T0)) [ /4 width=7 by cpx_zeta, lift_bind, lift_flat/ ] -V -V5 -T5 (**) (* auto too slow without trace *)
- @(cpxs_strap2 … (ⓓ{b}V0.ⓐV2.T0)) [ /3 width=3/ ] -V1 /3 width=1/
+ lapply (cpxs_lift … HV13 (L.ⓓV0) … HV12 … HV34) -V3 /2 width=2 by ldrop_drop/ #HV24
+ @(cpxs_trans … (+ⓓV.ⓐV2.ⓓ{b}V5.T5)) [ /3 width=1 by cpxs_flat_dx, cpxs_bind_dx/ ] -T
+ @(cpxs_strap2 … (ⓐV1.ⓓ{b}V0.T0)) [ /4 width=7 by cpx_zeta, lift_bind, lift_flat/ ] -V -V5 -T5
+ @(cpxs_strap2 … (ⓓ{b}V0.ⓐV2.T0)) /3 width=3 by cpxs_pair_sn, cpxs_bind_dx, cpr_cpx, cpr_theta/
]
]
qed-.
lemma cpxs_fwd_cast: ∀h,g,G,L,W,T,U. ⦃G, L⦄ ⊢ ⓝW.T ➡*[h, g] U →
∨∨ ⓝW. T ≃ U | ⦃G, L⦄ ⊢ T ➡*[h, g] U | ⦃G, L⦄ ⊢ W ➡*[h, g] U.
#h #g #G #L #W #T #U #H
-elim (cpxs_inv_cast1 … H) -H /2 width=1/ *
-#W0 #T0 #_ #_ #H destruct /2 width=1/
+elim (cpxs_inv_cast1 … H) -H /2 width=1 by or3_intro1, or3_intro2/ *
+#W0 #T0 #_ #_ #H destruct /2 width=1 by tstc_pair, or3_intro0/
qed-.
#h #g #G #L #T #H1T #H2T #Vs elim Vs -Vs [ @(cpxs_fwd_cnx … H2T) ] (**) (* /2 width=3 by cpxs_fwd_cnx/ does not work *)
#V #Vs #IHVs #U #H
elim (cpxs_inv_appl1 … H) -H *
-[ -IHVs #V0 #T0 #_ #_ #H destruct /2 width=1/
+[ -IHVs #V0 #T0 #_ #_ #H destruct /2 width=1 by tstc_pair/
| #a #W0 #T0 #HT0 #HU
lapply (IHVs … HT0) -IHVs -HT0 #HT0
elim (tstc_inv_bind_appls_simple … HT0) //
#h #g #G #L #k #Vs elim Vs -Vs /2 width=1 by cpxs_fwd_sort/
#V #Vs #IHVs #U #H
elim (cpxs_inv_appl1 … H) -H *
-[ -IHVs #V1 #T1 #_ #_ #H destruct /2 width=1/
+[ -IHVs #V1 #T1 #_ #_ #H destruct /2 width=1 by tstc_pair, or_introl/
| #a #W1 #T1 #HT1 #HU
elim (IHVs … HT1) -IHVs -HT1 #HT1
[ elim (tstc_inv_bind_appls_simple … HT1) //
| @or_intror (**) (* explicit constructor *)
@(cpxs_trans … HU) -U
- @(cpxs_strap1 … (ⓐV.ⓛ{a}W1.T1)) [ /2 width=1/ ] -Vs /3 width=1/
+ @(cpxs_strap1 … (ⓐV.ⓛ{a}W1.T1)) /3 width=1 by cpxs_flat_dx, cpr_cpx, cpr_beta/
]
| #a #V1 #V2 #V3 #T1 #HV01 #HV12 #HT1 #HU
elim (IHVs … HT1) -IHVs -HT1 #HT1
[ elim (tstc_inv_bind_appls_simple … HT1) //
| @or_intror (**) (* explicit constructor *)
@(cpxs_trans … HU) -U
- @(cpxs_strap1 … (ⓐV1.ⓓ{a}V3.T1)) [ /2 width=1/ ] -Vs /3 width=3/
+ @(cpxs_strap1 … (ⓐV1.ⓓ{a}V3.T1)) /3 width=3 by cpxs_flat, cpr_cpx, cpr_theta/
]
]
qed-.
#h #g #a #G #L #Vs elim Vs -Vs /2 width=1 by cpxs_fwd_beta/
#V0 #Vs #IHVs #V #W #T #U #H
elim (cpxs_inv_appl1 … H) -H *
-[ -IHVs #V1 #T1 #_ #_ #H destruct /2 width=1/
+[ -IHVs #V1 #T1 #_ #_ #H destruct /2 width=1 by tstc_pair, or_introl/
| #b #W1 #T1 #HT1 #HU
elim (IHVs … HT1) -IHVs -HT1 #HT1
[ elim (tstc_inv_bind_appls_simple … HT1) //
| @or_intror (**) (* explicit constructor *)
@(cpxs_trans … HU) -U
- @(cpxs_strap1 … (ⓐV0.ⓛ{b}W1.T1)) [ /2 width=1/ ] -V -Vs -T /3 width=1/
+ @(cpxs_strap1 … (ⓐV0.ⓛ{b}W1.T1)) /3 width=1 by cpxs_flat_dx, cpr_cpx, cpr_beta/
]
| #b #V1 #V2 #V3 #T1 #HV01 #HV12 #HT1 #HU
elim (IHVs … HT1) -IHVs -HT1 #HT1
[ elim (tstc_inv_bind_appls_simple … HT1) //
| @or_intror (**) (* explicit constructor *)
@(cpxs_trans … HU) -U
- @(cpxs_strap1 … (ⓐV1.ⓓ{b}V3.T1)) [ /2 width=1/ ] -V -V0 -Vs -T /3 width=3/
+ @(cpxs_strap1 … (ⓐV1.ⓓ{b}V3.T1)) /3 width=3 by cpxs_flat, cpr_cpx, cpr_theta/
]
]
qed-.
-lemma cpxs_fwd_delta_vector: ∀h,g,I,G,L,K,V1,i. ⇩[0, i] L ≡ K.ⓑ{I}V1 →
+lemma cpxs_fwd_delta_vector: ∀h,g,I,G,L,K,V1,i. ⇩[i] L ≡ K.ⓑ{I}V1 →
∀V2. ⇧[0, i + 1] V1 ≡ V2 →
∀Vs,U. ⦃G, L⦄ ⊢ ⒶVs.#i ➡*[h, g] U →
ⒶVs.#i ≃ U ∨ ⦃G, L⦄ ⊢ ⒶVs.V2 ➡*[h, g] U.
#h #g #I #G #L #K #V1 #i #HLK #V2 #HV12 #Vs elim Vs -Vs /2 width=5 by cpxs_fwd_delta/
#V #Vs #IHVs #U #H -K -V1
elim (cpxs_inv_appl1 … H) -H *
-[ -IHVs #V0 #T0 #_ #_ #H destruct /2 width=1/
+[ -IHVs #V0 #T0 #_ #_ #H destruct /2 width=1 by tstc_pair, or_introl/
| #b #W0 #T0 #HT0 #HU
elim (IHVs … HT0) -IHVs -HT0 #HT0
[ elim (tstc_inv_bind_appls_simple … HT0) //
| @or_intror -i (**) (* explicit constructor *)
@(cpxs_trans … HU) -U
- @(cpxs_strap1 … (ⓐV.ⓛ{b}W0.T0)) [ /2 width=1/ ] -V2 -Vs /3 width=1/
+ @(cpxs_strap1 … (ⓐV.ⓛ{b}W0.T0)) /3 width=1 by cpxs_flat_dx, cpr_cpx, cpr_beta/
]
| #b #V0 #V1 #V3 #T0 #HV0 #HV01 #HT0 #HU
elim (IHVs … HT0) -IHVs -HT0 #HT0
[ elim (tstc_inv_bind_appls_simple … HT0) //
| @or_intror -i (**) (* explicit constructor *)
@(cpxs_trans … HU) -U
- @(cpxs_strap1 … (ⓐV0.ⓓ{b}V3.T0)) [ /2 width=1/ ] -V -V2 -Vs /3 width=3/
+ @(cpxs_strap1 … (ⓐV0.ⓓ{b}V3.T0)) /3 width=3 by cpxs_flat, cpr_cpx, cpr_theta/
]
]
qed-.
lemma cpxs_fwd_theta_vector: ∀h,g,G,L,V1s,V2s. ⇧[0, 1] V1s ≡ V2s →
∀a,V,T,U. ⦃G, L⦄ ⊢ ⒶV1s.ⓓ{a}V.T ➡*[h, g] U →
ⒶV1s. ⓓ{a}V. T ≃ U ∨ ⦃G, L⦄ ⊢ ⓓ{a}V.ⒶV2s.T ➡*[h, g] U.
-#h #g #G #L #V1s #V2s * -V1s -V2s /3 width=1/
+#h #g #G #L #V1s #V2s * -V1s -V2s /3 width=1 by or_intror/
#V1s #V2s #V1a #V2a #HV12a #HV12s #a
generalize in match HV12a; -HV12a
generalize in match V2a; -V2a
elim HV12s -V1s -V2s /2 width=1 by cpxs_fwd_theta/
#V1s #V2s #V1b #V2b #HV12b #_ #IHV12s #V1a #V2a #HV12a #V #T #U #H
elim (cpxs_inv_appl1 … H) -H *
-[ -IHV12s -HV12a -HV12b #V0 #T0 #_ #_ #H destruct /2 width=1/
+[ -IHV12s -HV12a -HV12b #V0 #T0 #_ #_ #H destruct /2 width=1 by tstc_pair, or_introl/
| #b #W0 #T0 #HT0 #HU
elim (IHV12s … HV12b … HT0) -IHV12s -HT0 #HT0
[ -HV12a -HV12b -HU
[ -HV12a -HV12b #V1 #T1 #_ #_ #H destruct
| -V1b #X #HT1 #H #H0 destruct
elim (lift_inv_bind1 … H) -H #W1 #T1 #HW01 #HT01 #H destruct
- @(cpxs_trans … (+ⓓV.ⓐV2a.ⓛ{b}W1.T1)) [ /3 width=1/ ] -T -V2b -V2s
- @(cpxs_strap2 … (ⓐV1a.ⓛ{b}W0.T0)) [2: /2 width=1/ ]
- /4 width=7 by cpx_zeta, lift_bind, lift_flat/ (* auto too slow without trace *)
+ @(cpxs_trans … (+ⓓV.ⓐV2a.ⓛ{b}W1.T1)) [ /3 width=1 by cpxs_flat_dx, cpxs_bind_dx/ ] -T -V2b -V2s
+ @(cpxs_strap2 … (ⓐV1a.ⓛ{b}W0.T0))
+ /4 width=7 by cpxs_beta_dx, cpx_zeta, lift_bind, lift_flat/
]
]
| #b #V0a #Va #V0 #T0 #HV10a #HV0a #HT0 #HU
@(cpxs_trans … HU) -U
elim (cpxs_inv_abbr1 … HT0) -HT0 *
[ #V1 #T1 #HV1 #HT1 #H destruct
- lapply (cpxs_lift … HV10a (L.ⓓV) … HV12a … HV0a) -V1a -V0a [ /2 width=1/ ] #HV2a
- @(cpxs_trans … (ⓓ{a}V.ⓐV2a.T1)) [ /3 width=1/ ] -T -V2b -V2s /3 width=1/
+ lapply (cpxs_lift … HV10a (L.ⓓV) (Ⓣ) … HV12a … HV0a) -V1a -V0a [ /2 width=1 by ldrop_drop/ ] #HV2a
+ @(cpxs_trans … (ⓓ{a}V.ⓐV2a.T1)) /3 width=1 by cpxs_bind, cpxs_pair_sn, cpxs_flat_dx, cpxs_bind_dx/
| #X #HT1 #H #H0 destruct
elim (lift_inv_bind1 … H) -H #V1 #T1 #HW01 #HT01 #H destruct
- lapply (cpxs_lift … HV10a (L.ⓓV0) … HV12a … HV0a) -V0a [ /2 width=1/ ] #HV2a
- @(cpxs_trans … (+ⓓV.ⓐV2a.ⓓ{b}V1.T1)) [ /3 width=1/ ] -T -V2b -V2s
- @(cpxs_strap2 … (ⓐV1a.ⓓ{b}V0.T0)) [ /4 width=7 by cpx_zeta, lift_bind, lift_flat/ ] -V -V1 -T1 (* auto too slow without trace *)
- @(cpxs_strap2 … (ⓓ{b}V0.ⓐV2a.T0)) [ /3 width=3/ ] -V1a /3 width=1/
+ lapply (cpxs_lift … HV10a (L.ⓓV0) (Ⓣ) … HV12a … HV0a) -V0a [ /2 width=1 by ldrop_drop/ ] #HV2a
+ @(cpxs_trans … (+ⓓV.ⓐV2a.ⓓ{b}V1.T1)) [ /3 width=1 by cpxs_flat_dx, cpxs_bind_dx/ ] -T -V2b -V2s
+ @(cpxs_strap2 … (ⓐV1a.ⓓ{b}V0.T0)) [ /4 width=7 by cpx_zeta, lift_bind, lift_flat/ ] -V -V1 -T1
+ @(cpxs_strap2 … (ⓓ{b}V0.ⓐV2a.T0)) /3 width=3 by cpxs_pair_sn, cpxs_bind_dx, cpr_cpx, cpr_theta/
]
]
]
#h #g #G #L #Vs elim Vs -Vs /2 width=1 by cpxs_fwd_cast/
#V #Vs #IHVs #W #T #U #H
elim (cpxs_inv_appl1 … H) -H *
-[ -IHVs #V0 #T0 #_ #_ #H destruct /2 width=1/
-| #b #W0 #T0 #HT0 #HU
- elim (IHVs … HT0) -IHVs -HT0 #HT0
+[ -IHVs #V0 #T0 #_ #_ #H destruct /2 width=1 by tstc_pair, or3_intro0/
+| #b #W0 #T0 #HT0 #HU elim (IHVs … HT0) -IHVs -HT0 #HT0
[ elim (tstc_inv_bind_appls_simple … HT0) //
| @or3_intro1 -W (**) (* explicit constructor *)
@(cpxs_trans … HU) -U
- @(cpxs_strap1 … (ⓐV.ⓛ{b}W0.T0)) /2 width=1/
+ @(cpxs_strap1 … (ⓐV.ⓛ{b}W0.T0)) /2 width=1 by cpxs_flat_dx, cpx_beta/
| @or3_intro2 -T (**) (* explicit constructor *)
@(cpxs_trans … HU) -U
- @(cpxs_strap1 … (ⓐV.ⓛ{b}W0.T0)) /2 width=1/
+ @(cpxs_strap1 … (ⓐV.ⓛ{b}W0.T0)) /2 width=1 by cpxs_flat_dx, cpx_beta/
]
| #b #V0 #V1 #V2 #T0 #HV0 #HV01 #HT0 #HU
elim (IHVs … HT0) -IHVs -HT0 #HT0
[ elim (tstc_inv_bind_appls_simple … HT0) //
| @or3_intro1 -W (**) (* explicit constructor *)
@(cpxs_trans … HU) -U
- @(cpxs_strap1 … (ⓐV0.ⓓ{b}V2.T0)) [ /2 width=1/ ] -V -Vs -T /2 width=3/
+ @(cpxs_strap1 … (ⓐV0.ⓓ{b}V2.T0)) /2 width=3 by cpxs_flat, cpx_theta/
| @or3_intro2 -T (**) (* explicit constructor *)
@(cpxs_trans … HU) -U
- @(cpxs_strap1 … (ⓐV0.ⓓ{b}V2.T0)) [ /2 width=1/ ] -V -Vs -W /2 width=3/
+ @(cpxs_strap1 … (ⓐV0.ⓓ{b}V2.T0)) /2 width=3 by cpxs_flat, cpx_theta/
]
]
qed-.
(* Relocation properties ****************************************************)
(* Basic_1: was just: sn3_lift *)
-lemma csx_lift: ∀h,g,G,L2,L1,T1,d,e. ⦃G, L1⦄ ⊢ ⬊*[h, g] T1 →
- ∀T2. ⇩[d, e] L2 ≡ L1 → ⇧[d, e] T1 ≡ T2 → ⦃G, L2⦄ ⊢ ⬊*[h, g] T2.
-#h #g #G #L2 #L1 #T1 #d #e #H elim H -T1 #T1 #_ #IHT1 #T2 #HL21 #HT12
+lemma csx_lift: ∀h,g,G,L2,L1,T1,s,d,e. ⦃G, L1⦄ ⊢ ⬊*[h, g] T1 →
+ ∀T2. ⇩[s, d, e] L2 ≡ L1 → ⇧[d, e] T1 ≡ T2 → ⦃G, L2⦄ ⊢ ⬊*[h, g] T2.
+#h #g #G #L2 #L1 #T1 #s #d #e #H elim H -T1 #T1 #_ #IHT1 #T2 #HL21 #HT12
@csx_intro #T #HLT2 #HT2
elim (cpx_inv_lift1 … HLT2 … HL21 … HT12) -HLT2 #T0 #HT0 #HLT10
@(IHT1 … HLT10) // -L1 -L2 #H destruct
qed.
(* Basic_1: was just: sn3_gen_lift *)
-lemma csx_inv_lift: ∀h,g,G,L2,L1,T1,d,e. ⦃G, L1⦄ ⊢ ⬊*[h, g] T1 →
- ∀T2. ⇩[d, e] L1 ≡ L2 → ⇧[d, e] T2 ≡ T1 → ⦃G, L2⦄ ⊢ ⬊*[h, g] T2.
-#h #g #G #L2 #L1 #T1 #d #e #H elim H -T1 #T1 #_ #IHT1 #T2 #HL12 #HT21
+lemma csx_inv_lift: ∀h,g,G,L2,L1,T1,s,d,e. ⦃G, L1⦄ ⊢ ⬊*[h, g] T1 →
+ ∀T2. ⇩[s, d, e] L1 ≡ L2 → ⇧[d, e] T2 ≡ T1 → ⦃G, L2⦄ ⊢ ⬊*[h, g] T2.
+#h #g #G #L2 #L1 #T1 #s #d #e #H elim H -T1 #T1 #_ #IHT1 #T2 #HL12 #HT21
@csx_intro #T #HLT2 #HT2
elim (lift_total T d e) #T0 #HT0
lapply (cpx_lift … HLT2 … HL12 … HT21 … HT0) -HLT2 #HLT10
(* Advanced inversion lemmas ************************************************)
(* Basic_1: was: sn3_gen_def *)
-lemma csx_inv_lref_bind: ∀h,g,I,G,L,K,V,i. ⇩[0, i] L ≡ K.ⓑ{I}V →
+lemma csx_inv_lref_bind: ∀h,g,I,G,L,K,V,i. ⇩[i] L ≡ K.ⓑ{I}V →
⦃G, L⦄ ⊢ ⬊*[h, g] #i → ⦃G, K⦄ ⊢ ⬊*[h, g] V.
#h #g #I #G #L #K #V #i #HLK #Hi
elim (lift_total V 0 (i+1))
(* Advanced properties ******************************************************)
(* Basic_1: was just: sn3_abbr *)
-lemma csx_lref_bind: ∀h,g,I,G,L,K,V,i. ⇩[0, i] L ≡ K.ⓑ{I}V → ⦃G, K⦄ ⊢ ⬊*[h, g] V → ⦃G, L⦄ ⊢ ⬊*[h, g] #i.
+lemma csx_lref_bind: ∀h,g,I,G,L,K,V,i. ⇩[i] L ≡ K.ⓑ{I}V → ⦃G, K⦄ ⊢ ⬊*[h, g] V → ⦃G, L⦄ ⊢ ⬊*[h, g] #i.
#h #g #I #G #L #K #V #i #HLK #HV
@csx_intro #X #H #Hi
elim (cpx_inv_lref1 … H) -H
[ #H destruct elim Hi //
| -Hi * #I0 #K0 #V0 #V1 #HLK0 #HV01 #HV1
lapply (ldrop_mono … HLK0 … HLK) -HLK #H destruct
- /3 width=7 by csx_lift, csx_cpx_trans, ldrop_fwd_drop2/
+ /3 width=8 by csx_lift, csx_cpx_trans, ldrop_fwd_drop2/
]
qed.
lemma csx_fqu_conf: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ →
⦃G1, L1⦄ ⊢ ⬊*[h, g] T1 → ⦃G2, L2⦄ ⊢ ⬊*[h, g] T2.
#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2
-/2 width=7 by csx_inv_lref_bind, csx_inv_lift, csx_fwd_flat_dx, csx_fwd_bind_dx, csx_fwd_pair_sn/
+/2 width=8 by csx_inv_lref_bind, csx_inv_lift, csx_fwd_flat_dx, csx_fwd_bind_dx, csx_fwd_pair_sn/
qed-.
lemma csx_fquq_conf: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ →
theorem csx_acp: ∀h,g. acp (cpx h g) (eq …) (csx h g).
#h #g @mk_acp
[ #G #L elim (deg_total h g 0) /3 width=8 by cnx_sort_iter, ex_intro/
-| /3 width=12 by cnx_lift/
+| /3 width=13 by cnx_lift/
| /2 width=3 by csx_fwd_flat_dx/
| /2 width=1 by csx_cast/
]
lemma csx_lpx_conf: ∀h,g,G,L1,L2. ⦃G, L1⦄ ⊢ ➡[h, g] L2 →
∀T. ⦃G, L1⦄ ⊢ ⬊*[h, g] T → ⦃G, L2⦄ ⊢ ⬊*[h, g] T.
-#h #g #G #L1 #L2 #HL12 #T #H @(csx_ind_alt … H) -T #T #_ #IHT
-@csx_intro #T0 #HLT0 #HT0
-@IHT /2 width=2/ -IHT -HT0 /2 width=3 by lpx_cpx_trans/
+#h #g #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,g,a,G,L,W. ⦃G, L⦄ ⊢ ⬊*[h, g] W →
#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 /2 width=1/ /3 width=1/
-| -IHW -HLW0 -HT * #H destruct /3 width=1/
+ #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.
elim (cpx_inv_abbr1 … H1) -H1 *
[ #V1 #T1 #HLV1 #HLT1 #H destruct
elim (eq_false_inv_tpair_sn … H2) -H2
- [ #HV1 @IHV // /2 width=1/ -HV1
- @(csx_lpx_conf … (L.ⓓV)) /2 width=1/ -HLV1 /2 width=3 by csx_cpx_trans/
- | -IHV -HLV1 * #H destruct /3 width=1/
+ [ /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 #T0 #HLT0 #HT0
- lapply (csx_cpx_trans … HT … HLT0) -T #HLT0
- lapply (csx_inv_lift … HLT0 … HT0) -T0 /2 width=3/
+| -IHV -IHT -H2
+ /3 width=8 by csx_cpx_trans, csx_inv_lift, ldrop_drop/
]
qed.
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/ ] -H2
- lapply (lsubr_cpx_trans … HLT0 (L.ⓓⓝW.V) ?) -HLT0 [ /2 width=1/ ] /3 width=1/
+ @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_abst/
| -IHT1 -H2 #b #V0 #W0 #W2 #T0 #T2 #HLV0 #HLW02 #HLT02 #H1 #H3 destruct
- lapply (lsubr_cpx_trans … HLT02 (L.ⓓⓝW0.V) ?) -HLT02 [ /2 width=1/ ] #HT02
- @(csx_cpx_trans … HT1) -HT1 /3 width=1/
+ lapply (lsubr_cpx_trans … HLT02 (L.ⓓⓝW0.V) ?) -HLT02
+ /4 width=5 by csx_cpx_trans, cpx_bind, cpx_flat, lsubr_abst/
| -HT1 -IHT1 -H2 #b #V0 #V1 #W0 #W1 #T0 #T3 #_ #_ #_ #_ #H destruct
]
qed-.
| * #_ #H elim H //
]
| -H -HVT #H
- lapply (cpx_lift … HLV10 (L. ⓓV) … HV12 … HV04) -HLV10 -HV12 /2 width=1/ #HV24
- @(IHVT … H … HV04) -IHVT // -H -HV04 /4 width=1/
+ lapply (cpx_lift … HLV10 (L.ⓓV) (Ⓣ) … HV12 … HV04) -HLV10 -HV12 /2 width=1 by ldrop_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/ -T #HVT0
- lapply (csx_inv_lift … L … 1 HVT0 ? ? ?) -HVT0 [ /2 width=4/ |2,3: skip | /2 width=1/ ] -V2 -T0 #HVY
- @(csx_cpx_trans … HVY) /2 width=1/
+ 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, ldrop_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=1/ #HLV23
+ lapply (cpx_lift … HLV10 (L. ⓓW0) … HV12 … HV03) -HLV10 -HV12 -HV03 /2 width=2 by ldrop_drop/ #HLV23
@csx_abbr /2 width=3 by csx_cpx_trans/ -HV
- @(csx_lpx_conf … (L. ⓓW0)) /2 width=1/ -W1
- @(csx_cpxs_trans … HVT) -HVT /3 width=1/
+ @(csx_lpx_conf … (L.ⓓW0)) /2 width=1 by lpx_pair/ -W1
+ /4 width=5 by csx_cpxs_trans, cpx_cpxs, cpx_flat/
]
qed-.
#V0 #T0 #HLV0 #HLT10 #H0 destruct
elim (eq_false_inv_tpair_sn … H) -H
[ -IHT1 #HV0
- @(csx_cpx_trans … (ⓐV0.T1)) /2 width=1/ -HLT10
- @IHV -IHV // -H1T1 -H3T1 /2 width=1/ -HV0
- #T2 #HLT12 #HT12
- @(csx_cpx_trans … (ⓐV.T2)) /2 width=1/ -HLV0
- @H2T1 -H2T1 // -HLT12 /2 width=1/
+ @(csx_cpx_trans … (ⓐV0.T1)) /2 width=1 by cpx_flat/ -HLT10
+ @IHV -IHV /4 width=3 by csx_cpx_trans, cpx_pair_sn/
| -IHV -H1T1 -HLV0 * #H #H1T10 destruct
elim (tstc_dec T1 T0) #H2T10
- [ @IHT1 -IHT1 // /2 width=1/ -H1T10 /2 width=3/ -H3T1
- #T2 #HLT02 #HT02
- @H2T1 -H2T1 /2 width=3/ -HLT10 -HLT02 /3 width=3/
- | -IHT1 -H3T1 -H1T10
- @H2T1 -H2T1 /2 width=1/
+ [ @IHT1 -IHT1 /4 width=3 by cpxs_strap2, cpxs_strap1, tstc_canc_sn, simple_tstc_repl_dx/
+ | -IHT1 -H3T1 -H1T10 /3 width=1 by cpx_cpxs/
]
]
qed.
#h #g #G #L #T #H1T #H2T #Vs elim Vs -Vs [ #_ @(cnx_csx … H2T) ] (**) (* /2 width=1/ does not work *)
#V #Vs #IHV #H
elim (csxv_inv_cons … H) -H #HV #HVs
-@csx_appl_simple_tstc // -HV /2 width=1/ -IHV -HVs
+@csx_appl_simple_tstc /2 width=1 by applv_simple/ -IHV -HV -HVs
#X #H #H0
lapply (cpxs_fwd_cnx_vector … H) -H // -H1T -H2T #H
elim (H0) -H0 //
lemma csx_applv_sort: ∀h,g,G,L,k,Vs. ⦃G, L⦄ ⊢ ⬊*[h, g] Vs → ⦃G, L⦄ ⊢ ⬊*[h, g] ⒶVs.⋆k.
#h #g #G #L #k elim (deg_total h g k)
-#l generalize in match k; -k @(nat_ind_plus … l) -l [ /3 width=1/ ]
+#l generalize in match k; -k @(nat_ind_plus … l) -l [ /3 width=1 by csx_applv_cnx, cnx_sort, simple_atom/ ]
#l #IHl #k #Hkl lapply (deg_next_SO … Hkl) -Hkl
-#Hkl #Vs elim Vs -Vs /2 width=1/
+#Hkl #Vs elim Vs -Vs /2 width=1 by/
#V #Vs #IHVs #HVVs
elim (csxv_inv_cons … HVVs) #HV #HVs
-@csx_appl_simple_tstc // -HV /2 width=1/ -IHVs -HVs
+@csx_appl_simple_tstc /2 width=1 by applv_simple, simple_atom/ -IHVs -HV -HVs
#X #H #H0
elim (cpxs_fwd_sort_vector … H) -H #H
[ elim H0 -H0 //
-| -H0 @(csx_cpxs_trans … (Ⓐ(V@Vs).⋆(next h k))) /2 width=1/
+| -H0 @(csx_cpxs_trans … (Ⓐ(V@Vs).⋆(next h k))) /2 width=1 by cpxs_flat_dx/
]
qed.
(* Basic_1: was just: sn3_appls_beta *)
lemma csx_applv_beta: ∀h,g,a,G,L,Vs,V,W,T. ⦃G, L⦄ ⊢ ⬊*[h, g] ⒶVs.ⓓ{a}ⓝW.V.T →
⦃G, L⦄ ⊢ ⬊*[h, g] ⒶVs. ⓐV.ⓛ{a}W.T.
-#h #g #a #G #L #Vs elim Vs -Vs /2 width=1/
+#h #g #a #G #L #Vs elim Vs -Vs /2 width=1 by csx_appl_beta/
#V0 #Vs #IHV #V #W #T #H1T
lapply (csx_fwd_pair_sn … H1T) #HV0
lapply (csx_fwd_flat_dx … H1T) #H2T
-@csx_appl_simple_tstc // -HV0 /2 width=1/ -IHV -H2T
+@csx_appl_simple_tstc /2 width=1 by applv_simple, simple_flat/ -IHV -HV0 -H2T
#X #H #H0
elim (cpxs_fwd_beta_vector … H) -H #H
[ -H1T elim H0 -H0 //
-| -H0 @(csx_cpxs_trans … H1T) -H1T /2 width=1/
+| -H0 /3 width=5 by csx_cpxs_trans, cpxs_flat_dx/
]
qed.
-lemma csx_applv_delta: ∀h,g,I,G,L,K,V1,i. ⇩[0, i] L ≡ K.ⓑ{I}V1 →
+lemma csx_applv_delta: ∀h,g,I,G,L,K,V1,i. ⇩[i] L ≡ K.ⓑ{I}V1 →
∀V2. ⇧[0, i + 1] V1 ≡ V2 →
∀Vs. ⦃G, L⦄ ⊢ ⬊*[h, g] (ⒶVs.V2) → ⦃G, L⦄ ⊢ ⬊*[h, g] (ⒶVs.#i).
#h #g #I #G #L #K #V1 #i #HLK #V2 #HV12 #Vs elim Vs -Vs
-[ #H
- lapply (ldrop_fwd_drop2 … HLK) #HLK0
- lapply (csx_inv_lift … H … HLK0 HV12) -V2 -HLK0 /2 width=5/
+[ /4 width=12 by csx_inv_lift, csx_lref_bind, ldrop_fwd_drop2/
| #V #Vs #IHV #H1T
lapply (csx_fwd_pair_sn … H1T) #HV
lapply (csx_fwd_flat_dx … H1T) #H2T
- @csx_appl_simple_tstc // -HV /2 width=1/ -IHV -H2T
+ @csx_appl_simple_tstc /2 width=1 by applv_simple, simple_atom/ -IHV -HV -H2T
#X #H #H0
elim (cpxs_fwd_delta_vector … HLK … HV12 … H) -HLK -HV12 -H #H
[ -H1T elim H0 -H0 //
- | -H0 @(csx_cpxs_trans … H1T) -H1T /2 width=1/
+ | -H0 /3 width=5 by csx_cpxs_trans, cpxs_flat_dx/
]
]
qed.
lemma csx_applv_theta: ∀h,g,a,G,L,V1s,V2s. ⇧[0, 1] V1s ≡ V2s →
∀V,T. ⦃G, L⦄ ⊢ ⬊*[h, g] ⓓ{a}V.ⒶV2s.T →
⦃G, L⦄ ⊢ ⬊*[h, g] ⒶV1s.ⓓ{a}V.T.
-#h #g #a #G #L #V1s #V2s * -V1s -V2s /2 width=1/
+#h #g #a #G #L #V1s #V2s * -V1s -V2s /2 width=1 by/
#V1s #V2s #V1 #V2 #HV12 #H
generalize in match HV12; -HV12 generalize in match V2; -V2 generalize in match V1; -V1
-elim H -V1s -V2s /2 width=3/
+elim H -V1s -V2s /2 width=3 by csx_appl_theta/
#V1s #V2s #V1 #V2 #HV12 #HV12s #IHV12s #W1 #W2 #HW12 #V #T #H
lapply (csx_appl_theta … HW12 … H) -H -HW12 #H
lapply (csx_fwd_pair_sn … H) #HW1
lapply (csx_fwd_flat_dx … H) #H1
-@csx_appl_simple_tstc // -HW1 /2 width=3/ -IHV12s -H1 #X #H1 #H2
-elim (cpxs_fwd_theta_vector … (V2@V2s) … H1) -H1 /2 width=1/ -HV12s -HV12
+@csx_appl_simple_tstc /2 width=3 by simple_flat/ -IHV12s -HW1 -H1 #X #H1 #H2
+elim (cpxs_fwd_theta_vector … (V2@V2s) … H1) -H1 /2 width=1 by liftv_cons/ -HV12s -HV12
[ -H #H elim H2 -H2 //
-| -H2 #H1 @(csx_cpxs_trans … H) -H /2 width=1/
+| -H2 /3 width=5 by csx_cpxs_trans, cpxs_flat_dx/
]
qed.
(* Basic_1: was just: sn3_appls_cast *)
lemma csx_applv_cast: ∀h,g,G,L,Vs,W,T. ⦃G, L⦄ ⊢ ⬊*[h, g] ⒶVs.W → ⦃G, L⦄ ⊢ ⬊*[h, g] ⒶVs.T →
⦃G, L⦄ ⊢ ⬊*[h, g] ⒶVs.ⓝW.T.
-#h #g #G #L #Vs elim Vs -Vs /2 width=1/
+#h #g #G #L #Vs elim Vs -Vs /2 width=1 by csx_cast/
#V #Vs #IHV #W #T #H1W #H1T
lapply (csx_fwd_pair_sn … H1W) #HV
lapply (csx_fwd_flat_dx … H1W) #H2W
lapply (csx_fwd_flat_dx … H1T) #H2T
-@csx_appl_simple_tstc // -HV /2 width=1/ -IHV -H2W -H2T
+@csx_appl_simple_tstc /2 width=1 by applv_simple, simple_flat/ -IHV -HV -H2W -H2T
#X #H #H0
elim (cpxs_fwd_cast_vector … H) -H #H
[ -H1W -H1T elim H0 -H0 //
-| -H1W -H0 @(csx_cpxs_trans … H1T) -H1T /2 width=1/
-| -H1T -H0 @(csx_cpxs_trans … H1W) -H1W /2 width=1/
+| -H1W -H0 /3 width=5 by csx_cpxs_trans, cpxs_flat_dx/
+| -H1T -H0 /3 width=5 by csx_cpxs_trans, cpxs_flat_dx/
]
qed.
theorem csx_acr: ∀h,g. acr (cpx h g) (eq …) (csx h g) (λG,L,T. ⦃G, L⦄ ⊢ ⬊*[h, g] T).
#h #g @mk_acr //
-[ /3 width=1/
-|2,3,6: /2 width=1/
-| /2 width=7/
+[ /3 width=1 by csx_applv_cnx/
+|2,3,6: /2 width=1 by csx_applv_beta, csx_applv_sort, csx_applv_cast/
+| /2 width=7 by csx_applv_delta/
| #G #L #V1s #V2s #HV12s #a #V #T #H #HV
@(csx_applv_theta … HV12s) -HV12s
- @(csx_abbr) //
-| @csx_lift
+ @csx_abbr //
+| /2 width=8 by csx_lift/
]
qed.
∃∃T. ⦃G, L1⦄ ⊢ T1 ➡* T & ⦃G, L1⦄ ⊢ T0 ➡* T.
#G #L0 #T0 #T1 #HT01 #L1 #H elim H -L1
[ #L1 #HL01
- elim (cprs_lpr_conf_dx … HT01 … HL01) -L0 /2 width=3/
+ elim (cprs_lpr_conf_dx … HT01 … HL01) -L0 /2 width=3 by ex2_intro/
| #L #L1 #_ #HL1 * #T #HT1 #HT0 -L0
elim (cprs_lpr_conf_dx … HT1 … HL1) -HT1 #T2 #HT2 #HT12
elim (cprs_lpr_conf_dx … HT0 … HL1) -L #T3 #HT3 #HT03
elim (cprs_conf … HT2 … HT3) -T #T #HT2 #HT3
lapply (cprs_trans … HT03 … HT3) -T3
- lapply (cprs_trans … HT12 … HT2) -T2 /2 width=3/
+ lapply (cprs_trans … HT12 … HT2) -T2 /2 width=3 by ex2_intro/
]
qed-.
∃∃T. ⦃G, L0⦄ ⊢ T1 ➡* T & ⦃G, L1⦄ ⊢ T0 ➡* T.
#G #L0 #T0 #T1 #HT01 #L1 #HL01
elim (lprs_cprs_conf_dx … HT01 … HL01) -HT01 #T #HT1
-lapply (lprs_cprs_trans … HT1 … HL01) -HT1 /2 width=3/
+lapply (lprs_cprs_trans … HT1 … HL01) -HT1 /2 width=3 by ex2_intro/
qed-.
lemma lprs_cpr_conf_sn: ∀G,L0,T0,T1. ⦃G, L0⦄ ⊢ T0 ➡ T1 →
∀I,T1,T2. ⦃G, L.ⓑ{I}V2⦄ ⊢ T1 ➡* T2 →
∀a. ⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ➡* ⓑ{a,I}V2.T2.
#G #L #V1 #V2 #HV12 #I #T1 #T2 #HT12
-lapply (lprs_cprs_trans … HT12 (L.ⓑ{I}V1) ?) /2 width=1/
+lapply (lprs_cprs_trans … HT12 (L.ⓑ{I}V1) ?) /2 width=1 by lprs_pair, cprs_bind/
qed.
(* Inversion lemmas on context-sensitive parallel computation for terms *****)
lemma cprs_inv_abst1: ∀a,G,L,W1,T1,U2. ⦃G, L⦄ ⊢ ⓛ{a}W1.T1 ➡* U2 →
∃∃W2,T2. ⦃G, L⦄ ⊢ W1 ➡* W2 & ⦃G, L.ⓛW1⦄ ⊢ T1 ➡* T2 &
U2 = ⓛ{a}W2.T2.
-#a #G #L #V1 #T1 #U2 #H @(cprs_ind … H) -U2 /2 width=5/
+#a #G #L #V1 #T1 #U2 #H @(cprs_ind … H) -U2 /2 width=5 by ex3_2_intro/
#U0 #U2 #_ #HU02 * #V0 #T0 #HV10 #HT10 #H destruct
elim (cpr_inv_abst1 … HU02) -HU02 #V2 #T2 #HV02 #HT02 #H destruct
-lapply (lprs_cpr_trans … HT02 (L.ⓛV1) ?) /2 width=1/ -HT02 #HT02
+lapply (lprs_cpr_trans … HT02 (L.ⓛV1) ?) /2 width=1 by lprs_pair/ -HT02 #HT02
lapply (cprs_strap1 … HV10 … HV02) -V0
-lapply (cprs_trans … HT10 … HT02) -T0 /2 width=5/
+lapply (cprs_trans … HT10 … HT02) -T0 /2 width=5 by ex3_2_intro/
qed-.
lemma cprs_inv_abst: ∀a,G,L,W1,W2,T1,T2. ⦃G, L⦄ ⊢ ⓛ{a}W1.T1 ➡* ⓛ{a}W2.T2 →
⦃G, L⦄ ⊢ W1 ➡* W2 ∧ ⦃G, L.ⓛW1⦄ ⊢ T1 ➡* T2.
#a #G #L #W1 #W2 #T1 #T2 #H
-elim (cprs_inv_abst1 … H) -H #W #T #HW1 #HT1 #H destruct /2 width=1/
+elim (cprs_inv_abst1 … H) -H #W #T #HW1 #HT1 #H destruct /2 width=1 by conj/
qed-.
(* Basic_1: was pr3_gen_abbr *)
U2 = ⓓ{a}V2.T2
) ∨
∃∃T2. ⦃G, L.ⓓV1⦄ ⊢ T1 ➡* T2 & ⇧[0, 1] U2 ≡ T2 & a = true.
-#a #G #L #V1 #T1 #U2 #H @(cprs_ind … H) -U2 /3 width=5/
+#a #G #L #V1 #T1 #U2 #H @(cprs_ind … H) -U2 /3 width=5 by ex3_2_intro, or_introl/
#U0 #U2 #_ #HU02 * *
[ #V0 #T0 #HV10 #HT10 #H destruct
elim (cpr_inv_abbr1 … HU02) -HU02 *
[ #V2 #T2 #HV02 #HT02 #H destruct
- lapply (lprs_cpr_trans … HT02 (L.ⓓV1) ?) /2 width=1/ -HT02 #HT02
+ lapply (lprs_cpr_trans … HT02 (L.ⓓV1) ?) /2 width=1 by lprs_pair/ -HT02 #HT02
lapply (cprs_strap1 … HV10 … HV02) -V0
- lapply (cprs_trans … HT10 … HT02) -T0 /3 width=5/
+ lapply (cprs_trans … HT10 … HT02) -T0 /3 width=5 by ex3_2_intro, or_introl/
| #T2 #HT02 #HUT2
- lapply (lprs_cpr_trans … HT02 (L.ⓓV1) ?) -HT02 /2 width=1/ -V0 #HT02
- lapply (cprs_trans … HT10 … HT02) -T0 /3 width=3/
+ lapply (lprs_cpr_trans … HT02 (L.ⓓV1) ?) -HT02 /2 width=1 by lprs_pair/ -V0 #HT02
+ lapply (cprs_trans … HT10 … HT02) -T0 /3 width=3 by ex3_intro, or_intror/
]
| #U1 #HTU1 #HU01
elim (lift_total U2 0 1) #U #HU2
- lapply (cpr_lift … HU02 (L.ⓓV1) … HU01 … HU2) -U0 /2 width=1/ /4 width=3/
+ lapply (cpr_lift … HU02 (L.ⓓV1) … HU01 … HU2) -U0
+ /4 width=3 by cprs_strap1, ldrop_drop, ex3_intro, or_intror/
]
qed-.
]
| #U1 #HTU1 #HU01
elim (lift_total U2 0 1) #U #HU2
- /6 width=11 by cpxs_strap1, cpx_lift, ldrop_drop, ex3_intro, or_intror/
+ /6 width=12 by cpxs_strap1, cpx_lift, ldrop_drop, ex3_intro, or_intror/
]
qed-.
(* Basic_1: was: csubc_drop_conf_O *)
(* Note: the constant 0 can not be generalized *)
-lemma lsubc_ldrop_O1_trans: ∀RP,G,L1,L2. G ⊢ L1 ⊑[RP] L2 → ∀K2,e. ⇩[0, e] L2 ≡ K2 →
- ∃∃K1. ⇩[0, e] L1 ≡ K1 & G ⊢ K1 ⊑[RP] K2.
+lemma lsubc_ldrop_O1_trans: ∀RP,G,L1,L2. G ⊢ L1 ⊑[RP] L2 → ∀K2,s,e. ⇩[s, 0, e] L2 ≡ K2 →
+ ∃∃K1. ⇩[s, 0, e] L1 ≡ K1 & G ⊢ K1 ⊑[RP] K2.
#RP #G #L1 #L2 #H elim H -L1 -L2
-[ #X #e #H elim (ldrop_inv_atom1 … H) -H /2 width=3/
-| #I #L1 #L2 #V #_ #IHL12 #X #e #H
+[ #X #s #e #H elim (ldrop_inv_atom1 … H) -H /4 width=3 by ldrop_atom, ex2_intro/
+| #I #L1 #L2 #V #_ #IHL12 #X #s #e #H
elim (ldrop_inv_O1_pair1 … H) -H * #He #H destruct
- [ elim (IHL12 L2 0) -IHL12 // #X #H <(ldrop_inv_O2 … H) -H /3 width=3/
- | elim (IHL12 … H) -L2 /3 width=3/
+ [ elim (IHL12 L2 s 0) -IHL12 // #X #H <(ldrop_inv_O2 … H) -H
+ /3 width=3 by lsubc_pair, ldrop_pair, ex2_intro/
+ | elim (IHL12 … H) -L2 /3 width=3 by ldrop_drop_lt, ex2_intro/
]
-| #L1 #L2 #V #W #A #HV #H1W #H2W #_ #IHL12 #X #e #H
+| #L1 #L2 #V #W #A #HV #H1W #H2W #_ #IHL12 #X #s #e #H
elim (ldrop_inv_O1_pair1 … H) -H * #He #H destruct
- [ elim (IHL12 L2 0) -IHL12 // #X #H <(ldrop_inv_O2 … H) -H /3 width=8/
- | elim (IHL12 … H) -L2 /3 width=3/
+ [ elim (IHL12 L2 s 0) -IHL12 // #X #H <(ldrop_inv_O2 … H) -H
+ /3 width=8 by lsubc_abbr, ldrop_pair, ex2_intro/
+ | elim (IHL12 … H) -L2 /3 width=3 by ldrop_drop_lt, ex2_intro/
]
+]
qed-.
(* Basic_1: was: csubc_drop_conf_rev *)
lemma ldrop_lsubc_trans: ∀RR,RS,RP.
acp RR RS RP → acr RR RS RP (λG,L,T. RP G L T) →
- ∀G,L1,K1,d,e. ⇩[d, e] L1 ≡ K1 → ∀K2. G ⊢ K1 ⊑[RP] K2 →
- ∃∃L2. G ⊢ L1 ⊑[RP] L2 & ⇩[d, e] L2 ≡ K2.
+ ∀G,L1,K1,d,e. ⇩[Ⓕ, d, e] L1 ≡ K1 → ∀K2. G ⊢ K1 ⊑[RP] K2 →
+ ∃∃L2. G ⊢ L1 ⊑[RP] L2 & ⇩[Ⓕ, d, e] L2 ≡ K2.
#RR #RS #RP #Hacp #Hacr #G #L1 #K1 #d #e #H elim H -L1 -K1 -d -e
-[ #d #X #H elim (lsubc_inv_atom1 … H) -H /2 width=3/
+[ #d #e #He #X #H elim (lsubc_inv_atom1 … H) -H
+ >He /2 width=3 by ex2_intro/
| #L1 #I #V1 #X #H
elim (lsubc_inv_pair1 … H) -H *
- [ #K1 #HLK1 #H destruct /3 width=3/
- | #K1 #V #W1 #A #HV1 #H1W1 #H2W1 #HLK1 #H1 #H2 #H3 destruct /3 width=4/
+ [ #K1 #HLK1 #H destruct /3 width=3 by lsubc_pair, ldrop_pair, ex2_intro/
+ | #K1 #V #W1 #A #HV1 #H1W1 #H2W1 #HLK1 #H1 #H2 #H3 destruct
+ /3 width=4 by lsubc_abbr, ldrop_pair, ex2_intro/
]
-| #L1 #K1 #I #V1 #e #_ #IHLK1 #K2 #HK12
- elim (IHLK1 … HK12) -K1 /3 width=5/
-| #L1 #K1 #I #V1 #V2 #d #e #HLK1 #HV21 #IHLK1 #X #H
+| #I #L1 #K1 #V1 #e #_ #IHLK1 #K2 #HK12
+ elim (IHLK1 … HK12) -K1 /3 width=5 by lsubc_pair, ldrop_drop, ex2_intro/
+| #I #L1 #K1 #V1 #V2 #d #e #HLK1 #HV21 #IHLK1 #X #H
elim (lsubc_inv_pair1 … H) -H *
[ #K2 #HK12 #H destruct
- elim (IHLK1 … HK12) -K1 /3 width=5/
+ elim (IHLK1 … HK12) -K1 /3 width=5 by lsubc_pair, ldrop_skip, ex2_intro/
| #K2 #V #W2 #A #HV2 #H1W2 #H2W2 #HK12 #H1 #H2 #H3 destruct
elim (lift_inv_flat1 … HV21) -HV21 #W3 #V3 #HW23 #HV3 #H destruct
elim (IHLK1 … HK12) #K #HL1K #HK2
lapply (aacr_acr … Hacp Hacr A) -Hacp -Hacr #HA
lapply (s8 … HA … HV2 … HLK1 HV3) -HV2
- lapply (s8 … HA … H1W2 … HLK1 HW23) -H1W2 /4 width=10/
+ lapply (s8 … HA … H1W2 … HLK1 HW23) -H1W2
+ /4 width=11 by lsubc_abbr, aaa_lift, ldrop_skip, ex2_intro/
]
]
qed-.
(* Basic_1: was: csubc_drop1_conf_rev *)
lemma ldrops_lsubc_trans: ∀RR,RS,RP.
acp RR RS RP → acr RR RS RP (λG,L,T. RP G L T) →
- ∀G,L1,K1,des. ⇩*[des] L1 ≡ K1 → ∀K2. G ⊢ K1 ⊑[RP] K2 →
- ∃∃L2. G ⊢ L1 ⊑[RP] L2 & ⇩*[des] L2 ≡ K2.
+ ∀G,L1,K1,des. ⇩*[Ⓕ, des] L1 ≡ K1 → ∀K2. G ⊢ K1 ⊑[RP] K2 →
+ ∃∃L2. G ⊢ L1 ⊑[RP] L2 & ⇩*[Ⓕ, des] L2 ≡ K2.
#RR #RS #RP #Hacp #Hacr #G #L1 #K1 #des #H elim H -L1 -K1 -des
-[ /2 width=3/
+[ /2 width=3 by ldrops_nil, ex2_intro/
| #L1 #L #K1 #des #d #e #_ #HLK1 #IHL #K2 #HK12
elim (ldrop_lsubc_trans … Hacp Hacr … HLK1 … HK12) -Hacp -Hacr -K1 #K #HLK #HK2
- elim (IHL … HLK) -IHL -HLK /3 width=5/
+ elim (IHL … HLK) -IHL -HLK /3 width=5 by ldrops_cons, ex2_intro/
]
qed-.
(* Note: the constant 0 cannot be generalized *)
lemma lsubsv_ldrop_O1_conf: ∀h,g,G,L1,L2. G ⊢ L1 ¡⊑[h, g] L2 →
- ∀K1,e. ⇩[0, e] L1 ≡ K1 →
- ∃∃K2. G ⊢ K1 ¡⊑[h, g] K2 & ⇩[0, e] L2 ≡ K2.
+ ∀K1,s,e. ⇩[s, 0, e] L1 ≡ K1 →
+ ∃∃K2. G ⊢ K1 ¡⊑[h, g] K2 & ⇩[s, 0, e] L2 ≡ K2.
#h #g #G #L1 #L2 #H elim H -L1 -L2
-[ /2 width=3/
-| #I #L1 #L2 #V #_ #IHL12 #K1 #e #H
+[ /2 width=3 by ex2_intro/
+| #I #L1 #L2 #V #_ #IHL12 #K1 #s #e #H
elim (ldrop_inv_O1_pair1 … H) -H * #He #HLK1
[ destruct
- elim (IHL12 L1 0) -IHL12 // #X #HL12 #H
- <(ldrop_inv_O2 … H) in HL12; -H /3 width=3/
- | elim (IHL12 … HLK1) -L1 /3 width=3/
+ elim (IHL12 L1 s 0) -IHL12 // #X #HL12 #H
+ <(ldrop_inv_O2 … H) in HL12; -H /3 width=3 by lsubsv_pair, ldrop_pair, ex2_intro/
+ | elim (IHL12 … HLK1) -L1 /3 width=3 by ldrop_drop_lt, ex2_intro/
]
-| #L1 #L2 #W #V #l #H1W #HV #HVW #H2W #H1l #H2l #_ #IHL12 #K1 #e #H
+| #L1 #L2 #W #V #l #H1W #HV #HVW #H2W #H1l #H2l #_ #IHL12 #K1 #s #e #H
elim (ldrop_inv_O1_pair1 … H) -H * #He #HLK1
[ destruct
- elim (IHL12 L1 0) -IHL12 // #X #HL12 #H
- <(ldrop_inv_O2 … H) in HL12; -H /3 width=4/
- | elim (IHL12 … HLK1) -L1 /3 width=3/
+ elim (IHL12 L1 s 0) -IHL12 // #X #HL12 #H
+ <(ldrop_inv_O2 … H) in HL12; -H /3 width=4 by lsubsv_abbr, ldrop_pair, ex2_intro/
+ | elim (IHL12 … HLK1) -L1 /3 width=3 by ldrop_drop_lt, ex2_intro/
]
]
qed-.
(* Note: the constant 0 cannot be generalized *)
lemma lsubsv_ldrop_O1_trans: ∀h,g,G,L1,L2. G ⊢ L1 ¡⊑[h, g] L2 →
- ∀K2,e. ⇩[0, e] L2 ≡ K2 →
- ∃∃K1. G ⊢ K1 ¡⊑[h, g] K2 & ⇩[0, e] L1 ≡ K1.
+ ∀K2,s, e. ⇩[s, 0, e] L2 ≡ K2 →
+ ∃∃K1. G ⊢ K1 ¡⊑[h, g] K2 & ⇩[s, 0, e] L1 ≡ K1.
#h #g #G #L1 #L2 #H elim H -L1 -L2
-[ /2 width=3/
-| #I #L1 #L2 #V #_ #IHL12 #K2 #e #H
+[ /2 width=3 by ex2_intro/
+| #I #L1 #L2 #V #_ #IHL12 #K2 #s #e #H
elim (ldrop_inv_O1_pair1 … H) -H * #He #HLK2
[ destruct
- elim (IHL12 L2 0) -IHL12 // #X #HL12 #H
- <(ldrop_inv_O2 … H) in HL12; -H /3 width=3/
- | elim (IHL12 … HLK2) -L2 /3 width=3/
+ elim (IHL12 L2 s 0) -IHL12 // #X #HL12 #H
+ <(ldrop_inv_O2 … H) in HL12; -H /3 width=3 by lsubsv_pair, ldrop_pair, ex2_intro/
+ | elim (IHL12 … HLK2) -L2 /3 width=3 by ldrop_drop_lt, ex2_intro/
]
-| #L1 #L2 #W #V #l #H1W #HV #HVW #H2W #H1l #H2l #_ #IHL12 #K2 #e #H
+| #L1 #L2 #W #V #l #H1W #HV #HVW #H2W #H1l #H2l #_ #IHL12 #K2 #s #e #H
elim (ldrop_inv_O1_pair1 … H) -H * #He #HLK2
[ destruct
- elim (IHL12 L2 0) -IHL12 // #X #HL12 #H
- <(ldrop_inv_O2 … H) in HL12; -H /3 width=4/
- | elim (IHL12 … HLK2) -L2 /3 width=3/
+ elim (IHL12 L2 s 0) -IHL12 // #X #HL12 #H
+ <(ldrop_inv_O2 … H) in HL12; -H /3 width=4 by lsubsv_abbr, ldrop_pair, ex2_intro/
+ | elim (IHL12 … HLK2) -L2 /3 width=3 by ldrop_drop_lt, ex2_intro/
]
]
qed-.
∀L1. G ⊢ L1 ¡⊑[h, g] L2 →
∃∃U1. ⦃G, L1⦄ ⊢ T •*[h, g, l1] U1 & ⦃G, L1⦄ ⊢ U1 ⬌* U2.
#h #g #G #L2 #T #U #l1 #H @(lsstas_ind_alt … H) -G -L2 -T -U -l1
-[1,2: /2 width=3/
+[1,2: /2 width=3 by lstar_O, ex2_intro/
| #G #L2 #K2 #X #Y #U #i #l1 #HLK2 #_ #HYU #IHXY #l2 #Hl12 #Hl2 #L1 #HL12
elim (da_inv_lref … Hl2) -Hl2 * #K0 #V0 [| #l0 ] #HK0 #HV0
lapply (ldrop_mono … HK0 … HLK2) -HK0 #H destruct
elim (IHXY … Hl12 HV0 … HK12) -K2 -l2 #T #HXT #HTY
lapply (ldrop_fwd_drop2 … HLK1) #H
elim (lift_total T 0 (i+1))
- /3 width=11 by lsstas_ldef, cpcs_lift, ex2_intro/
+ /3 width=12 by lsstas_ldef, cpcs_lift, ex2_intro/
| #V #l0 #_ #_ #_ #_ #_ #_ #_ #H destruct
]
| #G #L2 #K2 #X #Y #U #i #l1 #l #HLK2 #_ #_ #HYU #IHXY #l2 #Hl12 #Hl2 #L1 #HL12 -l
elim (IHXY … Hl12 HV0 … HK12) -K2 -Hl12 #Y0
lapply (ldrop_fwd_drop2 … HLK1)
elim (lift_total Y0 0 (i+1))
- /3 width=11 by lsstas_ldec, cpcs_lift, ex2_intro/
+ /3 width=12 by lsstas_ldec, cpcs_lift, ex2_intro/
| #V #l #_ #_ #HVX #_ #HV #HX #HK12 #_ #H destruct
lapply (da_mono … HX … HV0) -HX #H destruct
elim (IHXY … Hl12 HV0 … HK12) -K2 #Y0 #HXY0 #HY0
lapply (cpcs_trans … HWY0 … HY0) -Y0
lapply (ldrop_fwd_drop2 … HLK1)
elim (lift_total W 0 (i+1))
- /4 width=11 by lsstas_ldef, lsstas_cast, cpcs_lift, ex2_intro/
+ /4 width=12 by lsstas_ldef, lsstas_cast, cpcs_lift, ex2_intro/
]
| #a #I #G #L2 #V2 #T2 #U2 #l1 #_ #IHTU2 #l2 #Hl12 #Hl2 #L1 #HL12
lapply (da_inv_bind … Hl2) -Hl2 #Hl2
(* activate genv *)
inductive snv (h:sh) (g:sd h): relation3 genv lenv term ≝
| snv_sort: ∀G,L,k. snv h g G L (⋆k)
-| snv_lref: ∀I,G,L,K,V,i. ⇩[0, i] L ≡ K.ⓑ{I}V → snv h g G K V → snv h g G L (#i)
+| snv_lref: ∀I,G,L,K,V,i. ⇩[i] L ≡ K.ⓑ{I}V → snv h g G K V → snv h g G L (#i)
| snv_bind: ∀a,I,G,L,V,T. snv h g G L V → snv h g G (L.ⓑ{I}V) T → snv h g G L (ⓑ{a,I}V.T)
| snv_appl: ∀a,G,L,V,W,W0,T,U,l. snv h g G L V → snv h g G L T →
⦃G, L⦄ ⊢ V ▪[h, g] l+1 → ⦃G, L⦄ ⊢ V •[h, g] W → ⦃G, L⦄ ⊢ W ➡* W0 →
(* Basic inversion lemmas ***************************************************)
fact snv_inv_lref_aux: ∀h,g,G,L,X. ⦃G, L⦄ ⊢ X ¡[h, g] → ∀i. X = #i →
- ∃∃I,K,V. ⇩[0, i] L ≡ K.ⓑ{I}V & ⦃G, K⦄ ⊢ V ¡[h, g].
+ ∃∃I,K,V. ⇩[i] L ≡ K.ⓑ{I}V & ⦃G, K⦄ ⊢ V ¡[h, g].
#h #g #G #L #X * -G -L -X
[ #G #L #k #i #H destruct
-| #I #G #L #K #V #i0 #HLK #HV #i #H destruct /2 width=5/
+| #I #G #L #K #V #i0 #HLK #HV #i #H destruct /2 width=5 by ex2_3_intro/
| #a #I #G #L #V #T #_ #_ #i #H destruct
| #a #G #L #V #W #W0 #T #U #l #_ #_ #_ #_ #_ #_ #i #H destruct
| #G #L #W #T #U #l #_ #_ #_ #_ #_ #i #H destruct
qed-.
lemma snv_inv_lref: ∀h,g,G,L,i. ⦃G, L⦄ ⊢ #i ¡[h, g] →
- ∃∃I,K,V. ⇩[0, i] L ≡ K.ⓑ{I}V & ⦃G, K⦄ ⊢ V ¡[h, g].
+ ∃∃I,K,V. ⇩[i] L ≡ K.ⓑ{I}V & ⦃G, K⦄ ⊢ V ¡[h, g].
/2 width=3 by snv_inv_lref_aux/ qed-.
fact snv_inv_gref_aux: ∀h,g,G,L,X. ⦃G, L⦄ ⊢ X ¡[h, g] → ∀p. X = §p → ⊥.
#h #g #G #L #X * -G -L -X
[ #G #L #k #a #I #V #T #H destruct
| #I0 #G #L #K #V0 #i #_ #_ #a #I #V #T #H destruct
-| #b #I0 #G #L #V0 #T0 #HV0 #HT0 #a #I #V #T #H destruct /2 width=1/
+| #b #I0 #G #L #V0 #T0 #HV0 #HT0 #a #I #V #T #H destruct /2 width=1 by conj/
| #b #G #L #V0 #W0 #W00 #T0 #U0 #l #_ #_ #_ #_#_ #_ #a #I #V #T #H destruct
| #G #L #W0 #T0 #U0 #l #_ #_ #_ #_ #_ #a #I #V #T #H destruct
]
[ #G #L #k #V #T #H destruct
| #I #G #L #K #V0 #i #_ #_ #V #T #H destruct
| #a #I #G #L #V0 #T0 #_ #_ #V #T #H destruct
-| #a #G #L #V0 #W0 #W00 #T0 #U0 #l #HV0 #HT0 #Hl #HVW0 #HW00 #HTU0 #V #T #H destruct /2 width=8/
+| #a #G #L #V0 #W0 #W00 #T0 #U0 #l #HV0 #HT0 #Hl #HVW0 #HW00 #HTU0 #V #T #H destruct /2 width=8 by ex6_5_intro/
| #G #L #W0 #T0 #U0 #l #_ #_ #_ #_ #_ #V #T #H destruct
]
qed-.
| #I #G #L #K #V #i #_ #_ #W #T #H destruct
| #a #I #G #L #V #T0 #_ #_ #W #T #H destruct
| #a #G #L #V #W0 #W00 #T0 #U #l #_ #_ #_ #_ #_ #_ #W #T #H destruct
-| #G #L #W0 #T0 #U0 #l #HW0 #HT0 #Hl #HTU0 #HUW0 #W #T #H destruct /2 width=4/
+| #G #L #W0 #T0 #U0 #l #HW0 #HT0 #Hl #HTU0 #HUW0 #W #T #H destruct /2 width=4 by ex5_2_intro/
]
qed-.
#h #g #G0 #L0 #T0 #IH3 #IH2 #IH1 #G1 #L1 * * [|||| * ]
[ #k #_ #_ #_ #_ #l #H2 #X3 #H3 #L2 #_ -IH3 -IH2 -IH1
lapply (da_inv_sort … H2) -H2
- lapply (cpr_inv_sort1 … H3) -H3 #H destruct /2 width=1/
+ lapply (cpr_inv_sort1 … H3) -H3 #H destruct /2 width=1 by da_sort/
| #i #HG0 #HL0 #HT0 #H1 #l #H2 #X3 #H3 #L2 #HL12 destruct -IH3 -IH2
elim (snv_inv_lref … H1) -H1 #I0 #K0 #X0 #H #HX0
elim (da_inv_lref … H2) -H2 * #K1 [ #V1 | #W1 #l1 ] #HLK1 [ #HV1 | #HW1 #H ] destruct
elim (lpr_ldrop_conf … HLK1 … HL12) -HLK1 -HL12 #X #H #HLK2
elim (lpr_inv_pair1 … H) -H #K2 #V2 #HK12 #_ #H destruct
lapply (ldrop_fwd_drop2 … HLK2) -V2
- /4 width=7 by da_lift, fqup_fpbg/
+ /4 width=8 by da_lift, fqup_fpbg/
]
| #p #_ #_ #HT0 #H1 destruct -IH3 -IH2 -IH1
elim (snv_inv_gref … H1)
(* Relocation properties ****************************************************)
-lemma snv_lift: ∀h,g,G,K,T. ⦃G, K⦄ ⊢ T ¡[h, g] → ∀L,d,e. ⇩[d, e] L ≡ K →
+lemma snv_lift: ∀h,g,G,K,T. ⦃G, K⦄ ⊢ T ¡[h, g] → ∀L,s,d,e. ⇩[s, d, e] L ≡ K →
∀U. ⇧[d, e] T ≡ U → ⦃G, L⦄ ⊢ U ¡[h, g].
#h #g #G #K #T #H elim H -G -K -T
-[ #G #K #k #L #d #e #_ #X #H
+[ #G #K #k #L #s #d #e #_ #X #H
>(lift_inv_sort1 … H) -X -K -d -e //
-| #I #G #K #K0 #V #i #HK0 #_ #IHV #L #d #e #HLK #X #H
+| #I #G #K #K0 #V #i #HK0 #_ #IHV #L #s #d #e #HLK #X #H
elim (lift_inv_lref1 … H) * #Hid #H destruct
- [ elim (ldrop_trans_le … HLK … HK0) -K /2 width=2/ #X #HL0 #H
- elim (ldrop_inv_skip2 … H) -H /2 width=1/ -Hid #L0 #W #HLK0 #HVW #H destruct
- /3 width=8/
- | lapply (ldrop_trans_ge … HLK … HK0 ?) -K // -Hid /3 width=8/
+ [ elim (ldrop_trans_le … HLK … HK0) -K /2 width=2 by lt_to_le/ #X #HL0 #H
+ elim (ldrop_inv_skip2 … H) -H /2 width=1 by lt_plus_to_minus_r/ -Hid #L0 #W #HLK0 #HVW #H destruct
+ /3 width=9 by snv_lref/
+ | lapply (ldrop_trans_ge … HLK … HK0 ?) -K
+ /3 width=9 by snv_lref, ldrop_inv_gen/
]
-| #a #I #G #K #V #T #_ #_ #IHV #IHT #L #d #e #HLK #X #H
+| #a #I #G #K #V #T #_ #_ #IHV #IHT #L #s #d #e #HLK #X #H
elim (lift_inv_bind1 … H) -H #W #U #HVW #HTU #H destruct
- /4 width=4/
-| #a #G #K #V #V0 #V1 #T #T1 #l #_ #_ #Hl #HV0 #HV01 #HT1 #IHV #IHT #L #d #e #HLK #X #H
+ /4 width=5 by snv_bind, ldrop_skip/
+| #a #G #K #V #V0 #V1 #T #T1 #l #_ #_ #Hl #HV0 #HV01 #HT1 #IHV #IHT #L #s #d #e #HLK #X #H
elim (lift_inv_flat1 … H) -H #W #U #HVW #HTU #H destruct
elim (lift_total V0 d e) #W0 #HVW0
elim (lift_total V1 d e) #W1 #HVW1
elim (lift_total T1 (d+1) e) #U1 #HTU1
@(snv_appl … a … W0 … W1 … U1 l)
- [1,2: /2 width=4/ | /2 width=7/ |4,5: /2 width=9/ ]
- @(cpds_lift … HT1 … HLK … HTU) /2 width=1/
-| #G #K #V0 #T #V #l #_ #_ #Hl #HTV #HV0 #IHV0 #IHT #L #d #e #HLK #X #H
+ [1,2,3,4,5: /2 width=10 by cprs_lift, ssta_lift, da_lift/ ]
+ @(cpds_lift … HT1 … HLK … HTU) /2 width=1 by lift_bind/ (**) (* full auto raises typecjhecker failure *)
+| #G #K #V0 #T #V #l #_ #_ #Hl #HTV #HV0 #IHV0 #IHT #L #s #d #e #HLK #X #H
elim (lift_inv_flat1 … H) -H #W0 #U #HVW0 #HTU #H destruct
- elim (lift_total V d e) #W #HVW
- @(snv_cast … W l) [1,2: /2 width=4/ | /2 width=7/ |4,5: /2 width=9/ ]
+ elim (lift_total V d e)
+ /3 width=12 by snv_cast, cpcs_lift, ssta_lift, da_lift/
]
qed.
-lemma snv_inv_lift: ∀h,g,G,L,U. ⦃G, L⦄ ⊢ U ¡[h, g] → ∀K,d,e. ⇩[d, e] L ≡ K →
+lemma snv_inv_lift: ∀h,g,G,L,U. ⦃G, L⦄ ⊢ U ¡[h, g] → ∀K,s,d,e. ⇩[s, d, e] L ≡ K →
∀T. ⇧[d, e] T ≡ U → ⦃G, K⦄ ⊢ T ¡[h, g].
#h #g #G #L #U #H elim H -G -L -U
-[ #G #L #k #K #d #e #_ #X #H
+[ #G #L #k #K #s #d #e #_ #X #H
>(lift_inv_sort2 … H) -X -L -d -e //
-| #I #G #L #L0 #W #i #HL0 #_ #IHW #K #d #e #HLK #X #H
+| #I #G #L #L0 #W #i #HL0 #_ #IHW #K #s #d #e #HLK #X #H
elim (lift_inv_lref2 … H) * #Hid #H destruct
- [ elim (ldrop_conf_le … HLK … HL0) -L /2 width=2/ #X #HK0 #H
- elim (ldrop_inv_skip1 … H) -H /2 width=1/ -Hid #K0 #V #HLK0 #HVW #H destruct
- /3 width=8/
- | lapply (ldrop_conf_ge … HLK … HL0 ?) -L // -Hid /3 width=8/
+ [ elim (ldrop_conf_le … HLK … HL0) -L /2 width=2 by lt_to_le/ #X #HK0 #H
+ elim (ldrop_inv_skip1 … H) -H /2 width=1 by lt_plus_to_minus_r/ -Hid #K0 #V #HLK0 #HVW #H destruct
+ /3 width=12 by snv_lref/
+ | lapply (ldrop_conf_ge … HLK … HL0 ?) -L /3 width=9 by snv_lref/
]
-| #a #I #G #L #W #U #_ #_ #IHW #IHU #K #d #e #HLK #X #H
- elim (lift_inv_bind2 … H) -H #V #T #HVW #HTU #H destruct /4 width=4/
-| #a #G #L #W #W0 #W1 #U #U1 #l #_ #_ #Hl #HW0 #HW01 #HU1 #IHW #IHU #K #d #e #HLK #X #H
+| #a #I #G #L #W #U #_ #_ #IHW #IHU #K #s #d #e #HLK #X #H
+ elim (lift_inv_bind2 … H) -H #V #T #HVW #HTU #H destruct
+ /4 width=5 by snv_bind, ldrop_skip/
+| #a #G #L #W #W0 #W1 #U #U1 #l #_ #_ #Hl #HW0 #HW01 #HU1 #IHW #IHU #K #s #d #e #HLK #X #H
elim (lift_inv_flat2 … H) -H #V #T #HVW #HTU #H destruct
lapply (da_inv_lift … Hl … HLK … HVW) -Hl #Hl
elim (ssta_inv_lift1 … HW0 … HLK … HVW) -HW0 #V0 #HVW0 #HV0
elim (cprs_inv_lift1 … HW01 … HLK … HVW0) -W0 #V1 #HVW1 #HV01
elim (cpds_inv_lift1 … HU1 … HLK … HTU) -HU1 #X #H #HTU
elim (lift_inv_bind2 … H) -H #Y #T1 #HY #HTU1 #H destruct
- lapply (lift_inj … HY … HVW1) -HY #H destruct /3 width=8/
-| #G #L #W0 #U #W #l #_ #_ #Hl #HUW #HW0 #IHW0 #IHU #K #d #e #HLK #X #H
+ lapply (lift_inj … HY … HVW1) -HY #H destruct
+ /3 width=8 by snv_appl/
+| #G #L #W0 #U #W #l #_ #_ #Hl #HUW #HW0 #IHW0 #IHU #K #s #d #e #HLK #X #H
elim (lift_inv_flat2 … H) -H #V0 #T #HVW0 #HTU #H destruct
lapply (da_inv_lift … Hl … HLK … HTU) -Hl #Hl
elim (ssta_inv_lift1 … HUW … HLK … HTU) -HUW #V #HVW #HTV
- lapply (cpcs_inv_lift G … HLK … HVW … HVW0 ?) // -W /3 width=4/
+ lapply (cpcs_inv_lift G … HLK … HVW … HVW0 ?) // -W
+ /3 width=8 by snv_cast/
]
qed-.
elim (snv_inv_lref … H) -H #I2 #L2 #V2 #H #HV2
lapply (ldrop_inv_O2 … H) -H #H destruct //
|2: *
-|5,6: /3 width=7 by snv_inv_lift/
+|5,6: /3 width=8 by snv_inv_lift/
]
[1,3: #a #I #G1 #L1 #V1 #T1 #H elim (snv_inv_bind … H) -H //
|2,4: * #G1 #L1 #V1 #T1 #H
[ #H destruct -HLK1 /4 width=10 by fqup_fpbg, snv_lref/
| * #K0 #V0 #W0 #H #HVW0 #W0 -HV12
lapply (ldrop_mono … H … HLK1) -HLK1 -H #H destruct
- lapply (ldrop_fwd_drop2 … HLK2) -HLK2 /4 width=7 by fqup_fpbg, snv_lift/
+ lapply (ldrop_fwd_drop2 … HLK2) -HLK2 /4 width=8 by fqup_fpbg, snv_lift/
]
| #p #HG0 #HL0 #HT0 #H1 #X #H2 #L2 #HL12 destruct -IH4 -IH3 -IH2 -IH1
elim (snv_inv_gref … H1)
elim (ssta_cpr_lpr_aux … IH3 … HVW1 … HV10 … HL12) /2 width=2 by fqup_fpbg/ -IH3 -HVW1 #X #H1 #H2
lapply (cpcs_canc_sn … H2 HW10) -W10 #H2
elim (lift_total X 0 1) #W20 #H3
- lapply (ssta_lift … H1 (L2.ⓓW2) … HV02 … H3) /2 width=1 by ldrop_drop/ -H1 #HVW20
- lapply (cpcs_lift … (L2.ⓓW2) … H3 … HW13 H2) /2 width=1 by ldrop_drop/ -HW13 -H3 -H2 #HW320
+ lapply (ssta_lift … H1 (L2.ⓓW2) … HV02 … H3) /2 width=2 by ldrop_drop/ -H1 #HVW20
+ lapply (cpcs_lift … (L2.ⓓW2) … H3 … HW13 H2) /2 width=2 by ldrop_drop/ -HW13 -H3 -H2 #HW320
lapply (cpcs_cprs_strap1 … HW320 … HW1) -W3 #HW20
elim (cpcs_inv_cprs … HW20) -HW20 #W3 #HW203 #HW3
lapply (cpds_cprs_trans … (ⓛ{a}W3.U2) HTU2 ?) /2 width=1 by cprs_bind/ -HW3 -HTU2 #HTU2
lapply (IH2 … Hl0 … HV10 … HL12) /2 width=1 by fqup_fpbg/ -IH2 -Hl0 #Hl0
- lapply (da_lift … Hl0 (L2.ⓓW2) … HV02) /2 width=1 by ldrop_drop/ -Hl0 #Hl0
+ lapply (da_lift … Hl0 (L2.ⓓW2) … HV02) /2 width=2 by ldrop_drop/ -Hl0 #Hl0
lapply (IH1 … HW02 … HL12) /2 width=1 by fqup_fpbg/ -HW0 #HW2
lapply (IH1 … HV10 … HL12) /2 width=1 by fqup_fpbg/ -HV1 -HV10 #HV0
lapply (IH1 … HT02 (L2.ⓓW2) ?) /2 width=1 by fqup_fpbg, lpr_pair/ -L1 #HT2
]
[ elim (IH1 … HWl1 … HW0 … HW12 … HK12) -IH1 -HW0 /2 width=1 by fqup_fpbg/ #V2 #HWV2 #HV2
elim (lift_total V2 0 (i+1))
- /6 width=11 by fqup_fpbg, cpcs_lift, lsstas_ldec, ex2_intro/
+ /6 width=12 by fqup_fpbg, cpcs_lift, lsstas_ldec, ex2_intro/
| elim (IH1 … HVl1 … HW0 … HV12 … HK12) -IH1 -HVl1 -HW0 -HV12 -HK12 -IH2 /2 width=1 by fqup_fpbg/ #W2 #HVW2 #HW02
elim (lift_total W2 0 (i+1))
- /4 width=11 by cpcs_lift, lsstas_ldef, ex2_intro/
+ /4 width=12 by cpcs_lift, lsstas_ldef, ex2_intro/
| elim (IH1 … HVl1 … HW0 … HVX0 … HK12) -IH1 -HVl1 -HW0 -HVX0 -HK12 -IH2 -V2 /2 width=1 by fqup_fpbg/ -l1 #W2 #HXW2 #HW02
elim (lift_total W2 0 (i+1))
- /3 width=11 by cpcs_lift, lsstas_lift, ex2_intro/
+ /3 width=12 by cpcs_lift, lsstas_lift, ex2_intro/
]
| #p #_ #_ #HT0 #H1 destruct -IH4 -IH3 -IH2 -IH1
elim (snv_inv_gref … H1)
#G #L #T1 #T2 #H @(cpcs_ind … H) -T2
[ /3 width=3/
| #T #T2 #_ #HT2 * #T0 #HT10 elim HT2 -HT2 #HT2 #HT0
- [ elim (cprs_strip … HT0 … HT2) -T #T #HT0 #HT2
- lapply (cprs_strap1 … HT10 … HT0) -T0 /2 width=3/
- | lapply (cprs_strap2 … HT2 … HT0) -T /2 width=3/
+ [ elim (cprs_strip … HT0 … HT2) -T /3 width=3 by cprs_strap1, ex2_intro/
+ | /3 width=5 by cprs_strap2, ex2_intro/
]
]
qed-.
(* Basic_1: was: pc3_gen_sort *)
lemma cpcs_inv_sort: ∀G,L,k1,k2. ⦃G, L⦄ ⊢ ⋆k1 ⬌* ⋆k2 → k1 = k2.
-#G #L #k1 #k2 #H
-elim (cpcs_inv_cprs … H) -H #T #H1
->(cprs_inv_sort1 … H1) -T #H2
+#G #L #k1 #k2 #H elim (cpcs_inv_cprs … H) -H
+#T #H1 >(cprs_inv_sort1 … H1) -T #H2
lapply (cprs_inv_sort1 … H2) -L #H destruct //
qed-.
#a #G #L #W1 #T1 #T #H
elim (cpcs_inv_cprs … H) -H #X #H1 #H2
elim (cprs_inv_abst1 … H1) -H1 #W2 #T2 #HW12 #HT12 #H destruct
-@(ex2_2_intro … H2) -H2 /2 width=2/ (**) (* explicit constructor, /3 width=6/ is slow *)
+/3 width=6 by cprs_bind, ex2_2_intro/
qed-.
lemma cpcs_inv_abst2: ∀a,G,L,W1,T1,T. ⦃G, L⦄ ⊢ T ⬌* ⓛ{a}W1.T1 →
qed-.
(* Basic_1: was: pc3_gen_lift *)
-lemma cpcs_inv_lift: ∀G,L,K,d,e. ⇩[d, e] L ≡ K →
+lemma cpcs_inv_lift: ∀G,L,K,s,d,e. ⇩[s, d, e] L ≡ K →
∀T1,U1. ⇧[d, e] T1 ≡ U1 → ∀T2,U2. ⇧[d, e] T2 ≡ U2 →
⦃G, L⦄ ⊢ U1 ⬌* U2 → ⦃G, K⦄ ⊢ T1 ⬌* T2.
-#G #L #K #d #e #HLK #T1 #U1 #HTU1 #T2 #U2 #HTU2 #HU12
+#G #L #K #s #d #e #HLK #T1 #U1 #HTU1 #T2 #U2 #HTU2 #HU12
elim (cpcs_inv_cprs … HU12) -HU12 #U #HU1 #HU2
elim (cprs_inv_lift1 … HU1 … HLK … HTU1) -U1 #T #HTU #HT1
elim (cprs_inv_lift1 … HU2 … HLK … HTU2) -L -U2 #X #HXU
->(lift_inj … HXU … HTU) -X -U -d -e /2 width=3/
+>(lift_inj … HXU … HTU) -X -U -d -e /2 width=3 by cprs_div/
qed-.
(* Advanced properties ******************************************************)
lemma lpr_cpcs_trans: ∀G,L1,L2. ⦃G, L1⦄ ⊢ ➡ L2 →
∀T1,T2. ⦃G, L2⦄ ⊢ T1 ⬌* T2 → ⦃G, L1⦄ ⊢ T1 ⬌* T2.
-#G #L1 #L2 #HL12 #T1 #T2 #H
-elim (cpcs_inv_cprs … H) -H #T #HT1 #HT2
-lapply (lpr_cprs_trans … HT1 … HL12) -HT1
-lapply (lpr_cprs_trans … HT2 … HL12) -L2 /2 width=3/
+#G #L1 #L2 #HL12 #T1 #T2 #H elim (cpcs_inv_cprs … H) -H
+/4 width=5 by cprs_div, lpr_cprs_trans/
qed-.
lemma lprs_cpcs_trans: ∀G,L1,L2. ⦃G, L1⦄ ⊢ ➡* L2 →
∀T1,T2. ⦃G, L2⦄ ⊢ T1 ⬌* T2 → ⦃G, L1⦄ ⊢ T1 ⬌* T2.
-#G #L1 #L2 #HL12 #T1 #T2 #H
-elim (cpcs_inv_cprs … H) -H #T #HT1 #HT2
-lapply (lprs_cprs_trans … HT1 … HL12) -HT1
-lapply (lprs_cprs_trans … HT2 … HL12) -L2 /2 width=3/
+#G #L1 #L2 #HL12 #T1 #T2 #H elim (cpcs_inv_cprs … H) -H
+/4 width=5 by cprs_div, lprs_cprs_trans/
qed-.
lemma cpr_cprs_conf_cpcs: ∀G,L,T,T1,T2. ⦃G, L⦄ ⊢ T ➡* T1 → ⦃G, L⦄ ⊢ T ➡ T2 → ⦃G, L⦄ ⊢ T1 ⬌* T2.
-#G #L #T #T1 #T2 #HT1 #HT2
-elim (cprs_strip … HT1 … HT2) /2 width=3 by cpr_cprs_div/
+#G #L #T #T1 #T2 #HT1 #HT2 elim (cprs_strip … HT1 … HT2) -HT1 -HT2
+/2 width=3 by cpr_cprs_div/
qed-.
lemma cprs_cpr_conf_cpcs: ∀G,L,T,T1,T2. ⦃G, L⦄ ⊢ T ➡* T1 → ⦃G, L⦄ ⊢ T ➡ T2 → ⦃G, L⦄ ⊢ T2 ⬌* T1.
-#G #L #T #T1 #T2 #HT1 #HT2
-elim (cprs_strip … HT1 … HT2) /2 width=3 by cprs_cpr_div/
+#G #L #T #T1 #T2 #HT1 #HT2 elim (cprs_strip … HT1 … HT2) -HT1 -HT2
+/2 width=3 by cprs_cpr_div/
qed-.
lemma cprs_conf_cpcs: ∀G,L,T,T1,T2. ⦃G, L⦄ ⊢ T ➡* T1 → ⦃G, L⦄ ⊢ T ➡* T2 → ⦃G, L⦄ ⊢ T1 ⬌* T2.
-#G #L #T #T1 #T2 #HT1 #HT2
-elim (cprs_conf … HT1 … HT2) /2 width=3/
+#G #L #T #T1 #T2 #HT1 #HT2 elim (cprs_conf … HT1 … HT2) -HT1 -HT2
+/2 width=3 by cprs_div/
qed-.
lemma lprs_cprs_conf: ∀G,L1,L2. ⦃G, L1⦄ ⊢ ➡* L2 →
∀T1,T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ⦃G, L2⦄ ⊢ T1 ⬌* T2.
-#G #L1 #L2 #HL12 #T1 #T2 #HT12
-elim (lprs_cprs_conf_dx … HT12 … HL12) -L1 /2 width=3/
+#G #L1 #L2 #HL12 #T1 #T2 #HT12 elim (lprs_cprs_conf_dx … HT12 … HL12) -L1
+/2 width=3 by cprs_div/
qed-.
(* Basic_1: was: pc3_wcpr0_t *)
(* Basic_1: was only: pc3_thin_dx *)
lemma cpcs_flat: ∀G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ⬌* V2 → ∀T1,T2. ⦃G, L⦄ ⊢ T1 ⬌* T2 →
∀I. ⦃G, L⦄ ⊢ ⓕ{I}V1.T1 ⬌* ⓕ{I}V2.T2.
-#G #L #V1 #V2 #HV12 #T1 #T2 #HT12 #I
-elim (cpcs_inv_cprs … HV12) -HV12 #V #HV1 #HV2
-elim (cpcs_inv_cprs … HT12) -HT12 /3 width=5 by cprs_flat, cprs_div/ (**) (* /3 width=5/ is too slow *)
+#G #L #V1 #V2 #HV12 #T1 #T2 #HT12
+elim (cpcs_inv_cprs … HV12) -HV12
+elim (cpcs_inv_cprs … HT12) -HT12
+/3 width=5 by cprs_flat, cprs_div/
qed.
lemma cpcs_flat_dx_cpr_rev: ∀G,L,V1,V2. ⦃G, L⦄ ⊢ V2 ➡ V1 → ∀T1,T2. ⦃G, L⦄ ⊢ T1 ⬌* T2 →
∀I. ⦃G, L⦄ ⊢ ⓕ{I}V1.T1 ⬌* ⓕ{I}V2.T2.
-/3 width=1/ qed.
+/3 width=1 by cpr_cpcs_sn, cpcs_flat/ qed.
lemma cpcs_bind_dx: ∀a,I,G,L,V,T1,T2. ⦃G, L.ⓑ{I}V⦄ ⊢ T1 ⬌* T2 →
⦃G, L⦄ ⊢ ⓑ{a,I}V.T1 ⬌* ⓑ{a,I}V.T2.
-#a #I #G #L #V #T1 #T2 #HT12
-elim (cpcs_inv_cprs … HT12) -HT12 /3 width=5 by cprs_div, cprs_bind/ (**) (* /3 width=5/ is a bit slow *)
+#a #I #G #L #V #T1 #T2 #HT12 elim (cpcs_inv_cprs … HT12) -HT12
+/3 width=5 by cprs_div, cprs_bind/
qed.
lemma cpcs_bind_sn: ∀a,I,G,L,V1,V2,T. ⦃G, L⦄ ⊢ V1 ⬌* V2 → ⦃G, L⦄ ⊢ ⓑ{a,I}V1. T ⬌* ⓑ{a,I}V2. T.
-#a #I #G #L #V1 #V2 #T #HV12
-elim (cpcs_inv_cprs … HV12) -HV12 /3 width=5 by cprs_div, cprs_bind/ (**) (* /3 width=5/ is a bit slow *)
+#a #I #G #L #V1 #V2 #T #HV12 elim (cpcs_inv_cprs … HV12) -HV12
+/3 width=5 by cprs_div, cprs_bind/
qed.
lemma lsubr_cpcs_trans: ∀G,L1,T1,T2. ⦃G, L1⦄ ⊢ T1 ⬌* T2 →
∀L2. L2 ⊑ L1 → ⦃G, L2⦄ ⊢ T1 ⬌* T2.
-#G #L1 #T1 #T2 #HT12
-elim (cpcs_inv_cprs … HT12) -HT12
-/3 width=5 by cprs_div, lsubr_cprs_trans/ (**) (* /3 width=5/ is a bit slow *)
+#G #L1 #T1 #T2 #HT12 elim (cpcs_inv_cprs … HT12) -HT12
+/3 width=5 by cprs_div, lsubr_cprs_trans/
qed-.
(* Basic_1: was: pc3_lift *)
-lemma cpcs_lift: ∀G,L,K,d,e. ⇩[d, e] L ≡ K →
+lemma cpcs_lift: ∀G,L,K,s,d,e. ⇩[s, d, e] L ≡ K →
∀T1,U1. ⇧[d, e] T1 ≡ U1 → ∀T2,U2. ⇧[d, e] T2 ≡ U2 →
⦃G, K⦄ ⊢ T1 ⬌* T2 → ⦃G, L⦄ ⊢ U1 ⬌* U2.
-#G #L #K #d #e #HLK #T1 #U1 #HTU1 #T2 #U2 #HTU2 #HT12
+#G #L #K #s #d #e #HLK #T1 #U1 #HTU1 #T2 #U2 #HTU2 #HT12
elim (cpcs_inv_cprs … HT12) -HT12 #T #HT1 #HT2
-elim (lift_total T d e) #U #HTU
-lapply (cprs_lift … HT1 … HLK … HTU1 … HTU) -T1 #HU1
-lapply (cprs_lift … HT2 … HLK … HTU2 … HTU) -K -T2 -T -d -e /2 width=3/
+elim (lift_total T d e) /3 width=12 by cprs_div, cprs_lift/
qed.
lemma cpcs_strip: ∀G,L,T1,T. ⦃G, L⦄ ⊢ T ⬌* T1 → ∀T2. ⦃G, L⦄ ⊢ T ⬌ T2 →
elim (cpcs_inv_cprs … H) -H #T #H1 #H2
elim (cprs_inv_abst1 … H1) -H1 #W0 #T0 #HW10 #HT10 #H destruct
elim (cprs_inv_abst1 … H2) -H2 #W #T #HW2 #HT2 #H destruct
-lapply (lprs_cprs_conf … (L.ⓛW) … HT2) /2 width=1/ -HT2 #HT2
-lapply (lprs_cpcs_trans … (L.ⓛW1) … HT2) /2 width=1/ -HT2 #HT2
+lapply (lprs_cprs_conf … (L.ⓛW) … HT2) /2 width=1 by lprs_pair/ -HT2 #HT2
+lapply (lprs_cpcs_trans … (L.ⓛW1) … HT2) /2 width=1 by lprs_pair/ -HT2 #HT2
/4 width=3 by and3_intro, cprs_div, cpcs_cprs_div, cpcs_sym/
qed-.
lemma cpcs_inv_abst_dx: ∀a1,a2,G,L,W1,W2,T1,T2. ⦃G, L⦄ ⊢ ⓛ{a1}W1.T1 ⬌* ⓛ{a2}W2.T2 →
∧∧ ⦃G, L⦄ ⊢ W1 ⬌* W2 & ⦃G, L.ⓛW2⦄ ⊢ T1 ⬌* T2 & a1 = a2.
-#a1 #a2 #G #L #W1 #W2 #T1 #T2 #HT12
-lapply (cpcs_sym … HT12) -HT12 #HT12
-elim (cpcs_inv_abst_sn … HT12) -HT12 /3 width=1/
+#a1 #a2 #G #L #W1 #W2 #T1 #T2 #HT12 lapply (cpcs_sym … HT12) -HT12
+#HT12 elim (cpcs_inv_abst_sn … HT12) -HT12 /3 width=1 by cpcs_sym, and3_intro/
qed-.
(* Main properties **********************************************************)
#G #L #T1 #T #HT1 #T2 @(trans_TC … HT1) qed-.
theorem cpcs_canc_sn: ∀G,L,T,T1,T2. ⦃G, L⦄ ⊢ T ⬌* T1 → ⦃G, L⦄ ⊢ T ⬌* T2 → ⦃G, L⦄ ⊢ T1 ⬌* T2.
-/3 width=3 by cpcs_trans, cpcs_sym/ qed-. (**) (* /3 width=3/ is too slow *)
+/3 width=3 by cpcs_trans, cpcs_sym/ qed-.
theorem cpcs_canc_dx: ∀G,L,T,T1,T2. ⦃G, L⦄ ⊢ T1 ⬌* T → ⦃G, L⦄ ⊢ T2 ⬌* T → ⦃G, L⦄ ⊢ T1 ⬌* T2.
-/3 width=3 by cpcs_trans, cpcs_sym/ qed-. (**) (* /3 width=3/ is too slow *)
+/3 width=3 by cpcs_trans, cpcs_sym/ qed-.
lemma cpcs_bind1: ∀a,I,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ⬌* V2 →
∀T1,T2. ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ⬌* T2 →
⦃G, L⦄ ⊢ ⓑ{a,I}V1. T1 ⬌* ⓑ{a,I}V2. T2.
-#a #I #G #L #V1 #V2 #HV12 #T1 #T2 #HT12
-@(cpcs_trans … (ⓑ{a,I}V1.T2)) /2 width=1/
-qed.
+/3 width=3 by cpcs_trans, cpcs_bind_sn, cpcs_bind_dx/ qed.
lemma cpcs_bind2: ∀a,I,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ⬌* V2 →
∀T1,T2. ⦃G, L.ⓑ{I}V2⦄ ⊢ T1 ⬌* T2 →
⦃G, L⦄ ⊢ ⓑ{a,I}V1. T1 ⬌* ⓑ{a,I}V2. T2.
-#a #I #G #L #V1 #V2 #HV12 #T1 #T2 #HT12
-@(cpcs_trans … (ⓑ{a,I}V2.T1)) /2 width=1/
-qed.
+/3 width=3 by cpcs_trans, cpcs_bind_sn, cpcs_bind_dx/ qed.
(* Basic_1: was: pc3_wcpr0 *)
lemma lpr_cpcs_conf: ∀G,L1,L2. ⦃G, L1⦄ ⊢ ➡ L2 →
∀T1,T2. ⦃G, L1⦄ ⊢ T1 ⬌* T2 → ⦃G, L2⦄ ⊢ T1 ⬌* T2.
-#G #L1 #L2 #HL12 #T1 #T2 #H
-elim (cpcs_inv_cprs … H) -H /3 width=5 by cpcs_canc_dx, lpr_cprs_conf/
+#G #L1 #L2 #HL12 #T1 #T2 #H elim (cpcs_inv_cprs … H) -H
+/3 width=5 by cpcs_canc_dx, lpr_cprs_conf/
qed-.
@⦃i, des⦄ ≡ i0 & des ▭ i ≡ des0.
#L1 #L #des #H elim H -L1 -L -des
[ /2 width=7 by ldrops_nil, minuss_nil, at_nil, ex4_3_intro/
-| #L1 #L3 #L #des3 #d #e #_ #HL3 #IHL13 #L2 #i #HL2
+| #L1 #L0 #L #des #d #e #_ #HL0 #IHL0 #L2 #i #HL2
elim (lt_or_ge i d) #Hid
- [ elim (ldrop_trans_le … HL3 … HL2) -L /2 width=2 by lt_to_le/
- #L #HL3 #HL2 elim (IHL13 … HL3) -L3 /3 width=7 by ldrops_cons, minuss_lt, at_lt, ex4_3_intro/
- | lapply (ldrop_trans_ge … HL3 … HL2 ?) -L // #HL32
- elim (IHL13 … HL32) -L3 /3 width=7 by minuss_ge, at_ge, ex4_3_intro/
+ [ elim (ldrop_trans_le … HL0 … HL2) -L /2 width=2 by lt_to_le/
+ #L #HL0 #HL2 elim (IHL0 … HL0) -L0 /3 width=7 by ldrops_cons, minuss_lt, at_lt, ex4_3_intro/
+ | lapply (ldrop_trans_ge … HL0 … HL2 ?) -L // #HL02
+ elim (IHL0 … HL02) -L0 /3 width=7 by minuss_ge, at_ge, ex4_3_intro/
]
]
qed-.
+
Closure of context-sensitive extended computation
for native validity.
</news>
+ <news date="2014 January 20.">
+ Parametrized slicing for local environments
+ comprises both versions of this operation
+ (one from basic_1, the other used in basic_2 till now).
+ </news>
<news date="2013 August 7.">
Passive support for global environments.
</news>
projects / helm.git / commitdiff