(* Advanced properties of "qrst" parallel computation on closures ***********)
-lemma fpbs_fpbu_trans: ∀h,g,F1,F2,K1,K2,T1,T2. ⦃F1, K1, T1⦄ ≥[h, g] ⦃F2, K2, T2⦄ →
- ∀G2,L2,U2. ⦃F2, K2, T2⦄ ≻[h, g] ⦃G2, L2, U2⦄ →
- ∃∃G1,L1,U1. ⦃F1, K1, T1⦄ ≻[h, g] ⦃G1, L1, U1⦄ & ⦃G1, L1, U1⦄ ≥[h, g] ⦃G2, L2, U2⦄.
+lemma fpbs_fpb_trans: ∀h,g,F1,F2,K1,K2,T1,T2. ⦃F1, K1, T1⦄ ≥[h, g] ⦃F2, K2, T2⦄ →
+ ∀G2,L2,U2. ⦃F2, K2, T2⦄ ≻[h, g] ⦃G2, L2, U2⦄ →
+ ∃∃G1,L1,U1. ⦃F1, K1, T1⦄ ≻[h, g] ⦃G1, L1, U1⦄ & ⦃G1, L1, U1⦄ ≥[h, g] ⦃G2, L2, U2⦄.
#h #g #F1 #F2 #K1 #K2 #T1 #T2 #H elim (fpbs_fpbg … H) -H
[ #H12 #G2 #L2 #U2 #H2 elim (fleq_fpb_trans … H12 … H2) -F2 -K2 -T2
/3 width=5 by fleq_fpbs, ex2_3_intro/
(* Basic eliminators ********************************************************)
lemma fsb_ind_alt: ∀h,g. ∀R: relation3 …. (
- â\88\80G1,L1,T1. â¦\83G1, L1â¦\84 â\8a¢ ⦥[h,g] T1 → (
+ â\88\80G1,L1,T1. ⦥[h,g] â¦\83G1, L1, T1â¦\84 → (
∀G2,L2,T2. ⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, L2, T2⦄ → R G2 L2 T2
) → R G1 L1 T1
) →
- â\88\80G,L,T. â¦\83G, Lâ¦\84 â\8a¢ ⦥[h, g] T → R G L T.
+ â\88\80G,L,T. ⦥[h, g] â¦\83G, L, Tâ¦\84 → R G L T.
#h #g #R #IH #G #L #T #H elim H -G -L -T
/4 width=1 by fsb_intro/
qed-.
(* Basic inversion lemmas ***************************************************)
-lemma fsb_inv_csx: â\88\80h,g,G,L,T. â¦\83G, Lâ¦\84 â\8a¢ ⦥[h, g] T → ⦃G, L⦄ ⊢ ⬊*[h, g] T.
+lemma fsb_inv_csx: â\88\80h,g,G,L,T. ⦥[h, g] â¦\83G, L, Tâ¦\84 → ⦃G, L⦄ ⊢ ⬊*[h, g] T.
#h #g #G #L #T #H elim H -G -L -T /5 width=1 by csx_intro, fpb_cpx/
qed-.
(* Main properties **********************************************************)
(* Note: this is the "big tree" theorem ("RST" version) *)
-theorem aaa_fsb: â\88\80h,g,G,L,T,A. â¦\83G, Lâ¦\84 â\8a¢ T â\81\9d A â\86\92 â¦\83G, Lâ¦\84 â\8a¢ ⦥[h, g] T.
+theorem aaa_fsb: â\88\80h,g,G,L,T,A. â¦\83G, Lâ¦\84 â\8a¢ T â\81\9d A â\86\92 ⦥[h, g] â¦\83G, L, Tâ¦\84.
/3 width=2 by aaa_csx, csx_fsb/ qed.
(* Note: this is the "big tree" theorem ("QRST" version) *)
-theorem aaa_fsba: â\88\80h,g,G,L,T,A. â¦\83G, Lâ¦\84 â\8a¢ T â\81\9d A â\86\92 â¦\83G, Lâ¦\84 â\8a¢ ⦥⦥[h, g] T.
+theorem aaa_fsba: â\88\80h,g,G,L,T,A. â¦\83G, Lâ¦\84 â\8a¢ T â\81\9d A â\86\92 ⦥⦥[h, g] â¦\83G, L, Tâ¦\84.
/3 width=2 by fsb_fsba, aaa_fsb/ qed.
(* Advanced eliminators on atomica arity assignment for terms ***************)
-fact aaa_ind_fpbu_aux: ∀h,g. ∀R:relation3 genv lenv term.
- (∀G1,L1,T1,A. ⦃G1, L1⦄ ⊢ T1 ⁝ A →
- (∀G2,L2,T2. ⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, L2, T2⦄ → R G2 L2 T2) →
- R G1 L1 T1
- ) →
- ∀G,L,T. ⦃G, L⦄ ⊢ ⬊*[h, g] T → ∀A. ⦃G, L⦄ ⊢ T ⁝ A → R G L T.
-#h #g #R #IH #G #L #T #H @(csx_ind_fpbu … H) -G -L -T
+fact aaa_ind_fpb_aux: ∀h,g. ∀R:relation3 genv lenv term.
+ (∀G1,L1,T1,A. ⦃G1, L1⦄ ⊢ T1 ⁝ A →
+ (∀G2,L2,T2. ⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, L2, T2⦄ → R G2 L2 T2) →
+ R G1 L1 T1
+ ) →
+ ∀G,L,T. ⦃G, L⦄ ⊢ ⬊*[h, g] T → ∀A. ⦃G, L⦄ ⊢ T ⁝ A → R G L T.
+#h #g #R #IH #G #L #T #H @(csx_ind_fpb … H) -G -L -T
#G1 #L1 #T1 #H1 #IH1 #A1 #HTA1 @IH -IH //
#G2 #L2 #T2 #H12 elim (fpbs_aaa_conf h g … G2 … L2 … T2 … HTA1) -A1
/2 width=2 by fpb_fpbs/
qed-.
-lemma aaa_ind_fpbu: ∀h,g. ∀R:relation3 genv lenv term.
- (∀G1,L1,T1,A. ⦃G1, L1⦄ ⊢ T1 ⁝ A →
- (∀G2,L2,T2. ⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, L2, T2⦄ → R G2 L2 T2) →
- R G1 L1 T1
- ) →
- ∀G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → R G L T.
-/4 width=4 by aaa_ind_fpbu_aux, aaa_csx/ qed-.
+lemma aaa_ind_fpb: ∀h,g. ∀R:relation3 genv lenv term.
+ (∀G1,L1,T1,A. ⦃G1, L1⦄ ⊢ T1 ⁝ A →
+ (∀G2,L2,T2. ⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, L2, T2⦄ → R G2 L2 T2) →
+ R G1 L1 T1
+ ) →
+ ∀G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → R G L T.
+/4 width=4 by aaa_ind_fpb_aux, aaa_csx/ qed-.
fact aaa_ind_fpbg_aux: ∀h,g. ∀R:relation3 genv lenv term.
(∀G1,L1,T1,A. ⦃G1, L1⦄ ⊢ T1 ⁝ A →
(* Basic eliminators ********************************************************)
lemma fsba_ind_alt: ∀h,g. ∀R: relation3 …. (
- â\88\80G1,L1,T1. â¦\83G1, L1â¦\84 â\8a¢ ⦥⦥[h,g] T1 → (
+ â\88\80G1,L1,T1. ⦥⦥[h,g] â¦\83G1, L1, T1â¦\84 → (
∀G2,L2,T2. ⦃G1, L1, T1⦄ >≡[h, g] ⦃G2, L2, T2⦄ → R G2 L2 T2
) → R G1 L1 T1
) →
- â\88\80G,L,T. â¦\83G, Lâ¦\84 â\8a¢ ⦥⦥[h, g] T → R G L T.
+ â\88\80G,L,T. ⦥⦥[h, g] â¦\83G, L, Tâ¦\84 → R G L T.
#h #g #R #IH #G #L #T #H elim H -G -L -T
/4 width=1 by fsba_intro/
qed-.
(* Basic properties *********************************************************)
-lemma fsba_fpbs_trans: â\88\80h,g,G1,L1,T1. â¦\83G1, L1â¦\84 â\8a¢ ⦥⦥[h, g] T1 →
- â\88\80G2,L2,T2. â¦\83G1, L1, T1â¦\84 â\89¥[h, g] â¦\83G2, L2, T2â¦\84 â\86\92 â¦\83G2, L2â¦\84 â\8a¢ ⦥⦥[h, g] T2.
+lemma fsba_fpbs_trans: â\88\80h,g,G1,L1,T1. ⦥⦥[h, g] â¦\83G1, L1, T1â¦\84 →
+ â\88\80G2,L2,T2. â¦\83G1, L1, T1â¦\84 â\89¥[h, g] â¦\83G2, L2, T2â¦\84 â\86\92 ⦥⦥[h, g] â¦\83G2, L2, T2â¦\84.
#h #g #G1 #L1 #T1 #H @(fsba_ind_alt … H) -G1 -L1 -T1
/4 width=5 by fsba_intro, fpbs_fpbg_trans/
qed-.
(* Main properties **********************************************************)
-theorem fsb_fsba: â\88\80h,g,G,L,T. â¦\83G, Lâ¦\84 â\8a¢ ⦥[h, g] T â\86\92 â¦\83G, Lâ¦\84 â\8a¢ ⦥⦥[h, g] T.
+theorem fsb_fsba: â\88\80h,g,G,L,T. ⦥[h, g] â¦\83G, L, Tâ¦\84 â\86\92 ⦥⦥[h, g] â¦\83G, L, Tâ¦\84.
#h #g #G #L #T #H @(fsb_ind_alt … H) -G -L -T
#G1 #L1 #T1 #_ #IH @fsba_intro
#G2 #L2 #T2 * /3 width=5 by fsba_fpbs_trans/
(* Main inversion lemmas ****************************************************)
-theorem fsba_inv_fsb: â\88\80h,g,G,L,T. â¦\83G, Lâ¦\84 â\8a¢ ⦥⦥[h, g] T â\86\92 â¦\83G, Lâ¦\84 â\8a¢ ⦥[h, g] T.
+theorem fsba_inv_fsb: â\88\80h,g,G,L,T. ⦥⦥[h, g] â¦\83G, L, Tâ¦\84 â\86\92 ⦥[h, g] â¦\83G, L, Tâ¦\84.
#h #g #G #L #T #H @(fsba_ind_alt … H) -G -L -T
/4 width=1 by fsb_intro, fpb_fpbg/
qed-.
(* Advanced properties ******************************************************)
-lemma fsb_fpbs_trans: â\88\80h,g,G1,L1,T1. â¦\83G1, L1â¦\84 â\8a¢ ⦥[h, g] T1 →
- â\88\80G2,L2,T2. â¦\83G1, L1, T1â¦\84 â\89¥[h, g] â¦\83G2, L2, T2â¦\84 â\86\92 â¦\83G2, L2â¦\84 â\8a¢ ⦥[h, g] T2.
+lemma fsb_fpbs_trans: â\88\80h,g,G1,L1,T1. ⦥[h, g] â¦\83G1, L1, T1â¦\84 →
+ â\88\80G2,L2,T2. â¦\83G1, L1, T1â¦\84 â\89¥[h, g] â¦\83G2, L2, T2â¦\84 â\86\92 ⦥[h, g] â¦\83G2, L2, T2â¦\84.
/4 width=5 by fsba_inv_fsb, fsb_fsba, fsba_fpbs_trans/ qed-.
(* Advanced eliminators *****************************************************)
lemma fsb_ind_fpbg: ∀h,g. ∀R:relation3 genv lenv term.
- (â\88\80G1,L1,T1. â¦\83G1, L1â¦\84 â\8a¢ ⦥[h, g] T1 →
+ (â\88\80G1,L1,T1. ⦥[h, g] â¦\83G1, L1, T1â¦\84 →
(∀G2,L2,T2. ⦃G1, L1, T1⦄ >≡[h, g] ⦃G2, L2, T2⦄ → R G2 L2 T2) →
R G1 L1 T1
) →
- â\88\80G1,L1,T1. â¦\83G1, L1â¦\84 â\8a¢ ⦥[h, g] T1 → R G1 L1 T1.
+ â\88\80G1,L1,T1. ⦥[h, g] â¦\83G1, L1, T1â¦\84 → R G1 L1 T1.
#h #g #R #IH #G1 #L1 #T1 #H @(fsba_ind_alt h g … G1 L1 T1)
/3 width=1 by fsba_inv_fsb, fsb_fsba/
qed-.
(* Advanced propreties on context-sensitive extended normalizing terms ******)
lemma csx_fsb_fpbs: ∀h,g,G1,L1,T1. ⦃G1, L1⦄ ⊢ ⬊*[h, g] T1 →
- â\88\80G2,L2,T2. â¦\83G1, L1, T1â¦\84 â\89¥[h, g] â¦\83G2, L2, T2â¦\84 â\86\92 â¦\83G2, L2â¦\84 â\8a¢ ⦥[h, g] T2.
+ â\88\80G2,L2,T2. â¦\83G1, L1, T1â¦\84 â\89¥[h, g] â¦\83G2, L2, T2â¦\84 â\86\92 ⦥[h, g] â¦\83G2, L2, T2â¦\84.
#h #g #G1 #L1 #T1 #H @(csx_ind … H) -T1
#T1 #HT1 #IHc #G2 #L2 #T2 @(fqup_wf_ind … G2 L2 T2) -G2 -L2 -T2
#G0 #L0 #T0 #IHu #H10 lapply (csx_fpbs_conf … H10) // -HT1
]
qed.
-lemma csx_fsb: â\88\80h,g,G,L,T. â¦\83G, Lâ¦\84 â\8a¢ â¬\8a*[h, g] T â\86\92 â¦\83G, Lâ¦\84 â\8a¢ ⦥[h, g] T.
+lemma csx_fsb: â\88\80h,g,G,L,T. â¦\83G, Lâ¦\84 â\8a¢ â¬\8a*[h, g] T â\86\92 ⦥[h, g] â¦\83G, L, Tâ¦\84.
/2 width=5 by csx_fsb_fpbs/ qed.
(* Advanced eliminators *****************************************************)
-lemma csx_ind_fpbu: ∀h,g. ∀R:relation3 genv lenv term.
- (∀G1,L1,T1. ⦃G1, L1⦄ ⊢ ⬊*[h, g] T1 →
- (∀G2,L2,T2. ⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, L2, T2⦄ → R G2 L2 T2) →
- R G1 L1 T1
- ) →
- ∀G,L,T. ⦃G, L⦄ ⊢ ⬊*[h, g] T → R G L T.
+lemma csx_ind_fpb: ∀h,g. ∀R:relation3 genv lenv term.
+ (∀G1,L1,T1. ⦃G1, L1⦄ ⊢ ⬊*[h, g] T1 →
+ (∀G2,L2,T2. ⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, L2, T2⦄ → R G2 L2 T2) →
+ R G1 L1 T1
+ ) →
+ ∀G,L,T. ⦃G, L⦄ ⊢ ⬊*[h, g] T → R G L T.
/4 width=4 by fsb_inv_csx, csx_fsb, fsb_ind_alt/ qed-.
lemma csx_ind_fpbg: ∀h,g. ∀R:relation3 genv lenv term.
#h #g #G #L1 #T1 #HT1 #T2 #H
@(cprs_ind … H) -T2 /3 width=5 by snv_cpr_lpr/
qed-.
+
+lemma da_cprs_lpr: ∀h,g,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, g] →
+ ∀l. ⦃G, L1⦄ ⊢ T1 ▪[h, g] l →
+ ∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ T2 ▪[h, g] l.
+#h #g #G #L1 #T1 #HT1 #l #Hl #T2 #H
+@(cprs_ind … H) -T2 /3 width=6 by snv_cprs_lpr, da_cpr_lpr/
+qed-.
+
+lemma lstas_cprs_lpr: ∀h,g,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, g] →
+ ∀l1,l2. l2 ≤ l1 → ⦃G, L1⦄ ⊢ T1 ▪[h, g] l1 →
+ ∀U1. ⦃G, L1⦄ ⊢ T1 •*[h, l2] U1 →
+ ∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 →
+ ∃∃U2. ⦃G, L2⦄ ⊢ T2 •*[h, l2] U2 & ⦃G, L2⦄ ⊢ U1 ⬌* U2.
+#h #g #G #L1 #T1 #HT1 #l1 #l2 #Hl21 #Hl1 #U1 #HTU1 #T2 #H
+@(cprs_ind … H) -T2 [ /2 width=10 by lstas_cpr_lpr/ ]
+#T #T2 #HT1T #HTT2 #IHT1 #L2 #HL12
+elim (IHT1 L1) // -IHT1 #U #HTU #HU1
+elim (lstas_cpr_lpr … g … Hl21 … HTU … HTT2 … HL12) -HTU -HTT2
+[2,3: /2 width=7 by snv_cprs_lpr, da_cprs_lpr/ ] -T1 -T -l1
+/4 width=5 by lpr_cpcs_conf, cpcs_trans, ex2_intro/
+qed-.
+
+lemma lstas_cpcs_lpr: ∀h,g,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, g] →
+ ∀l,l1. l ≤ l1 → ⦃G, L1⦄ ⊢ T1 ▪[h, g] l1 → ∀U1. ⦃G, L1⦄ ⊢ T1 •*[h, l] U1 →
+ ∀T2. ⦃G, L1⦄ ⊢ T2 ¡[h, g] →
+ ∀l2. l ≤ l2 → ⦃G, L1⦄ ⊢ T2 ▪[h, g] l2 → ∀U2. ⦃G, L1⦄ ⊢ T2 •*[h, l] U2 →
+ ⦃G, L1⦄ ⊢ T1 ⬌* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ U1 ⬌* U2.
+#h #g #G #L1 #T1 #HT1 #l #l1 #Hl1 #HTl1 #U1 #HTU1 #T2 #HT2 #l2 #Hl2 #HTl2 #U2 #HTU2 #H #L2 #HL12
+elim (cpcs_inv_cprs … H) -H #T #H1 #H2
+elim (lstas_cprs_lpr … HT1 … Hl1 HTl1 … HTU1 … H1 … HL12) -T1 #W1 #H1 #HUW1
+elim (lstas_cprs_lpr … HT2 … Hl2 HTl2 … HTU2 … H2 … HL12) -T2 #W2 #H2 #HUW2
+lapply (lstas_mono … H1 … H2) -h -T -l #H destruct /2 width=3 by cpcs_canc_dx/
+qed-.
-lemma da_cprs_lpr: ∀h,g,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, g] →
- ∀l. ⦃G, L1⦄ ⊢ T1 ▪[h, g] l →
- ∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ T2 ▪[h, g] l.
-#h #g #G #L1 #T1 #HT1 #l #Hl #T2 #H
-@(cprs_ind … H) -T2 /3 width=6 by snv_cprs_lpr, da_cpr_lpr/
-qed-.
-
lemma da_cpcs: ∀h,g,G,L,T1. ⦃G, L⦄ ⊢ T1 ¡[h, g] →
∀T2. ⦃G, L⦄ ⊢ T2 ¡[h, g] →
∀l1. ⦃G, L⦄ ⊢ T1 ▪[h, g] l1 → ∀l2. ⦃G, L⦄ ⊢ T2 ▪[h, g] l2 →
/3 width=3 by lstas_inv_SO, sta_lstas, ex2_intro/
qed-.
-lemma lstas_cprs_lpr: ∀h,g,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, g] →
- ∀l1,l2. l2 ≤ l1 → ⦃G, L1⦄ ⊢ T1 ▪[h, g] l1 →
- ∀U1. ⦃G, L1⦄ ⊢ T1 •*[h, l2] U1 →
- ∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 →
- ∃∃U2. ⦃G, L2⦄ ⊢ T2 •*[h, l2] U2 & ⦃G, L2⦄ ⊢ U1 ⬌* U2.
-#h #g #G #L1 #T1 #HT1 #l1 #l2 #Hl21 #Hl1 #U1 #HTU1 #T2 #H
-@(cprs_ind … H) -T2 [ /2 width=10 by lstas_cpr_lpr/ ]
-#T #T2 #HT1T #HTT2 #IHT1 #L2 #HL12
-elim (IHT1 L1) // -IHT1 #U #HTU #HU1
-elim (lstas_cpr_lpr … g … Hl21 … HTU … HTT2 … HL12) -HTU -HTT2
-[2,3: /2 width=7 by snv_cprs_lpr, da_cprs_lpr/ ] -T1 -T -l1
-/4 width=5 by lpr_cpcs_conf, cpcs_trans, ex2_intro/
-qed-.
-
-lemma lstas_cpcs_lpr: ∀h,g,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, g] →
- ∀l,l1. l ≤ l1 → ⦃G, L1⦄ ⊢ T1 ▪[h, g] l1 → ∀U1. ⦃G, L1⦄ ⊢ T1 •*[h, l] U1 →
- ∀T2. ⦃G, L1⦄ ⊢ T2 ¡[h, g] →
- ∀l2. l ≤ l2 → ⦃G, L1⦄ ⊢ T2 ▪[h, g] l2 → ∀U2. ⦃G, L1⦄ ⊢ T2 •*[h, l] U2 →
- ⦃G, L1⦄ ⊢ T1 ⬌* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ U1 ⬌* U2.
-#h #g #G #L1 #T1 #HT1 #l #l1 #Hl1 #HTl1 #U1 #HTU1 #T2 #HT2 #l2 #Hl2 #HTl2 #U2 #HTU2 #H #L2 #HL12
-elim (cpcs_inv_cprs … H) -H #T #H1 #H2
-elim (lstas_cprs_lpr … HT1 … Hl1 HTl1 … HTU1 … H1 … HL12) -T1 #W1 #H1 #HUW1
-elim (lstas_cprs_lpr … HT2 … Hl2 HTl2 … HTU2 … H2 … HL12) -T2 #W2 #H2 #HUW2
-lapply (lstas_mono … H1 … H2) -h -T -l #H destruct /2 width=3 by cpcs_canc_dx/
-qed-.
-
lemma snv_sta: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ T ¡[h, g] →
∀l. ⦃G, L⦄ ⊢ T ▪[h, g] l+1 →
∀U. ⦃G, L⦄ ⊢ T •[h] U → ⦃G, L⦄ ⊢ U ¡[h, g].
lapply (cpcs_canc_sn … HW12 HWU1) -W1 #H
elim (cpcs_inv_cprs … H) -H /3 width=7 by ex4_3_intro, ex2_intro/
qed-.
+
+(* Note: missing da_scpds_lpr, da_scpes *)
+
+lemma scpds_cpr_lpr: ∀h,g,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, g] →
+ ∀U1,l. ⦃G, L1⦄ ⊢ T1 •*➡*[h, g, l] U1 →
+ ∀T2. ⦃G, L1⦄ ⊢ T1 ➡ T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 →
+ ∃∃U2. ⦃G, L2⦄ ⊢ T2 •*➡*[h, g, l] U2 & ⦃G, L2⦄ ⊢ U1 ➡* U2.
+#h #g #G #L1 #T1 #HT1 #U1 #l2 * #W1 #l1 #Hl21 #HTl1 #HTW1 #HWU1 #T2 #HT12 #L2 #HL12
+elim (lstas_cpr_lpr … HTl1 … HTW1 … HT12 … HL12) // #W2 #HTW2 #HW12
+lapply (da_cpr_lpr … HTl1 … HT12 … HL12) // -T1
+lapply (lpr_cprs_conf … HL12 … HWU1) -L1 #HWU1
+lapply (cpcs_canc_sn … HW12 HWU1) -W1 #H
+elim (cpcs_inv_cprs … H) -H /3 width=6 by ex4_2_intro, ex2_intro/
+qed-.
+
+lemma scpes_cpr_lpr: ∀h,g,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, g] →
+ ∀T2. ⦃G, L1⦄ ⊢ T2 ¡[h, g] →
+ ∀l1,l2. ⦃G, L1⦄ ⊢ T1 •*⬌*[h, g, l1, l2] T2 →
+ ∀U1. ⦃G, L1⦄ ⊢ T1 ➡ U1 → ∀U2. ⦃G, L1⦄ ⊢ T2 ➡ U2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 →
+ ⦃G, L2⦄ ⊢ U1 •*⬌*[h, g, l1, l2] U2.
+#h #g #G #L1 #T1 #HT1 #T2 #HT2 #l1 #l2 * #T0 #HT10 #HT20 #U1 #HTU1 #U2 #HTU2 #L2 #HL12
+elim (scpds_cpr_lpr … HT10 … HTU1 … HL12) -HT10 -HTU1 // #X1 #HUX1 #H1
+elim (scpds_cpr_lpr … HT20 … HTU2 … HL12) -HT20 -HTU2 // #X2 #HUX2 #H2
+elim (cprs_conf … H1 … H2) -T0 /3 width=5 by scpds_div, scpds_cprs_trans/
+qed-.
+
+(* Note: missing lstas_scpds, scpes_le *)
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( â¦\83 term 46 G, break term 46 L â¦\84 â\8a¢ ⦥ break [ term 46 h , break term 46 g ] break term 46 T )"
+notation "hvbox( ⦥ [ term 46 h, break term 46 g ] break â¦\83 term 46 G, break term 46 L, break term 46 T â¦\84 )"
non associative with precedence 45
for @{ 'BTSN $h $g $G $L $T }.
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( â¦\83 term 46 G, break term 46 L â¦\84 â\8a¢ ⦥ ⦥ break [ term 46 h , break term 46 g ] break term 46 T )"
+notation "hvbox( ⦥ ⦥ [ term 46 h, break term 46 g ] break â¦\83 term 46 G, break term 46 L, break term 46 T â¦\84 )"
non associative with precedence 45
for @{ 'BTSNAlt $h $g $G $L $T }.
}
]
[ { "strongly normalizing qrst-computation" * } {
- [ "fsb ( â¦\83?,?â¦\84 â\8a¢ ⦥[?,?] ? )" "fsb_alt ( â¦\83?,?â¦\84 â\8a¢ ⦥⦥[?,?] ? )" "fsb_aaa" + "fsb_csx" * ]
+ [ "fsb ( ⦥[?,?] â¦\83?,?,?â¦\84 )" "fsb_alt ( ⦥⦥[?,?] â¦\83?,?,?â¦\84 )" "fsb_aaa" + "fsb_csx" * ]
}
]
[ { "strongly normalizing rt-computation" * } {
projects / helm.git / commitdiff