| #i #H1i #IH #H2i
elim (drops_ldec_dec L i) [ * #K #W #HLK | -H1i -IH #HnX ]
[ lapply (cnv_inv_lref_pair … H2i … HLK) -H2i #H2W
- lapply (csx_inv_lref_pair … HLK H1i) -H1i #H1W
+ lapply (csx_inv_lref_pair_drops … HLK H1i) -H1i #H1W
elim (cpue_total_csx … H1W) -H1W #X
elim (abst_dec X) [ * | -IH ]
[ #p #V1 #U #H destruct * #n #HWU #_
--- /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 *)
+(* *)
+(**************************************************************************)
+
+(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
+
+notation "hvbox( G ⊢ break term 46 L1 ⊒[ break term 46 h] break term 46 L2 )"
+ non associative with precedence 45
+ for @{ 'ToPRedTySNStrong $h $G $L1 $L2 }.
+++ /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 *)
-(* *)
-(**************************************************************************)
-
-(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-
-notation "hvbox( G ⊢ break term 46 L1 ⊒[ break term 46 h, break term 46 f ] break term 46 L2 )"
- non associative with precedence 45
- for @{ 'ToPRedTySNStrong $h $f $G $L1 $L2 }.
(* Advanced properties ******************************************************)
-lemma csx_tdeq_trans: ∀h,G,L,T1. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃T1⦄ →
- ∀T2. T1 ≛ T2 → ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃T2⦄.
+lemma csx_tdeq_trans (h) (G):
+ ∀L,T1. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃T1⦄ →
+ ∀T2. T1 ≛ T2 → ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃T2⦄.
#h #G #L #T1 #H @(csx_ind … H) -T1 #T #_ #IH #T2 #HT2
@csx_intro #T1 #HT21 #HnT21 elim (tdeq_cpx_trans … HT2 … HT21) -HT21
/4 width=5 by tdeq_repl/
qed-.
-lemma csx_cpx_trans: ∀h,G,L,T1. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃T1⦄ →
- ∀T2. ⦃G,L⦄ ⊢ T1 ⬈[h] T2 → ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃T2⦄.
+lemma csx_cpx_trans (h) (G):
+ ∀L,T1. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃T1⦄ →
+ ∀T2. ⦃G,L⦄ ⊢ T1 ⬈[h] T2 → ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃T2⦄.
#h #G #L #T1 #H @(csx_ind … H) -T1 #T1 #HT1 #IHT1 #T2 #HLT12
elim (tdeq_dec T1 T2) /3 width=4 by csx_tdeq_trans/
qed-.
(* Basic_1: was just: sn3_cast *)
-lemma csx_cast: ∀h,G,L,W. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃W⦄ →
- ∀T. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃T⦄ → ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃ⓝW.T⦄.
+lemma csx_cast (h) (G):
+ ∀L,W. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃W⦄ →
+ ∀T. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃T⦄ → ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃ⓝW.T⦄.
#h #G #L #W #HW @(csx_ind … HW) -W
#W #HW #IHW #T #HT @(csx_ind … HT) -T
#T #HT #IHT @csx_intro
(* Basic_1: was just: sn3_abbr *)
(* Basic_2A1: was: csx_lref_bind *)
-lemma csx_lref_pair: ∀h,I,G,L,K,V,i. ⬇*[i] L ≘ K.ⓑ{I}V →
- ⦃G,K⦄ ⊢ ⬈*[h] 𝐒⦃V⦄ → ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃#i⦄.
-#h #I #G #L #K #V #i #HLK #HV
+lemma csx_lref_pair_drops (h) (G):
+ ∀I,L,K,V,i. ⬇*[i] L ≘ K.ⓑ{I}V →
+ ⦃G,K⦄ ⊢ ⬈*[h] 𝐒⦃V⦄ → ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃#i⦄.
+#h #G #I #L #K #V #i #HLK #HV
@csx_intro #X #H #Hi elim (cpx_inv_lref1_drops … H) -H
[ #H destruct elim Hi //
| -Hi * #I0 #K0 #V0 #V1 #HLK0 #HV01 #HV1
(* Basic_1: was: sn3_gen_def *)
(* Basic_2A1: was: csx_inv_lref_bind *)
-lemma csx_inv_lref_pair: ∀h,I,G,L,K,V,i. ⬇*[i] L ≘ K.ⓑ{I}V →
- ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃#i⦄ → ⦃G,K⦄ ⊢ ⬈*[h] 𝐒⦃V⦄.
-#h #I #G #L #K #V #i #HLK #Hi
+lemma csx_inv_lref_pair_drops (h) (G):
+ ∀I,L,K,V,i. ⬇*[i] L ≘ K.ⓑ{I}V →
+ ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃#i⦄ → ⦃G,K⦄ ⊢ ⬈*[h] 𝐒⦃V⦄.
+#h #G #I #L #K #V #i #HLK #Hi
elim (lifts_total V (𝐔❴↑i❵))
/4 width=9 by csx_inv_lifts, csx_cpx_trans, cpx_delta_drops, drops_isuni_fwd_drop2/
qed-.
-lemma csx_inv_lref: ∀h,G,L,i. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃#i⦄ →
- ∨∨ ⬇*[Ⓕ,𝐔❴i❵] L ≘ ⋆
- | ∃∃I,K. ⬇*[i] L ≘ K.ⓤ{I}
- | ∃∃I,K,V. ⬇*[i] L ≘ K.ⓑ{I}V & ⦃G,K⦄ ⊢ ⬈*[h] 𝐒⦃V⦄.
+lemma csx_inv_lref_drops (h) (G):
+ ∀L,i. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃#i⦄ →
+ ∨∨ ⬇*[Ⓕ,𝐔❴i❵] L ≘ ⋆
+ | ∃∃I,K. ⬇*[i] L ≘ K.ⓤ{I}
+ | ∃∃I,K,V. ⬇*[i] L ≘ K.ⓑ{I}V & ⦃G,K⦄ ⊢ ⬈*[h] 𝐒⦃V⦄.
#h #G #L #i #H elim (drops_F_uni L i) /2 width=1 by or3_intro0/
-* * /4 width=9 by csx_inv_lref_pair, ex2_3_intro, ex1_2_intro, or3_intro2, or3_intro1/
+* * /4 width=9 by csx_inv_lref_pair_drops, ex2_3_intro, ex1_2_intro, or3_intro2, or3_intro1/
qed-.
(* Advanced properties ************************************* ****************)
(* Basic_1: was just: sn3_appls_beta *)
-lemma csx_applv_beta: ∀h,p,G,L,Vs,V,W,T. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃ⒶVs.ⓓ{p}ⓝW.V.T⦄ →
- ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃ⒶVs.ⓐV.ⓛ{p}W.T⦄.
-#h #p #G #L #Vs elim Vs -Vs /2 width=1 by csx_appl_beta/
+lemma csx_applv_beta (h) (G):
+ ∀p,L,Vs,V,W,T. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃ⒶVs.ⓓ{p}ⓝW.V.T⦄ →
+ ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃ⒶVs.ⓐV.ⓛ{p}W.T⦄.
+#h #G #p #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
]
qed.
-lemma csx_applv_delta: ∀h,I,G,L,K,V1,i. ⬇*[i] L ≘ K.ⓑ{I}V1 →
- ∀V2. ⬆*[↑i] V1 ≘ V2 →
- ∀Vs. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃ⒶVs.V2⦄ → ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃ⒶVs.#i⦄.
-#h #I #G #L #K #V1 #i #HLK #V2 #HV12 #Vs elim Vs -Vs
-[ /4 width=11 by csx_inv_lifts, csx_lref_pair, drops_isuni_fwd_drop2/
+lemma csx_applv_delta_drops (h) (G):
+ ∀I,L,K,V1,i. ⬇*[i] L ≘ K.ⓑ{I}V1 →
+ ∀V2. ⬆*[↑i] V1 ≘ V2 →
+ ∀Vs. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃ⒶVs.V2⦄ → ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃ⒶVs.#i⦄.
+#h #G #I #L #K #V1 #i #HLK #V2 #HV12 #Vs elim Vs -Vs
+[ /4 width=11 by csx_inv_lifts, csx_lref_pair_drops, drops_isuni_fwd_drop2/
| #V #Vs #IHV #H1T
lapply (csx_fwd_pair_sn … H1T) #HV
lapply (csx_fwd_flat_dx … H1T) #H2T
qed.
(* Basic_1: was just: sn3_appls_abbr *)
-lemma csx_applv_theta: ∀h,p,G,L,V1b,V2b. ⬆*[1] V1b ≘ V2b →
- ∀V,T. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃ⓓ{p}V.ⒶV2b.T⦄ →
- ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃ⒶV1b.ⓓ{p}V.T⦄.
-#h #p #G #L #V1b #V2b * -V1b -V2b /2 width=1 by/
+lemma csx_applv_theta (h) (G):
+ ∀p,L,V1b,V2b. ⬆*[1] V1b ≘ V2b →
+ ∀V,T. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃ⓓ{p}V.ⒶV2b.T⦄ → ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃ⒶV1b.ⓓ{p}V.T⦄.
+#h #G #p #L #V1b #V2b * -V1b -V2b /2 width=1 by/
#V1b #V2b #V1 #V2 #HV12 #H
generalize in match HV12; -HV12 generalize in match V2; -V2 generalize in match V1; -V1
elim H -V1b -V2b /2 width=3 by csx_appl_theta/
qed.
(* Basic_1: was just: sn3_appls_cast *)
-lemma csx_applv_cast: ∀h,G,L,Vs,U. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃ⒶVs.U⦄ →
- ∀T. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃ⒶVs.T⦄ → ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃ⒶVs.ⓝU.T⦄.
+lemma csx_applv_cast (h) (G):
+ ∀L,Vs,U. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃ⒶVs.U⦄ →
+ ∀T. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃ⒶVs.T⦄ → ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃ⒶVs.ⓝU.T⦄.
#h #G #L #Vs elim Vs -Vs /2 width=1 by csx_cast/
#V #Vs #IHV #U #H1U #T #H1T
lapply (csx_fwd_pair_sn … H1U) #HV
(* Properties with extended supclosure **************************************)
-lemma csx_fqu_conf: ∀h,b,G1,G2,L1,L2,T1,T2. ⦃G1,L1,T1⦄ ⬂[b] ⦃G2,L2,T2⦄ →
- ⦃G1,L1⦄ ⊢ ⬈*[h] 𝐒⦃T1⦄ → ⦃G2,L2⦄ ⊢ ⬈*[h] 𝐒⦃T2⦄.
+lemma csx_fqu_conf (h) (b):
+ ∀G1,G2,L1,L2,T1,T2. ⦃G1,L1,T1⦄ ⬂[b] ⦃G2,L2,T2⦄ →
+ ⦃G1,L1⦄ ⊢ ⬈*[h] 𝐒⦃T1⦄ → ⦃G2,L2⦄ ⊢ ⬈*[h] 𝐒⦃T2⦄.
#h #b #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2
-[ /3 width=5 by csx_inv_lref_pair, drops_refl/
+[ /3 width=5 by csx_inv_lref_pair_drops, drops_refl/
| /2 width=3 by csx_fwd_pair_sn/
| /2 width=2 by csx_fwd_bind_dx/
| /2 width=4 by csx_fwd_bind_dx_unit/
]
qed-.
-lemma csx_fquq_conf: ∀h,b,G1,G2,L1,L2,T1,T2. ⦃G1,L1,T1⦄ ⬂⸮[b] ⦃G2,L2,T2⦄ →
- ⦃G1,L1⦄ ⊢ ⬈*[h] 𝐒⦃T1⦄ → ⦃G2,L2⦄ ⊢ ⬈*[h] 𝐒⦃T2⦄.
+lemma csx_fquq_conf (h) (b):
+ ∀G1,G2,L1,L2,T1,T2. ⦃G1,L1,T1⦄ ⬂⸮[b] ⦃G2,L2,T2⦄ →
+ ⦃G1,L1⦄ ⊢ ⬈*[h] 𝐒⦃T1⦄ → ⦃G2,L2⦄ ⊢ ⬈*[h] 𝐒⦃T2⦄.
#h #b #G1 #G2 #L1 #L2 #T1 #T2 * /2 width=6 by csx_fqu_conf/
* #HG #HL #HT destruct //
qed-.
-lemma csx_fqup_conf: ∀h,b,G1,G2,L1,L2,T1,T2. ⦃G1,L1,T1⦄ ⬂+[b] ⦃G2,L2,T2⦄ →
- ⦃G1,L1⦄ ⊢ ⬈*[h] 𝐒⦃T1⦄ → ⦃G2,L2⦄ ⊢ ⬈*[h] 𝐒⦃T2⦄.
+lemma csx_fqup_conf (h) (b):
+ ∀G1,G2,L1,L2,T1,T2. ⦃G1,L1,T1⦄ ⬂+[b] ⦃G2,L2,T2⦄ →
+ ⦃G1,L1⦄ ⊢ ⬈*[h] 𝐒⦃T1⦄ → ⦃G2,L2⦄ ⊢ ⬈*[h] 𝐒⦃T2⦄.
#h #b #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind … H) -G2 -L2 -T2
/3 width=6 by csx_fqu_conf/
qed-.
-lemma csx_fqus_conf: ∀h,b,G1,G2,L1,L2,T1,T2. ⦃G1,L1,T1⦄ ⬂*[b] ⦃G2,L2,T2⦄ →
- ⦃G1,L1⦄ ⊢ ⬈*[h] 𝐒⦃T1⦄ → ⦃G2,L2⦄ ⊢ ⬈*[h] 𝐒⦃T2⦄.
+lemma csx_fqus_conf (h) (b):
+ ∀G1,G2,L1,L2,T1,T2. ⦃G1,L1,T1⦄ ⬂*[b] ⦃G2,L2,T2⦄ →
+ ⦃G1,L1⦄ ⊢ ⬈*[h] 𝐒⦃T1⦄ → ⦃G2,L2⦄ ⊢ ⬈*[h] 𝐒⦃T2⦄.
#h #b #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqus_ind … H) -H
/3 width=6 by csx_fquq_conf/
qed-.
(* Main properties with generic candidates of reducibility ******************)
-theorem csx_gcr: ∀h. gcr (cpx h) tdeq (csx h) (csx h).
+theorem csx_gcr (h): gcr (cpx h) tdeq (csx h) (csx h).
#h @mk_gcr
[ //
| #G #L #Vs #Hvs #T #HT #H
@(csx_applv_cnx … H) -H // (**) (* auto fails *)
| /2 width=1 by csx_applv_beta/
-| /2 width=7 by csx_applv_delta/
+| /2 width=7 by csx_applv_delta_drops/
| /3 width=3 by csx_applv_theta, csx_abbr/
| /2 width=1 by csx_applv_cast/
]
(* Properties with unbound parallel rt-transition on all entries ************)
-lemma csx_lpx_conf: ∀h,G,L1,T. ⦃G,L1⦄ ⊢ ⬈*[h] 𝐒⦃T⦄ →
- ∀L2. ⦃G,L1⦄ ⊢ ⬈[h] L2 → ⦃G,L2⦄ ⊢ ⬈*[h] 𝐒⦃T⦄.
+lemma csx_lpx_conf (h) (G):
+ ∀L1,T. ⦃G,L1⦄ ⊢ ⬈*[h] 𝐒⦃T⦄ →
+ ∀L2. ⦃G,L1⦄ ⊢ ⬈[h] L2 → ⦃G,L2⦄ ⊢ ⬈*[h] 𝐒⦃T⦄.
#h #G #L1 #T #H @(csx_ind_cpxs … H) -T
/4 width=3 by csx_intro, lpx_cpx_trans/
qed-.
(* Advanced properties ******************************************************)
-lemma csx_abst: ∀h,p,G,L,W. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃W⦄ →
- ∀T. ⦃G,L.ⓛW⦄ ⊢ ⬈*[h] 𝐒⦃T⦄ → ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃ⓛ{p}W.T⦄.
-#h #p #G #L #W #HW
+lemma csx_abst (h) (G):
+ ∀p,L,W. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃W⦄ →
+ ∀T. ⦃G,L.ⓛW⦄ ⊢ ⬈*[h] 𝐒⦃T⦄ → ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃ⓛ{p}W.T⦄.
+#h #G #p #L #W #HW
@(csx_ind … HW) -W #W #_ #IHW #T #HT
@(csx_ind … HT) -T #T #HT #IHT
@csx_intro #X #H1 #H2
]
qed.
-lemma csx_abbr: ∀h,p,G,L,V. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃V⦄ →
- ∀T. ⦃G,L.ⓓV⦄ ⊢ ⬈*[h] 𝐒⦃T⦄ → ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃ⓓ{p}V.T⦄.
-#h #p #G #L #V #HV
+lemma csx_abbr (h) (G):
+ ∀p,L,V. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃V⦄ →
+ ∀T. ⦃G,L.ⓓV⦄ ⊢ ⬈*[h] 𝐒⦃T⦄ → ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃ⓓ{p}V.T⦄.
+#h #G #p #L #V #HV
@(csx_ind … HV) -V #V #_ #IHV #T #HT
@(csx_ind_cpxs … HT) -T #T #HT #IHT
@csx_intro #X #H1 #H2
]
qed.
-fact csx_appl_theta_aux: ∀h,p,G,L,U. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃U⦄ → ∀V1,V2. ⬆*[1] V1 ≘ V2 →
- ∀V,T. U = ⓓ{p}V.ⓐV2.T → ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃ⓐV1.ⓓ{p}V.T⦄.
-#h #p #G #L #X #H
+lemma csx_bind (h) (G):
+ ∀p,I,L,V. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃V⦄ →
+ ∀T. ⦃G,L.ⓑ{I}V⦄ ⊢ ⬈*[h] 𝐒⦃T⦄ → ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃ⓑ{p,I}V.T⦄.
+#h #G #p * #L #V #HV #T #HT
+/2 width=1 by csx_abbr, csx_abst/
+qed.
+
+fact csx_appl_theta_aux (h) (G):
+ ∀p,L,U. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃U⦄ → ∀V1,V2. ⬆*[1] V1 ≘ V2 →
+ ∀V,T. U = ⓓ{p}V.ⓐV2.T → ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃ⓐV1.ⓓ{p}V.T⦄.
+#h #G #p #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
]
qed-.
-lemma csx_appl_theta: ∀h,p,G,L,V,V2,T. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃ⓓ{p}V.ⓐV2.T⦄ →
- ∀V1. ⬆*[1] V1 ≘ V2 → ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃ⓐV1.ⓓ{p}V.T⦄.
+lemma csx_appl_theta (h) (G):
+ ∀p,L,V,V2,T. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃ⓓ{p}V.ⓐV2.T⦄ →
+ ∀V1. ⬆*[1] V1 ≘ V2 → ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃ⓐV1.ⓓ{p}V.T⦄.
/2 width=5 by csx_appl_theta_aux/ qed.
(* Advanced properties ******************************************************)
-fact csx_appl_beta_aux: ∀h,p,G,L,U1. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃U1⦄ →
- ∀V,W,T1. U1 = ⓓ{p}ⓝW.V.T1 → ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃ⓐV.ⓛ{p}W.T1⦄.
-#h #p #G #L #X #H @(csx_ind … H) -X
+fact csx_appl_beta_aux (h) (G):
+ ∀p,L,U1. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃U1⦄ →
+ ∀V,W,T1. U1 = ⓓ{p}ⓝW.V.T1 → ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃ⓐV.ⓛ{p}W.T1⦄.
+#h #G #p #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 *
qed-.
(* Basic_1: was just: sn3_beta *)
-lemma csx_appl_beta: ∀h,p,G,L,V,W,T. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃ⓓ{p}ⓝW.V.T⦄ → ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃ⓐV.ⓛ{p}W.T⦄.
+lemma csx_appl_beta (h) (G):
+ ∀p,L,V,W,T. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃ⓓ{p}ⓝW.V.T⦄ → ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃ⓐV.ⓛ{p}W.T⦄.
/2 width=3 by csx_appl_beta_aux/ qed.
(* Advanced forward lemmas **************************************************)
-fact csx_fwd_bind_dx_unit_aux: ∀h,G,L,U. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃U⦄ →
- ∀p,I,J,V,T. U = ⓑ{p,I}V.T → ⦃G,L.ⓤ{J}⦄ ⊢ ⬈*[h] 𝐒⦃T⦄.
+fact csx_fwd_bind_dx_unit_aux (h) (G):
+ ∀L,U. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃U⦄ →
+ ∀p,I,J,V,T. U = ⓑ{p,I}V.T → ⦃G,L.ⓤ{J}⦄ ⊢ ⬈*[h] 𝐒⦃T⦄.
#h #G #L #U #H elim H -H #U0 #_ #IH #p #I #J #V #T #H destruct
@csx_intro #T2 #HLT2 #HT2
@(IH (ⓑ{p, I}V.T2)) -IH /2 width=4 by cpx_bind_unit/ -HLT2
#H elim (tdeq_inv_pair … H) -H /2 width=1 by/
qed-.
-lemma csx_fwd_bind_dx_unit: ∀h,p,I,G,L,V,T. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃ⓑ{p,I}V.T⦄ →
- ∀J. ⦃G,L.ⓤ{J}⦄ ⊢ ⬈*[h] 𝐒⦃T⦄.
+lemma csx_fwd_bind_dx_unit (h) (G):
+ ∀p,I,L,V,T. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃ⓑ{p,I}V.T⦄ →
+ ∀J. ⦃G,L.ⓤ{J}⦄ ⊢ ⬈*[h] 𝐒⦃T⦄.
/2 width=6 by csx_fwd_bind_dx_unit_aux/ qed-.
-lemma csx_fwd_bind_unit: ∀h,p,I,G,L,V,T. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃ⓑ{p,I}V.T⦄ →
- ∀J. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃V⦄ ∧ ⦃G,L.ⓤ{J}⦄ ⊢ ⬈*[h] 𝐒⦃T⦄.
+lemma csx_fwd_bind_unit (h) (G):
+ ∀p,I,L,V,T. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃ⓑ{p,I}V.T⦄ →
+ ∀J. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃V⦄ ∧ ⦃G,L.ⓤ{J}⦄ ⊢ ⬈*[h] 𝐒⦃T⦄.
/3 width=4 by csx_fwd_pair_sn, csx_fwd_bind_dx_unit, conj/ qed-.
+
+(* Properties with restricted refinement for local environments *************)
+
+lemma csx_lsubr_conf (h) (G):
+ ∀L1,T. ⦃G,L1⦄ ⊢ ⬈*[h] 𝐒⦃T⦄ → ∀L2. L1 ⫃ L2 → ⦃G,L2⦄ ⊢ ⬈*[h] 𝐒⦃T⦄.
+#h #G #L1 #T #H
+@(csx_ind … H) -T #T1 #_ #IH #L2 #HL12
+@csx_intro #T2 #HT12 #HnT12
+/3 width=3 by lsubr_cpx_trans/
+qed-.
(* *)
(**************************************************************************)
-include "basic_2/notation/relations/topredtysnstrong_5.ma".
+include "basic_2/notation/relations/topredtysnstrong_4.ma".
include "basic_2/rt_computation/rsx.ma".
(* COMPATIBILITY OF STRONG NORMALIZATION FOR UNBOUND RT-TRANSITION **********)
(* Note: this should be an instance of a more general sex *)
(* Basic_2A1: uses: lcosx *)
-inductive jsx (h) (G): rtmap → relation lenv ≝
-| jsx_atom: ∀f. jsx h G f (⋆) (⋆)
-| jsx_push: ∀f,I,K1,K2. jsx h G f K1 K2 →
- jsx h G (⫯f) (K1.ⓘ{I}) (K2.ⓘ{I})
-| jsx_unit: ∀f,I,K1,K2. jsx h G f K1 K2 →
- jsx h G (↑f) (K1.ⓤ{I}) (K2.ⓧ)
-| jsx_pair: ∀f,I,K1,K2,V. G ⊢ ⬈*[h,V] 𝐒⦃K2⦄ →
- jsx h G f K1 K2 → jsx h G (↑f) (K1.ⓑ{I}V) (K2.ⓧ)
+inductive jsx (h) (G): relation lenv ≝
+| jsx_atom: jsx h G (⋆) (⋆)
+| jsx_bind: ∀I,K1,K2. jsx h G K1 K2 →
+ jsx h G (K1.ⓘ{I}) (K2.ⓘ{I})
+| jsx_pair: ∀I,K1,K2,V. jsx h G K1 K2 →
+ G ⊢ ⬈*[h,V] 𝐒⦃K2⦄ → jsx h G (K1.ⓑ{I}V) (K2.ⓧ)
.
interpretation
"strong normalization for unbound parallel rt-transition (compatibility)"
- 'ToPRedTySNStrong h f G L1 L2 = (jsx h G f L1 L2).
+ 'ToPRedTySNStrong h G L1 L2 = (jsx h G L1 L2).
(* Basic inversion lemmas ***************************************************)
fact jsx_inv_atom_sn_aux (h) (G):
- ∀g,L1,L2. G ⊢ L1 ⊒[h,g] L2 → L1 = ⋆ → L2 = ⋆.
-#h #G #g #L1 #L2 * -g -L1 -L2 //
-[ #f #I #K1 #K2 #_ #H destruct
-| #f #I #K1 #K2 #_ #H destruct
-| #f #I #K1 #K2 #V #_ #_ #H destruct
+ ∀L1,L2. G ⊢ L1 ⊒[h] L2 → L1 = ⋆ → L2 = ⋆.
+#h #G #L1 #L2 * -L1 -L2
+[ //
+| #I #K1 #K2 #_ #H destruct
+| #I #K1 #K2 #V #_ #_ #H destruct
]
qed-.
-lemma jsx_inv_atom_sn (h) (G): ∀g,L2. G ⊢ ⋆ ⊒[h,g] L2 → L2 = ⋆.
-/2 width=7 by jsx_inv_atom_sn_aux/ qed-.
-
-fact jsx_inv_push_sn_aux (h) (G):
- ∀g,L1,L2. G ⊢ L1 ⊒[h,g] L2 →
- ∀f,I,K1. g = ⫯f → L1 = K1.ⓘ{I} →
- ∃∃K2. G ⊢ K1 ⊒[h,f] K2 & L2 = K2.ⓘ{I}.
-#h #G #g #L1 #L2 * -g -L1 -L2
-[ #f #g #J #L1 #_ #H destruct
-| #f #I #K1 #K2 #HK12 #g #J #L1 #H1 #H2 destruct
- <(injective_push … H1) -g /2 width=3 by ex2_intro/
-| #f #I #K1 #K2 #_ #g #J #L1 #H
- elim (discr_next_push … H)
-| #f #I #K1 #K2 #V #_ #_ #g #J #L1 #H
- elim (discr_next_push … H)
+lemma jsx_inv_atom_sn (h) (G): ∀L2. G ⊢ ⋆ ⊒[h] L2 → L2 = ⋆.
+/2 width=5 by jsx_inv_atom_sn_aux/ qed-.
+
+fact jsx_inv_bind_sn_aux (h) (G):
+ ∀L1,L2. G ⊢ L1 ⊒[h] L2 →
+ ∀I,K1. L1 = K1.ⓘ{I} →
+ ∨∨ ∃∃K2. G ⊢ K1 ⊒[h] K2 & L2 = K2.ⓘ{I}
+ | ∃∃J,K2,V. G ⊢ K1 ⊒[h] K2 & G ⊢ ⬈*[h,V] 𝐒⦃K2⦄ & I = BPair J V & L2 = K2.ⓧ.
+#h #G #L1 #L2 * -L1 -L2
+[ #J #L1 #H destruct
+| #I #K1 #K2 #HK12 #J #L1 #H destruct /3 width=3 by ex2_intro, or_introl/
+| #I #K1 #K2 #V #HK12 #HV #J #L1 #H destruct /3 width=7 by ex4_3_intro, or_intror/
]
qed-.
-lemma jsx_inv_push_sn (h) (G):
- ∀f,I,K1,L2. G ⊢ K1.ⓘ{I} ⊒[h,⫯f] L2 →
- ∃∃K2. G ⊢ K1 ⊒[h,f] K2 & L2 = K2.ⓘ{I}.
-/2 width=5 by jsx_inv_push_sn_aux/ qed-.
-
-fact jsx_inv_unit_sn_aux (h) (G):
- ∀g,L1,L2. G ⊢ L1 ⊒[h,g] L2 →
- ∀f,I,K1. g = ↑f → L1 = K1.ⓤ{I} →
- ∃∃K2. G ⊢ K1 ⊒[h,f] K2 & L2 = K2.ⓧ.
-#h #G #g #L1 #L2 * -g -L1 -L2
-[ #f #g #J #L1 #_ #H destruct
-| #f #I #K1 #K2 #_ #g #J #L1 #H
- elim (discr_push_next … H)
-| #f #I #K1 #K2 #HK12 #g #J #L1 #H1 #H2 destruct
- <(injective_next … H1) -g /2 width=3 by ex2_intro/
-| #f #I #K1 #K2 #V #_ #_ #g #J #L1 #_ #H destruct
-]
-qed-.
+lemma jsx_inv_bind_sn (h) (G):
+ ∀I,K1,L2. G ⊢ K1.ⓘ{I} ⊒[h] L2 →
+ ∨∨ ∃∃K2. G ⊢ K1 ⊒[h] K2 & L2 = K2.ⓘ{I}
+ | ∃∃J,K2,V. G ⊢ K1 ⊒[h] K2 & G ⊢ ⬈*[h,V] 𝐒⦃K2⦄ & I = BPair J V & L2 = K2.ⓧ.
+/2 width=3 by jsx_inv_bind_sn_aux/ qed-.
-lemma jsx_inv_unit_sn (h) (G):
- ∀f,I,K1,L2. G ⊢ K1.ⓤ{I} ⊒[h,↑f] L2 →
- ∃∃K2. G ⊢ K1 ⊒[h,f] K2 & L2 = K2.ⓧ.
-/2 width=6 by jsx_inv_unit_sn_aux/ qed-.
-
-fact jsx_inv_pair_sn_aux (h) (G):
- ∀g,L1,L2. G ⊢ L1 ⊒[h,g] L2 →
- ∀f,I,K1,V. g = ↑f → L1 = K1.ⓑ{I}V →
- ∃∃K2. G ⊢ ⬈*[h,V] 𝐒⦃K2⦄ & G ⊢ K1 ⊒[h,f] K2 & L2 = K2.ⓧ.
-#h #G #g #L1 #L2 * -g -L1 -L2
-[ #f #g #J #L1 #W #_ #H destruct
-| #f #I #K1 #K2 #_ #g #J #L1 #W #H
- elim (discr_push_next … H)
-| #f #I #K1 #K2 #_ #g #J #L1 #W #_ #H destruct
-| #f #I #K1 #K2 #V #HV #HK12 #g #J #L1 #W #H1 #H2 destruct
- <(injective_next … H1) -g /2 width=4 by ex3_intro/
-]
-qed-.
+(* Advanced inversion lemmas ************************************************)
(* Basic_2A1: uses: lcosx_inv_pair *)
lemma jsx_inv_pair_sn (h) (G):
- ∀f,I,K1,L2,V. G ⊢ K1.ⓑ{I}V ⊒[h,↑f] L2 →
- ∃∃K2. G ⊢ ⬈*[h,V] 𝐒⦃K2⦄ & G ⊢ K1 ⊒[h,f] K2 & L2 = K2.ⓧ.
-/2 width=6 by jsx_inv_pair_sn_aux/ qed-.
-
-(* Advanced inversion lemmas ************************************************)
-
-lemma jsx_inv_pair_sn_gen (h) (G): ∀g,I,K1,L2,V. G ⊢ K1.ⓑ{I}V ⊒[h,g] L2 →
- ∨∨ ∃∃f,K2. G ⊢ K1 ⊒[h,f] K2 & g = ⫯f & L2 = K2.ⓑ{I}V
- | ∃∃f,K2. G ⊢ ⬈*[h,V] 𝐒⦃K2⦄ & G ⊢ K1 ⊒[h,f] K2 & g = ↑f & L2 = K2.ⓧ.
-#h #G #g #I #K1 #L2 #V #H
-elim (pn_split g) * #f #Hf destruct
-[ elim (jsx_inv_push_sn … H) -H /3 width=5 by ex3_2_intro, or_introl/
-| elim (jsx_inv_pair_sn … H) -H /3 width=6 by ex4_2_intro, or_intror/
+ ∀I,K1,L2,V. G ⊢ K1.ⓑ{I}V ⊒[h] L2 →
+ ∨∨ ∃∃K2. G ⊢ K1 ⊒[h] K2 & L2 = K2.ⓑ{I}V
+ | ∃∃K2. G ⊢ K1 ⊒[h] K2 & G ⊢ ⬈*[h,V] 𝐒⦃K2⦄ & L2 = K2.ⓧ.
+#h #G #I #K1 #L2 #V #H elim (jsx_inv_bind_sn … H) -H *
+[ /3 width=3 by ex2_intro, or_introl/
+| #J #K2 #X #HK12 #HX #H1 #H2 destruct /3 width=4 by ex3_intro, or_intror/
]
qed-.
+lemma jsx_inv_void_sn (h) (G):
+ ∀K1,L2. G ⊢ K1.ⓧ ⊒[h] L2 →
+ ∃∃K2. G ⊢ K1 ⊒[h] K2 & L2 = K2.ⓧ.
+#h #G #K1 #L2 #H elim (jsx_inv_bind_sn … H) -H *
+/2 width=3 by ex2_intro/
+qed-.
+
(* Advanced forward lemmas **************************************************)
lemma jsx_fwd_bind_sn (h) (G):
- ∀g,I1,K1,L2. G ⊢ K1.ⓘ{I1} ⊒[h,g] L2 →
- ∃∃I2,K2. G ⊢ K1 ⊒[h,⫱g] K2 & L2 = K2.ⓘ{I2}.
-#h #G #g #I1 #K1 #L2
-elim (pn_split g) * #f #Hf destruct
-[ #H elim (jsx_inv_push_sn … H) -H
-| cases I1 -I1 #I1
- [ #H elim (jsx_inv_unit_sn … H) -H
- | #V #H elim (jsx_inv_pair_sn … H) -H
- ]
-]
+ ∀I1,K1,L2. G ⊢ K1.ⓘ{I1} ⊒[h] L2 →
+ ∃∃I2,K2. G ⊢ K1 ⊒[h] K2 & L2 = K2.ⓘ{I2}.
+#h #G #I1 #K1 #L2 #H elim (jsx_inv_bind_sn … H) -H *
/2 width=4 by ex2_2_intro/
qed-.
-(* Basic properties *********************************************************)
-
-lemma jsx_eq_repl_back (h) (G): ∀L1,L2. eq_repl_back … (λf. G ⊢ L1 ⊒[h,f] L2).
-#h #G #L1 #L2 #f1 #H elim H -L1 -L2 -f1 //
-[ #f #I #L1 #L2 #_ #IH #x #H
- elim (eq_inv_px … H) -H /3 width=3 by jsx_push/
-| #f #I #L1 #L2 #_ #IH #x #H
- elim (eq_inv_nx … H) -H /3 width=3 by jsx_unit/
-| #f #I #L1 #L2 #V #HV #_ #IH #x #H
- elim (eq_inv_nx … H) -H /3 width=3 by jsx_pair/
-]
-qed-.
-
-lemma jsx_eq_repl_fwd (h) (G): ∀L1,L2. eq_repl_fwd … (λf. G ⊢ L1 ⊒[h,f] L2).
-#h #G #L1 #L2 @eq_repl_sym /2 width=3 by jsx_eq_repl_back/
-qed-.
-
(* Advanced properties ******************************************************)
(* Basic_2A1: uses: lcosx_O *)
-lemma jsx_refl (h) (G): ∀f. 𝐈⦃f⦄ → reflexive … (jsx h G f).
-#h #G #f #Hf #L elim L -L
-/3 width=3 by jsx_eq_repl_back, jsx_push, eq_push_inv_isid/
+lemma jsx_refl (h) (G): reflexive … (jsx h G).
+#h #G #L elim L -L /2 width=1 by jsx_atom, jsx_bind/
qed.
(* Basic_2A1: removed theorems 2:
--- /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/rsx_csx.ma".
+include "basic_2/rt_computation/jsx_drops.ma".
+include "basic_2/rt_computation/jsx_lsubr.ma".
+
+(* COMPATIBILITY OF STRONG NORMALIZATION FOR UNBOUND RT-TRANSITION **********)
+
+(* Properties with strongly rt-normalizing terms ****************************)
+
+lemma jsx_csx_conf (h) (G):
+ ∀L1,L2. G ⊢ L1 ⊒[h] L2 →
+ ∀T. ⦃G,L1⦄ ⊢ ⬈*[h] 𝐒⦃T⦄ → ⦃G,L2⦄ ⊢ ⬈*[h] 𝐒⦃T⦄.
+/3 width=5 by jsx_fwd_lsubr, csx_lsubr_conf/ qed-.
+
+(* Properties with strongly rt-normalizing referred local environments ******)
+
+(* Note: Try by induction on the 2nd premise by generalizing V with f *)
+lemma rsx_jsx_trans (h) (G):
+ ∀L1,V. G ⊢ ⬈*[h,V] 𝐒⦃L1⦄ →
+ ∀L2. G ⊢ L1 ⊒[h] L2 → G ⊢ ⬈*[h,V] 𝐒⦃L2⦄.
+#h #G #L1 #V @(fqup_wf_ind_eq (Ⓕ) … G L1 V) -G -L1 -V
+#G0 #L0 #V0 #IH #G #L1 * *
+[ //
+| #i #HG #HL #HV #H #L2 #HL12 destruct
+ elim (rsx_inv_lref_drops … H) -H [|*: * ]
+ [ #HL1 -IH
+ lapply (jsx_fwd_drops_atom_sn … HL12 … HL1) -L1
+ /2 width=1 by rsx_lref_atom_drops/
+ | #I #K1 #HLK1 -IH
+ elim (jsx_fwd_drops_unit_sn … HL12 … HLK1) -L1 [| // ] #K2 #HK12 #HLK2
+ /2 width=3 by rsx_lref_unit_drops/
+ | #I #K1 #V1 #HLK1 #HV1 #HK1
+ elim (jsx_fwd_drops_pair_sn … HL12 … HLK1) -HL12 [3: // |*: * ]
+ [ #K2 #HK12 #HLK2
+ /4 width=6 by rsx_lref_pair_drops, jsx_csx_conf, fqup_lref/
+ | #K2 #_ #HLK2 #_
+ /2 width=3 by rsx_lref_unit_drops/
+ ]
+ ]
+| //
+| #p #I #V #T #HG #HL #HV #H #L2 #HL12 destruct
+ elim (rsx_inv_bind_void … H) -H #HV #HT
+ /4 width=4 by jsx_bind, rsx_bind_void/
+| #I #V #T #HG #HL #HV #H #L2 #HL12 destruct
+ elim (rsx_inv_flat … H) -H #HV #HT
+ /3 width=4 by rsx_flat/
+]
+qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "static_2/relocation/drops.ma".
+include "basic_2/rt_computation/jsx.ma".
+
+(* COMPATIBILITY OF STRONG NORMALIZATION FOR UNBOUND RT-TRANSITION **********)
+
+(* Forward lemmas with uniform slicing for local environments ***************)
+
+lemma jsx_fwd_drops_atom_sn (h) (b) (G):
+ ∀L1,L2. G ⊢ L1 ⊒[h] L2 →
+ ∀f. 𝐔⦃f⦄ → ⬇*[b,f]L1 ≘ ⋆ → ⬇*[b,f]L2 ≘ ⋆.
+#h #b #G #L1 #L2 #H elim H -L1 -L2
+[ #f #_ #H //
+| #I #K1 #K2 #_ #IH #f #Hf #H
+| #I #K1 #K2 #V #_ #HV #IH #f #Hf #H
+]
+elim (drops_inv_bind1_isuni … H) -H [3,6: // |*: * -Hf ]
+[1,3: #_ #H destruct
+|2,4: #g #Hg #HK1 #H destruct /3 width=1 by drops_drop/
+]
+qed-.
+
+lemma jsx_fwd_drops_unit_sn (h) (b) (G):
+ ∀L1,L2. G ⊢ L1 ⊒[h] L2 →
+ ∀f. 𝐔⦃f⦄ → ∀I,K1. ⬇*[b,f]L1 ≘ K1.ⓤ{I} →
+ ∃∃K2. G ⊢ K1 ⊒[h] K2 & ⬇*[b,f]L2 ≘ K2.ⓤ{I}.
+#h #b #G #L1 #L2 #H elim H -L1 -L2
+[ #f #_ #J #Y1 #H
+ lapply (drops_inv_atom1 … H) -H * #H #_ destruct
+| #I #K1 #K2 #HK12 #IH #f #Hf #J #Y1 #H
+| #I #K1 #K2 #V #HK12 #HV #IH #f #Hf #J #Y1 #H
+]
+elim (drops_inv_bind1_isuni … H) -H [3,6: // |*: * -Hf ]
+[1,3: #Hf #H destruct -IH /3 width=3 by drops_refl, ex2_intro/
+|2,4:
+ #g #Hg #HK1 #H destruct
+ elim (IH … Hg … HK1) -K1 -Hg #Y2 #HY12 #HKY2
+ /3 width=3 by drops_drop, ex2_intro/
+]
+qed-.
+
+lemma jsx_fwd_drops_pair_sn (h) (b) (G):
+ ∀L1,L2. G ⊢ L1 ⊒[h] L2 →
+ ∀f. 𝐔⦃f⦄ → ∀I,K1,V. ⬇*[b,f]L1 ≘ K1.ⓑ{I}V →
+ ∨∨ ∃∃K2. G ⊢ K1 ⊒[h] K2 & ⬇*[b,f]L2 ≘ K2.ⓑ{I}V
+ | ∃∃K2. G ⊢ K1 ⊒[h] K2 & ⬇*[b,f]L2 ≘ K2.ⓧ & G ⊢ ⬈*[h,V] 𝐒⦃K2⦄.
+#h #b #G #L1 #L2 #H elim H -L1 -L2
+[ #f #_ #J #Y1 #X1 #H
+ lapply (drops_inv_atom1 … H) -H * #H #_ destruct
+| #I #K1 #K2 #HK12 #IH #f #Hf #J #Y1 #X1 #H
+| #I #K1 #K2 #V #HK12 #HV #IH #f #Hf #J #Y1 #X1 #H
+]
+elim (drops_inv_bind1_isuni … H) -H [3,6: // |*: * -Hf ]
+[1,3:
+ #Hf #H destruct -IH
+ /4 width=4 by drops_refl, ex3_intro, ex2_intro, or_introl, or_intror/
+|2,4:
+ #g #Hg #HK1 #H destruct
+ elim (IH … Hg … HK1) -K1 -Hg * #Y2 #HY12 #HKY2 [2,4: #HX1 ]
+ /4 width=4 by drops_drop, ex3_intro, ex2_intro, or_introl, or_intror/
+]
+qed-.
(* *)
(**************************************************************************)
-include "basic_2/rt_computation/jsx.ma".
+include "basic_2/rt_computation/jsx_csx.ma".
(* COMPATIBILITY OF STRONG NORMALIZATION FOR UNBOUND RT-TRANSITION **********)
(* Main properties **********************************************************)
-theorem jsx_fix (h) (G):
- ∀f,L1,L. G ⊢ L1 ⊒[h,f] L → ∀L2. G ⊢ L ⊒[h,f] L2 → L = L2.
-#h #G #f #L1 #L #H elim H -f -L1 -L
-[ #f #L2 #H
+theorem jsx_trans (h) (G): Transitive … (jsx h G).
+#h #G #L1 #L #H elim H -L1 -L
+[ #L2 #H
>(jsx_inv_atom_sn … H) -L2 //
-| #f #I #K1 #K2 #_ #IH #L2 #H
- elim (jsx_inv_push_sn … H) -H /3 width=1 by eq_f2/
-| #f #I #K1 #K2 #_ #IH #L2 #H
- elim (jsx_inv_unit_sn … H) -H /3 width=1 by eq_f2/
-| #f #I #K1 #K2 #V #_ #_ #IH #L2 #H
- elim (jsx_inv_unit_sn … H) -H /3 width=1 by eq_f2/
+| #I #K1 #K #_ #IH #L2 #H
+ elim (jsx_inv_bind_sn … H) -H *
+ [ #K2 #HK2 #H destruct /3 width=1 by jsx_bind/
+ | #J #K2 #V #HK2 #HV #H1 #H2 destruct /3 width=1 by jsx_pair/
+ ]
+| #I #K1 #K #V #_ #HV #IH #L2 #H
+ elim (jsx_inv_void_sn … H) -H #K2 #HK2 #H destruct
+ /3 width=3 by rsx_jsx_trans, jsx_pair/
]
qed-.
-
-theorem jsx_trans (h) (G): ∀f. Transitive … (jsx h G f).
-#h #G #f #L1 #L #H1 #L2 #H2
-<(jsx_fix … H1 … H2) -L2 //
-qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "static_2/static/lsubr.ma".
+include "basic_2/rt_computation/jsx.ma".
+
+(* COMPATIBILITY OF STRONG NORMALIZATION FOR UNBOUND RT-TRANSITION **********)
+
+(* Forward lemmas with restricted refinement for local environments *********)
+
+lemma jsx_fwd_lsubr (h) (G): ∀L1,L2. G ⊢ L1 ⊒[h] L2 → L1 ⫃ L2.
+#h #G #L1 #L2 #H elim H -L1 -L2
+/2 width=1 by lsubr_bind, lsubr_unit/
+qed-.
(* Basic_2A1: uses: lsx_cpx_trans_lcosx *)
lemma rsx_cpx_trans_jsx (h) (G):
∀L0,T1,T2. ⦃G,L0⦄ ⊢ T1 ⬈[h] T2 →
- ∀f,L. G ⊢ L0 ⊒[h,f] L →
- G ⊢ ⬈*[h,T1] 𝐒⦃L⦄ → G ⊢ ⬈*[h,T2] 𝐒⦃L⦄.
+ ∀L. G ⊢ L0 ⊒[h] L → G ⊢ ⬈*[h,T1] 𝐒⦃L⦄ → G ⊢ ⬈*[h,T2] 𝐒⦃L⦄.
#h #G #L0 #T1 #T2 #H @(cpx_ind … H) -G -L0 -T1 -T2
[ //
| //
-| #I0 #G #K0 #V1 #V2 #W2 #_ #IH #HVW2 #g #L #HK0 #HL
- elim (jsx_inv_pair_sn_gen … HK0) -HK0 *
- [ #f #K #HK0 #H1 #H2 destruct
+| #I0 #G #K0 #V1 #V2 #W2 #_ #IH #HVW2 #L #HK0 #HL
+ elim (jsx_inv_pair_sn … HK0) -HK0 *
+ [ #K #HK0 #H destruct
/4 width=8 by rsx_lifts, rsx_fwd_pair, drops_refl, drops_drop/
- | #f #K #HV1 #HK0 #H1 #H2 destruct
+ | #K #HK0 #HV1 #H destruct
/4 width=8 by rsx_lifts, drops_refl, drops_drop/
]
-| #I0 #G #K0 #T #U #i #_ #IH #HTU #g #L #HK0 #HL
+| #I0 #G #K0 #T #U #i #_ #IH #HTU #L #HK0 #HL
elim (jsx_fwd_bind_sn … HK0) -HK0 #I #K #HK0 #H destruct
/6 width=8 by rsx_inv_lifts, rsx_lifts, drops_refl, drops_drop/
-| #p #I0 #G #L0 #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #f #L #HL0 #HL
+| #p #I0 #G #L0 #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L #HL0 #HL
elim (rsx_inv_bind_void … HL) -HL
/4 width=2 by jsx_pair, rsx_bind_void/
-| #I0 #G #L0 #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #f #L #HL0 #HL
+| #I0 #G #L0 #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L #HL0 #HL
elim (rsx_inv_flat … HL) -HL /3 width=2 by rsx_flat/
-| #G #L0 #V #U1 #T1 #T2 #HTU1 #_ #IHT12 #f #L #HL0 #HL
+| #G #L0 #V #U1 #T1 #T2 #HTU1 #_ #IHT12 #L #HL0 #HL
elim (rsx_inv_bind_void … HL) -HL #HV #HU1
/5 width=8 by rsx_inv_lifts, drops_refl, drops_drop/
-| #G #L0 #V #T1 #T2 #_ #IHT12 #f #L #HL0 #HL
+| #G #L0 #V #T1 #T2 #_ #IHT12 #L #HL0 #HL
elim (rsx_inv_flat … HL) -HL /2 width=2 by/
-| #G #L0 #V1 #V2 #T #_ #IHV12 #f #L #HL0 #HL
+| #G #L0 #V1 #V2 #T #_ #IHV12 #L #HL0 #HL
elim (rsx_inv_flat … HL) -HL /2 width=2 by/
-| #p #G #L0 #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV12 #IHW12 #IHT12 #f #L #HL0 #HL
+| #p #G #L0 #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV12 #IHW12 #IHT12 #L #HL0 #HL
elim (rsx_inv_flat … HL) -HL #HV1 #HL
elim (rsx_inv_bind_void … HL) -HL #HW1 #HT1
/4 width=2 by jsx_pair, rsx_bind_void, rsx_flat/
-| #p #G #L0 #V1 #V2 #U2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV12 #IHW12 #IHT12 #HVU2 #f #L #HL0 #HL
+| #p #G #L0 #V1 #V2 #U2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV12 #IHW12 #IHT12 #HVU2 #L #HL0 #HL
elim (rsx_inv_flat … HL) -HL #HV1 #HL
elim (rsx_inv_bind_void … HL) -HL #HW1 #HT1
/6 width=8 by jsx_pair, rsx_lifts, rsx_bind_void, rsx_flat, drops_refl, drops_drop/
(* STRONGLY NORMALIZING REFERRED LOCAL ENV.S FOR UNBOUND RT-TRANSITION ******)
-(* Advanced properties ******************************************************)
+(* Forward lemmas with strongly rt-normalizing terms ************************)
+
+fact rsx_fwd_lref_pair_csx_aux (h) (G):
+ ∀L. G ⊢ ⬈*[h,#0] 𝐒⦃L⦄ →
+ ∀I,K,V. L = K.ⓑ{I}V → ⦃G,K⦄ ⊢ ⬈*[h] 𝐒⦃V⦄.
+#h #G #L #H
+@(rsx_ind … H) -L #L #_ #IH #I #K #V1 #H destruct
+@csx_intro #V2 #HV12 #HnV12
+@(IH … I) -IH [1,4: // | -HnV12 | -G #H ]
+[ /2 width=1 by lpx_pair/
+| elim (rdeq_inv_zero_pair_sn … H) -H #Y #X #_ #H1 #H2 destruct -I
+ /2 width=1 by/
+]
+qed-.
+
+lemma rsx_fwd_lref_pair_csx (h) (G):
+ ∀I,K,V. G ⊢ ⬈*[h,#0] 𝐒⦃K.ⓑ{I}V⦄ → ⦃G,K⦄ ⊢ ⬈*[h] 𝐒⦃V⦄.
+/2 width=4 by rsx_fwd_lref_pair_csx_aux/ qed-.
+
+lemma rsx_fwd_lref_pair_csx_drops (h) (G):
+ ∀I,K,V,i,L. ⬇*[i] L ≘ K.ⓑ{I}V → G ⊢ ⬈*[h,#i] 𝐒⦃L⦄ → ⦃G,K⦄ ⊢ ⬈*[h] 𝐒⦃V⦄.
+#h #G #I #K #V #i elim i -i
+[ #L #H >(drops_fwd_isid … H) -H
+ /2 width=2 by rsx_fwd_lref_pair_csx/
+| #i #IH #L #H1 #H2
+ elim (drops_inv_bind2_isuni_next … H1) -H1 // #J #Y #HY #H destruct
+ lapply (rsx_inv_lifts … H2 … (𝐔❴1❵) ?????) -H2
+ /3 width=6 by drops_refl, drops_drop/
+]
+qed-.
+
+(* Inversion lemmas with strongly rt-normalizing terms **********************)
+
+lemma rsx_inv_lref_pair (h) (G):
+ ∀I,K,V. G ⊢ ⬈*[h,#0] 𝐒⦃K.ⓑ{I}V⦄ →
+ ∧∧ ⦃G,K⦄ ⊢ ⬈*[h] 𝐒⦃V⦄ & G ⊢ ⬈*[h,V] 𝐒⦃K⦄.
+/3 width=2 by rsx_fwd_lref_pair_csx, rsx_fwd_pair, conj/ qed-.
+
+lemma rsx_inv_lref_pair_drops (h) (G):
+ ∀I,K,V,i,L. ⬇*[i] L ≘ K.ⓑ{I}V → G ⊢ ⬈*[h,#i] 𝐒⦃L⦄ →
+ ∧∧ ⦃G,K⦄ ⊢ ⬈*[h] 𝐒⦃V⦄ & G ⊢ ⬈*[h,V] 𝐒⦃K⦄.
+/3 width=5 by rsx_fwd_lref_pair_csx_drops, rsx_fwd_lref_pair_drops, conj/ qed-.
+
+lemma rsx_inv_lref_drops (h) (G):
+ ∀L,i. G ⊢ ⬈*[h,#i] 𝐒⦃L⦄ →
+ ∨∨ ⬇*[Ⓕ,𝐔❴i❵] L ≘ ⋆
+ | ∃∃I,K. ⬇*[i] L ≘ K.ⓤ{I}
+ | ∃∃I,K,V. ⬇*[i] L ≘ K.ⓑ{I}V & ⦃G,K⦄ ⊢ ⬈*[h] 𝐒⦃V⦄ & G ⊢ ⬈*[h,V] 𝐒⦃K⦄.
+#h #G #L #i #H elim (drops_F_uni L i)
+[ /2 width=1 by or3_intro0/
+| * * /4 width=10 by rsx_fwd_lref_pair_csx_drops, rsx_fwd_lref_pair_drops, ex3_3_intro, ex1_2_intro, or3_intro2, or3_intro1/
+]
+qed-.
+
+(* Properties with strongly rt-normalizing terms ****************************)
(* Note: swapping the eliminations to avoid rsx_cpx_trans: no solution found *)
(* Basic_2A1: uses: lsx_lref_be_lpxs *)
-lemma rsx_pair_lpxs (h) (G):
+lemma rsx_lref_pair_lpxs (h) (G):
∀K1,V. ⦃G,K1⦄ ⊢ ⬈*[h] 𝐒⦃V⦄ →
∀K2. G ⊢ ⬈*[h,V] 𝐒⦃K2⦄ → ⦃G,K1⦄ ⊢ ⬈*[h] K2 →
∀I. G ⊢ ⬈*[h,#0] 𝐒⦃K2.ⓑ{I}V⦄.
]
qed.
+lemma rsx_lref_pair (h) (G):
+ ∀K,V. ⦃G,K⦄ ⊢ ⬈*[h] 𝐒⦃V⦄ → G ⊢ ⬈*[h,V] 𝐒⦃K⦄ → ∀I. G ⊢ ⬈*[h,#0] 𝐒⦃K.ⓑ{I}V⦄.
+/2 width=3 by rsx_lref_pair_lpxs/ qed.
+
(* Basic_2A1: uses: lsx_lref_be *)
lemma rsx_lref_pair_drops (h) (G):
∀K,V. ⦃G,K⦄ ⊢ ⬈*[h] 𝐒⦃V⦄ → G ⊢ ⬈*[h,V] 𝐒⦃K⦄ →
∀I,i,L. ⬇*[i] L ≘ K.ⓑ{I}V → G ⊢ ⬈*[h,#i] 𝐒⦃L⦄.
#h #G #K #V #HV #HK #I #i elim i -i
-[ #L #H >(drops_fwd_isid … H) -H /2 width=3 by rsx_pair_lpxs/
+[ #L #H >(drops_fwd_isid … H) -H /2 width=1 by rsx_lref_pair/
| #i #IH #L #H
elim (drops_inv_bind2_isuni_next … H) -H // #J #Y #HY #H destruct
@(rsx_lifts … (𝐔❴1❵)) /3 width=6 by drops_refl, drops_drop/ (**) (* full auto fails *)
]
qed.
-(* Main properties **********************************************************)
+(* Main properties with strongly rt-normalizing terms ***********************)
(* Basic_2A1: uses: csx_lsx *)
-theorem csx_rsx (h): ∀G,L,T. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃T⦄ → G ⊢ ⬈*[h,T] 𝐒⦃L⦄.
-#h #G #L #T @(fqup_wf_ind_eq (Ⓕ) … G L T) -G -L -T
-#Z #Y #X #IH #G #L * * //
-[ #i #HG #HL #HT #H destruct
- elim (csx_inv_lref … H) -H [ |*: * ]
- [ /2 width=1 by rsx_lref_atom/
- | /2 width=3 by rsx_lref_unit/
+theorem csx_rsx (h) (G): ∀L,T. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃T⦄ → G ⊢ ⬈*[h,T] 𝐒⦃L⦄.
+#h #G #L #T @(fqup_wf_ind_eq (Ⓣ) … G L T) -G -L -T
+#Z #Y #X #IH #G #L * *
+[ //
+| #i #HG #HL #HT #H destruct
+ elim (csx_inv_lref_drops … H) -H [ |*: * ]
+ [ /2 width=1 by rsx_lref_atom_drops/
+ | /2 width=3 by rsx_lref_unit_drops/
| /4 width=6 by rsx_lref_pair_drops, fqup_lref/
]
+| //
| #p #I #V #T #HG #HL #HT #H destruct
- elim (csx_fwd_bind_unit … H Void) -H /3 width=1 by rsx_bind_void/
+ elim (csx_fwd_bind … H) -H /3 width=1 by rsx_bind/
| #I #V #T #HG #HL #HT #H destruct
elim (csx_fwd_flat … H) -H /3 width=1 by rsx_flat/
]
(* Advanced properties ******************************************************)
(* Basic_2A1: uses: lsx_lref_free *)
-lemma rsx_lref_atom (h) (G): ∀L,i. ⬇*[Ⓕ,𝐔❴i❵] L ≘ ⋆ → G ⊢ ⬈*[h,#i] 𝐒⦃L⦄.
+lemma rsx_lref_atom_drops (h) (G): ∀L,i. ⬇*[Ⓕ,𝐔❴i❵] L ≘ ⋆ → G ⊢ ⬈*[h,#i] 𝐒⦃L⦄.
#h #G #L1 #i #HL1
@(rsx_lifts … (#0) … HL1) -HL1 //
qed.
(* Basic_2A1: uses: lsx_lref_skip *)
-lemma rsx_lref_unit (h) (G): ∀I,L,K,i. ⬇*[i] L ≘ K.ⓤ{I} → G ⊢ ⬈*[h,#i] 𝐒⦃L⦄.
+lemma rsx_lref_unit_drops (h) (G): ∀I,L,K,i. ⬇*[i] L ≘ K.ⓤ{I} → G ⊢ ⬈*[h,#i] 𝐒⦃L⦄.
#h #G #I #L1 #K1 #i #HL1
@(rsx_lifts … (#0) … HL1) -HL1 //
qed.
(* Advanced forward lemmas **************************************************)
(* Basic_2A1: uses: lsx_fwd_lref_be *)
-lemma rsx_fwd_lref_pair (h) (G):
+lemma rsx_fwd_lref_pair_drops (h) (G):
∀L,i. G ⊢ ⬈*[h,#i] 𝐒⦃L⦄ →
∀I,K,V. ⬇*[i] L ≘ K.ⓑ{I}V → G ⊢ ⬈*[h,V] 𝐒⦃K⦄.
#h #G #L #i #HL #I #K #V #HLK
}
]
[ { "unbound context-sensitive parallel rt-computation" * } {
- [ [ "compatibility for lenvs on selected entries" ] "jsx" + "( ? ⊢ ? ⊒[?,?] ? )" "jsx_rsx" + "jsx_jsx" * ]
+ [ [ "compatibility for lenvs" ] "jsx" + "( ? ⊢ ? ⊒[?] ? )" "jsx_drops" + "jsx_lsubr" + "jsx_csx" + "jsx_rsx" + "jsx_jsx" * ]
[ [ "strongly normalizing for lenvs on referred entries" ] "rsx" + "( ? ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" "rsx_length" + "rsx_drops" + "rsx_fqup" + "rsx_cpxs" + "rsx_csx" + "rsx_rsx" * ]
[ [ "strongly normalizing for term vectors" ] "csx_vector" + "( ⦃?,?⦄ ⊢ ⬈*[?] 𝐒⦃?⦄ )" "csx_cnx_vector" + "csx_csx_vector" * ]
[ [ "strongly normalizing for terms" ] "csx" + "( ⦃?,?⦄ ⊢ ⬈*[?] 𝐒⦃?⦄ )" "csx_simple" + "csx_simple_theq" + "csx_drops" + "csx_fqus" + "csx_lsubr" + "csx_rdeq" + "csx_fdeq" + "csx_aaa" + "csx_gcp" + "csx_gcr" + "csx_lpx" + "csx_cnx" + "csx_fpbq" + "csx_cpxs" + "csx_lpxs" + "csx_csx" * ]
lemma lsubr_inv_atom1: ∀L2. ⋆ ⫃ L2 → L2 = ⋆.
/2 width=3 by lsubr_inv_atom1_aux/ qed-.
-fact lsubr_inv_bind1_aux: ∀L1,L2. L1 ⫃ L2 → ∀I,K1. L1 = K1.ⓘ{I} →
- ∨∨ ∃∃K2. K1 ⫃ K2 & L2 = K2.ⓘ{I}
- | ∃∃K2,V,W. K1 ⫃ K2 & L2 = K2.ⓛW &
- I = BPair Abbr (ⓝW.V)
- | ∃∃J1,J2,K2,V. K1 ⫃ K2 & L2 = K2.ⓤ{J2} &
- I = BPair J1 V.
+fact lsubr_inv_bind1_aux:
+ ∀L1,L2. L1 ⫃ L2 → ∀I,K1. L1 = K1.ⓘ{I} →
+ ∨∨ ∃∃K2. K1 ⫃ K2 & L2 = K2.ⓘ{I}
+ | ∃∃K2,V,W. K1 ⫃ K2 & L2 = K2.ⓛW & I = BPair Abbr (ⓝW.V)
+ | ∃∃J1,J2,K2,V. K1 ⫃ K2 & L2 = K2.ⓤ{J2} & I = BPair J1 V.
#L1 #L2 * -L1 -L2
[ #J #K1 #H destruct
| #I #L1 #L2 #HL12 #J #K1 #H destruct /3 width=3 by or3_intro0, ex2_intro/
qed-.
(* Basic_2A1: uses: lsubr_inv_pair1 *)
-lemma lsubr_inv_bind1: ∀I,K1,L2. K1.ⓘ{I} ⫃ L2 →
- ∨∨ ∃∃K2. K1 ⫃ K2 & L2 = K2.ⓘ{I}
- | ∃∃K2,V,W. K1 ⫃ K2 & L2 = K2.ⓛW &
- I = BPair Abbr (ⓝW.V)
- | ∃∃J1,J2,K2,V. K1 ⫃ K2 & L2 = K2.ⓤ{J2} &
- I = BPair J1 V.
+lemma lsubr_inv_bind1:
+ ∀I,K1,L2. K1.ⓘ{I} ⫃ L2 →
+ ∨∨ ∃∃K2. K1 ⫃ K2 & L2 = K2.ⓘ{I}
+ | ∃∃K2,V,W. K1 ⫃ K2 & L2 = K2.ⓛW & I = BPair Abbr (ⓝW.V)
+ | ∃∃J1,J2,K2,V. K1 ⫃ K2 & L2 = K2.ⓤ{J2} & I = BPair J1 V.
/2 width=3 by lsubr_inv_bind1_aux/ qed-.
fact lsubr_inv_atom2_aux: ∀L1,L2. L1 ⫃ L2 → L2 = ⋆ → L1 = ⋆.
lemma lsubr_inv_atom2: ∀L1. L1 ⫃ ⋆ → L1 = ⋆.
/2 width=3 by lsubr_inv_atom2_aux/ qed-.
-fact lsubr_inv_bind2_aux: ∀L1,L2. L1 ⫃ L2 → ∀I,K2. L2 = K2.ⓘ{I} →
- ∨∨ ∃∃K1. K1 ⫃ K2 & L1 = K1.ⓘ{I}
- | ∃∃K1,W,V. K1 ⫃ K2 & L1 = K1.ⓓⓝW.V & I = BPair Abst W
- | ∃∃J1,J2,K1,V. K1 ⫃ K2 & L1 = K1.ⓑ{J1}V & I = BUnit J2.
+fact lsubr_inv_bind2_aux:
+ ∀L1,L2. L1 ⫃ L2 → ∀I,K2. L2 = K2.ⓘ{I} →
+ ∨∨ ∃∃K1. K1 ⫃ K2 & L1 = K1.ⓘ{I}
+ | ∃∃K1,W,V. K1 ⫃ K2 & L1 = K1.ⓓⓝW.V & I = BPair Abst W
+ | ∃∃J1,J2,K1,V. K1 ⫃ K2 & L1 = K1.ⓑ{J1}V & I = BUnit J2.
#L1 #L2 * -L1 -L2
[ #J #K2 #H destruct
| #I #L1 #L2 #HL12 #J #K2 #H destruct /3 width=3 by ex2_intro, or3_intro0/
]
qed-.
-lemma lsubr_inv_bind2: ∀I,L1,K2. L1 ⫃ K2.ⓘ{I} →
- ∨∨ ∃∃K1. K1 ⫃ K2 & L1 = K1.ⓘ{I}
- | ∃∃K1,W,V. K1 ⫃ K2 & L1 = K1.ⓓⓝW.V & I = BPair Abst W
- | ∃∃J1,J2,K1,V. K1 ⫃ K2 & L1 = K1.ⓑ{J1}V & I = BUnit J2.
+lemma lsubr_inv_bind2:
+ ∀I,L1,K2. L1 ⫃ K2.ⓘ{I} →
+ ∨∨ ∃∃K1. K1 ⫃ K2 & L1 = K1.ⓘ{I}
+ | ∃∃K1,W,V. K1 ⫃ K2 & L1 = K1.ⓓⓝW.V & I = BPair Abst W
+ | ∃∃J1,J2,K1,V. K1 ⫃ K2 & L1 = K1.ⓑ{J1}V & I = BUnit J2.
/2 width=3 by lsubr_inv_bind2_aux/ qed-.
(* Advanced inversion lemmas ************************************************)
-lemma lsubr_inv_abst1: ∀K1,L2,W. K1.ⓛW ⫃ L2 →
- ∨∨ ∃∃K2. K1 ⫃ K2 & L2 = K2.ⓛW
- | ∃∃I2,K2. K1 ⫃ K2 & L2 = K2.ⓤ{I2}.
+lemma lsubr_inv_abst1:
+ ∀K1,L2,W. K1.ⓛW ⫃ L2 →
+ ∨∨ ∃∃K2. K1 ⫃ K2 & L2 = K2.ⓛW
+ | ∃∃I2,K2. K1 ⫃ K2 & L2 = K2.ⓤ{I2}.
#K1 #L2 #W #H elim (lsubr_inv_bind1 … H) -H *
/3 width=4 by ex2_2_intro, ex2_intro, or_introl, or_intror/
#K2 #V2 #W2 #_ #_ #H destruct
qed-.
-lemma lsubr_inv_unit1: ∀I,K1,L2. K1.ⓤ{I} ⫃ L2 →
- ∃∃K2. K1 ⫃ K2 & L2 = K2.ⓤ{I}.
+lemma lsubr_inv_unit1:
+ ∀I,K1,L2. K1.ⓤ{I} ⫃ L2 →
+ ∃∃K2. K1 ⫃ K2 & L2 = K2.ⓤ{I}.
#I #K1 #L2 #H elim (lsubr_inv_bind1 … H) -H *
[ #K2 #HK12 #H destruct /2 width=3 by ex2_intro/
| #K2 #V #W #_ #_ #H destruct
-| #I1 #I2 #K2 #V #_ #_ #H destruct
+| #J1 #J2 #K2 #V #_ #_ #H destruct
]
qed-.
-lemma lsubr_inv_pair2: ∀I,L1,K2,W. L1 ⫃ K2.ⓑ{I}W →
- ∨∨ ∃∃K1. K1 ⫃ K2 & L1 = K1.ⓑ{I}W
- | ∃∃K1,V. K1 ⫃ K2 & L1 = K1.ⓓⓝW.V & I = Abst.
+lemma lsubr_inv_pair2:
+ ∀I,L1,K2,W. L1 ⫃ K2.ⓑ{I}W →
+ ∨∨ ∃∃K1. K1 ⫃ K2 & L1 = K1.ⓑ{I}W
+ | ∃∃K1,V. K1 ⫃ K2 & L1 = K1.ⓓⓝW.V & I = Abst.
#I #L1 #K2 #W #H elim (lsubr_inv_bind2 … H) -H *
[ /3 width=3 by ex2_intro, or_introl/
-| #K2 #X #V #HK12 #H1 #H2 destruct /3 width=4 by ex3_2_intro, or_intror/
-| #I1 #I1 #K2 #V #_ #_ #H destruct
+| #K1 #X #V #HK12 #H1 #H2 destruct /3 width=4 by ex3_2_intro, or_intror/
+| #J1 #J1 #K1 #V #_ #_ #H destruct
]
qed-.
-lemma lsubr_inv_abbr2: ∀L1,K2,V. L1 ⫃ K2.ⓓV →
- ∃∃K1. K1 ⫃ K2 & L1 = K1.ⓓV.
+lemma lsubr_inv_abbr2:
+ ∀L1,K2,V. L1 ⫃ K2.ⓓV →
+ ∃∃K1. K1 ⫃ K2 & L1 = K1.ⓓV.
#L1 #K2 #V #H elim (lsubr_inv_pair2 … H) -H *
[ /2 width=3 by ex2_intro/
| #K1 #X #_ #_ #H destruct
]
qed-.
-lemma lsubr_inv_abst2: ∀L1,K2,W. L1 ⫃ K2.ⓛW →
- ∨∨ ∃∃K1. K1 ⫃ K2 & L1 = K1.ⓛW
- | ∃∃K1,V. K1 ⫃ K2 & L1 = K1.ⓓⓝW.V.
+lemma lsubr_inv_abst2:
+ ∀L1,K2,W. L1 ⫃ K2.ⓛW →
+ ∨∨ ∃∃K1. K1 ⫃ K2 & L1 = K1.ⓛW
+ | ∃∃K1,V. K1 ⫃ K2 & L1 = K1.ⓓⓝW.V.
#L1 #K2 #W #H elim (lsubr_inv_pair2 … H) -H *
/3 width=4 by ex2_2_intro, ex2_intro, or_introl, or_intror/
qed-.
-lemma lsubr_inv_unit2: ∀I,L1,K2. L1 ⫃ K2.ⓤ{I} →
- ∨∨ ∃∃K1. K1 ⫃ K2 & L1 = K1.ⓤ{I}
- | ∃∃J,K1,V. K1 ⫃ K2 & L1 = K1.ⓑ{J}V.
+lemma lsubr_inv_unit2:
+ ∀I,L1,K2. L1 ⫃ K2.ⓤ{I} →
+ ∨∨ ∃∃K1. K1 ⫃ K2 & L1 = K1.ⓤ{I}
+ | ∃∃J,K1,V. K1 ⫃ K2 & L1 = K1.ⓑ{J}V.
#I #L1 #K2 #H elim (lsubr_inv_bind2 … H) -H *
[ /3 width=3 by ex2_intro, or_introl/
| #K1 #W #V #_ #_ #H destruct
-| #I1 #I2 #K1 #V #HK12 #H1 #H2 destruct /3 width=5 by ex2_3_intro, or_intror/
+| #J1 #J2 #K1 #V #HK12 #H1 #H2 destruct /3 width=5 by ex2_3_intro, or_intror/
]
qed-.
(* Basic forward lemmas *****************************************************)
-lemma lsubr_fwd_bind1: ∀I1,K1,L2. K1.ⓘ{I1} ⫃ L2 →
- ∃∃I2,K2. K1 ⫃ K2 & L2 = K2.ⓘ{I2}.
+lemma lsubr_fwd_bind1:
+ ∀I1,K1,L2. K1.ⓘ{I1} ⫃ L2 →
+ ∃∃I2,K2. K1 ⫃ K2 & L2 = K2.ⓘ{I2}.
#I1 #K1 #L2 #H elim (lsubr_inv_bind1 … H) -H *
[ #K2 #HK12 #H destruct /3 width=4 by ex2_2_intro/
| #K2 #W1 #V1 #HK12 #H1 #H2 destruct /3 width=4 by ex2_2_intro/
-| #I1 #I2 #K2 #V1 #HK12 #H1 #H2 destruct /3 width=4 by ex2_2_intro/
+| #J1 #J2 #K2 #V1 #HK12 #H1 #H2 destruct /3 width=4 by ex2_2_intro/
]
qed-.
-lemma lsubr_fwd_bind2: ∀I2,L1,K2. L1 ⫃ K2.ⓘ{I2} →
- ∃∃I1,K1. K1 ⫃ K2 & L1 = K1.ⓘ{I1}.
+lemma lsubr_fwd_bind2:
+ ∀I2,L1,K2. L1 ⫃ K2.ⓘ{I2} →
+ ∃∃I1,K1. K1 ⫃ K2 & L1 = K1.ⓘ{I1}.
#I2 #L1 #K2 #H elim (lsubr_inv_bind2 … H) -H *
[ #K1 #HK12 #H destruct /3 width=4 by ex2_2_intro/
| #K1 #W1 #V1 #HK12 #H1 #H2 destruct /3 width=4 by ex2_2_intro/
-| #I1 #I2 #K1 #V1 #HK12 #H1 #H2 destruct /3 width=4 by ex2_2_intro/
+| #J1 #J2 #K1 #V1 #HK12 #H1 #H2 destruct /3 width=4 by ex2_2_intro/
]
qed-.
(* Forward lemmas with generic slicing for local environments ***************)
(* Basic_2A1: includes: lsubr_fwd_drop2_pair *)
-lemma lsubr_fwd_drops2_bind: ∀L1,L2. L1 ⫃ L2 →
- ∀b,f,I,K2. 𝐔⦃f⦄ → ⬇*[b,f] L2 ≘ K2.ⓘ{I} →
- ∨∨ ∃∃K1. K1 ⫃ K2 & ⬇*[b,f] L1 ≘ K1.ⓘ{I}
- | ∃∃K1,W,V. K1 ⫃ K2 & ⬇*[b,f] L1 ≘ K1.ⓓⓝW.V & I = BPair Abst W
- | ∃∃J1,J2,K1,V. K1 ⫃ K2 & ⬇*[b,f] L1 ≘ K1.ⓑ{J1}V & I = BUnit J2.
+lemma lsubr_fwd_drops2_bind:
+ ∀L1,L2. L1 ⫃ L2 →
+ ∀b,f,I,K2. 𝐔⦃f⦄ → ⬇*[b,f] L2 ≘ K2.ⓘ{I} →
+ ∨∨ ∃∃K1. K1 ⫃ K2 & ⬇*[b,f] L1 ≘ K1.ⓘ{I}
+ | ∃∃K1,W,V. K1 ⫃ K2 & ⬇*[b,f] L1 ≘ K1.ⓓⓝW.V & I = BPair Abst W
+ | ∃∃J1,J2,K1,V. K1 ⫃ K2 & ⬇*[b,f] L1 ≘ K1.ⓑ{J1}V & I = BUnit J2.
#L1 #L2 #H elim H -L1 -L2
[ #b #f #I #K2 #_ #H
elim (drops_inv_atom1 … H) -H #H destruct
qed-.
(* Basic_2A1: includes: lsubr_fwd_drop2_abbr *)
-lemma lsubr_fwd_drops2_abbr: ∀L1,L2. L1 ⫃ L2 →
- ∀b,f,K2,V. 𝐔⦃f⦄ → ⬇*[b,f] L2 ≘ K2.ⓓV →
- ∃∃K1. K1 ⫃ K2 & ⬇*[b,f] L1 ≘ K1.ⓓV.
+lemma lsubr_fwd_drops2_abbr:
+ ∀L1,L2. L1 ⫃ L2 →
+ ∀b,f,K2,V. 𝐔⦃f⦄ → ⬇*[b,f] L2 ≘ K2.ⓓV →
+ ∃∃K1. K1 ⫃ K2 & ⬇*[b,f] L1 ≘ K1.ⓓV.
#L1 #L2 #HL12 #b #f #K2 #V #Hf #HLK2
elim (lsubr_fwd_drops2_bind … HL12 … Hf HLK2) -L2 -Hf // *
[ #K1 #W #V #_ #_ #H destruct
theorem lsubr_trans: Transitive … lsubr.
#L1 #L #H elim H -L1 -L //
[ #I #L1 #L #_ #IH #X #H elim (lsubr_inv_bind1 … H) -H *
- [ #L2 #HL2 #H | #L2 #V #W #HL2 #H1 #H2 | #I1 #I2 #L2 #V #Hl2 #H1 #H2 ]
+ [ #L2 #HL2 #H | #L2 #V #W #HL2 #H1 #H2 | #I1 #I2 #L2 #V #HL2 #H1 #H2 ]
destruct /3 width=1 by lsubr_bind, lsubr_beta, lsubr_unit/
| #L1 #L #V #W #_ #IH #X #H elim (lsubr_inv_abst1 … H) -H *
[ #L2 #HL2 #H | #I #L2 #HL2 #H ]
destruct /3 width=1 by lsubr_beta, lsubr_unit/
| #I1 #I2 #L1 #L #V #_ #IH #X #H elim (lsubr_inv_unit1 … H) -H
- /4 width=1 by lsubr_unit/
+ #L2 #HL2 #H destruct /4 width=1 by lsubr_unit/
]
qed-.
projects / helm.git / commitdiff