(* Properties on degree assignment for terms ********************************)
fact da_cpr_lpr_aux: ∀h,o,G0,L0,T0.
- (â\88\80G1,L1,T1. â¦\83G0, L0, T0â¦\84 >â\89¡[h, o] ⦃G1, L1, T1⦄ → IH_snv_lstas h o G1 L1 T1) →
- (â\88\80G1,L1,T1. â¦\83G0, L0, T0â¦\84 >â\89¡[h, o] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h o G1 L1 T1) →
- (â\88\80G1,L1,T1. â¦\83G0, L0, T0â¦\84 >â\89¡[h, o] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h o G1 L1 T1) →
+ (â\88\80G1,L1,T1. â¦\83G0, L0, T0â¦\84 >â\89\9b[h, o] ⦃G1, L1, T1⦄ → IH_snv_lstas h o G1 L1 T1) →
+ (â\88\80G1,L1,T1. â¦\83G0, L0, T0â¦\84 >â\89\9b[h, o] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h o G1 L1 T1) →
+ (â\88\80G1,L1,T1. â¦\83G0, L0, T0â¦\84 >â\89\9b[h, o] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h o G1 L1 T1) →
∀G1,L1,T1. G0 = G1 → L0 = L1 → T0 = T1 → IH_da_cpr_lpr h o G1 L1 T1.
#h #o #G0 #L0 #T0 #IH3 #IH2 #IH1 #G1 #L1 * * [|||| * ]
[ #s #_ #_ #_ #_ #d #H2 #X3 #H3 #L2 #_ -IH3 -IH2 -IH1
(* Properties on context-free parallel reduction for local environments *****)
fact snv_cpr_lpr_aux: ∀h,o,G0,L0,T0.
- (â\88\80G1,L1,T1. â¦\83G0, L0, T0â¦\84 >â\89¡[h, o] ⦃G1, L1, T1⦄ → IH_snv_lstas h o G1 L1 T1) →
- (â\88\80G1,L1,T1. â¦\83G0, L0, T0â¦\84 >â\89¡[h, o] ⦃G1, L1, T1⦄ → IH_lstas_cpr_lpr h o G1 L1 T1) →
- (â\88\80G1,L1,T1. â¦\83G0, L0, T0â¦\84 >â\89¡[h, o] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h o G1 L1 T1) →
- (â\88\80G1,L1,T1. â¦\83G0, L0, T0â¦\84 >â\89¡[h, o] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h o G1 L1 T1) →
+ (â\88\80G1,L1,T1. â¦\83G0, L0, T0â¦\84 >â\89\9b[h, o] ⦃G1, L1, T1⦄ → IH_snv_lstas h o G1 L1 T1) →
+ (â\88\80G1,L1,T1. â¦\83G0, L0, T0â¦\84 >â\89\9b[h, o] ⦃G1, L1, T1⦄ → IH_lstas_cpr_lpr h o G1 L1 T1) →
+ (â\88\80G1,L1,T1. â¦\83G0, L0, T0â¦\84 >â\89\9b[h, o] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h o G1 L1 T1) →
+ (â\88\80G1,L1,T1. â¦\83G0, L0, T0â¦\84 >â\89\9b[h, o] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h o G1 L1 T1) →
∀G1,L1,T1. G0 = G1 → L0 = L1 → T0 = T1 → IH_snv_cpr_lpr h o G1 L1 T1.
#h #o #G0 #L0 #T0 #IH4 #IH3 #IH2 #IH1 #G1 #L1 * * [|||| * ]
[ #s #HG0 #HL0 #HT0 #H1 #X #H2 #L2 #_ destruct -IH4 -IH3 -IH2 -IH1 -H1
(* Properties on nat-iterated stratified static type assignment for terms ***)
fact snv_lstas_aux: ∀h,o,G0,L0,T0.
- (â\88\80G1,L1,T1. â¦\83G0, L0, T0â¦\84 >â\89¡[h, o] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h o G1 L1 T1) →
- (â\88\80G1,L1,T1. â¦\83G0, L0, T0â¦\84 >â\89¡[h, o] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h o G1 L1 T1) →
- (â\88\80G1,L1,T1. â¦\83G0, L0, T0â¦\84 >â\89¡[h, o] ⦃G1, L1, T1⦄ → IH_lstas_cpr_lpr h o G1 L1 T1) →
- (â\88\80G1,L1,T1. â¦\83G0, L0, T0â¦\84 >â\89¡[h, o] ⦃G1, L1, T1⦄ → IH_snv_lstas h o G1 L1 T1) →
+ (â\88\80G1,L1,T1. â¦\83G0, L0, T0â¦\84 >â\89\9b[h, o] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h o G1 L1 T1) →
+ (â\88\80G1,L1,T1. â¦\83G0, L0, T0â¦\84 >â\89\9b[h, o] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h o G1 L1 T1) →
+ (â\88\80G1,L1,T1. â¦\83G0, L0, T0â¦\84 >â\89\9b[h, o] ⦃G1, L1, T1⦄ → IH_lstas_cpr_lpr h o G1 L1 T1) →
+ (â\88\80G1,L1,T1. â¦\83G0, L0, T0â¦\84 >â\89\9b[h, o] ⦃G1, L1, T1⦄ → IH_snv_lstas h o G1 L1 T1) →
∀G1,L1,T1. G0 = G1 → L0 = L1 → T0 = T1 → IH_snv_lstas h o G1 L1 T1.
#h #o #G0 #L0 #T0 #IH4 #IH3 #IH2 #IH1 #G1 #L1 * * [|||| * ]
[ #s #HG0 #HL0 #HT0 #_ #d1 #d2 #Hd21 #Hd1 #X #H2 destruct -IH4 -IH3 -IH2 -IH1
(* Properties on sn parallel reduction for local environments ***************)
fact lstas_cpr_lpr_aux: ∀h,o,G0,L0,T0.
- (â\88\80G1,L1,T1. â¦\83G0, L0, T0â¦\84 >â\89¡[h, o] ⦃G1, L1, T1⦄ → IH_snv_lstas h o G1 L1 T1) →
- (â\88\80G1,L1,T1. â¦\83G0, L0, T0â¦\84 >â\89¡[h, o] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h o G1 L1 T1) →
- (â\88\80G1,L1,T1. â¦\83G0, L0, T0â¦\84 >â\89¡[h, o] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h o G1 L1 T1) →
- (â\88\80G1,L1,T1. â¦\83G0, L0, T0â¦\84 >â\89¡[h, o] ⦃G1, L1, T1⦄ → IH_lstas_cpr_lpr h o G1 L1 T1) →
+ (â\88\80G1,L1,T1. â¦\83G0, L0, T0â¦\84 >â\89\9b[h, o] ⦃G1, L1, T1⦄ → IH_snv_lstas h o G1 L1 T1) →
+ (â\88\80G1,L1,T1. â¦\83G0, L0, T0â¦\84 >â\89\9b[h, o] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h o G1 L1 T1) →
+ (â\88\80G1,L1,T1. â¦\83G0, L0, T0â¦\84 >â\89\9b[h, o] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h o G1 L1 T1) →
+ (â\88\80G1,L1,T1. â¦\83G0, L0, T0â¦\84 >â\89\9b[h, o] ⦃G1, L1, T1⦄ → IH_lstas_cpr_lpr h o G1 L1 T1) →
∀G1,L1,T1. G0 = G1 → L0 = L1 → T0 = T1 → IH_lstas_cpr_lpr h o G1 L1 T1.
#h #o #G0 #L0 #T0 #IH4 #IH3 #IH2 #IH1 #G1 #L1 * * [|||| * ]
[ #s #_ #_ #_ #_ #d1 #d2 #_ #_ #X2 #H2 #X3 #H3 #L2 #_ -IH4 -IH3 -IH2 -IH1
(* Properties for the preservation results **********************************)
fact snv_cprs_lpr_aux: ∀h,o,G0,L0,T0.
- (â\88\80G1,L1,T1. â¦\83G0, L0, T0â¦\84 >â\89¡[h, o] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h o G1 L1 T1) →
- â\88\80G,L1,T1. â¦\83G0, L0, T0â¦\84 >â\89¡[h, o] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, o] →
+ (â\88\80G1,L1,T1. â¦\83G0, L0, T0â¦\84 >â\89\9b[h, o] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h o G1 L1 T1) →
+ â\88\80G,L1,T1. â¦\83G0, L0, T0â¦\84 >â\89\9b[h, o] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, o] →
∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ T2 ¡[h, o].
#h #o #G0 #L0 #T0 #IH #G #L1 #T1 #HLT0 #HT1 #T2 #H
@(cprs_ind … H) -T2 /4 width=6 by fpbg_fpbs_trans, cprs_fpbs/
qed-.
fact da_cprs_lpr_aux: ∀h,o,G0,L0,T0.
- (â\88\80G1,L1,T1. â¦\83G0, L0, T0â¦\84 >â\89¡[h, o] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h o G1 L1 T1) →
- (â\88\80G1,L1,T1. â¦\83G0, L0, T0â¦\84 >â\89¡[h, o] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h o G1 L1 T1) →
- â\88\80G,L1,T1. â¦\83G0, L0, T0â¦\84 >â\89¡[h, o] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, o] →
+ (â\88\80G1,L1,T1. â¦\83G0, L0, T0â¦\84 >â\89\9b[h, o] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h o G1 L1 T1) →
+ (â\88\80G1,L1,T1. â¦\83G0, L0, T0â¦\84 >â\89\9b[h, o] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h o G1 L1 T1) →
+ â\88\80G,L1,T1. â¦\83G0, L0, T0â¦\84 >â\89\9b[h, o] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, o] →
∀d. ⦃G, L1⦄ ⊢ T1 ▪[h, o] d →
∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ T2 ▪[h, o] d.
#h #o #G0 #L0 #T0 #IH2 #IH1 #G #L1 #T1 #HLT0 #HT1 #d #Hd #T2 #H
qed-.
fact da_scpds_lpr_aux: ∀h,o,G0,L0,T0.
- (â\88\80G1,L1,T1. â¦\83G0, L0, T0â¦\84 >â\89¡[h, o] ⦃G1, L1, T1⦄ → IH_snv_lstas h o G1 L1 T1) →
- (â\88\80G1,L1,T1. â¦\83G0, L0, T0â¦\84 >â\89¡[h, o] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h o G1 L1 T1) →
- (â\88\80G1,L1,T1. â¦\83G0, L0, T0â¦\84 >â\89¡[h, o] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h o G1 L1 T1) →
- â\88\80G,L1,T1. â¦\83G0, L0, T0â¦\84 >â\89¡[h, o] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, o] →
+ (â\88\80G1,L1,T1. â¦\83G0, L0, T0â¦\84 >â\89\9b[h, o] ⦃G1, L1, T1⦄ → IH_snv_lstas h o G1 L1 T1) →
+ (â\88\80G1,L1,T1. â¦\83G0, L0, T0â¦\84 >â\89\9b[h, o] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h o G1 L1 T1) →
+ (â\88\80G1,L1,T1. â¦\83G0, L0, T0â¦\84 >â\89\9b[h, o] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h o G1 L1 T1) →
+ â\88\80G,L1,T1. â¦\83G0, L0, T0â¦\84 >â\89\9b[h, o] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, o] →
∀d1. ⦃G, L1⦄ ⊢ T1 ▪[h, o] d1 →
∀T2,d2. ⦃G, L1⦄ ⊢ T1 •*➡*[h, o, d2] T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 →
d2 ≤ d1 ∧ ⦃G, L2⦄ ⊢ T2 ▪[h, o] d1-d2.
qed-.
fact da_scpes_aux: ∀h,o,G0,L0,T0.
- (â\88\80G1,L1,T1. â¦\83G0, L0, T0â¦\84 >â\89¡[h, o] ⦃G1, L1, T1⦄ → IH_snv_lstas h o G1 L1 T1) →
- (â\88\80G1,L1,T1. â¦\83G0, L0, T0â¦\84 >â\89¡[h, o] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h o G1 L1 T1) →
- (â\88\80G1,L1,T1. â¦\83G0, L0, T0â¦\84 >â\89¡[h, o] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h o G1 L1 T1) →
- â\88\80G,L,T1. â¦\83G0, L0, T0â¦\84 >â\89¡[h, o] ⦃G, L, T1⦄ → ⦃G, L⦄ ⊢ T1 ¡[h, o] →
- â\88\80T2. â¦\83G0, L0, T0â¦\84 >â\89¡[h, o] ⦃G, L, T2⦄ → ⦃G, L⦄ ⊢ T2 ¡[h, o] →
+ (â\88\80G1,L1,T1. â¦\83G0, L0, T0â¦\84 >â\89\9b[h, o] ⦃G1, L1, T1⦄ → IH_snv_lstas h o G1 L1 T1) →
+ (â\88\80G1,L1,T1. â¦\83G0, L0, T0â¦\84 >â\89\9b[h, o] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h o G1 L1 T1) →
+ (â\88\80G1,L1,T1. â¦\83G0, L0, T0â¦\84 >â\89\9b[h, o] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h o G1 L1 T1) →
+ â\88\80G,L,T1. â¦\83G0, L0, T0â¦\84 >â\89\9b[h, o] ⦃G, L, T1⦄ → ⦃G, L⦄ ⊢ T1 ¡[h, o] →
+ â\88\80T2. â¦\83G0, L0, T0â¦\84 >â\89\9b[h, o] ⦃G, L, T2⦄ → ⦃G, L⦄ ⊢ T2 ¡[h, o] →
∀d11. ⦃G, L⦄ ⊢ T1 ▪[h, o] d11 → ∀d12. ⦃G, L⦄ ⊢ T2 ▪[h, o] d12 →
∀d21,d22. ⦃G, L⦄ ⊢ T1 •*⬌*[h, o, d21, d22] T2 →
∧∧ d21 ≤ d11 & d22 ≤ d12 & d11 - d21 = d12 - d22.
qed-.
fact lstas_cprs_lpr_aux: ∀h,o,G0,L0,T0.
- (â\88\80G1,L1,T1. â¦\83G0, L0, T0â¦\84 >â\89¡[h, o] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h o G1 L1 T1) →
- (â\88\80G1,L1,T1. â¦\83G0, L0, T0â¦\84 >â\89¡[h, o] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h o G1 L1 T1) →
- (â\88\80G1,L1,T1. â¦\83G0, L0, T0â¦\84 >â\89¡[h, o] ⦃G1, L1, T1⦄ → IH_lstas_cpr_lpr h o G1 L1 T1) →
- â\88\80G,L1,T1. â¦\83G0, L0, T0â¦\84 >â\89¡[h, o] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, o] →
+ (â\88\80G1,L1,T1. â¦\83G0, L0, T0â¦\84 >â\89\9b[h, o] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h o G1 L1 T1) →
+ (â\88\80G1,L1,T1. â¦\83G0, L0, T0â¦\84 >â\89\9b[h, o] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h o G1 L1 T1) →
+ (â\88\80G1,L1,T1. â¦\83G0, L0, T0â¦\84 >â\89\9b[h, o] ⦃G1, L1, T1⦄ → IH_lstas_cpr_lpr h o G1 L1 T1) →
+ â\88\80G,L1,T1. â¦\83G0, L0, T0â¦\84 >â\89\9b[h, o] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, o] →
∀d1,d2. d2 ≤ d1 → ⦃G, L1⦄ ⊢ T1 ▪[h, o] d1 →
∀U1. ⦃G, L1⦄ ⊢ T1 •*[h, d2] U1 →
∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 →
qed-.
fact scpds_cpr_lpr_aux: ∀h,o,G0,L0,T0.
- (â\88\80G1,L1,T1. â¦\83G0, L0, T0â¦\84 >â\89¡[h, o] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h o G1 L1 T1) →
- (â\88\80G1,L1,T1. â¦\83G0, L0, T0â¦\84 >â\89¡[h, o] ⦃G1, L1, T1⦄ → IH_lstas_cpr_lpr h o G1 L1 T1) →
- â\88\80G,L1,T1. â¦\83G0, L0, T0â¦\84 >â\89¡[h, o] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, o] →
+ (â\88\80G1,L1,T1. â¦\83G0, L0, T0â¦\84 >â\89\9b[h, o] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h o G1 L1 T1) →
+ (â\88\80G1,L1,T1. â¦\83G0, L0, T0â¦\84 >â\89\9b[h, o] ⦃G1, L1, T1⦄ → IH_lstas_cpr_lpr h o G1 L1 T1) →
+ â\88\80G,L1,T1. â¦\83G0, L0, T0â¦\84 >â\89\9b[h, o] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, o] →
∀U1,d. ⦃G, L1⦄ ⊢ T1 •*➡*[h, o, d] U1 →
∀T2. ⦃G, L1⦄ ⊢ T1 ➡ T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 →
∃∃U2. ⦃G, L2⦄ ⊢ T2 •*➡*[h, o, d] U2 & ⦃G, L2⦄ ⊢ U1 ➡* U2.
qed-.
fact scpes_cpr_lpr_aux: ∀h,o,G0,L0,T0.
- (â\88\80G1,L1,T1. â¦\83G0, L0, T0â¦\84 >â\89¡[h, o] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h o G1 L1 T1) →
- (â\88\80G1,L1,T1. â¦\83G0, L0, T0â¦\84 >â\89¡[h, o] ⦃G1, L1, T1⦄ → IH_lstas_cpr_lpr h o G1 L1 T1) →
- â\88\80G,L1,T1. â¦\83G0, L0, T0â¦\84 >â\89¡[h, o] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, o] →
- â\88\80T2. â¦\83G0, L0, T0â¦\84 >â\89¡[h, o] ⦃G, L1, T2⦄ → ⦃G, L1⦄ ⊢ T2 ¡[h, o] →
+ (â\88\80G1,L1,T1. â¦\83G0, L0, T0â¦\84 >â\89\9b[h, o] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h o G1 L1 T1) →
+ (â\88\80G1,L1,T1. â¦\83G0, L0, T0â¦\84 >â\89\9b[h, o] ⦃G1, L1, T1⦄ → IH_lstas_cpr_lpr h o G1 L1 T1) →
+ â\88\80G,L1,T1. â¦\83G0, L0, T0â¦\84 >â\89\9b[h, o] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, o] →
+ â\88\80T2. â¦\83G0, L0, T0â¦\84 >â\89\9b[h, o] ⦃G, L1, T2⦄ → ⦃G, L1⦄ ⊢ T2 ¡[h, o] →
∀d1,d2. ⦃G, L1⦄ ⊢ T1 •*⬌*[h, o, d1, d2] T2 →
∀U1. ⦃G, L1⦄ ⊢ T1 ➡ U1 → ∀U2. ⦃G, L1⦄ ⊢ T2 ➡ U2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 →
⦃G, L2⦄ ⊢ U1 •*⬌*[h, o, d1, d2] U2.
qed-.
fact lstas_scpds_aux: ∀h,o,G0,L0,T0.
- (â\88\80G1,L1,T1. â¦\83G0, L0, T0â¦\84 >â\89¡[h, o] ⦃G1, L1, T1⦄ → IH_snv_lstas h o G1 L1 T1) →
- (â\88\80G1,L1,T1. â¦\83G0, L0, T0â¦\84 >â\89¡[h, o] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h o G1 L1 T1) →
- (â\88\80G1,L1,T1. â¦\83G0, L0, T0â¦\84 >â\89¡[h, o] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h o G1 L1 T1) →
- (â\88\80G1,L1,T1. â¦\83G0, L0, T0â¦\84 >â\89¡[h, o] ⦃G1, L1, T1⦄ → IH_lstas_cpr_lpr h o G1 L1 T1) →
- â\88\80G,L,T. â¦\83G0, L0, T0â¦\84 >â\89¡[h, o] ⦃G, L, T⦄ → ⦃G, L⦄ ⊢ T ¡[h, o] →
+ (â\88\80G1,L1,T1. â¦\83G0, L0, T0â¦\84 >â\89\9b[h, o] ⦃G1, L1, T1⦄ → IH_snv_lstas h o G1 L1 T1) →
+ (â\88\80G1,L1,T1. â¦\83G0, L0, T0â¦\84 >â\89\9b[h, o] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h o G1 L1 T1) →
+ (â\88\80G1,L1,T1. â¦\83G0, L0, T0â¦\84 >â\89\9b[h, o] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h o G1 L1 T1) →
+ (â\88\80G1,L1,T1. â¦\83G0, L0, T0â¦\84 >â\89\9b[h, o] ⦃G1, L1, T1⦄ → IH_lstas_cpr_lpr h o G1 L1 T1) →
+ â\88\80G,L,T. â¦\83G0, L0, T0â¦\84 >â\89\9b[h, o] ⦃G, L, T⦄ → ⦃G, L⦄ ⊢ T ¡[h, o] →
∀d,d1. d1 ≤ d → ⦃G, L⦄ ⊢ T ▪[h, o] d → ∀T1. ⦃G, L⦄ ⊢ T •*[h, d1] T1 →
∀T2,d2. ⦃G, L⦄ ⊢ T •*➡*[h, o, d2] T2 → ⦃G, L⦄ ⊢ T1 •*⬌*[h, o, d2-d1, d1-d2] T2.
#h #o #G0 #L0 #T0 #IH4 #IH3 #IH2 #IH1 #G #L #T #H0 #HT #d #d1 #Hd1 #HTd #T1 #HT1 #T2 #d2 * #X #d0 #Hd20 #H #HTX #HXT2
qed-.
fact scpes_le_aux: ∀h,o,G0,L0,T0.
- (â\88\80G1,L1,T1. â¦\83G0, L0, T0â¦\84 >â\89¡[h, o] ⦃G1, L1, T1⦄ → IH_snv_lstas h o G1 L1 T1) →
- (â\88\80G1,L1,T1. â¦\83G0, L0, T0â¦\84 >â\89¡[h, o] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h o G1 L1 T1) →
- (â\88\80G1,L1,T1. â¦\83G0, L0, T0â¦\84 >â\89¡[h, o] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h o G1 L1 T1) →
- (â\88\80G1,L1,T1. â¦\83G0, L0, T0â¦\84 >â\89¡[h, o] ⦃G1, L1, T1⦄ → IH_lstas_cpr_lpr h o G1 L1 T1) →
- â\88\80G,L,T1. â¦\83G0, L0, T0â¦\84 >â\89¡[h, o] ⦃G, L, T1⦄ → ⦃G, L⦄ ⊢ T1 ¡[h, o] →
- â\88\80T2. â¦\83G0, L0, T0â¦\84 >â\89¡[h, o] ⦃G, L, T2⦄ → ⦃G, L⦄ ⊢ T2 ¡[h, o] →
+ (â\88\80G1,L1,T1. â¦\83G0, L0, T0â¦\84 >â\89\9b[h, o] ⦃G1, L1, T1⦄ → IH_snv_lstas h o G1 L1 T1) →
+ (â\88\80G1,L1,T1. â¦\83G0, L0, T0â¦\84 >â\89\9b[h, o] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h o G1 L1 T1) →
+ (â\88\80G1,L1,T1. â¦\83G0, L0, T0â¦\84 >â\89\9b[h, o] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h o G1 L1 T1) →
+ (â\88\80G1,L1,T1. â¦\83G0, L0, T0â¦\84 >â\89\9b[h, o] ⦃G1, L1, T1⦄ → IH_lstas_cpr_lpr h o G1 L1 T1) →
+ â\88\80G,L,T1. â¦\83G0, L0, T0â¦\84 >â\89\9b[h, o] ⦃G, L, T1⦄ → ⦃G, L⦄ ⊢ T1 ¡[h, o] →
+ â\88\80T2. â¦\83G0, L0, T0â¦\84 >â\89\9b[h, o] ⦃G, L, T2⦄ → ⦃G, L⦄ ⊢ T2 ¡[h, o] →
∀d11. ⦃G, L⦄ ⊢ T1 ▪[h, o] d11 → ∀d12. ⦃G, L⦄ ⊢ T2 ▪[h, o] d12 →
∀d21,d22,d. d21 + d ≤ d11 → d22 + d ≤ d12 →
⦃G, L⦄ ⊢ T1 •*⬌*[h, o, d21, d22] T2 → ⦃G, L⦄ ⊢ T1 •*⬌*[h, o, d21+d, d22+d] T2.
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( L . break ⓓ T1 )"
+notation "hvbox( L. break ⓓ T1 )"
left associative with precedence 50
for @{ 'DxAbbr $L $T1 }.
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( L . break ⓛ T1 )"
+notation "hvbox( L. break ⓛ T1 )"
left associative with precedence 51
for @{ 'DxAbst $L $T1 }.
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( L . break ⓤ { term 46 I } )"
+notation "hvbox( L. break ⓤ { term 46 I } )"
non associative with precedence 47
for @{ 'DxBind1 $L $I }.
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( L . break ⓑ { term 46 I } break term 49 T1 )"
+notation "hvbox( L. break ⓑ { term 46 I } break term 49 T1 )"
non associative with precedence 48
for @{ 'DxBind2 $L $I $T1 }.
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( L . ⓘ { break term 46 I } )"
+notation "hvbox( L. ⓘ { break term 46 I } )"
non associative with precedence 46
for @{'DxItem $L $I }.
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( L . ⓧ )"
+notation "hvbox( L. ⓧ )"
non associative with precedence 49
for @{ 'DxVoid $L }.
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( ⓓ { term 46 p } break term 55 T1 . break term 55 T2 )"
+notation "hvbox( ⓓ { term 46 p } break term 55 T1. break term 55 T2 )"
non associative with precedence 55
for @{ 'SnAbbr $p $T1 $T2 }.
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( - ⓓ term 55 T1 . break term 55 T2 )"
+notation "hvbox( - ⓓ term 55 T1. break term 55 T2 )"
non associative with precedence 55
for @{ 'SnAbbrNeg $T1 $T2 }.
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( + ⓓ term 55 T1 . break term 55 T2 )"
+notation "hvbox( + ⓓ term 55 T1. break term 55 T2 )"
non associative with precedence 55
for @{ 'SnAbbrPos $T1 $T2 }.
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( ⓛ { term 46 p } break term 55 T1 . break term 55 T2 )"
+notation "hvbox( ⓛ { term 46 p } break term 55 T1. break term 55 T2 )"
non associative with precedence 55
for @{ 'SnAbst $p $T1 $T2 }.
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( - ⓛ term 55 T1 . break term 55 T2 )"
+notation "hvbox( - ⓛ term 55 T1. break term 55 T2 )"
non associative with precedence 55
for @{ 'SnAbstNeg $T1 $T2 }.
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( + ⓛ term 55 T1 . break term 55 T2 )"
+notation "hvbox( + ⓛ term 55 T1. break term 55 T2 )"
non associative with precedence 55
for @{ 'SnAbstPos $T1 $T2 }.
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( ⓐ term 55 T1 . break term 55 T2 )"
+notation "hvbox( ⓐ term 55 T1. break term 55 T2 )"
non associative with precedence 55
for @{ 'SnAppl $T1 $T2 }.
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( ⓑ { term 46 p , break term 46 I } break term 55 T1 . break term 55 T )"
+notation "hvbox( ⓑ { term 46 p, break term 46 I } break term 55 T1. break term 55 T )"
non associative with precedence 55
for @{ 'SnBind2 $p $I $T1 $T }.
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( - ⓑ { term 46 I } break term 55 T1 . break term 55 T )"
+notation "hvbox( - ⓑ { term 46 I } break term 55 T1. break term 55 T )"
non associative with precedence 55
for @{ 'SnBind2Neg $I $T1 $T }.
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( + ⓑ { term 46 I } break term 55 T1 . break term 55 T )"
+notation "hvbox( + ⓑ { term 46 I } break term 55 T1. break term 55 T )"
non associative with precedence 55
for @{ 'SnBind2Pos $I $T1 $T }.
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( ⓝ term 55 T1 . break term 55 T2 )"
+notation "hvbox( ⓝ term 55 T1. break term 55 T2 )"
non associative with precedence 55
for @{ 'SnCast $T1 $T2 }.
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( ⓕ { term 46 I } break term 55 T1 . break term 55 T )"
+notation "hvbox( ⓕ { term 46 I } break term 55 T1. break term 55 T )"
non associative with precedence 55
for @{ 'SnFlat2 $I $T1 $T }.
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( ② term 55 T1 . break term 55 T )"
+notation "hvbox( ② term 55 T1. break term 55 T )"
non associative with precedence 55
for @{ 'SnItem2 $T1 $T }.
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( ② { term 46 I } break term 55 T1 . break term 55 T )"
+notation "hvbox( ② { term 46 I } break term 55 T1. break term 55 T )"
non associative with precedence 55
for @{ 'SnItem2 $I $T1 $T }.
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( ⓓ term 55 T . break term 55 L )"
+notation "hvbox( ⓓ term 55 T. break term 55 L )"
non associative with precedence 55
for @{ 'SnAbbr $T $L }.
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( ⓛ term 55 T . break term 55 L )"
+notation "hvbox( ⓛ term 55 T. break term 55 L )"
non associative with precedence 55
for @{ 'SnAbst $T $L }.
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( Ⓐ term 55 T1 . break term 55 T )"
+notation "hvbox( Ⓐ term 55 T1. break term 55 T )"
non associative with precedence 55
for @{ 'SnApplVector $T1 $T }.
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( ⓤ { term 46 I } . break term 55 L )"
+notation "hvbox( ⓤ { term 46 I }. break term 55 L )"
non associative with precedence 55
for @{ 'SnBind1 $I $L }.
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( ⓑ { term 46 I } break term 55 T . break term 55 L )"
+notation "hvbox( ⓑ { term 46 I } break term 55 T. break term 55 L )"
non associative with precedence 55
for @{ 'SnBind2 $I $T $L }.
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( ⓘ { term 46 I } . break term 55 L )"
+notation "hvbox( ⓘ { term 46 I }. break term 55 L )"
non associative with precedence 55
for @{ 'SnItem $I $L }.
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( ⓧ . term 55 L )"
+notation "hvbox( ⓧ. term 55 L )"
non associative with precedence 55
for @{ 'SnVoid $L }.
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( ♯ { term 46 L , break term 46 T } )"
+notation "hvbox( ♯ { term 46 L, break term 46 T } )"
non associative with precedence 90
for @{ 'Weight $L $T }.
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( ♯ { term 46 G , break term 46 L , break term 46 T } )"
+notation "hvbox( ♯ { term 46 G, break term 46 L, break term 46 T } )"
non associative with precedence 90
for @{ 'Weight $G $L $T }.
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( ⦃ term 46 G1, break term 46 L1, break term 46 T1 ⦄ ≽ [ break term 46 h ] ⦃ break term 46 G2, break term 46 L2 , break term 46 T2 ⦄ )"
+notation "hvbox( ⦃ term 46 G1, break term 46 L1, break term 46 T1 ⦄ ≽ [ break term 46 h ] ⦃ break term 46 G2, break term 46 L2, break term 46 T2 ⦄ )"
non associative with precedence 45
for @{ 'BTPRed $h $G1 $L1 $T1 $G2 $L2 $T2 }.
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( ⦃ term 46 G1, break term 46 L1, break term 46 T1 ⦄ ≻ [ break term 46 h, break term 46 o ] ⦃ break term 46 G2, break term 46 L2 , break term 46 T2 ⦄ )"
+notation "hvbox( ⦃ term 46 G1, break term 46 L1, break term 46 T1 ⦄ ≻ [ break term 46 h, break term 46 o ] ⦃ break term 46 G2, break term 46 L2, break term 46 T2 ⦄ )"
non associative with precedence 45
for @{ 'BTPRedProper $h $o $G1 $L1 $T1 $G2 $L2 $T2 }.
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( ⦃ term 46 G1, break term 46 L1, break term 46 T1 ⦄ ≥ [ break term 46 h, break term 46 o ] ⦃ break term 46 G2, break term 46 L2 , break term 46 T2 ⦄ )"
+notation "hvbox( ⦃ term 46 G1, break term 46 L1, break term 46 T1 ⦄ ≥ [ break term 46 h, break term 46 o ] ⦃ break term 46 G2, break term 46 L2, break term 46 T2 ⦄ )"
non associative with precedence 45
for @{ 'BTPRedStar $h $o $G1 $L1 $T1 $G2 $L2 $T2 }.
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( ⦃ term 46 G1, break term 46 L1, break term 46 T1 ⦄ ≥ ≥ [ break term 46 h, break term 46 o ] ⦃ break term 46 G2, break term 46 L2 , break term 46 T2 ⦄ )"
+notation "hvbox( ⦃ term 46 G1, break term 46 L1, break term 46 T1 ⦄ ≥ ≥ [ break term 46 h, break term 46 o ] ⦃ break term 46 G2, break term 46 L2, break term 46 T2 ⦄ )"
non associative with precedence 45
for @{ 'BTPRedStarAlt $h $o $G1 $L1 $T1 $G2 $L2 $T2 }.
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( ⦃ term 46 G , break term 46 L ⦄ ⊢ break term 46 T1 • * ⬌ * [ break term 46 h , break term 46 o , break term 46 n1 , break term 46 n2 ] break term 46 T2 )"
+notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ break term 46 T1 • * ⬌ * [ break term 46 h, break term 46 o, break term 46 n1, break term 46 n2 ] break term 46 T2 )"
non associative with precedence 45
for @{ 'DPConvStar $h $o $n1 $n2 $G $L $T1 $T2 }.
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( ⦃ term 46 G , break term 46 L ⦄ ⊢ break term 46 T1 • * ➡ * [ break term 46 h , break term 46 o , break term 46 n ] break term 46 T2 )"
+notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ break term 46 T1 • * ➡ * [ break term 46 h, break term 46 o, break term 46 n ] break term 46 T2 )"
non associative with precedence 45
for @{ 'DPRedStar $h $o $n $G $L $T1 $T2 }.
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( ⦃ term 46 G1, break term 46 L1, break term 46 T1 ⦄ >≡ [ break term 46 h, break term 46 o ] ⦃ break term 46 G2, break term 46 L2 , break term 46 T2 ⦄ )"
+notation "hvbox( ⦃ term 46 G1, break term 46 L1, break term 46 T1 ⦄ >≡ [ break term 46 h, break term 46 o ] ⦃ break term 46 G2, break term 46 L2, break term 46 T2 ⦄ )"
non associative with precedence 45
for @{ 'LazyBTPRedStarProper $h $o $G1 $L1 $T1 $G2 $L2 $T2 }.
+++ /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( T1 ≡ [ break term 46 h , break term 46 o ] break term 46 T2 )"
- non associative with precedence 45
- for @{ 'LazyEq $h $o $T1 $T2 }.
+++ /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( L ⊢ break term 46 T1 ≡ [ break term 46 h , break term 46 o ] break term 46 T2 )"
- non associative with precedence 45
- for @{ 'LazyEq $h $o $L $T1 $T2 }.
+++ /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( L1 ≡ [ break term 46 h , break term 46 o , break term 46 T ] break term 46 L2 )"
- non associative with precedence 45
- for @{ 'LazyEqSn $h $o $T $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( ⦃ term 46 G1, break term 46 L1, break term 46 T1 ⦄ ≡ [ break term 46 h , break term 46 o ] ⦃ break term 46 G2, break term 46 L2 , break term 46 T2 ⦄ )"
- non associative with precedence 45
- for @{ 'LazyEqSn $h $o $G1 $L1 $T1 $G2 $L2 $T2 }.
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( ⦃ term 46 G , break term 46 L ⦄ ⊢ break term 46 T ¡ [ break term 46 h, break term 46 o ] )"
+notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ break term 46 T ¡ [ break term 46 h, break term 46 o ] )"
non associative with precedence 45
for @{ 'NativeValid $h $o $G $L $T }.
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( ⦃ term 46 G , break term 46 L ⦄ ⊢ break term 46 T ¡ [ break term 46 h , break term 46 o , break term 46 d ] )"
+notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ break term 46 T ¡ [ break term 46 h, break term 46 o, break term 46 d ] )"
non associative with precedence 45
for @{ 'NativeValid $h $o $d $G $L $T }.
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( ⦃ term 46 G, break term 46 L1 ⦄ ⊢ ➡ [ break term 46 h , break term 46 T ] break term 46 L2 )"
+notation "hvbox( ⦃ term 46 G, break term 46 L1 ⦄ ⊢ ➡ [ break term 46 h, break term 46 T ] break term 46 L2 )"
non associative with precedence 45
for @{ 'PRedSn $h $T $G $L1 $L2 }.
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( ⦃ term 46 G , break term 46 L1 ⦄ ⊢ ➡* break term 46 L2 )"
+notation "hvbox( ⦃ term 46 G, break term 46 L1 ⦄ ⊢ ➡* break term 46 L2 )"
non associative with precedence 45
for @{ 'PRedSnStar $G $L1 $L2 }.
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( ⦃ term 46 G, break term 46 L1 ⦄ ⊢ ➡ * [ break term 46 h , break term 46 o ] break term 46 L2 )"
+notation "hvbox( ⦃ term 46 G, break term 46 L1 ⦄ ⊢ ➡ * [ break term 46 h, break term 46 o ] break term 46 L2 )"
non associative with precedence 45
for @{ 'PRedSnStar $h $o $G $L1 $L2 }.
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( ⦃ term 46 G , term 46 L ⦄ ⊢ break term 46 T1 ➡ * break term 46 T2 )"
+notation "hvbox( ⦃ term 46 G, term 46 L ⦄ ⊢ break term 46 T1 ➡ * break term 46 T2 )"
non associative with precedence 45
for @{ 'PRedStar $G $L $T1 $T2 }.
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ break term 46 T1 ➡ * [ break term 46 h , break term 46 o ] break term 46 T2 )"
+notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ break term 46 T1 ➡ * [ break term 46 h, break term 46 o ] break term 46 T2 )"
non associative with precedence 45
for @{ 'PRedStar $h $o $G $L $T1 $T2 }.
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ break term 46 T1 ⬈ [ break term 46 Rt , break term 46 c , break term 46 h ] break term 46 T2 )"
+notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ break term 46 T1 ⬈ [ break term 46 Rt, break term 46 c, break term 46 h ] break term 46 T2 )"
non associative with precedence 45
for @{ 'PRedTy $Rt $c $h $G $L $T1 $T2 }.
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ ⬈ [ break term 46 h , break term 46 o ] 𝐍 ⦃ break term 46 T ⦄ )"
+notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ ⬈ [ break term 46 h, break term 46 o ] 𝐍 ⦃ break term 46 T ⦄ )"
non associative with precedence 45
for @{ 'PRedTyNormal $h $o $G $L $T }.
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( ⦃ term 46 G, break term 46 L1 ⦄ ⊢ ⬈ [ break term 46 h , break term 46 T ] break term 46 L2 )"
+notation "hvbox( ⦃ term 46 G, break term 46 L1 ⦄ ⊢ ⬈ [ break term 46 h, break term 46 T ] break term 46 L2 )"
non associative with precedence 45
for @{ 'PRedTySn $h $T $G $L1 $L2 }.
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( ⦃ term 46 G, break term 46 L1 ⦄ ⊢ ⬈ * [ break term 46 h , break term 46 T ] break term 46 L2 )"
+notation "hvbox( ⦃ term 46 G, break term 46 L1 ⦄ ⊢ ⬈ * [ break term 46 h, break term 46 T ] break term 46 L2 )"
non associative with precedence 45
for @{ 'PRedTySnStar $h $T $G $L1 $L2 }.
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( G ⊢ ⬈ * [ break term 46 h , break term 46 o , break term 46 T ] 𝐒 ⦃ break term 46 L ⦄ )"
+notation "hvbox( G ⊢ ⬈ * [ break term 46 h, break term 46 o, break term 46 T ] 𝐒 ⦃ break term 46 L ⦄ )"
non associative with precedence 45
for @{ 'PRedTySNStrong $h $o $T $G $L }.
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ ⬈ * [ break term 46 h , break term 46 o ] 𝐒 ⦃ break term 46 T ⦄ )"
+notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ ⬈ * [ break term 46 h, break term 46 o ] 𝐒 ⦃ break term 46 T ⦄ )"
non associative with precedence 45
for @{ 'PRedTyStrong $h $o $G $L $T }.
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( ⬇ * [ term 46 b , break term 46 f ] break term 46 L1 ≡ break term 46 L2 )"
+notation "hvbox( ⬇ * [ term 46 b, break term 46 f ] break term 46 L1 ≡ break term 46 L2 )"
non associative with precedence 45
for @{ 'RDropStar $b $f $L1 $L2 }.
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( L1 ⪤ * [ break term 46 R , break term 46 T ] break term 46 L2 )"
+notation "hvbox( L1 ⪤ * [ break term 46 R, break term 46 T ] break term 46 L2 )"
non associative with precedence 45
for @{ 'RelationStar $R $T $L1 $L2 }.
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( L1 ⪤ * [ break term 46 R1 , break term 46 R2 , break term 46 f ] break term 46 L2 )"
+notation "hvbox( L1 ⪤ * [ break term 46 R1, break term 46 R2, break term 46 f ] break term 46 L2 )"
non associative with precedence 45
for @{ 'RelationStar $R1 $R2 $f $L1 $L2 }.
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( L1 ⪤ * * [ break term 46 R , break term 46 T ] break term 46 L2 )"
+notation "hvbox( L1 ⪤ * * [ break term 46 R, break term 46 T ] break term 46 L2 )"
non associative with precedence 45
for @{ 'RelationStarStar $R $T $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( T1 ≛ [ break term 46 h, break term 46 o ] break term 46 T2 )"
+ non associative with precedence 45
+ for @{ 'StarEq $h $o $T1 $T2 }.
--- /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( L ⊢ break term 46 T1 ≛ [ break term 46 h, break term 46 o ] break term 46 T2 )"
+ non associative with precedence 45
+ for @{ 'StarEq $h $o $L $T1 $T2 }.
--- /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( L1 ≛ [ break term 46 h, break term 46 o, break term 46 T ] break term 46 L2 )"
+ non associative with precedence 45
+ for @{ 'StarEqSn $h $o $T $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( ⦃ term 46 G1, break term 46 L1, break term 46 T1 ⦄ ≛ [ break term 46 h, break term 46 o ] ⦃ break term 46 G2, break term 46 L2, break term 46 T2 ⦄ )"
+ non associative with precedence 45
+ for @{ 'StarEqSn $h $o $G1 $L1 $T1 $G2 $L2 $T2 }.
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( ⦃ term 46 G1, break term 46 L1, break term 46 T1 ⦄ ⊐ ⦃ break term 46 G2, break term 46 L2 , break term 46 T2 ⦄ )"
+notation "hvbox( ⦃ term 46 G1, break term 46 L1, break term 46 T1 ⦄ ⊐ ⦃ break term 46 G2, break term 46 L2, break term 46 T2 ⦄ )"
non associative with precedence 45
for @{ 'SupTerm $G1 $L1 $T1 $G2 $L2 $T2 }.
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( ⦃ term 46 G1, break term 46 L1, break term 46 T1 ⦄ ⊐ [ break term 46 b ] ⦃ break term 46 G2, break term 46 L2 , break term 46 T2 ⦄ )"
+notation "hvbox( ⦃ term 46 G1, break term 46 L1, break term 46 T1 ⦄ ⊐ [ break term 46 b ] ⦃ break term 46 G2, break term 46 L2, break term 46 T2 ⦄ )"
non associative with precedence 45
for @{ 'SupTerm $b $G1 $L1 $T1 $G2 $L2 $T2 }.
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( ⦃ term 46 G1, break term 46 L1, break term 46 T1 ⦄ ⊐⸮ ⦃ break term 46 G2, break term 46 L2 , break term 46 T2 ⦄ )"
+notation "hvbox( ⦃ term 46 G1, break term 46 L1, break term 46 T1 ⦄ ⊐⸮ ⦃ break term 46 G2, break term 46 L2, break term 46 T2 ⦄ )"
non associative with precedence 45
for @{ 'SupTermOpt $G1 $L1 $T1 $G2 $L2 $T2 }.
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( ⦃ term 46 G1, break term 46 L1, break term 46 T1 ⦄ ⊐⸮ [ break term 46 b ] ⦃ break term 46 G2, break term 46 L2 , break term 46 T2 ⦄ )"
+notation "hvbox( ⦃ term 46 G1, break term 46 L1, break term 46 T1 ⦄ ⊐⸮ [ break term 46 b ] ⦃ break term 46 G2, break term 46 L2, break term 46 T2 ⦄ )"
non associative with precedence 45
for @{ 'SupTermOpt $b $G1 $L1 $T1 $G2 $L2 $T2 }.
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( ⦃ term 46 G1, term 46 L1, break term 46 T1 ⦄ ⊐ + ⦃ break term 46 G2, term 46 L2 , break term 46 T2 ⦄ )"
+notation "hvbox( ⦃ term 46 G1, term 46 L1, break term 46 T1 ⦄ ⊐ + ⦃ break term 46 G2, term 46 L2, break term 46 T2 ⦄ )"
non associative with precedence 45
for @{ 'SupTermPlus $G1 $L1 $T1 $G2 $L2 $T2 }.
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( ⦃ term 46 G1, term 46 L1, break term 46 T1 ⦄ ⊐ + [ break term 46 b ] ⦃ break term 46 G2, term 46 L2 , break term 46 T2 ⦄ )"
+notation "hvbox( ⦃ term 46 G1, term 46 L1, break term 46 T1 ⦄ ⊐ + [ break term 46 b ] ⦃ break term 46 G2, term 46 L2, break term 46 T2 ⦄ )"
non associative with precedence 45
for @{ 'SupTermPlus $b $G1 $L1 $T1 $G2 $L2 $T2 }.
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( ⦃ term 46 G1, term 46 L1, break term 46 T1 ⦄ ⊐ * ⦃ break term 46 G2, break term 46 L2 , break term 46 T2 ⦄ )"
+notation "hvbox( ⦃ term 46 G1, term 46 L1, break term 46 T1 ⦄ ⊐ * ⦃ break term 46 G2, break term 46 L2, break term 46 T2 ⦄ )"
non associative with precedence 45
for @{ 'SupTermStar $G1 $L1 $T1 $G2 $L2 $T2 }.
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( ⦃ term 46 G1, term 46 L1, break term 46 T1 ⦄ ⊐ * [ break term 46 b ] ⦃ break term 46 G2, break term 46 L2 , break term 46 T2 ⦄ )"
+notation "hvbox( ⦃ term 46 G1, term 46 L1, break term 46 T1 ⦄ ⊐ * [ break term 46 b ] ⦃ break term 46 G2, break term 46 L2, break term 46 T2 ⦄ )"
non associative with precedence 45
for @{ 'SupTermStar $b $G1 $L1 $T1 $G2 $L2 $T2 }.
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( T1 ⩳ [ break term 46 h , break term 46 o ] break term 46 T2 )"
+notation "hvbox( T1 ⩳ [ break term 46 h, break term 46 o ] break term 46 T2 )"
non associative with precedence 45
for @{ 'TopIso $h $o $T1 $T2 }.
(* Inversion lemmas with normal terms ***************************************)
lemma cpxs_inv_cnx1: ∀h,o,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 → ⦃G, L⦄ ⊢ ⬈[h, o] 𝐍⦃T1⦄ →
- T1 â\89¡[h, o] T2.
+ T1 â\89\9b[h, o] T2.
#h #o #G #L #T1 #T2 #H @(cpxs_ind_dx … H) -T1
/5 width=8 by cnx_tdeq_trans, tdeq_trans/
qed-.
(* Note: a proof based on fqu_cpx_trans_ntdeq might exist *)
lemma fqu_cpxs_trans_ntdeq: ∀h,o,b,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐[b] ⦃G2, L2, T2⦄ →
- â\88\80U2. â¦\83G2, L2â¦\84 â\8a¢ T2 â¬\88*[h] U2 â\86\92 (T2 â\89¡[h, o] U2 → ⊥) →
- â\88\83â\88\83U1. â¦\83G1, L1â¦\84 â\8a¢ T1 â¬\88*[h] U1 & T1 â\89¡[h, o] U1 → ⊥ & ⦃G1, L1, U1⦄ ⊐[b] ⦃G2, L2, U2⦄.
+ â\88\80U2. â¦\83G2, L2â¦\84 â\8a¢ T2 â¬\88*[h] U2 â\86\92 (T2 â\89\9b[h, o] U2 → ⊥) →
+ â\88\83â\88\83U1. â¦\83G1, L1â¦\84 â\8a¢ T1 â¬\88*[h] U1 & T1 â\89\9b[h, o] U1 → ⊥ & ⦃G1, L1, U1⦄ ⊐[b] ⦃G2, L2, U2⦄.
#h #o #b #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2
[ #I #G #L #V1 #V2 #HV12 #_ elim (lifts_total V2 𝐔❴1❵)
#U2 #HVU2 @(ex3_intro … U2)
qed-.
lemma fquq_cpxs_trans_ntdeq: ∀h,o,b,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐⸮[b] ⦃G2, L2, T2⦄ →
- â\88\80U2. â¦\83G2, L2â¦\84 â\8a¢ T2 â¬\88*[h] U2 â\86\92 (T2 â\89¡[h, o] U2 → ⊥) →
- â\88\83â\88\83U1. â¦\83G1, L1â¦\84 â\8a¢ T1 â¬\88*[h] U1 & T1 â\89¡[h, o] U1 → ⊥ & ⦃G1, L1, U1⦄ ⊐⸮[b] ⦃G2, L2, U2⦄.
+ â\88\80U2. â¦\83G2, L2â¦\84 â\8a¢ T2 â¬\88*[h] U2 â\86\92 (T2 â\89\9b[h, o] U2 → ⊥) →
+ â\88\83â\88\83U1. â¦\83G1, L1â¦\84 â\8a¢ T1 â¬\88*[h] U1 & T1 â\89\9b[h, o] U1 → ⊥ & ⦃G1, L1, U1⦄ ⊐⸮[b] ⦃G2, L2, U2⦄.
#h #o #b #G1 #G2 #L1 #L2 #T1 #T2 #H12 elim H12 -H12
[ #H12 #U2 #HTU2 #H elim (fqu_cpxs_trans_ntdeq … H12 … HTU2 H) -T2
/3 width=4 by fqu_fquq, ex3_intro/
qed-.
lemma fqup_cpxs_trans_ntdeq: ∀h,o,b,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐+[b] ⦃G2, L2, T2⦄ →
- â\88\80U2. â¦\83G2, L2â¦\84 â\8a¢ T2 â¬\88*[h] U2 â\86\92 (T2 â\89¡[h, o] U2 → ⊥) →
- â\88\83â\88\83U1. â¦\83G1, L1â¦\84 â\8a¢ T1 â¬\88*[h] U1 & T1 â\89¡[h, o] U1 → ⊥ & ⦃G1, L1, U1⦄ ⊐+[b] ⦃G2, L2, U2⦄.
+ â\88\80U2. â¦\83G2, L2â¦\84 â\8a¢ T2 â¬\88*[h] U2 â\86\92 (T2 â\89\9b[h, o] U2 → ⊥) →
+ â\88\83â\88\83U1. â¦\83G1, L1â¦\84 â\8a¢ T1 â¬\88*[h] U1 & T1 â\89\9b[h, o] U1 → ⊥ & ⦃G1, L1, U1⦄ ⊐+[b] ⦃G2, L2, U2⦄.
#h #o #b #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind_dx … H) -G1 -L1 -T1
[ #G1 #L1 #T1 #H12 #U2 #HTU2 #H elim (fqu_cpxs_trans_ntdeq … H12 … HTU2 H) -T2
/3 width=4 by fqu_fqup, ex3_intro/
qed-.
lemma fqus_cpxs_trans_ntdeq: ∀h,o,b,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐*[b] ⦃G2, L2, T2⦄ →
- â\88\80U2. â¦\83G2, L2â¦\84 â\8a¢ T2 â¬\88*[h] U2 â\86\92 (T2 â\89¡[h, o] U2 → ⊥) →
- â\88\83â\88\83U1. â¦\83G1, L1â¦\84 â\8a¢ T1 â¬\88*[h] U1 & T1 â\89¡[h, o] U1 → ⊥ & ⦃G1, L1, U1⦄ ⊐*[b] ⦃G2, L2, U2⦄.
+ â\88\80U2. â¦\83G2, L2â¦\84 â\8a¢ T2 â¬\88*[h] U2 â\86\92 (T2 â\89\9b[h, o] U2 → ⊥) →
+ â\88\83â\88\83U1. â¦\83G1, L1â¦\84 â\8a¢ T1 â¬\88*[h] U1 & T1 â\89\9b[h, o] U1 → ⊥ & ⦃G1, L1, U1⦄ ⊐*[b] ⦃G2, L2, U2⦄.
#h #o #b #G1 #G2 #L1 #L2 #T1 #T2 #H12 #U2 #HTU2 #H elim (fqus_inv_fqup … H12) -H12
[ #H12 elim (fqup_cpxs_trans_ntdeq … H12 … HTU2 H) -T2
/3 width=4 by fqup_fqus, ex3_intro/
(* Basic_2A1: was just: lleq_cpxs_trans *)
lemma lfdeq_cpxs_trans: ∀h,o,G,L0,T0,T1. ⦃G, L0⦄ ⊢ T0 ⬈*[h] T1 →
- â\88\80L2. L2 â\89¡[h, o, T0] L0 →
- â\88\83â\88\83T. â¦\83G, L2â¦\84 â\8a¢ T0 â¬\88*[h] T & T â\89¡[h, o] T1.
+ â\88\80L2. L2 â\89\9b[h, o, T0] L0 →
+ â\88\83â\88\83T. â¦\83G, L2â¦\84 â\8a¢ T0 â¬\88*[h] T & T â\89\9b[h, o] T1.
#h #o #G #L0 #T0 #T1 #H @(cpxs_ind_dx … H) -T0 /2 width=3 by ex2_intro/
#T0 #T #HT0 #_ #IH #L2 #HL2
elim (lfdeq_cpx_trans … HL2 … HT0) #U1 #H1 #H2
(* Basic_2A1: was just: cpxs_lleq_conf *)
lemma cpxs_lfdeq_trans: ∀h,o,G,L0,T0,T1. ⦃G, L0⦄ ⊢ T0 ⬈*[h] T1 →
- â\88\80L2. L0 â\89¡[h, o, T0] L2 →
- â\88\83â\88\83T. â¦\83G, L2â¦\84 â\8a¢ T0 â¬\88*[h] T & T â\89¡[h, o] T1.
+ â\88\80L2. L0 â\89\9b[h, o, T0] L2 →
+ â\88\83â\88\83T. â¦\83G, L2â¦\84 â\8a¢ T0 â¬\88*[h] T & T â\89\9b[h, o] T1.
/3 width=3 by lfdeq_cpxs_trans, lfdeq_sym/ qed-.
(* Basic_2A1: was just: cpxs_lleq_conf_dx *)
lemma cpxs_lfdeq_conf_dx: ∀h,o,G,L2,T1,T2. ⦃G, L2⦄ ⊢ T1 ⬈*[h] T2 →
- â\88\80L1. L1 â\89¡[h, o, T1] L2 â\86\92 L1 â\89¡[h, o, T2] L2.
+ â\88\80L1. L1 â\89\9b[h, o, T1] L2 â\86\92 L1 â\89\9b[h, o, T2] L2.
#h #o #G #L2 #T1 #T2 #H @(cpxs_ind … H) -T2 /3 width=6 by cpx_lfdeq_conf_dx/
qed-.
(* Basic_2A1: was just: lleq_conf_sn *)
lemma cpxs_lfdeq_conf_sn: ∀h,o,G,L1,T1,T2. ⦃G, L1⦄ ⊢ T1 ⬈*[h] T2 →
- â\88\80L2. L1 â\89¡[h, o, T1] L2 â\86\92 L1 â\89¡[h, o, T2] L2.
+ â\88\80L2. L1 â\89\9b[h, o, T1] L2 â\86\92 L1 â\89\9b[h, o, T2] L2.
/4 width=6 by cpxs_lfdeq_conf_dx, lfdeq_sym/ qed-.
(* Properties with degree-based equivalence for terms ***********************)
-lemma tdeq_cpxs_trans: â\88\80h,o,U1,T1. U1 â\89¡[h, o] T1 → ∀G,L,T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 →
- â\88\83â\88\83U2. â¦\83G, Lâ¦\84 â\8a¢ U1 â¬\88*[h] U2 & U2 â\89¡[h, o] T2.
+lemma tdeq_cpxs_trans: â\88\80h,o,U1,T1. U1 â\89\9b[h, o] T1 → ∀G,L,T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 →
+ â\88\83â\88\83U2. â¦\83G, Lâ¦\84 â\8a¢ U1 â¬\88*[h] U2 & U2 â\89\9b[h, o] T2.
#h #o #U1 #T1 #HUT1 #G #L #T2 #HT12 @(cpxs_ind … HT12) -T2 /2 width=3 by ex2_intro/
#T #T2 #_ #HT2 * #U #HU1 #HUT elim (tdeq_cpx_trans … HUT … HT2) -T -T1
/3 width=3 by ex2_intro, cpxs_strap1/
qed-.
(* Note: this requires tdeq to be symmetric *)
-lemma cpxs_tdneq_inv_step_sn: â\88\80h,o,G,L,T1,T2. â¦\83G, Lâ¦\84 â\8a¢ T1 â¬\88*[h] T2 â\86\92 (T1 â\89¡[h, o] T2 → ⊥) →
- â\88\83â\88\83T,T0. â¦\83G, Lâ¦\84 â\8a¢ T1 â¬\88[h] T & T1 â\89¡[h, o] T â\86\92 â\8a¥ & â¦\83G, Lâ¦\84 â\8a¢ T â¬\88*[h] T0 & T0 â\89¡[h, o] T2.
+lemma cpxs_tdneq_inv_step_sn: â\88\80h,o,G,L,T1,T2. â¦\83G, Lâ¦\84 â\8a¢ T1 â¬\88*[h] T2 â\86\92 (T1 â\89\9b[h, o] T2 → ⊥) →
+ â\88\83â\88\83T,T0. â¦\83G, Lâ¦\84 â\8a¢ T1 â¬\88[h] T & T1 â\89\9b[h, o] T â\86\92 â\8a¥ & â¦\83G, Lâ¦\84 â\8a¢ T â¬\88*[h] T0 & T0 â\89\9b[h, o] T2.
#h #o #G #L #T1 #T2 #H @(cpxs_ind_dx … H) -T1
[ #H elim H -H //
| #T1 #T #H1 #H2 #IH #Hn12 elim (tdeq_dec h o T1 T) #H destruct
lemma csx_ind: ∀h,o,G,L. ∀R:predicate term.
(∀T1. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T1⦄ →
- (â\88\80T2. â¦\83G, Lâ¦\84 â\8a¢ T1 â¬\88[h] T2 â\86\92 (T1 â\89¡[h, o] T2 → ⊥) → R T2) →
+ (â\88\80T2. â¦\83G, Lâ¦\84 â\8a¢ T1 â¬\88[h] T2 â\86\92 (T1 â\89\9b[h, o] T2 → ⊥) → R T2) →
R T1
) →
∀T. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄ → R T.
(* Basic_1: was just: sn3_pr2_intro *)
lemma csx_intro: ∀h,o,G,L,T1.
- (â\88\80T2. â¦\83G, Lâ¦\84 â\8a¢ T1 â¬\88[h] T2 â\86\92 (T1 â\89¡[h, o] T2 → ⊥) → ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T2⦄) →
+ (â\88\80T2. â¦\83G, Lâ¦\84 â\8a¢ T1 â¬\88[h] T2 â\86\92 (T1 â\89\9b[h, o] T2 → ⊥) → ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T2⦄) →
⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T1⦄.
/4 width=1 by SN_intro/ qed.
fact aaa_ind_csx_aux: ∀h,o,G,L,A. ∀R:predicate term.
(∀T1. ⦃G, L⦄ ⊢ T1 ⁝ A →
- (â\88\80T2. â¦\83G, Lâ¦\84 â\8a¢ T1 â¬\88[h] T2 â\86\92 (T1 â\89¡[h, o] T2 → ⊥) → R T2) → R T1
+ (â\88\80T2. â¦\83G, Lâ¦\84 â\8a¢ T1 â¬\88[h] T2 â\86\92 (T1 â\89\9b[h, o] T2 → ⊥) → R T2) → R T1
) →
∀T. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄ → ⦃G, L⦄ ⊢ T ⁝ A → R T.
#h #o #G #L #A #R #IH #T #H @(csx_ind … H) -T /4 width=5 by cpx_aaa_conf/
lemma aaa_ind_csx: ∀h,o,G,L,A. ∀R:predicate term.
(∀T1. ⦃G, L⦄ ⊢ T1 ⁝ A →
- (â\88\80T2. â¦\83G, Lâ¦\84 â\8a¢ T1 â¬\88[h] T2 â\86\92 (T1 â\89¡[h, o] T2 → ⊥) → R T2) → R T1
+ (â\88\80T2. â¦\83G, Lâ¦\84 â\8a¢ T1 â¬\88[h] T2 â\86\92 (T1 â\89\9b[h, o] T2 → ⊥) → R T2) → R T1
) →
∀T. ⦃G, L⦄ ⊢ T ⁝ A → R T.
/5 width=9 by aaa_ind_csx_aux, aaa_csx/ qed-.
fact aaa_ind_csx_cpxs_aux: ∀h,o,G,L,A. ∀R:predicate term.
(∀T1. ⦃G, L⦄ ⊢ T1 ⁝ A →
- (â\88\80T2. â¦\83G, Lâ¦\84 â\8a¢ T1 â¬\88*[h] T2 â\86\92 (T1 â\89¡[h, o] T2 → ⊥) → R T2) → R T1
+ (â\88\80T2. â¦\83G, Lâ¦\84 â\8a¢ T1 â¬\88*[h] T2 â\86\92 (T1 â\89\9b[h, o] T2 → ⊥) → R T2) → R T1
) →
∀T. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄ → ⦃G, L⦄ ⊢ T ⁝ A → R T.
#h #o #G #L #A #R #IH #T #H @(csx_ind_cpxs … H) -T /4 width=5 by cpxs_aaa_conf/
(* Basic_2A1: was: aaa_ind_csx_alt *)
lemma aaa_ind_csx_cpxs: ∀h,o,G,L,A. ∀R:predicate term.
(∀T1. ⦃G, L⦄ ⊢ T1 ⁝ A →
- (â\88\80T2. â¦\83G, Lâ¦\84 â\8a¢ T1 â¬\88*[h] T2 â\86\92 (T1 â\89¡[h, o] T2 → ⊥) → R T2) → R T1
+ (â\88\80T2. â¦\83G, Lâ¦\84 â\8a¢ T1 â¬\88*[h] T2 â\86\92 (T1 â\89\9b[h, o] T2 → ⊥) → R T2) → R T1
) →
∀T. ⦃G, L⦄ ⊢ T ⁝ A → R T.
/5 width=9 by aaa_ind_csx_cpxs_aux, aaa_csx/ qed-.
(* Basic_1: was just: sn3_intro *)
lemma csx_intro_cpxs: ∀h,o,G,L,T1.
- (â\88\80T2. â¦\83G, Lâ¦\84 â\8a¢ T1 â¬\88*[h] T2 â\86\92 (T1 â\89¡[h, o] T2 → ⊥) → ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T2⦄) →
+ (â\88\80T2. â¦\83G, Lâ¦\84 â\8a¢ T1 â¬\88*[h] T2 â\86\92 (T1 â\89\9b[h, o] T2 → ⊥) → ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T2⦄) →
⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T1⦄.
/4 width=1 by cpx_cpxs, csx_intro/ qed-.
lemma csx_ind_cpxs_tdeq: ∀h,o,G,L. ∀R:predicate term.
(∀T1. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T1⦄ →
- (â\88\80T2. â¦\83G, Lâ¦\84 â\8a¢ T1 â¬\88*[h] T2 â\86\92 (T1 â\89¡[h, o] T2 → ⊥) → R T2) → R T1
+ (â\88\80T2. â¦\83G, Lâ¦\84 â\8a¢ T1 â¬\88*[h] T2 â\86\92 (T1 â\89\9b[h, o] T2 → ⊥) → R T2) → R T1
) →
∀T1. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T1⦄ →
- â\88\80T0. â¦\83G, Lâ¦\84 â\8a¢ T1 â¬\88*[h] T0 â\86\92 â\88\80T2. T0 â\89¡[h, o] T2 → R T2.
+ â\88\80T0. â¦\83G, Lâ¦\84 â\8a¢ T1 â¬\88*[h] T0 â\86\92 â\88\80T2. T0 â\89\9b[h, o] T2 → R T2.
#h #o #G #L #R #IH #T1 #H @(csx_ind … H) -T1
#T1 #HT1 #IH1 #T0 #HT10 #T2 #HT02
@IH -IH /3 width=3 by csx_cpxs_trans, csx_tdeq_trans/ -HT1 #V2 #HTV2 #HnTV2
(* Basic_2A1: was: csx_ind_alt *)
lemma csx_ind_cpxs: ∀h,o,G,L. ∀R:predicate term.
(∀T1. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T1⦄ →
- (â\88\80T2. â¦\83G, Lâ¦\84 â\8a¢ T1 â¬\88*[h] T2 â\86\92 (T1 â\89¡[h, o] T2 → ⊥) → R T2) → R T1
+ (â\88\80T2. â¦\83G, Lâ¦\84 â\8a¢ T1 â¬\88*[h] T2 â\86\92 (T1 â\89\9b[h, o] T2 → ⊥) → R T2) → R T1
) →
∀T. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄ → R T.
#h #o #G #L #R #IH #T #HT
(* Advanced properties ******************************************************)
lemma csx_tdeq_trans: ∀h,o,G,L,T1. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T1⦄ →
- â\88\80T2. T1 â\89¡[h, o] T2 → ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T2⦄.
+ â\88\80T2. T1 â\89\9b[h, o] T2 → ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T2⦄.
#h #o #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/
(* Basic_2A1: uses: csx_lleq_conf *)
lemma csx_lfdeq_conf: ∀h,o,G,L1,T. ⦃G, L1⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄ →
- â\88\80L2. L1 â\89¡[h, o, T] L2 → ⦃G, L2⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄.
+ â\88\80L2. L1 â\89\9b[h, o, T] L2 → ⦃G, L2⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄.
#h #o #G #L1 #T #H
@(csx_ind … H) -T #T1 #_ #IH #L2 #HL12
@csx_intro #T2 #HT12 #HnT12
qed-.
(* Basic_2A1: uses: csx_lleq_conf *)
-lemma csx_lfdeq_trans: â\88\80h,o,L1,L2,T. L1 â\89¡[h, o, T] L2 →
+lemma csx_lfdeq_trans: â\88\80h,o,L1,L2,T. L1 â\89\9b[h, o, T] L2 →
∀G. ⦃G, L2⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄ → ⦃G, L1⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄.
/3 width=3 by csx_lfdeq_conf, lfdeq_sym/ qed-.
(* Properties with simple terms *********************************************)
lemma csx_appl_simple: ∀h,o,G,L,V. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃V⦄ → ∀T1.
- (â\88\80T2. â¦\83G, Lâ¦\84 â\8a¢ T1 â¬\88[h] T2 â\86\92 (T1 â\89¡[h, o] T2 → ⊥) → ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃ⓐV.T2⦄) →
+ (â\88\80T2. â¦\83G, Lâ¦\84 â\8a¢ T1 â¬\88[h] T2 â\86\92 (T1 â\89\9b[h, o] T2 → ⊥) → ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃ⓐV.T2⦄) →
𝐒⦃T1⦄ → ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃ⓐV.T1⦄.
#h #o #G #L #V #H @(csx_ind … H) -V
#V #_ #IHV #T1 #IHT1 #HT1
(* Basic properties *********************************************************)
lemma fpb_fpbg: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≻[h, o] ⦃G2, L2, T2⦄ →
- â¦\83G1, L1, T1â¦\84 >â\89¡[h, o] ⦃G2, L2, T2⦄.
+ â¦\83G1, L1, T1â¦\84 >â\89\9b[h, o] ⦃G2, L2, T2⦄.
/2 width=5 by ex2_3_intro/ qed.
lemma fpbg_fpbq_trans: ∀h,o,G1,G,G2,L1,L,L2,T1,T,T2.
- â¦\83G1, L1, T1â¦\84 >â\89¡[h, o] ⦃G, L, T⦄ → ⦃G, L, T⦄ ≽[h, o] ⦃G2, L2, T2⦄ →
- â¦\83G1, L1, T1â¦\84 >â\89¡[h, o] ⦃G2, L2, T2⦄.
+ â¦\83G1, L1, T1â¦\84 >â\89\9b[h, o] ⦃G, L, T⦄ → ⦃G, L, T⦄ ≽[h, o] ⦃G2, L2, T2⦄ →
+ â¦\83G1, L1, T1â¦\84 >â\89\9b[h, o] ⦃G2, L2, T2⦄.
#h #o #G1 #G #G2 #L1 #L #L2 #T1 #T #T2 *
/3 width=9 by fpbs_strap1, ex2_3_intro/
qed-.
(* Properties on lazy equivalence for closures ******************************)
-lemma fpbg_fleq_trans: â\88\80h,o,G1,G,L1,L,T1,T. â¦\83G1, L1, T1â¦\84 >â\89¡[h, o] ⦃G, L, T⦄ →
- â\88\80G2,L2,T2. â¦\83G, L, Tâ¦\84 â\89¡[0] â¦\83G2, L2, T2â¦\84 â\86\92 â¦\83G1, L1, T1â¦\84 >â\89¡[h, o] ⦃G2, L2, T2⦄.
+lemma fpbg_fleq_trans: â\88\80h,o,G1,G,L1,L,T1,T. â¦\83G1, L1, T1â¦\84 >â\89\9b[h, o] ⦃G, L, T⦄ →
+ â\88\80G2,L2,T2. â¦\83G, L, Tâ¦\84 â\89¡[0] â¦\83G2, L2, T2â¦\84 â\86\92 â¦\83G1, L1, T1â¦\84 >â\89\9b[h, o] ⦃G2, L2, T2⦄.
/3 width=5 by fpbg_fpbq_trans, fleq_fpbq/ qed-.
-lemma fleq_fpbg_trans: â\88\80h,o,G,G2,L,L2,T,T2. â¦\83G, L, Tâ¦\84 >â\89¡[h, o] ⦃G2, L2, T2⦄ →
- â\88\80G1,L1,T1. â¦\83G1, L1, T1â¦\84 â\89¡[0] â¦\83G, L, Tâ¦\84 â\86\92 â¦\83G1, L1, T1â¦\84 >â\89¡[h, o] ⦃G2, L2, T2⦄.
+lemma fleq_fpbg_trans: â\88\80h,o,G,G2,L,L2,T,T2. â¦\83G, L, Tâ¦\84 >â\89\9b[h, o] ⦃G2, L2, T2⦄ →
+ â\88\80G1,L1,T1. â¦\83G1, L1, T1â¦\84 â\89¡[0] â¦\83G, L, Tâ¦\84 â\86\92 â¦\83G1, L1, T1â¦\84 >â\89\9b[h, o] ⦃G2, L2, T2⦄.
#h #o #G #G2 #L #L2 #T #T2 * #G0 #L0 #T0 #H0 #H02 #G1 #L1 #T1 #H1
elim (fleq_fpb_trans … H1 … H0) -G -L -T
/4 width=9 by fpbs_strap2, fleq_fpbq, ex2_3_intro/
qed.
lemma fpbg_fwd_fpbs: ∀h,o,G1,G2,L1,L2,T1,T2.
- â¦\83G1, L1, T1â¦\84 >â\89¡[h,o] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄.
+ â¦\83G1, L1, T1â¦\84 >â\89\9b[h,o] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄.
#h #o #G1 #G2 #L1 #L2 #T1 #T2 *
/3 width=5 by fpbs_strap2, fpb_fpbq/
qed-.
lemma fpbs_fpbg: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄ →
⦃G1, L1, T1⦄ ≡[0] ⦃G2, L2, T2⦄ ∨
- â¦\83G1, L1, T1â¦\84 >â\89¡[h, o] ⦃G2, L2, T2⦄.
+ â¦\83G1, L1, T1â¦\84 >â\89\9b[h, o] ⦃G2, L2, T2⦄.
#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H @(fpbs_ind … H) -G2 -L2 -T2
[ /2 width=1 by or_introl/
| #G #G2 #L #L2 #T #T2 #_ #H2 * #H1 @(fpbq_ind_alt … H2) -H2 #H2
(* Properties on "qrst" parallel reduction on closures **********************)
lemma fpb_fpbg_trans: ∀h,o,G1,G,G2,L1,L,L2,T1,T,T2.
- â¦\83G1, L1, T1â¦\84 â\89»[h, o] â¦\83G, L, Tâ¦\84 â\86\92 â¦\83G, L, Tâ¦\84 >â\89¡[h, o] ⦃G2, L2, T2⦄ →
- â¦\83G1, L1, T1â¦\84 >â\89¡[h, o] ⦃G2, L2, T2⦄.
+ â¦\83G1, L1, T1â¦\84 â\89»[h, o] â¦\83G, L, Tâ¦\84 â\86\92 â¦\83G, L, Tâ¦\84 >â\89\9b[h, o] ⦃G2, L2, T2⦄ →
+ â¦\83G1, L1, T1â¦\84 >â\89\9b[h, o] ⦃G2, L2, T2⦄.
/3 width=5 by fpbg_fwd_fpbs, ex2_3_intro/ qed-.
lemma fpbq_fpbg_trans: ∀h,o,G1,G,G2,L1,L,L2,T1,T,T2.
- â¦\83G1, L1, T1â¦\84 â\89½[h, o] â¦\83G, L, Tâ¦\84 â\86\92 â¦\83G, L, Tâ¦\84 >â\89¡[h, o] ⦃G2, L2, T2⦄ →
- â¦\83G1, L1, T1â¦\84 >â\89¡[h, o] ⦃G2, L2, T2⦄.
+ â¦\83G1, L1, T1â¦\84 â\89½[h, o] â¦\83G, L, Tâ¦\84 â\86\92 â¦\83G, L, Tâ¦\84 >â\89\9b[h, o] ⦃G2, L2, T2⦄ →
+ â¦\83G1, L1, T1â¦\84 >â\89\9b[h, o] ⦃G2, L2, T2⦄.
#h #o #G1 #G #G2 #L1 #L #L2 #T1 #T #T2 #H1 #H2 @(fpbq_ind_alt … H1) -H1
/2 width=5 by fleq_fpbg_trans, fpb_fpbg_trans/
qed-.
(* Properties on "qrst" parallel compuutation on closures *******************)
lemma fpbs_fpbg_trans: ∀h,o,G1,G,L1,L,T1,T. ⦃G1, L1, T1⦄ ≥[h, o] ⦃G, L, T⦄ →
- â\88\80G2,L2,T2. â¦\83G, L, Tâ¦\84 >â\89¡[h, o] â¦\83G2, L2, T2â¦\84 â\86\92 â¦\83G1, L1, T1â¦\84 >â\89¡[h, o] ⦃G2, L2, T2⦄.
+ â\88\80G2,L2,T2. â¦\83G, L, Tâ¦\84 >â\89\9b[h, o] â¦\83G2, L2, T2â¦\84 â\86\92 â¦\83G1, L1, T1â¦\84 >â\89\9b[h, o] ⦃G2, L2, T2⦄.
#h #o #G1 #G #L1 #L #T1 #T #H @(fpbs_ind … H) -G -L -T /3 width=5 by fpbq_fpbg_trans/
qed-.
(* Note: this is used in the closure proof *)
lemma fpbg_fpbs_trans: ∀h,o,G,G2,L,L2,T,T2. ⦃G, L, T⦄ ≥[h, o] ⦃G2, L2, T2⦄ →
- â\88\80G1,L1,T1. â¦\83G1, L1, T1â¦\84 >â\89¡[h, o] â¦\83G, L, Tâ¦\84 â\86\92 â¦\83G1, L1, T1â¦\84 >â\89¡[h, o] ⦃G2, L2, T2⦄.
+ â\88\80G1,L1,T1. â¦\83G1, L1, T1â¦\84 >â\89\9b[h, o] â¦\83G, L, Tâ¦\84 â\86\92 â¦\83G1, L1, T1â¦\84 >â\89\9b[h, o] ⦃G2, L2, T2⦄.
#h #o #G #G2 #L #L2 #T #T2 #H @(fpbs_ind_dx … H) -G -L -T /3 width=5 by fpbg_fpbq_trans/
qed-.
(* Note: this is used in the closure proof *)
-lemma fqup_fpbg: â\88\80h,o,G1,G2,L1,L2,T1,T2. â¦\83G1, L1, T1â¦\84 â\8a\90+ â¦\83G2, L2, T2â¦\84 â\86\92 â¦\83G1, L1, T1â¦\84 >â\89¡[h, o] ⦃G2, L2, T2⦄.
+lemma fqup_fpbg: â\88\80h,o,G1,G2,L1,L2,T1,T2. â¦\83G1, L1, T1â¦\84 â\8a\90+ â¦\83G2, L2, T2â¦\84 â\86\92 â¦\83G1, L1, T1â¦\84 >â\89\9b[h, o] ⦃G2, L2, T2⦄.
#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H elim (fqup_inv_step_sn … H) -H
/3 width=5 by fqus_fpbs, fpb_fqu, ex2_3_intro/
qed.
lemma cpxs_fpbg: ∀h,o,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡*[h, o] T2 →
- (T1 = T2 â\86\92 â\8a¥) â\86\92 â¦\83G, L, T1â¦\84 >â\89¡[h, o] ⦃G, L, T2⦄.
+ (T1 = T2 â\86\92 â\8a¥) â\86\92 â¦\83G, L, T1â¦\84 >â\89\9b[h, o] ⦃G, L, T2⦄.
#h #o #G #L #T1 #T2 #H #H0 elim (cpxs_neq_inv_step_sn … H … H0) -H -H0
/4 width=5 by cpxs_fpbs, fpb_cpx, ex2_3_intro/
qed.
lemma lstas_fpbg: ∀h,o,G,L,T1,T2,d2. ⦃G, L⦄ ⊢ T1 •*[h, d2] T2 → (T1 = T2 → ⊥) →
- â\88\80d1. d2 â\89¤ d1 â\86\92 â¦\83G, Lâ¦\84 â\8a¢ T1 â\96ª[h, o] d1 â\86\92 â¦\83G, L, T1â¦\84 >â\89¡[h, o] ⦃G, L, T2⦄.
+ â\88\80d1. d2 â\89¤ d1 â\86\92 â¦\83G, Lâ¦\84 â\8a¢ T1 â\96ª[h, o] d1 â\86\92 â¦\83G, L, T1â¦\84 >â\89\9b[h, o] ⦃G, L, T2⦄.
/3 width=5 by lstas_cpxs, cpxs_fpbg/ qed.
lemma lpxs_fpbg: ∀h,o,G,L1,L2,T. ⦃G, L1⦄ ⊢ ➡*[h, o] L2 →
- (L1 â\89¡[T, 0] L2 â\86\92 â\8a¥) â\86\92 â¦\83G, L1, Tâ¦\84 >â\89¡[h, o] ⦃G, L2, T⦄.
+ (L1 â\89¡[T, 0] L2 â\86\92 â\8a¥) â\86\92 â¦\83G, L1, Tâ¦\84 >â\89\9b[h, o] ⦃G, L2, T⦄.
#h #o #G #L1 #L2 #T #H #H0 elim (lpxs_nlleq_inv_step_sn … H … H0) -H -H0
/4 width=5 by fpb_lpx, lpxs_lleq_fpbs, ex2_3_intro/
qed.
(* Advanced properties ******************************************************)
lemma sta_fpbg: ∀h,o,G,L,T1,T2,d. ⦃G, L⦄ ⊢ T1 ▪[h, o] d+1 →
- â¦\83G, Lâ¦\84 â\8a¢ T1 â\80¢*[h, 1] T2 â\86\92 â¦\83G, L, T1â¦\84 >â\89¡[h, o] ⦃G, L, T2⦄.
+ â¦\83G, Lâ¦\84 â\8a¢ T1 â\80¢*[h, 1] T2 â\86\92 â¦\83G, L, T1â¦\84 >â\89\9b[h, o] ⦃G, L, T2⦄.
/4 width=2 by fpb_fpbg, sta_fpb/ qed.
fact aaa_ind_fpbg_aux: ∀h,o. ∀R:relation3 genv lenv term.
(∀G1,L1,T1,A. ⦃G1, L1⦄ ⊢ T1 ⁝ A →
- (â\88\80G2,L2,T2. â¦\83G1, L1, T1â¦\84 >â\89¡[h, o] ⦃G2, L2, T2⦄ → R G2 L2 T2) →
+ (â\88\80G2,L2,T2. â¦\83G1, L1, T1â¦\84 >â\89\9b[h, o] ⦃G2, L2, T2⦄ → R G2 L2 T2) →
R G1 L1 T1
) →
∀G,L,T. ⦃G, L⦄ ⊢ ⬊*[h, o] T → ∀A. ⦃G, L⦄ ⊢ T ⁝ A → R G L T.
lemma aaa_ind_fpbg: ∀h,o. ∀R:relation3 genv lenv term.
(∀G1,L1,T1,A. ⦃G1, L1⦄ ⊢ T1 ⁝ A →
- (â\88\80G2,L2,T2. â¦\83G1, L1, T1â¦\84 >â\89¡[h, o] ⦃G2, L2, T2⦄ → R G2 L2 T2) →
+ (â\88\80G2,L2,T2. â¦\83G1, L1, T1â¦\84 >â\89\9b[h, o] ⦃G2, L2, T2⦄ → R G2 L2 T2) →
R G1 L1 T1
) →
∀G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → R G L T.
(* Note: alternative definition of fsb *)
inductive fsba (h) (o): relation3 genv lenv term ≝
| fsba_intro: ∀G1,L1,T1. (
- â\88\80G2,L2,T2. â¦\83G1, L1, T1â¦\84 >â\89¡[h, o] ⦃G2, L2, T2⦄ → fsba h o G2 L2 T2
+ â\88\80G2,L2,T2. â¦\83G1, L1, T1â¦\84 >â\89\9b[h, o] ⦃G2, L2, T2⦄ → fsba h o G2 L2 T2
) → fsba h o G1 L1 T1.
interpretation
lemma fsba_ind_alt: ∀h,o. ∀R: relation3 …. (
∀G1,L1,T1. ⦥⦥[h,o] ⦃G1, L1, T1⦄ → (
- â\88\80G2,L2,T2. â¦\83G1, L1, T1â¦\84 >â\89¡[h, o] ⦃G2, L2, T2⦄ → R G2 L2 T2
+ â\88\80G2,L2,T2. â¦\83G1, L1, T1â¦\84 >â\89\9b[h, o] ⦃G2, L2, T2⦄ → R G2 L2 T2
) → R G1 L1 T1
) →
∀G,L,T. ⦥⦥[h, o] ⦃G, L, T⦄ → R G L T.
lemma fsb_ind_fpbg: ∀h,o. ∀R:relation3 genv lenv term.
(∀G1,L1,T1. ⦥[h, o] ⦃G1, L1, T1⦄ →
- (â\88\80G2,L2,T2. â¦\83G1, L1, T1â¦\84 >â\89¡[h, o] ⦃G2, L2, T2⦄ → R G2 L2 T2) →
+ (â\88\80G2,L2,T2. â¦\83G1, L1, T1â¦\84 >â\89\9b[h, o] ⦃G2, L2, T2⦄ → R G2 L2 T2) →
R G1 L1 T1
) →
∀G1,L1,T1. ⦥[h, o] ⦃G1, L1, T1⦄ → R G1 L1 T1.
lemma csx_ind_fpbg: ∀h,o. ∀R:relation3 genv lenv term.
(∀G1,L1,T1. ⦃G1, L1⦄ ⊢ ⬊*[h, o] T1 →
- (â\88\80G2,L2,T2. â¦\83G1, L1, T1â¦\84 >â\89¡[h, o] ⦃G2, L2, T2⦄ → R G2 L2 T2) →
+ (â\88\80G2,L2,T2. â¦\83G1, L1, T1â¦\84 >â\89\9b[h, o] ⦃G2, L2, T2⦄ → R G2 L2 T2) →
R G1 L1 T1
) →
∀G,L,T. ⦃G, L⦄ ⊢ ⬊*[h, o] T → R G L T.
(* Basic_2A1: was: lleq_lpxs_trans *)
lemma lfdeq_lfpxs_trans: ∀h,o,G,L2,K2,T. ⦃G, L2⦄ ⊢ ⬈*[h, T] K2 →
- â\88\80L1. L1 â\89¡[h, o, T] L2 →
- â\88\83â\88\83K1. â¦\83G, L1â¦\84 â\8a¢ â¬\88*[h, T] K1 & K1 â\89¡[h, o, T] K2.
+ â\88\80L1. L1 â\89\9b[h, o, T] L2 →
+ â\88\83â\88\83K1. â¦\83G, L1â¦\84 â\8a¢ â¬\88*[h, T] K1 & K1 â\89\9b[h, o, T] K2.
#h #o #G #L2 #K2 #T #H @(lfpxs_ind_sn … H) -K2 /2 width=3 by ex2_intro/
#K #K2 #_ #HK2 #IH #L1 #HT elim (IH … HT) -L2
#L #HL1 #HT elim (lfdeq_lfpx_trans … HK2 … HT) -K
qed-.
(* Basic_2A1: was: lpxs_nlleq_inv_step_sn *)
-lemma lfpxs_lfdneq_inv_step_sn: â\88\80h,o,G,L1,L2,T. â¦\83G, L1â¦\84 â\8a¢ â¬\88*[h, T] L2 â\86\92 (L1 â\89¡[h, o, T] L2 → ⊥) →
- â\88\83â\88\83L,L0. â¦\83G, L1â¦\84 â\8a¢ â¬\88[h, T] L & L1 â\89¡[h, o, T] L â\86\92 â\8a¥ & â¦\83G, Lâ¦\84 â\8a¢ â¬\88*[h, T] L0 & L0 â\89¡[h, o, T] L2.
+lemma lfpxs_lfdneq_inv_step_sn: â\88\80h,o,G,L1,L2,T. â¦\83G, L1â¦\84 â\8a¢ â¬\88*[h, T] L2 â\86\92 (L1 â\89\9b[h, o, T] L2 → ⊥) →
+ â\88\83â\88\83L,L0. â¦\83G, L1â¦\84 â\8a¢ â¬\88[h, T] L & L1 â\89\9b[h, o, T] L â\86\92 â\8a¥ & â¦\83G, Lâ¦\84 â\8a¢ â¬\88*[h, T] L0 & L0 â\89\9b[h, o, T] L2.
#h #o #G #L1 #L2 #T #H @(lfpxs_ind_dx … H) -L1
[ #H elim H -H //
| #L1 #L #H1 #H2 #IH2 #H12 elim (lfdeq_dec h o L1 L T) #H
(* Basic_2A1: uses: lsx_ind *)
lemma lfsx_ind: ∀h,o,G,T. ∀R:predicate lenv.
(∀L1. G ⊢ ⬈*[h, o, T] 𝐒⦃L1⦄ →
- (â\88\80L2. â¦\83G, L1â¦\84 â\8a¢ â¬\88[h, T] L2 â\86\92 (L1 â\89¡[h, o, T] L2 → ⊥) → R L2) →
+ (â\88\80L2. â¦\83G, L1â¦\84 â\8a¢ â¬\88[h, T] L2 â\86\92 (L1 â\89\9b[h, o, T] L2 → ⊥) → R L2) →
R L1
) →
∀L. G ⊢ ⬈*[h, o, T] 𝐒⦃L⦄ → R L.
(* Basic_2A1: uses: lsx_intro *)
lemma lfsx_intro: ∀h,o,G,L1,T.
- (â\88\80L2. â¦\83G, L1â¦\84 â\8a¢ â¬\88[h, T] L2 â\86\92 (L1 â\89¡[h, o, T] L2 → ⊥) → G ⊢ ⬈*[h, o, T] 𝐒⦃L2⦄) →
+ (â\88\80L2. â¦\83G, L1â¦\84 â\8a¢ â¬\88[h, T] L2 â\86\92 (L1 â\89\9b[h, o, T] L2 → ⊥) → G ⊢ ⬈*[h, o, T] 𝐒⦃L2⦄) →
G ⊢ ⬈*[h, o, T] 𝐒⦃L1⦄.
/5 width=1 by lfdeq_sym, SN_intro/ qed.
(* Basic_2A1: uses: lsx_intro_alt *)
lemma lfsx_intro_lfpxs: ∀h,o,G,L1,T.
- (â\88\80L2. â¦\83G, L1â¦\84 â\8a¢ â¬\88*[h, T] L2 â\86\92 (L1 â\89¡[h, o, T] L2 → ⊥) → G ⊢ ⬈*[h, o, T] 𝐒⦃L2⦄) →
+ (â\88\80L2. â¦\83G, L1â¦\84 â\8a¢ â¬\88*[h, T] L2 â\86\92 (L1 â\89\9b[h, o, T] L2 → ⊥) → G ⊢ ⬈*[h, o, T] 𝐒⦃L2⦄) →
G ⊢ ⬈*[h, o, T] 𝐒⦃L1⦄.
/4 width=1 by lfpx_lfpxs, lfsx_intro/ qed-.
lemma lfsx_ind_lfpxs_lfdeq: ∀h,o,G,T. ∀R:predicate lenv.
(∀L1. G ⊢ ⬈*[h, o, T] 𝐒⦃L1⦄ →
- (â\88\80L2. â¦\83G, L1â¦\84 â\8a¢ â¬\88*[h, T] L2 â\86\92 (L1 â\89¡[h, o, T] L2 → ⊥) → R L2) →
+ (â\88\80L2. â¦\83G, L1â¦\84 â\8a¢ â¬\88*[h, T] L2 â\86\92 (L1 â\89\9b[h, o, T] L2 → ⊥) → R L2) →
R L1
) →
∀L1. G ⊢ ⬈*[h, o, T] 𝐒⦃L1⦄ →
- â\88\80L0. â¦\83G, L1â¦\84 â\8a¢ â¬\88*[h, T] L0 â\86\92 â\88\80L2. L0 â\89¡[h, o, T] L2 → R L2.
+ â\88\80L0. â¦\83G, L1â¦\84 â\8a¢ â¬\88*[h, T] L0 â\86\92 â\88\80L2. L0 â\89\9b[h, o, T] L2 → R L2.
#h #o #G #T #R #IH #L1 #H @(lfsx_ind … H) -L1
#L1 #HL1 #IH1 #L0 #HL10 #L2 #HL02
@IH -IH /3 width=3 by lfsx_lfpxs_trans, lfsx_lfdeq_trans/ -HL1 #K2 #HLK2 #HnLK2
(* Basic_2A1: uses: lsx_ind_alt *)
lemma lfsx_ind_lfpxs: ∀h,o,G,T. ∀R:predicate lenv.
(∀L1. G ⊢ ⬈*[h, o, T] 𝐒⦃L1⦄ →
- (â\88\80L2. â¦\83G, L1â¦\84 â\8a¢ â¬\88*[h, T] L2 â\86\92 (L1 â\89¡[h, o, T] L2 → ⊥) → R L2) →
+ (â\88\80L2. â¦\83G, L1â¦\84 â\8a¢ â¬\88*[h, T] L2 â\86\92 (L1 â\89\9b[h, o, T] L2 → ⊥) → R L2) →
R L1
) →
∀L. G ⊢ ⬈*[h, o, T] 𝐒⦃L⦄ → R L.
(* Basic_2A1: uses: lsx_lleq_trans *)
lemma lfsx_lfdeq_trans: ∀h,o,G,L1,T. G ⊢ ⬈*[h, o, T] 𝐒⦃L1⦄ →
- â\88\80L2. L1 â\89¡[h, o, T] L2 → G ⊢ ⬈*[h, o, T] 𝐒⦃L2⦄.
+ â\88\80L2. L1 â\89\9b[h, o, T] L2 → G ⊢ ⬈*[h, o, T] 𝐒⦃L2⦄.
#h #o #G #L1 #T #H @(lfsx_ind … H) -L1
#L1 #_ #IHL1 #L2 #HL12 @lfsx_intro
#L #HL2 #HnL2 elim (lfdeq_lfpx_trans … HL2 … HL12) -HL2
(* Advanced properties ******************************************************)
lemma cnx_tdeq_trans: ∀h,o,G,L,T1. ⦃G, L⦄ ⊢ ⬈[h, o] 𝐍⦃T1⦄ →
- â\88\80T2. T1 â\89¡[h, o] T2 → ⦃G, L⦄ ⊢ ⬈[h, o] 𝐍⦃T2⦄.
+ â\88\80T2. T1 â\89\9b[h, o] T2 → ⦃G, L⦄ ⊢ ⬈[h, o] 𝐍⦃T2⦄.
#h #o #G #L #T1 #HT1 #T2 #HT12 #T #HT2
elim (tdeq_cpx_trans … HT12 … HT2) -HT2 #T0 #HT10 #HT0
lapply (HT1 … HT10) -HT1 -HT10 /2 width=5 by tdeq_repl/ (**) (* full auto fails *)
qed-.
lemma fqu_cpx_trans_ntdeq: ∀h,o,b,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐[b] ⦃G2, L2, T2⦄ →
- â\88\80U2. â¦\83G2, L2â¦\84 â\8a¢ T2 â¬\88[h] U2 â\86\92 (T2 â\89¡[h, o] U2 → ⊥) →
- â\88\83â\88\83U1. â¦\83G1, L1â¦\84 â\8a¢ T1 â¬\88[h] U1 & T1 â\89¡[h, o] U1 → ⊥ & ⦃G1, L1, U1⦄ ⊐[b] ⦃G2, L2, U2⦄.
+ â\88\80U2. â¦\83G2, L2â¦\84 â\8a¢ T2 â¬\88[h] U2 â\86\92 (T2 â\89\9b[h, o] U2 → ⊥) →
+ â\88\83â\88\83U1. â¦\83G1, L1â¦\84 â\8a¢ T1 â¬\88[h] U1 & T1 â\89\9b[h, o] U1 → ⊥ & ⦃G1, L1, U1⦄ ⊐[b] ⦃G2, L2, U2⦄.
#h #o #b #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2
[ #I #G #L #V1 #V2 #HV12 #_ elim (lifts_total V2 𝐔❴1❵)
#U2 #HVU2 @(ex3_intro … U2)
qed-.
lemma fquq_cpx_trans_ntdeq: ∀h,o,b,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐⸮[b] ⦃G2, L2, T2⦄ →
- â\88\80U2. â¦\83G2, L2â¦\84 â\8a¢ T2 â¬\88[h] U2 â\86\92 (T2 â\89¡[h, o] U2 → ⊥) →
- â\88\83â\88\83U1. â¦\83G1, L1â¦\84 â\8a¢ T1 â¬\88[h] U1 & T1 â\89¡[h, o] U1 → ⊥ & ⦃G1, L1, U1⦄ ⊐⸮[b] ⦃G2, L2, U2⦄.
+ â\88\80U2. â¦\83G2, L2â¦\84 â\8a¢ T2 â¬\88[h] U2 â\86\92 (T2 â\89\9b[h, o] U2 → ⊥) →
+ â\88\83â\88\83U1. â¦\83G1, L1â¦\84 â\8a¢ T1 â¬\88[h] U1 & T1 â\89\9b[h, o] U1 → ⊥ & ⦃G1, L1, U1⦄ ⊐⸮[b] ⦃G2, L2, U2⦄.
#h #o #b #G1 #G2 #L1 #L2 #T1 #T2 #H12 elim H12 -H12
[ #H12 #U2 #HTU2 #H elim (fqu_cpx_trans_ntdeq … H12 … HTU2 H) -T2
/3 width=4 by fqu_fquq, ex3_intro/
qed-.
lemma fqup_cpx_trans_ntdeq: ∀h,o,b,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐+[b] ⦃G2, L2, T2⦄ →
- â\88\80U2. â¦\83G2, L2â¦\84 â\8a¢ T2 â¬\88[h] U2 â\86\92 (T2 â\89¡[h, o] U2 → ⊥) →
- â\88\83â\88\83U1. â¦\83G1, L1â¦\84 â\8a¢ T1 â¬\88[h] U1 & T1 â\89¡[h, o] U1 → ⊥ & ⦃G1, L1, U1⦄ ⊐+[b] ⦃G2, L2, U2⦄.
+ â\88\80U2. â¦\83G2, L2â¦\84 â\8a¢ T2 â¬\88[h] U2 â\86\92 (T2 â\89\9b[h, o] U2 → ⊥) →
+ â\88\83â\88\83U1. â¦\83G1, L1â¦\84 â\8a¢ T1 â¬\88[h] U1 & T1 â\89\9b[h, o] U1 → ⊥ & ⦃G1, L1, U1⦄ ⊐+[b] ⦃G2, L2, U2⦄.
#h #o #b #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind_dx … H) -G1 -L1 -T1
[ #G1 #L1 #T1 #H12 #U2 #HTU2 #H elim (fqu_cpx_trans_ntdeq … H12 … HTU2 H) -T2
/3 width=4 by fqu_fqup, ex3_intro/
qed-.
lemma fqus_cpx_trans_ntdeq: ∀h,o,b,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐*[b] ⦃G2, L2, T2⦄ →
- â\88\80U2. â¦\83G2, L2â¦\84 â\8a¢ T2 â¬\88[h] U2 â\86\92 (T2 â\89¡[h, o] U2 → ⊥) →
- â\88\83â\88\83U1. â¦\83G1, L1â¦\84 â\8a¢ T1 â¬\88[h] U1 & T1 â\89¡[h, o] U1 → ⊥ & ⦃G1, L1, U1⦄ ⊐*[b] ⦃G2, L2, U2⦄.
+ â\88\80U2. â¦\83G2, L2â¦\84 â\8a¢ T2 â¬\88[h] U2 â\86\92 (T2 â\89\9b[h, o] U2 → ⊥) →
+ â\88\83â\88\83U1. â¦\83G1, L1â¦\84 â\8a¢ T1 â¬\88[h] U1 & T1 â\89\9b[h, o] U1 → ⊥ & ⦃G1, L1, U1⦄ ⊐*[b] ⦃G2, L2, U2⦄.
#h #o #b #G1 #G2 #L1 #L2 #T1 #T2 #H12 #U2 #HTU2 #H elim (fqus_inv_fqup … H12) -H12
[ #H12 elim (fqup_cpx_trans_ntdeq … H12 … HTU2 H) -T2
/3 width=4 by fqup_fqus, ex3_intro/
(* Basic_2A1: was just: cpx_lleq_conf_dx *)
lemma cpx_lfdeq_conf_dx: ∀h,o,G,L2,T1,T2. ⦃G, L2⦄ ⊢ T1 ⬈[h] T2 →
- â\88\80L1. L1 â\89¡[h, o, T1] L2 â\86\92 L1 â\89¡[h, o, T2] L2.
+ â\88\80L1. L1 â\89\9b[h, o, T1] L2 â\86\92 L1 â\89\9b[h, o, T2] L2.
/4 width=4 by cpx_lfdeq_conf_sn, lfdeq_sym/ qed-.
inductive fpb (h) (o) (G1) (L1) (T1): relation3 genv lenv term ≝
| fpb_fqu : ∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊐ ⦃G2, L2, T2⦄ → fpb h o G1 L1 T1 G2 L2 T2
-| fpb_cpx : â\88\80T2. â¦\83G1, L1â¦\84 â\8a¢ T1 â¬\88[h] T2 â\86\92 (T1 â\89¡[h, o] T2 → ⊥) → fpb h o G1 L1 T1 G1 L1 T2
-| fpb_lfpx: â\88\80L2. â¦\83G1, L1â¦\84 â\8a¢ â¬\88[h, T1] L2 â\86\92 (L1 â\89¡[h, o, T1] L2 → ⊥) → fpb h o G1 L1 T1 G1 L2 T1
+| fpb_cpx : â\88\80T2. â¦\83G1, L1â¦\84 â\8a¢ T1 â¬\88[h] T2 â\86\92 (T1 â\89\9b[h, o] T2 → ⊥) → fpb h o G1 L1 T1 G1 L1 T2
+| fpb_lfpx: â\88\80L2. â¦\83G1, L1â¦\84 â\8a¢ â¬\88[h, T1] L2 â\86\92 (L1 â\89\9b[h, o, T1] L2 → ⊥) → fpb h o G1 L1 T1 G1 L2 T1
.
interpretation
(* Basic properties *********************************************************)
(* Basic_2A1: includes: cpr_fpb *)
-lemma cpm_fpb: â\88\80n,h,o,G,L,T1,T2. â¦\83G, Lâ¦\84 â\8a¢ T1 â\9e¡[n, h] T2 â\86\92 (T1 â\89¡[h, o] T2 → ⊥) →
+lemma cpm_fpb: â\88\80n,h,o,G,L,T1,T2. â¦\83G, Lâ¦\84 â\8a¢ T1 â\9e¡[n, h] T2 â\86\92 (T1 â\89\9b[h, o] T2 → ⊥) →
⦃G, L, T1⦄ ≻[h, o] ⦃G, L, T2⦄.
/3 width=2 by fpb_cpx, cpm_fwd_cpx/ qed.
(* Basic_2A1: includes: lpr_fpb *)
-lemma lfpr_fpb: â\88\80h,o,G,L1,L2,T. â¦\83G, L1â¦\84 â\8a¢ â\9e¡[h, T] L2 â\86\92 (L1 â\89¡[h, o, T] L2 → ⊥) →
+lemma lfpr_fpb: â\88\80h,o,G,L1,L2,T. â¦\83G, L1â¦\84 â\8a¢ â\9e¡[h, T] L2 â\86\92 (L1 â\89\9b[h, o, T] L2 → ⊥) →
⦃G, L1, T⦄ ≻[h, o] ⦃G, L2, T⦄.
/3 width=1 by fpb_lfpx, lfpr_fwd_lfpx/ qed.
(* Properties with degree-based equivalence for local environments **********)
(* Basic_2A1: was just: lleq_fpb_trans *)
-lemma lfdeq_fpb_trans: â\88\80h,o,F,K1,K2,T. K1 â\89¡[h, o, T] K2 →
+lemma lfdeq_fpb_trans: â\88\80h,o,F,K1,K2,T. K1 â\89\9b[h, o, T] K2 →
∀G,L2,U. ⦃F, K2, T⦄ ≻[h, o] ⦃G, L2, U⦄ →
- â\88\83â\88\83L1,U0. â¦\83F, K1, Tâ¦\84 â\89»[h, o] â¦\83G, L1, U0â¦\84 & U0 â\89¡[h, o] U & L1 â\89¡[h, o, U] L2.
+ â\88\83â\88\83L1,U0. â¦\83F, K1, Tâ¦\84 â\89»[h, o] â¦\83G, L1, U0â¦\84 & U0 â\89\9b[h, o] U & L1 â\89\9b[h, o, U] L2.
#h #o #F #K1 #K2 #T #HT #G #L2 #U * -G -L2 -U
[ #G #L2 #U #H2 elim (lfdeq_fqu_trans … H2 … HT) -K2
/3 width=5 by fpb_fqu, ex3_2_intro/
(* Properties with degree-based equivalence for local environments **********)
lemma lfpx_pair_sn_split: ∀h,G,L1,L2,V. ⦃G, L1⦄ ⊢ ⬈[h, V] L2 → ∀o,I,T.
- â\88\83â\88\83L. â¦\83G, L1â¦\84 â\8a¢ â¬\88[h, â\91¡{I}V.T] L & L â\89¡[h, o, V] L2.
+ â\88\83â\88\83L. â¦\83G, L1â¦\84 â\8a¢ â¬\88[h, â\91¡{I}V.T] L & L â\89\9b[h, o, V] L2.
/3 width=5 by lfpx_frees_conf, lfxs_pair_sn_split/ qed-.
lemma lfpx_flat_dx_split: ∀h,G,L1,L2,T. ⦃G, L1⦄ ⊢ ⬈[h, T] L2 → ∀o,I,V.
- â\88\83â\88\83L. â¦\83G, L1â¦\84 â\8a¢ â¬\88[h, â\93\95{I}V.T] L & L â\89¡[h, o, T] L2.
+ â\88\83â\88\83L. â¦\83G, L1â¦\84 â\8a¢ â¬\88[h, â\93\95{I}V.T] L & L â\89\9b[h, o, T] L2.
/3 width=5 by lfpx_frees_conf, lfxs_flat_dx_split/ qed-.
lemma lfpx_bind_dx_split: ∀h,I,G,L1,L2,V1,T. ⦃G, L1.ⓑ{I}V1⦄ ⊢ ⬈[h, T] L2 → ∀o,p.
- â\88\83â\88\83L,V. â¦\83G, L1â¦\84 â\8a¢ â¬\88[h, â\93\91{p,I}V1.T] L & L.â\93\91{I}V â\89¡[h, o, T] L2 & ⦃G, L1⦄ ⊢ V1 ⬈[h] V.
+ â\88\83â\88\83L,V. â¦\83G, L1â¦\84 â\8a¢ â¬\88[h, â\93\91{p,I}V1.T] L & L.â\93\91{I}V â\89\9b[h, o, T] L2 & ⦃G, L1⦄ ⊢ V1 ⬈[h] V.
/3 width=5 by lfpx_frees_conf, lfxs_bind_dx_split/ qed-.
lemma lfpx_bind_dx_split_void: ∀h,G,K1,L2,T. ⦃G, K1.ⓧ⦄ ⊢ ⬈[h, T] L2 → ∀o,p,I,V.
- â\88\83â\88\83K2. â¦\83G, K1â¦\84 â\8a¢ â¬\88[h, â\93\91{p,I}V.T] K2 & K2.â\93§ â\89¡[h, o, T] L2.
+ â\88\83â\88\83K2. â¦\83G, K1â¦\84 â\8a¢ â¬\88[h, â\93\91{p,I}V.T] K2 & K2.â\93§ â\89\9b[h, o, T] L2.
/3 width=5 by lfpx_frees_conf, lfxs_bind_dx_split_void/ qed-.
lemma cpx_tdeq_conf_lexs: ∀h,o,G. R_confluent2_lfxs … (cpx h G) (cdeq h o) (cpx h G) (cdeq h o).
qed-.
lemma cpx_tdeq_conf: ∀h,o,G,L. ∀T0:term. ∀T1. ⦃G, L⦄ ⊢ T0 ⬈[h] T1 →
- â\88\80T2. T0 â\89¡[h, o] T2 →
- â\88\83â\88\83T. T1 â\89¡[h, o] T & ⦃G, L⦄ ⊢ T2 ⬈[h] T.
+ â\88\80T2. T0 â\89\9b[h, o] T2 →
+ â\88\83â\88\83T. T1 â\89\9b[h, o] T & ⦃G, L⦄ ⊢ T2 ⬈[h] T.
#h #o #G #L #T0 #T1 #HT01 #T2 #HT02
elim (cpx_tdeq_conf_lexs … HT01 … HT02 L … L) -HT01 -HT02
/2 width=3 by lfxs_refl, ex2_intro/
qed-.
-lemma tdeq_cpx_trans: â\88\80h,o,G,L,T2. â\88\80T0:term. T2 â\89¡[h, o] T0 →
+lemma tdeq_cpx_trans: â\88\80h,o,G,L,T2. â\88\80T0:term. T2 â\89\9b[h, o] T0 →
∀T1. ⦃G, L⦄ ⊢ T0 ⬈[h] T1 →
- â\88\83â\88\83T. â¦\83G, Lâ¦\84 â\8a¢ T2 â¬\88[h] T & T â\89¡[h, o] T1.
+ â\88\83â\88\83T. â¦\83G, Lâ¦\84 â\8a¢ T2 â¬\88[h] T & T â\89\9b[h, o] T1.
#h #o #G #L #T2 #T0 #HT20 #T1 #HT01
elim (cpx_tdeq_conf … HT01 T2) -HT01 /3 width=3 by tdeq_sym, ex2_intro/
qed-.
(* Basic_2A1: uses: cpx_lleq_conf *)
lemma cpx_lfdeq_conf: ∀h,o,G,L0,T0,T1. ⦃G, L0⦄ ⊢ T0 ⬈[h] T1 →
- â\88\80L2. L0 â\89¡[h, o, T0] L2 →
- â\88\83â\88\83T. â¦\83G, L2â¦\84 â\8a¢ T0 â¬\88[h] T & T1 â\89¡[h, o] T.
+ â\88\80L2. L0 â\89\9b[h, o, T0] L2 →
+ â\88\83â\88\83T. â¦\83G, L2â¦\84 â\8a¢ T0 â¬\88[h] T & T1 â\89\9b[h, o] T.
#h #o #G #L0 #T0 #T1 #HT01 #L2 #HL02
elim (cpx_tdeq_conf_lexs … HT01 T0 … L0 … HL02) -HT01 -HL02
/2 width=3 by lfxs_refl, ex2_intro/
qed-.
(* Basic_2A1: uses: lleq_cpx_trans *)
-lemma lfdeq_cpx_trans: â\88\80h,o,G,L2,L0,T0. L2 â\89¡[h, o, T0] L0 →
+lemma lfdeq_cpx_trans: â\88\80h,o,G,L2,L0,T0. L2 â\89\9b[h, o, T0] L0 →
∀T1. ⦃G, L0⦄ ⊢ T0 ⬈[h] T1 →
- â\88\83â\88\83T. â¦\83G, L2â¦\84 â\8a¢ T0 â¬\88[h] T & T â\89¡[h, o] T1.
+ â\88\83â\88\83T. â¦\83G, L2â¦\84 â\8a¢ T0 â¬\88[h] T & T â\89\9b[h, o] T1.
#h #o #G #L2 #L0 #T0 #HL20 #T1 #HT01
elim (cpx_lfdeq_conf … o … HT01 L2) -HT01
/3 width=3 by lfdeq_sym, tdeq_sym, ex2_intro/
(* Basic_2A1: uses: lleq_lpx_trans *)
lemma lfdeq_lfpx_trans: ∀h,o,G,T,L2,K2. ⦃G, L2⦄ ⊢ ⬈[h, T] K2 →
- â\88\80L1. L1 â\89¡[h, o, T] L2 →
- â\88\83â\88\83K1. â¦\83G, L1â¦\84 â\8a¢ â¬\88[h, T] K1 & K1 â\89¡[h, o, T] K2.
+ â\88\80L1. L1 â\89\9b[h, o, T] L2 →
+ â\88\83â\88\83K1. â¦\83G, L1â¦\84 â\8a¢ â¬\88[h, T] K1 & K1 â\89\9b[h, o, T] K2.
#h #o #G #T #L2 #K2 #HLK2 #L1 #HL12
elim (lfpx_lfdeq_conf … o … HLK2 L1)
/3 width=3 by lfdeq_sym, ex2_intro/
(* Properties with degree-based equivalence on referred entries *************)
-lemma aaa_tdeq_conf_fldeq: â\88\80h,o,G,L1,T1,A. â¦\83G, L1â¦\84 â\8a¢ T1 â\81\9d A â\86\92 â\88\80T2. T1 â\89¡[h, o] T2 →
- â\88\80L2. L1 â\89¡[h, o, T1] L2 → ⦃G, L2⦄ ⊢ T2 ⁝ A.
+lemma aaa_tdeq_conf_fldeq: â\88\80h,o,G,L1,T1,A. â¦\83G, L1â¦\84 â\8a¢ T1 â\81\9d A â\86\92 â\88\80T2. T1 â\89\9b[h, o] T2 →
+ â\88\80L2. L1 â\89\9b[h, o, T1] L2 → ⦃G, L2⦄ ⊢ T2 ⁝ A.
#h #o #G #L1 #T1 #A #H elim H -G -L1 -T1 -A
[ #G #L1 #s1 #X #H1 elim (tdeq_inv_sort1 … H1) -H1 //
| #I #G #L1 #V1 #B #_ #IH #X #H1 >(tdeq_inv_lref1 … H1) -H1
(* *)
(**************************************************************************)
-include "basic_2/notation/relations/lazyeqsn_8.ma".
+include "basic_2/notation/relations/stareqsn_8.ma".
include "basic_2/syntax/genv.ma".
include "basic_2/static/lfdeq.ma".
(* DEGREE-BASED EQUIVALENCE FOR CLOSURES ON REFERRED ENTRIES ****************)
inductive ffdeq (h) (o) (G) (L1) (T): relation3 genv lenv term ≝
-| ffdeq_intro: â\88\80L2. L1 â\89¡[h, o, T] L2 → ffdeq h o G L1 T G L2 T
+| ffdeq_intro: â\88\80L2. L1 â\89\9b[h, o, T] L2 → ffdeq h o G L1 T G L2 T
.
interpretation
"degree-based equivalence on referred entries (closure)"
- 'LazyEqSn h o G1 L1 T1 G2 L2 T2 = (ffdeq h o G1 L1 T1 G2 L2 T2).
+ 'StarEqSn h o G1 L1 T1 G2 L2 T2 = (ffdeq h o G1 L1 T1 G2 L2 T2).
(* Basic properties *********************************************************)
(* Basic inversion lemmas ***************************************************)
-lemma ffdeq_inv_gen: â\88\80h,o,G1,G2,L1,L2,T1,T2. â¦\83G1, L1, T1â¦\84 â\89¡[h, o] ⦃G2, L2, T2⦄ →
- â\88§â\88§ G1 = G2 & L1 â\89¡[h, o, T1] L2 & T1 = T2.
+lemma ffdeq_inv_gen: â\88\80h,o,G1,G2,L1,L2,T1,T2. â¦\83G1, L1, T1â¦\84 â\89\9b[h, o] ⦃G2, L2, T2⦄ →
+ â\88§â\88§ G1 = G2 & L1 â\89\9b[h, o, T1] L2 & T1 = T2.
#h #o #G1 #G2 #L1 #L2 #T1 #T2 * -G2 -L2 -T2 /2 width=1 by and3_intro/
qed-.
qed-.
theorem ffdeq_canc_sn: ∀h,o,G,G1,G2,L,L1,L2,T,T1,T2.
- â¦\83G, L, Tâ¦\84 â\89¡[h, o] â¦\83G1, L1, T1â¦\84â\86\92 â¦\83G, L, Tâ¦\84 â\89¡[h, o] â¦\83G2, L2, T2â¦\84 â\86\92 â¦\83G1, L1, T1â¦\84 â\89¡[h, o] ⦃G2, L2, T2⦄.
+ â¦\83G, L, Tâ¦\84 â\89\9b[h, o] â¦\83G1, L1, T1â¦\84â\86\92 â¦\83G, L, Tâ¦\84 â\89\9b[h, o] â¦\83G2, L2, T2â¦\84 â\86\92 â¦\83G1, L1, T1â¦\84 â\89\9b[h, o] ⦃G2, L2, T2⦄.
/3 width=5 by ffdeq_trans, ffdeq_sym/ qed-.
theorem ffdeq_canc_dx: ∀h,o,G1,G2,G,L1,L2,L,T1,T2,T.
- â¦\83G1, L1, T1â¦\84 â\89¡[h, o] â¦\83G, L, Tâ¦\84 â\86\92 â¦\83G2, L2, T2â¦\84 â\89¡[h, o] â¦\83G, L, Tâ¦\84 â\86\92 â¦\83G1, L1, T1â¦\84 â\89¡[h, o] ⦃G2, L2, T2⦄.
+ â¦\83G1, L1, T1â¦\84 â\89\9b[h, o] â¦\83G, L, Tâ¦\84 â\86\92 â¦\83G2, L2, T2â¦\84 â\89\9b[h, o] â¦\83G, L, Tâ¦\84 â\86\92 â¦\83G1, L1, T1â¦\84 â\89\9b[h, o] ⦃G2, L2, T2⦄.
/3 width=5 by ffdeq_trans, ffdeq_sym/ qed-.
(* *)
(**************************************************************************)
-include "basic_2/notation/relations/lazyeqsn_5.ma".
+include "basic_2/notation/relations/stareqsn_5.ma".
include "basic_2/syntax/tdeq_ext.ma".
include "basic_2/static/lfxs.ma".
interpretation
"degree-based equivalence on referred entries (local environment)"
- 'LazyEqSn h o T L1 L2 = (lfdeq h o T L1 L2).
+ 'StarEqSn h o T L1 L2 = (lfdeq h o T L1 L2).
interpretation
"degree-based ranged equivalence (local environment)"
- 'LazyEqSn h o f L1 L2 = (lexs (cdeq_ext h o) cfull f L1 L2).
+ 'StarEqSn h o f L1 L2 = (lexs (cdeq_ext h o) cfull f L1 L2).
(*
definition lfdeq_transitive: predicate (relation3 lenv term term) ≝
- λR. â\88\80L2,T1,T2. R L2 T1 T2 â\86\92 â\88\80L1. L1 â\89¡[h, o, T1] L2 → R L1 T1 T2.
+ λR. â\88\80L2,T1,T2. R L2 T1 T2 â\86\92 â\88\80L1. L1 â\89\9b[h, o, T1] L2 → R L1 T1 T2.
*)
(* Basic properties ***********************************************************)
-lemma frees_tdeq_conf_lexs: â\88\80h,o,f,L1,T1. L1 â\8a¢ ð\9d\90\85*â¦\83T1â¦\84 â\89¡ f â\86\92 â\88\80T2. T1 â\89¡[h, o] T2 →
- â\88\80L2. L1 â\89¡[h, o, f] L2 → L2 ⊢ 𝐅*⦃T2⦄ ≡ f.
+lemma frees_tdeq_conf_lexs: â\88\80h,o,f,L1,T1. L1 â\8a¢ ð\9d\90\85*â¦\83T1â¦\84 â\89¡ f â\86\92 â\88\80T2. T1 â\89\9b[h, o] T2 →
+ â\88\80L2. L1 â\89\9b[h, o, f] L2 → L2 ⊢ 𝐅*⦃T2⦄ ≡ f.
#h #o #f #L1 #T1 #H elim H -f -L1 -T1
[ #f #L1 #s1 #Hf #X #H1 #L2 #_
elim (tdeq_inv_sort1 … H1) -H1 #s2 #d #_ #_ #H destruct
qed-.
lemma frees_tdeq_conf: ∀h,o,f,L,T1. L ⊢ 𝐅*⦃T1⦄ ≡ f →
- â\88\80T2. T1 â\89¡[h, o] T2 → L ⊢ 𝐅*⦃T2⦄ ≡ f.
+ â\88\80T2. T1 â\89\9b[h, o] T2 → L ⊢ 𝐅*⦃T2⦄ ≡ f.
/4 width=7 by frees_tdeq_conf_lexs, lexs_refl, ext2_refl/ qed-.
lemma frees_lexs_conf: ∀h,o,f,L1,T. L1 ⊢ 𝐅*⦃T⦄ ≡ f →
- â\88\80L2. L1 â\89¡[h, o, f] L2 → L2 ⊢ 𝐅*⦃T⦄ ≡ f.
+ â\88\80L2. L1 â\89\9b[h, o, f] L2 → L2 ⊢ 𝐅*⦃T⦄ ≡ f.
/2 width=7 by frees_tdeq_conf_lexs, tdeq_refl/ qed-.
lemma frees_lfdeq_conf_lexs: ∀h,o. lexs_frees_confluent (cdeq_ext h o) cfull.
/4 width=7 by frees_tdeq_conf_lexs, lfxs_sym, tdeq_sym, ex2_intro/
qed-.
-lemma lfdeq_atom: â\88\80h,o,I. â\8b\86 â\89¡[h, o, ⓪{I}] ⋆.
+lemma lfdeq_atom: â\88\80h,o,I. â\8b\86 â\89\9b[h, o, ⓪{I}] ⋆.
/2 width=1 by lfxs_atom/ qed.
(* Basic_2A1: uses: lleq_sort *)
lemma lfdeq_sort: ∀h,o,I1,I2,L1,L2,s.
- L1 â\89¡[h, o, â\8b\86s] L2 â\86\92 L1.â\93\98{I1} â\89¡[h, o, ⋆s] L2.ⓘ{I2}.
+ L1 â\89\9b[h, o, â\8b\86s] L2 â\86\92 L1.â\93\98{I1} â\89\9b[h, o, ⋆s] L2.ⓘ{I2}.
/2 width=1 by lfxs_sort/ qed.
-lemma lfdeq_pair: â\88\80h,o,I,L1,L2,V1,V2. L1 â\89¡[h, o, V1] L2 â\86\92 V1 â\89¡[h, o] V2 →
- L1.â\93\91{I}V1 â\89¡[h, o, #0] L2.ⓑ{I}V2.
+lemma lfdeq_pair: â\88\80h,o,I,L1,L2,V1,V2. L1 â\89\9b[h, o, V1] L2 â\86\92 V1 â\89\9b[h, o] V2 →
+ L1.â\93\91{I}V1 â\89\9b[h, o, #0] L2.ⓑ{I}V2.
/2 width=1 by lfxs_pair/ qed.
(*
lemma lfdeq_unit: ∀h,o,f,I,L1,L2. 𝐈⦃f⦄ → L1 ⪤*[cdeq_ext h o, cfull, f] L2 →
- L1.â\93¤{I} â\89¡[h, o, #0] L2.ⓤ{I}.
+ L1.â\93¤{I} â\89\9b[h, o, #0] L2.ⓤ{I}.
/2 width=3 by lfxs_unit/ qed.
*)
lemma lfdeq_lref: ∀h,o,I1,I2,L1,L2,i.
- L1 â\89¡[h, o, #i] L2 â\86\92 L1.â\93\98{I1} â\89¡[h, o, #⫯i] L2.ⓘ{I2}.
+ L1 â\89\9b[h, o, #i] L2 â\86\92 L1.â\93\98{I1} â\89\9b[h, o, #⫯i] L2.ⓘ{I2}.
/2 width=1 by lfxs_lref/ qed.
(* Basic_2A1: uses: lleq_gref *)
lemma lfdeq_gref: ∀h,o,I1,I2,L1,L2,l.
- L1 â\89¡[h, o, §l] L2 â\86\92 L1.â\93\98{I1} â\89¡[h, o, §l] L2.ⓘ{I2}.
+ L1 â\89\9b[h, o, §l] L2 â\86\92 L1.â\93\98{I1} â\89\9b[h, o, §l] L2.ⓘ{I2}.
/2 width=1 by lfxs_gref/ qed.
lemma lfdeq_bind_repl_dx: ∀h,o,I,I1,L1,L2.∀T:term.
- L1.â\93\98{I} â\89¡[h, o, T] L2.ⓘ{I1} →
- â\88\80I2. I â\89¡[h, o] I2 →
- L1.â\93\98{I} â\89¡[h, o, T] L2.ⓘ{I2}.
+ L1.â\93\98{I} â\89\9b[h, o, T] L2.ⓘ{I1} →
+ â\88\80I2. I â\89\9b[h, o] I2 →
+ L1.â\93\98{I} â\89\9b[h, o, T] L2.ⓘ{I2}.
/2 width=2 by lfxs_bind_repl_dx/ qed-.
(* Basic inversion lemmas ***************************************************)
-lemma lfdeq_inv_atom_sn: â\88\80h,o,Y2. â\88\80T:term. â\8b\86 â\89¡[h, o, T] Y2 → Y2 = ⋆.
+lemma lfdeq_inv_atom_sn: â\88\80h,o,Y2. â\88\80T:term. â\8b\86 â\89\9b[h, o, T] Y2 → Y2 = ⋆.
/2 width=3 by lfxs_inv_atom_sn/ qed-.
-lemma lfdeq_inv_atom_dx: â\88\80h,o,Y1. â\88\80T:term. Y1 â\89¡[h, o, T] ⋆ → Y1 = ⋆.
+lemma lfdeq_inv_atom_dx: â\88\80h,o,Y1. â\88\80T:term. Y1 â\89\9b[h, o, T] ⋆ → Y1 = ⋆.
/2 width=3 by lfxs_inv_atom_dx/ qed-.
(*
-lemma lfdeq_inv_zero: â\88\80h,o,Y1,Y2. Y1 â\89¡[h, o, #0] Y2 →
+lemma lfdeq_inv_zero: â\88\80h,o,Y1,Y2. Y1 â\89\9b[h, o, #0] Y2 →
∨∨ Y1 = ⋆ ∧ Y2 = ⋆
- | â\88\83â\88\83I,L1,L2,V1,V2. L1 â\89¡[h, o, V1] L2 & V1 â\89¡[h, o] V2 &
+ | â\88\83â\88\83I,L1,L2,V1,V2. L1 â\89\9b[h, o, V1] L2 & V1 â\89\9b[h, o] V2 &
Y1 = L1.ⓑ{I}V1 & Y2 = L2.ⓑ{I}V2
| ∃∃f,I,L1,L2. 𝐈⦃f⦄ & L1 ⪤*[cdeq_ext h o, cfull, f] L2 &
Y1 = L1.ⓤ{I} & Y2 = L2.ⓤ{I}.
/3 width=9 by or3_intro0, or3_intro1, or3_intro2, ex4_5_intro, ex4_4_intro, conj/
qed-.
*)
-lemma lfdeq_inv_lref: â\88\80h,o,Y1,Y2,i. Y1 â\89¡[h, o, #⫯i] Y2 →
+lemma lfdeq_inv_lref: â\88\80h,o,Y1,Y2,i. Y1 â\89\9b[h, o, #⫯i] Y2 →
(Y1 = ⋆ ∧ Y2 = ⋆) ∨
- â\88\83â\88\83I1,I2,L1,L2. L1 â\89¡[h, o, #i] L2 &
+ â\88\83â\88\83I1,I2,L1,L2. L1 â\89\9b[h, o, #i] L2 &
Y1 = L1.ⓘ{I1} & Y2 = L2.ⓘ{I2}.
/2 width=1 by lfxs_inv_lref/ qed-.
(* Basic_2A1: uses: lleq_inv_bind lleq_inv_bind_O *)
-lemma lfdeq_inv_bind: â\88\80h,o,p,I,L1,L2,V,T. L1 â\89¡[h, o, ⓑ{p,I}V.T] L2 →
- L1 â\89¡[h, o, V] L2 â\88§ L1.â\93\91{I}V â\89¡[h, o, T] L2.ⓑ{I}V.
+lemma lfdeq_inv_bind: â\88\80h,o,p,I,L1,L2,V,T. L1 â\89\9b[h, o, ⓑ{p,I}V.T] L2 →
+ L1 â\89\9b[h, o, V] L2 â\88§ L1.â\93\91{I}V â\89\9b[h, o, T] L2.ⓑ{I}V.
/2 width=2 by lfxs_inv_bind/ qed-.
(* Basic_2A1: uses: lleq_inv_flat *)
-lemma lfdeq_inv_flat: â\88\80h,o,I,L1,L2,V,T. L1 â\89¡[h, o, ⓕ{I}V.T] L2 →
- L1 â\89¡[h, o, V] L2 â\88§ L1 â\89¡[h, o, T] L2.
+lemma lfdeq_inv_flat: â\88\80h,o,I,L1,L2,V,T. L1 â\89\9b[h, o, ⓕ{I}V.T] L2 →
+ L1 â\89\9b[h, o, V] L2 â\88§ L1 â\89\9b[h, o, T] L2.
/2 width=2 by lfxs_inv_flat/ qed-.
(* Advanced inversion lemmas ************************************************)
-lemma lfdeq_inv_zero_pair_sn: â\88\80h,o,I,Y2,L1,V1. L1.â\93\91{I}V1 â\89¡[h, o, #0] Y2 →
- â\88\83â\88\83L2,V2. L1 â\89¡[h, o, V1] L2 & V1 â\89¡[h, o] V2 & Y2 = L2.ⓑ{I}V2.
+lemma lfdeq_inv_zero_pair_sn: â\88\80h,o,I,Y2,L1,V1. L1.â\93\91{I}V1 â\89\9b[h, o, #0] Y2 →
+ â\88\83â\88\83L2,V2. L1 â\89\9b[h, o, V1] L2 & V1 â\89\9b[h, o] V2 & Y2 = L2.ⓑ{I}V2.
/2 width=1 by lfxs_inv_zero_pair_sn/ qed-.
-lemma lfdeq_inv_zero_pair_dx: â\88\80h,o,I,Y1,L2,V2. Y1 â\89¡[h, o, #0] L2.ⓑ{I}V2 →
- â\88\83â\88\83L1,V1. L1 â\89¡[h, o, V1] L2 & V1 â\89¡[h, o] V2 & Y1 = L1.ⓑ{I}V1.
+lemma lfdeq_inv_zero_pair_dx: â\88\80h,o,I,Y1,L2,V2. Y1 â\89\9b[h, o, #0] L2.ⓑ{I}V2 →
+ â\88\83â\88\83L1,V1. L1 â\89\9b[h, o, V1] L2 & V1 â\89\9b[h, o] V2 & Y1 = L1.ⓑ{I}V1.
/2 width=1 by lfxs_inv_zero_pair_dx/ qed-.
-lemma lfdeq_inv_lref_bind_sn: â\88\80h,o,I1,Y2,L1,i. L1.â\93\98{I1} â\89¡[h, o, #⫯i] Y2 →
- â\88\83â\88\83I2,L2. L1 â\89¡[h, o, #i] L2 & Y2 = L2.ⓘ{I2}.
+lemma lfdeq_inv_lref_bind_sn: â\88\80h,o,I1,Y2,L1,i. L1.â\93\98{I1} â\89\9b[h, o, #⫯i] Y2 →
+ â\88\83â\88\83I2,L2. L1 â\89\9b[h, o, #i] L2 & Y2 = L2.ⓘ{I2}.
/2 width=2 by lfxs_inv_lref_bind_sn/ qed-.
-lemma lfdeq_inv_lref_bind_dx: â\88\80h,o,I2,Y1,L2,i. Y1 â\89¡[h, o, #⫯i] L2.ⓘ{I2} →
- â\88\83â\88\83I1,L1. L1 â\89¡[h, o, #i] L2 & Y1 = L1.ⓘ{I1}.
+lemma lfdeq_inv_lref_bind_dx: â\88\80h,o,I2,Y1,L2,i. Y1 â\89\9b[h, o, #⫯i] L2.ⓘ{I2} →
+ â\88\83â\88\83I1,L1. L1 â\89\9b[h, o, #i] L2 & Y1 = L1.ⓘ{I1}.
/2 width=2 by lfxs_inv_lref_bind_dx/ qed-.
(* Basic forward lemmas *****************************************************)
lemma lfdeq_fwd_zero_pair: ∀h,o,I,K1,K2,V1,V2.
- K1.â\93\91{I}V1 â\89¡[h, o, #0] K2.â\93\91{I}V2 â\86\92 K1 â\89¡[h, o, V1] K2.
+ K1.â\93\91{I}V1 â\89\9b[h, o, #0] K2.â\93\91{I}V2 â\86\92 K1 â\89\9b[h, o, V1] K2.
/2 width=3 by lfxs_fwd_zero_pair/ qed-.
(* Basic_2A1: uses: lleq_fwd_bind_sn lleq_fwd_flat_sn *)
-lemma lfdeq_fwd_pair_sn: â\88\80h,o,I,L1,L2,V,T. L1 â\89¡[h, o, â\91¡{I}V.T] L2 â\86\92 L1 â\89¡[h, o, V] L2.
+lemma lfdeq_fwd_pair_sn: â\88\80h,o,I,L1,L2,V,T. L1 â\89\9b[h, o, â\91¡{I}V.T] L2 â\86\92 L1 â\89\9b[h, o, V] L2.
/2 width=3 by lfxs_fwd_pair_sn/ qed-.
(* Basic_2A1: uses: lleq_fwd_bind_dx lleq_fwd_bind_O_dx *)
lemma lfdeq_fwd_bind_dx: ∀h,o,p,I,L1,L2,V,T.
- L1 â\89¡[h, o, â\93\91{p,I}V.T] L2 â\86\92 L1.â\93\91{I}V â\89¡[h, o, T] L2.ⓑ{I}V.
+ L1 â\89\9b[h, o, â\93\91{p,I}V.T] L2 â\86\92 L1.â\93\91{I}V â\89\9b[h, o, T] L2.ⓑ{I}V.
/2 width=2 by lfxs_fwd_bind_dx/ qed-.
(* Basic_2A1: uses: lleq_fwd_flat_dx *)
-lemma lfdeq_fwd_flat_dx: â\88\80h,o,I,L1,L2,V,T. L1 â\89¡[h, o, â\93\95{I}V.T] L2 â\86\92 L1 â\89¡[h, o, T] L2.
+lemma lfdeq_fwd_flat_dx: â\88\80h,o,I,L1,L2,V,T. L1 â\89\9b[h, o, â\93\95{I}V.T] L2 â\86\92 L1 â\89\9b[h, o, T] L2.
/2 width=3 by lfxs_fwd_flat_dx/ qed-.
-lemma lfdeq_fwd_dx: â\88\80h,o,I2,L1,K2. â\88\80T:term. L1 â\89¡[h, o, T] K2.ⓘ{I2} →
+lemma lfdeq_fwd_dx: â\88\80h,o,I2,L1,K2. â\88\80T:term. L1 â\89\9b[h, o, T] K2.ⓘ{I2} →
∃∃I1,K1. L1 = K1.ⓘ{I1}.
/2 width=5 by lfxs_fwd_dx/ qed-.
/2 width=5 by lfxs_dropable_dx/ qed-.
(* Basic_2A1: uses: lleq_inv_lift_le lleq_inv_lift_be lleq_inv_lift_ge *)
-lemma lfdeq_inv_lifts_bi: â\88\80h,o,L1,L2,U. L1 â\89¡[h, o, U] L2 → ∀b,f. 𝐔⦃f⦄ →
+lemma lfdeq_inv_lifts_bi: â\88\80h,o,L1,L2,U. L1 â\89\9b[h, o, U] L2 → ∀b,f. 𝐔⦃f⦄ →
∀K1,K2. ⬇*[b, f] L1 ≡ K1 → ⬇*[b, f] L2 ≡ K2 →
- â\88\80T. â¬\86*[f] T â\89¡ U â\86\92 K1 â\89¡[h, o, T] K2.
+ â\88\80T. â¬\86*[f] T â\89¡ U â\86\92 K1 â\89\9b[h, o, T] K2.
/2 width=10 by lfxs_inv_lifts_bi/ qed-.
-lemma lfdeq_inv_lref_pair_sn: â\88\80h,o,L1,L2,i. L1 â\89¡[h, o, #i] L2 → ∀I,K1,V1. ⬇*[i] L1 ≡ K1.ⓑ{I}V1 →
- â\88\83â\88\83K2,V2. â¬\87*[i] L2 â\89¡ K2.â\93\91{I}V2 & K1 â\89¡[h, o, V1] K2 & V1 â\89¡[h, o] V2.
+lemma lfdeq_inv_lref_pair_sn: â\88\80h,o,L1,L2,i. L1 â\89\9b[h, o, #i] L2 → ∀I,K1,V1. ⬇*[i] L1 ≡ K1.ⓑ{I}V1 →
+ â\88\83â\88\83K2,V2. â¬\87*[i] L2 â\89¡ K2.â\93\91{I}V2 & K1 â\89\9b[h, o, V1] K2 & V1 â\89\9b[h, o] V2.
/2 width=3 by lfxs_inv_lref_pair_sn/ qed-.
-lemma lfdeq_inv_lref_pair_dx: â\88\80h,o,L1,L2,i. L1 â\89¡[h, o, #i] L2 → ∀I,K2,V2. ⬇*[i] L2 ≡ K2.ⓑ{I}V2 →
- â\88\83â\88\83K1,V1. â¬\87*[i] L1 â\89¡ K1.â\93\91{I}V1 & K1 â\89¡[h, o, V1] K2 & V1 â\89¡[h, o] V2.
+lemma lfdeq_inv_lref_pair_dx: â\88\80h,o,L1,L2,i. L1 â\89\9b[h, o, #i] L2 → ∀I,K2,V2. ⬇*[i] L2 ≡ K2.ⓑ{I}V2 →
+ â\88\83â\88\83K1,V1. â¬\87*[i] L1 â\89¡ K1.â\93\91{I}V1 & K1 â\89\9b[h, o, V1] K2 & V1 â\89\9b[h, o] V2.
/2 width=3 by lfxs_inv_lref_pair_dx/ qed-.
lemma lfdeq_refl: ∀h,o,T. reflexive … (lfdeq h o T).
/2 width=1 by lfxs_refl/ qed.
-lemma lfdeq_pair_refl: â\88\80h,o,V1,V2. V1 â\89¡[h, o] V2 →
- â\88\80I,L. â\88\80T:term. L.â\93\91{I}V1 â\89¡[h, o, T] L.ⓑ{I}V2.
+lemma lfdeq_pair_refl: â\88\80h,o,V1,V2. V1 â\89\9b[h, o] V2 →
+ â\88\80I,L. â\88\80T:term. L.â\93\91{I}V1 â\89\9b[h, o, T] L.ⓑ{I}V2.
/2 width=1 by lfxs_pair_refl/ qed.
(* Advanced inversion lemmas ************************************************)
-lemma lfdeq_inv_bind_void: â\88\80h,o,p,I,L1,L2,V,T. L1 â\89¡[h, o, ⓑ{p,I}V.T] L2 →
- L1 â\89¡[h, o, V] L2 â\88§ L1.â\93§ â\89¡[h, o, T] L2.ⓧ.
+lemma lfdeq_inv_bind_void: â\88\80h,o,p,I,L1,L2,V,T. L1 â\89\9b[h, o, ⓑ{p,I}V.T] L2 →
+ L1 â\89\9b[h, o, V] L2 â\88§ L1.â\93§ â\89\9b[h, o, T] L2.ⓧ.
/2 width=3 by lfxs_inv_bind_void/ qed-.
(* Advanced forward lemmas **************************************************)
lemma lfdeq_fwd_bind_dx_void: ∀h,o,p,I,L1,L2,V,T.
- L1 â\89¡[h, o, â\93\91{p,I}V.T] L2 â\86\92 L1.â\93§ â\89¡[h, o, T] L2.ⓧ.
+ L1 â\89\9b[h, o, â\93\91{p,I}V.T] L2 â\86\92 L1.â\93§ â\89\9b[h, o, T] L2.ⓧ.
/2 width=4 by lfxs_fwd_bind_dx_void/ qed-.
(* Properties with supclosure ***********************************************)
lemma fqu_tdeq_conf: ∀h,o,b,G1,G2,L1,L2,U1,T1. ⦃G1, L1, U1⦄ ⊐[b] ⦃G2, L2, T1⦄ →
- â\88\80U2. U1 â\89¡[h, o] U2 →
- â\88\83â\88\83L,T2. â¦\83G1, L1, U2â¦\84 â\8a\90[b] â¦\83G2, L, T2â¦\84 & L2 â\89¡[h, o, T1] L & T1 â\89¡[h, o] T2.
+ â\88\80U2. U1 â\89\9b[h, o] U2 →
+ â\88\83â\88\83L,T2. â¦\83G1, L1, U2â¦\84 â\8a\90[b] â¦\83G2, L, T2â¦\84 & L2 â\89\9b[h, o, T1] L & T1 â\89\9b[h, o] T2.
#h #o #b #G1 #G2 #L1 #L2 #U1 #T1 #H elim H -G1 -G2 -L1 -L2 -U1 -T1
[ #I #G #L #W #X #H >(tdeq_inv_lref1 … H) -X
/2 width=5 by fqu_lref_O, ex3_2_intro/
qed-.
lemma tdeq_fqu_trans: ∀h,o,b,G1,G2,L1,L2,U1,T1. ⦃G1, L1, U1⦄ ⊐[b] ⦃G2, L2, T1⦄ →
- â\88\80U2. U2 â\89¡[h, o] U1 →
- â\88\83â\88\83L,T2. â¦\83G1, L1, U2â¦\84 â\8a\90[b] â¦\83G2, L, T2â¦\84 & T2 â\89¡[h, o] T1 & L â\89¡[h, o, T1] L2.
+ â\88\80U2. U2 â\89\9b[h, o] U1 →
+ â\88\83â\88\83L,T2. â¦\83G1, L1, U2â¦\84 â\8a\90[b] â¦\83G2, L, T2â¦\84 & T2 â\89\9b[h, o] T1 & L â\89\9b[h, o, T1] L2.
#h #o #b #G1 #G2 #L1 #L2 #U1 #T1 #H12 #U2 #HU21
elim (fqu_tdeq_conf … o … H12 U2) -H12
/3 width=5 by lfdeq_sym, tdeq_sym, ex3_2_intro/
(* Basic_2A1: was just: lleq_fqu_trans *)
lemma lfdeq_fqu_trans: ∀h,o,b,G1,G2,L2,K2,T,U. ⦃G1, L2, T⦄ ⊐[b] ⦃G2, K2, U⦄ →
- â\88\80L1. L1 â\89¡[h, o, T] L2 →
- â\88\83â\88\83K1,U0. â¦\83G1, L1, Tâ¦\84 â\8a\90[b] â¦\83G2, K1, U0â¦\84 & U0 â\89¡[h, o] U & K1 â\89¡[h, o, U] K2.
+ â\88\80L1. L1 â\89\9b[h, o, T] L2 →
+ â\88\83â\88\83K1,U0. â¦\83G1, L1, Tâ¦\84 â\8a\90[b] â¦\83G2, K1, U0â¦\84 & U0 â\89\9b[h, o] U & K1 â\89\9b[h, o, U] K2.
#h #o #b #G1 #G2 #L2 #K2 #T #U #H elim H -G1 -G2 -L2 -K2 -T -U
[ #I #G #L2 #V2 #L1 #H elim (lfdeq_inv_zero_pair_dx … H) -H
#K1 #V1 #HV1 #HV12 #H destruct
(* Basic_2A1: was just: lleq_fquq_trans *)
lemma lfdeq_fquq_trans: ∀h,o,b,G1,G2,L2,K2,T,U. ⦃G1, L2, T⦄ ⊐⸮[b] ⦃G2, K2, U⦄ →
- â\88\80L1. L1 â\89¡[h, o, T] L2 →
- â\88\83â\88\83K1,U0. â¦\83G1, L1, Tâ¦\84 â\8a\90⸮[b] â¦\83G2, K1, U0â¦\84 & U0 â\89¡[h, o] U & K1 â\89¡[h, o, U] K2.
+ â\88\80L1. L1 â\89\9b[h, o, T] L2 →
+ â\88\83â\88\83K1,U0. â¦\83G1, L1, Tâ¦\84 â\8a\90⸮[b] â¦\83G2, K1, U0â¦\84 & U0 â\89\9b[h, o] U & K1 â\89\9b[h, o, U] K2.
#h #o #b #G1 #G2 #L2 #K2 #T #U #H elim H -H
[ #H #L1 #HL12 elim (lfdeq_fqu_trans … H … HL12) -L2 /3 width=5 by fqu_fquq, ex3_2_intro/
| * #HG #HL #HT destruct /2 width=5 by ex3_2_intro/
(* Basic_2A1: was just: lleq_fqup_trans *)
lemma lfdeq_fqup_trans: ∀h,o,b,G1,G2,L2,K2,T,U. ⦃G1, L2, T⦄ ⊐+[b] ⦃G2, K2, U⦄ →
- â\88\80L1. L1 â\89¡[h, o, T] L2 →
- â\88\83â\88\83K1,U0. â¦\83G1, L1, Tâ¦\84 â\8a\90+[b] â¦\83G2, K1, U0â¦\84 & U0 â\89¡[h, o] U & K1 â\89¡[h, o, U] K2.
+ â\88\80L1. L1 â\89\9b[h, o, T] L2 →
+ â\88\83â\88\83K1,U0. â¦\83G1, L1, Tâ¦\84 â\8a\90+[b] â¦\83G2, K1, U0â¦\84 & U0 â\89\9b[h, o] U & K1 â\89\9b[h, o, U] K2.
#h #o #b #G1 #G2 #L2 #K2 #T #U #H @(fqup_ind … H) -G2 -K2 -U
[ #G2 #K2 #U #HTU #L1 #HL12 elim (lfdeq_fqu_trans … HTU … HL12) -L2
/3 width=5 by fqu_fqup, ex3_2_intro/
(* Basic_2A1: was just: lleq_fqus_trans *)
lemma lfdeq_fqus_trans: ∀h,o,b,G1,G2,L2,K2,T,U. ⦃G1, L2, T⦄ ⊐*[b] ⦃G2, K2, U⦄ →
- â\88\80L1. L1 â\89¡[h, o, T] L2 →
- â\88\83â\88\83K1,U0. â¦\83G1, L1, Tâ¦\84 â\8a\90*[b] â¦\83G2, K1, U0â¦\84 & U0 â\89¡[h, o] U & K1 â\89¡[h, o, U] K2.
+ â\88\80L1. L1 â\89\9b[h, o, T] L2 →
+ â\88\83â\88\83K1,U0. â¦\83G1, L1, Tâ¦\84 â\8a\90*[b] â¦\83G2, K1, U0â¦\84 & U0 â\89\9b[h, o] U & K1 â\89\9b[h, o, U] K2.
#h #o #b #G1 #G2 #L2 #K2 #T #U #H #L1 #HL12 elim(fqus_inv_fqup … H) -H
[ #H elim (lfdeq_fqup_trans … H … HL12) -L2 /3 width=5 by fqup_fqus, ex3_2_intro/
| * #HG #HL #HT destruct /2 width=5 by ex3_2_intro/
(* Forward lemmas with length for local environments ************************)
(* Basic_2A1: lleq_fwd_length *)
-lemma lfdeq_fwd_length: â\88\80h,o,L1,L2. â\88\80T:term. L1 â\89¡[h, o, T] L2 → |L1| = |L2|.
+lemma lfdeq_fwd_length: â\88\80h,o,L1,L2. â\88\80T:term. L1 â\89\9b[h, o, T] L2 → |L1| = |L2|.
/2 width=3 by lfxs_fwd_length/ qed-.
(* Properties with length for local environments ****************************)
(* Basic_2A1: uses: lleq_lift_le lleq_lift_ge *)
-lemma lfdeq_lifts_bi: â\88\80L1,L2. |L1| = |L2| â\86\92 â\88\80h,o,K1,K2,T. K1 â\89¡[h, o, T] K2 →
+lemma lfdeq_lifts_bi: â\88\80L1,L2. |L1| = |L2| â\86\92 â\88\80h,o,K1,K2,T. K1 â\89\9b[h, o, T] K2 →
∀b,f. ⬇*[b, f] L1 ≡ K1 → ⬇*[b, f] L2 ≡ K2 →
- â\88\80U. â¬\86*[f] T â\89¡ U â\86\92 L1 â\89¡[h, o, U] L2.
+ â\88\80U. â¬\86*[f] T â\89¡ U â\86\92 L1 â\89\9b[h, o, U] L2.
/3 width=9 by lfxs_lifts_bi, tdeq_lifts_sn/ qed-.
(* Advanced properties ******************************************************)
(* Basic_2A1: uses: lleq_dec *)
-lemma lfdeq_dec: â\88\80h,o,L1,L2. â\88\80T:term. Decidable (L1 â\89¡[h, o, T] L2).
+lemma lfdeq_dec: â\88\80h,o,L1,L2. â\88\80T:term. Decidable (L1 â\89\9b[h, o, T] L2).
/3 width=1 by lfxs_dec, tdeq_dec/ qed-.
(* Main properties **********************************************************)
(* Basic_2A1: uses: lleq_bind lleq_bind_O *)
theorem lfdeq_bind: ∀h,o,p,I,L1,L2,V1,V2,T.
- L1 â\89¡[h, o, V1] L2 â\86\92 L1.â\93\91{I}V1 â\89¡[h, o, T] L2.ⓑ{I}V2 →
- L1 â\89¡[h, o, ⓑ{p,I}V1.T] L2.
+ L1 â\89\9b[h, o, V1] L2 â\86\92 L1.â\93\91{I}V1 â\89\9b[h, o, T] L2.ⓑ{I}V2 →
+ L1 â\89\9b[h, o, ⓑ{p,I}V1.T] L2.
/2 width=2 by lfxs_bind/ qed.
(* Basic_2A1: uses: lleq_flat *)
-theorem lfdeq_flat: â\88\80h,o,I,L1,L2,V,T. L1 â\89¡[h, o, V] L2 â\86\92 L1 â\89¡[h, o, T] L2 →
- L1 â\89¡[h, o, ⓕ{I}V.T] L2.
+theorem lfdeq_flat: â\88\80h,o,I,L1,L2,V,T. L1 â\89\9b[h, o, V] L2 â\86\92 L1 â\89\9b[h, o, T] L2 →
+ L1 â\89\9b[h, o, ⓕ{I}V.T] L2.
/2 width=1 by lfxs_flat/ qed.
theorem lfdeq_bind_void: ∀h,o,p,I,L1,L2,V,T.
- L1 â\89¡[h, o, V] L2 â\86\92 L1.â\93§ â\89¡[h, o, T] L2.ⓧ →
- L1 â\89¡[h, o, ⓑ{p,I}V.T] L2.
+ L1 â\89\9b[h, o, V] L2 â\86\92 L1.â\93§ â\89\9b[h, o, T] L2.ⓧ →
+ L1 â\89\9b[h, o, ⓑ{p,I}V.T] L2.
/2 width=1 by lfxs_bind_void/ qed.
(* Basic_2A1: uses: lleq_trans *)
theorem lfdeq_canc_dx: ∀h,o,T. right_cancellable … (lfdeq h o T).
/3 width=3 by lfdeq_trans, lfdeq_sym/ qed-.
-theorem lfdeq_repl: â\88\80h,o,L1,L2. â\88\80T:term. L1 â\89¡[h, o, T] L2 →
- â\88\80K1. L1 â\89¡[h, o, T] K1 â\86\92 â\88\80K2. L2 â\89¡[h, o, T] K2 â\86\92 K1 â\89¡[h, o, T] K2.
+theorem lfdeq_repl: â\88\80h,o,L1,L2. â\88\80T:term. L1 â\89\9b[h, o, T] L2 →
+ â\88\80K1. L1 â\89\9b[h, o, T] K1 â\86\92 â\88\80K2. L2 â\89\9b[h, o, T] K2 â\86\92 K1 â\89\9b[h, o, T] K2.
/3 width=3 by lfdeq_canc_sn, lfdeq_trans/ qed-.
(* Negated properties *******************************************************)
(* Note: auto works with /4 width=8/ so lfdeq_canc_sn is preferred **********)
(* Basic_2A1: uses: lleq_nlleq_trans *)
-lemma lfdeq_lfdneq_trans: â\88\80h,o.â\88\80T:term.â\88\80L1,L. L1 â\89¡[h, o, T] L →
- â\88\80L2. (L â\89¡[h, o, T] L2 â\86\92 â\8a¥) â\86\92 (L1 â\89¡[h, o, T] L2 → ⊥).
+lemma lfdeq_lfdneq_trans: â\88\80h,o.â\88\80T:term.â\88\80L1,L. L1 â\89\9b[h, o, T] L →
+ â\88\80L2. (L â\89\9b[h, o, T] L2 â\86\92 â\8a¥) â\86\92 (L1 â\89\9b[h, o, T] L2 → ⊥).
/3 width=3 by lfdeq_canc_sn/ qed-.
(* Basic_2A1: uses: nlleq_lleq_div *)
-lemma lfdneq_lfdeq_div: â\88\80h,o.â\88\80T:term.â\88\80L2,L. L2 â\89¡[h, o, T] L →
- â\88\80L1. (L1 â\89¡[h, o, T] L â\86\92 â\8a¥) â\86\92 (L1 â\89¡[h, o, T] L2 → ⊥).
+lemma lfdneq_lfdeq_div: â\88\80h,o.â\88\80T:term.â\88\80L2,L. L2 â\89\9b[h, o, T] L →
+ â\88\80L1. (L1 â\89\9b[h, o, T] L â\86\92 â\8a¥) â\86\92 (L1 â\89\9b[h, o, T] L2 → ⊥).
/3 width=3 by lfdeq_trans/ qed-.
-theorem lfdneq_lfdeq_canc_dx: â\88\80h,o,L1,L. â\88\80T:term. (L1 â\89¡[h, o, T] L → ⊥) →
- â\88\80L2. L2 â\89¡[h, o, T] L â\86\92 L1 â\89¡[h, o, T] L2 → ⊥.
+theorem lfdneq_lfdeq_canc_dx: â\88\80h,o,L1,L. â\88\80T:term. (L1 â\89\9b[h, o, T] L → ⊥) →
+ â\88\80L2. L2 â\89\9b[h, o, T] L â\86\92 L1 â\89\9b[h, o, T] L2 → ⊥.
/3 width=3 by lfdeq_trans/ qed-.
(* Negated inversion lemmas *************************************************)
(* Basic_2A1: uses: nlleq_inv_bind nlleq_inv_bind_O *)
-lemma lfdneq_inv_bind: â\88\80h,o,p,I,L1,L2,V,T. (L1 â\89¡[h, o, ⓑ{p,I}V.T] L2 → ⊥) →
- (L1 â\89¡[h, o, V] L2 â\86\92 â\8a¥) â\88¨ (L1.â\93\91{I}V â\89¡[h, o, T] L2.ⓑ{I}V → ⊥).
+lemma lfdneq_inv_bind: â\88\80h,o,p,I,L1,L2,V,T. (L1 â\89\9b[h, o, ⓑ{p,I}V.T] L2 → ⊥) →
+ (L1 â\89\9b[h, o, V] L2 â\86\92 â\8a¥) â\88¨ (L1.â\93\91{I}V â\89\9b[h, o, T] L2.ⓑ{I}V → ⊥).
/3 width=2 by lfnxs_inv_bind, tdeq_dec/ qed-.
(* Basic_2A1: uses: nlleq_inv_flat *)
-lemma lfdneq_inv_flat: â\88\80h,o,I,L1,L2,V,T. (L1 â\89¡[h, o, ⓕ{I}V.T] L2 → ⊥) →
- (L1 â\89¡[h, o, V] L2 â\86\92 â\8a¥) â\88¨ (L1 â\89¡[h, o, T] L2 → ⊥).
+lemma lfdneq_inv_flat: â\88\80h,o,I,L1,L2,V,T. (L1 â\89\9b[h, o, ⓕ{I}V.T] L2 → ⊥) →
+ (L1 â\89\9b[h, o, V] L2 â\86\92 â\8a¥) â\88¨ (L1 â\89\9b[h, o, T] L2 → ⊥).
/3 width=2 by lfnxs_inv_flat, tdeq_dec/ qed-.
-lemma lfdneq_inv_bind_void: â\88\80h,o,p,I,L1,L2,V,T. (L1 â\89¡[h, o, ⓑ{p,I}V.T] L2 → ⊥) →
- (L1 â\89¡[h, o, V] L2 â\86\92 â\8a¥) â\88¨ (L1.â\93§ â\89¡[h, o, T] L2.ⓧ → ⊥).
+lemma lfdneq_inv_bind_void: â\88\80h,o,p,I,L1,L2,V,T. (L1 â\89\9b[h, o, ⓑ{p,I}V.T] L2 → ⊥) →
+ (L1 â\89\9b[h, o, V] L2 â\86\92 â\8a¥) â\88¨ (L1.â\93§ â\89\9b[h, o, T] L2.ⓧ → ⊥).
/3 width=3 by lfnxs_inv_bind_void, tdeq_dec/ qed-.
(* *)
(**************************************************************************)
-include "basic_2/notation/relations/lazyeq_4.ma".
+include "basic_2/notation/relations/stareq_4.ma".
include "basic_2/syntax/item_sd.ma".
include "basic_2/syntax/term.ma".
interpretation
"context-free degree-based equivalence (term)"
- 'LazyEq h o T1 T2 = (tdeq h o T1 T2).
+ 'StarEq h o T1 T2 = (tdeq h o T1 T2).
(* Basic inversion lemmas ***************************************************)
-fact tdeq_inv_sort1_aux: â\88\80h,o,X,Y. X â\89¡[h, o] Y → ∀s1. X = ⋆s1 →
+fact tdeq_inv_sort1_aux: â\88\80h,o,X,Y. X â\89\9b[h, o] Y → ∀s1. X = ⋆s1 →
∃∃s2,d. deg h o s1 d & deg h o s2 d & Y = ⋆s2.
#h #o #X #Y * -X -Y
[ #s1 #s2 #d #Hs1 #Hs2 #s #H destruct /2 width=5 by ex3_2_intro/
]
qed-.
-lemma tdeq_inv_sort1: â\88\80h,o,Y,s1. â\8b\86s1 â\89¡[h, o] Y →
+lemma tdeq_inv_sort1: â\88\80h,o,Y,s1. â\8b\86s1 â\89\9b[h, o] Y →
∃∃s2,d. deg h o s1 d & deg h o s2 d & Y = ⋆s2.
/2 width=3 by tdeq_inv_sort1_aux/ qed-.
-fact tdeq_inv_lref1_aux: â\88\80h,o,X,Y. X â\89¡[h, o] Y → ∀i. X = #i → Y = #i.
+fact tdeq_inv_lref1_aux: â\88\80h,o,X,Y. X â\89\9b[h, o] Y → ∀i. X = #i → Y = #i.
#h #o #X #Y * -X -Y //
[ #s1 #s2 #d #_ #_ #j #H destruct
| #I #V1 #V2 #T1 #T2 #_ #_ #j #H destruct
]
qed-.
-lemma tdeq_inv_lref1: â\88\80h,o,Y,i. #i â\89¡[h, o] Y → Y = #i.
+lemma tdeq_inv_lref1: â\88\80h,o,Y,i. #i â\89\9b[h, o] Y → Y = #i.
/2 width=5 by tdeq_inv_lref1_aux/ qed-.
-fact tdeq_inv_gref1_aux: â\88\80h,o,X,Y. X â\89¡[h, o] Y → ∀l. X = §l → Y = §l.
+fact tdeq_inv_gref1_aux: â\88\80h,o,X,Y. X â\89\9b[h, o] Y → ∀l. X = §l → Y = §l.
#h #o #X #Y * -X -Y //
[ #s1 #s2 #d #_ #_ #k #H destruct
| #I #V1 #V2 #T1 #T2 #_ #_ #k #H destruct
]
qed-.
-lemma tdeq_inv_gref1: â\88\80h,o,Y,l. §l â\89¡[h, o] Y → Y = §l.
+lemma tdeq_inv_gref1: â\88\80h,o,Y,l. §l â\89\9b[h, o] Y → Y = §l.
/2 width=5 by tdeq_inv_gref1_aux/ qed-.
-fact tdeq_inv_pair1_aux: â\88\80h,o,X,Y. X â\89¡[h, o] Y → ∀I,V1,T1. X = ②{I}V1.T1 →
- â\88\83â\88\83V2,T2. V1 â\89¡[h, o] V2 & T1 â\89¡[h, o] T2 & Y = ②{I}V2.T2.
+fact tdeq_inv_pair1_aux: â\88\80h,o,X,Y. X â\89\9b[h, o] Y → ∀I,V1,T1. X = ②{I}V1.T1 →
+ â\88\83â\88\83V2,T2. V1 â\89\9b[h, o] V2 & T1 â\89\9b[h, o] T2 & Y = ②{I}V2.T2.
#h #o #X #Y * -X -Y
[ #s1 #s2 #d #_ #_ #J #W1 #U1 #H destruct
| #i #J #W1 #U1 #H destruct
]
qed-.
-lemma tdeq_inv_pair1: â\88\80h,o,I,V1,T1,Y. â\91¡{I}V1.T1 â\89¡[h, o] Y →
- â\88\83â\88\83V2,T2. V1 â\89¡[h, o] V2 & T1 â\89¡[h, o] T2 & Y = ②{I}V2.T2.
+lemma tdeq_inv_pair1: â\88\80h,o,I,V1,T1,Y. â\91¡{I}V1.T1 â\89\9b[h, o] Y →
+ â\88\83â\88\83V2,T2. V1 â\89\9b[h, o] V2 & T1 â\89\9b[h, o] T2 & Y = ②{I}V2.T2.
/2 width=3 by tdeq_inv_pair1_aux/ qed-.
(* Advanced inversion lemmas ************************************************)
-lemma tdeq_inv_sort1_deg: â\88\80h,o,Y,s1. â\8b\86s1 â\89¡[h, o] Y → ∀d. deg h o s1 d →
+lemma tdeq_inv_sort1_deg: â\88\80h,o,Y,s1. â\8b\86s1 â\89\9b[h, o] Y → ∀d. deg h o s1 d →
∃∃s2. deg h o s2 d & Y = ⋆s2.
#h #o #Y #s1 #H #d #Hs1 elim (tdeq_inv_sort1 … H) -H
#s2 #x #Hx <(deg_mono h o … Hx … Hs1) -s1 -d /2 width=3 by ex2_intro/
qed-.
-lemma tdeq_inv_sort_deg: â\88\80h,o,s1,s2. â\8b\86s1 â\89¡[h, o] ⋆s2 →
+lemma tdeq_inv_sort_deg: â\88\80h,o,s1,s2. â\8b\86s1 â\89\9b[h, o] ⋆s2 →
∀d1,d2. deg h o s1 d1 → deg h o s2 d2 →
d1 = d2.
#h #o #s1 #y #H #d1 #d2 #Hs1 #Hy
<(deg_mono h o … Hy … Hs2) -s2 -d1 //
qed-.
-lemma tdeq_inv_pair: â\88\80h,o,I1,I2,V1,V2,T1,T2. â\91¡{I1}V1.T1 â\89¡[h, o] ②{I2}V2.T2 →
- â\88§â\88§ I1 = I2 & V1 â\89¡[h, o] V2 & T1 â\89¡[h, o] T2.
+lemma tdeq_inv_pair: â\88\80h,o,I1,I2,V1,V2,T1,T2. â\91¡{I1}V1.T1 â\89\9b[h, o] ②{I2}V2.T2 →
+ â\88§â\88§ I1 = I2 & V1 â\89\9b[h, o] V2 & T1 â\89\9b[h, o] T2.
#h #o #I1 #I2 #V1 #V2 #T1 #T2 #H elim (tdeq_inv_pair1 … H) -H
#V0 #T0 #HV #HT #H destruct /2 width=1 by and3_intro/
qed-.
-lemma tdeq_inv_pair_xy_y: â\88\80h,o,I,T,V. â\91¡{I}V.T â\89¡[h, o] T → ⊥.
+lemma tdeq_inv_pair_xy_y: â\88\80h,o,I,T,V. â\91¡{I}V.T â\89\9b[h, o] T → ⊥.
#h #o #I #T elim T -T
[ #J #V #H elim (tdeq_inv_pair1 … H) -H #X #Y #_ #_ #H destruct
| #J #X #Y #_ #IHY #V #H elim (tdeq_inv_pair … H) -H #H #_ #HY destruct /2 width=2 by/
(* Basic forward lemmas *****************************************************)
-lemma tdeq_fwd_atom1: â\88\80h,o,I,Y. â\93ª{I} â\89¡[h, o] Y → ∃J. Y = ⓪{J}.
+lemma tdeq_fwd_atom1: â\88\80h,o,I,Y. â\93ª{I} â\89\9b[h, o] Y → ∃J. Y = ⓪{J}.
#h #o * #x #Y #H [ elim (tdeq_inv_sort1 … H) -H ]
/3 width=4 by tdeq_inv_gref1, tdeq_inv_lref1, ex_intro/
qed-.
/2 width=3 by tdeq_sort, tdeq_lref, tdeq_gref, tdeq_pair/
qed-.
-lemma tdeq_dec: â\88\80h,o,T1,T2. Decidable (T1 â\89¡[h, o] T2).
+lemma tdeq_dec: â\88\80h,o,T1,T2. Decidable (T1 â\89\9b[h, o] T2).
#h #o #T1 elim T1 -T1 [ * #s1 | #I1 #V1 #T1 #IHV #IHT ] * [1,3,5,7: * #s2 |*: #I2 #V2 #T2 ]
[ elim (deg_total h o s1) #d1 #H1
elim (deg_total h o s2) #d2 #H2
(* Negated inversion lemmas *************************************************)
lemma tdneq_inv_pair: ∀h,o,I1,I2,V1,V2,T1,T2.
- (â\91¡{I1}V1.T1 â\89¡[h, o] ②{I2}V2.T2 → ⊥) →
+ (â\91¡{I1}V1.T1 â\89\9b[h, o] ②{I2}V2.T2 → ⊥) →
∨∨ I1 = I2 → ⊥
- | (V1 â\89¡[h, o] V2 → ⊥)
- | (T1 â\89¡[h, o] T2 → ⊥).
+ | (V1 â\89\9b[h, o] V2 → ⊥)
+ | (T1 â\89\9b[h, o] T2 → ⊥).
#h #o #I1 #I2 #V1 #V2 #T1 #T2 #H12
elim (eq_item2_dec I1 I2) /3 width=1 by or3_intro0/ #H destruct
elim (tdeq_dec h o V1 V2) /3 width=1 by or3_intro1/
(* *)
(**************************************************************************)
-include "basic_2/notation/relations/lazyeq_5.ma".
+include "basic_2/notation/relations/stareq_5.ma".
include "basic_2/syntax/tdeq.ma".
include "basic_2/syntax/lenv_ext2.ma".
interpretation
"context-free degree-based equivalence (binder)"
- 'LazyEq h o I1 I2 = (tdeq_ext h o I1 I2).
+ 'StarEq h o I1 I2 = (tdeq_ext h o I1 I2).
interpretation
"context-dependent degree-based equivalence (term)"
- 'LazyEq h o L T1 T2 = (cdeq h o L T1 T2).
+ 'StarEq h o L T1 T2 = (cdeq h o L T1 T2).
interpretation
"context-dependent degree-based equivalence (binder)"
- 'LazyEq h o L I1 I2 = (cdeq_ext h o L I1 I2).
+ 'StarEq h o L I1 I2 = (cdeq_ext h o L I1 I2).
theorem tdeq_canc_dx: ∀h,o. right_cancellable … (tdeq h o).
/3 width=3 by tdeq_trans, tdeq_sym/ qed-.
-theorem tdeq_repl: â\88\80h,o,T1,T2. T1 â\89¡[h, o] T2 →
- â\88\80U1. T1 â\89¡[h, o] U1 â\86\92 â\88\80U2. T2 â\89¡[h, o] U2 â\86\92 U1 â\89¡[h, o] U2.
+theorem tdeq_repl: â\88\80h,o,T1,T2. T1 â\89\9b[h, o] T2 →
+ â\88\80U1. T1 â\89\9b[h, o] U1 â\86\92 â\88\80U2. T2 â\89\9b[h, o] U2 â\86\92 U1 â\89\9b[h, o] U2.
/3 width=3 by tdeq_canc_sn, tdeq_trans/ qed-.
(* Negated main properies ***************************************************)
-theorem tdeq_tdneq_trans: â\88\80h,o,T1,T. T1 â\89¡[h, o] T â\86\92 â\88\80T2. (T â\89¡[h, o] T2 → ⊥) →
- T1 â\89¡[h, o] T2 → ⊥.
+theorem tdeq_tdneq_trans: â\88\80h,o,T1,T. T1 â\89\9b[h, o] T â\86\92 â\88\80T2. (T â\89\9b[h, o] T2 → ⊥) →
+ T1 â\89\9b[h, o] T2 → ⊥.
/3 width=3 by tdeq_canc_sn/ qed-.
-theorem tdneq_tdeq_canc_dx: â\88\80h,o,T1,T. (T1 â\89¡[h, o] T â\86\92 â\8a¥) â\86\92 â\88\80T2. T2 â\89¡[h, o] T →
- T1 â\89¡[h, o] T2 → ⊥.
+theorem tdneq_tdeq_canc_dx: â\88\80h,o,T1,T. (T1 â\89\9b[h, o] T â\86\92 â\8a¥) â\86\92 â\88\80T2. T2 â\89\9b[h, o] T →
+ T1 â\89\9b[h, o] T2 → ⊥.
/3 width=3 by tdeq_trans/ qed-.
(* Properties with degree-based equivalence for terms ***********************)
-lemma tdeq_theq: â\88\80h,o,T1,T2. T1 â\89¡[h, o] T2 → T1 ⩳[h, o] T2.
+lemma tdeq_theq: â\88\80h,o,T1,T2. T1 â\89\9b[h, o] T2 → T1 ⩳[h, o] T2.
#h #o #T1 #T2 * -T1 -T2 /2 width=3 by theq_sort, theq_pair/
qed.
}
]
[ { "parallel qrst-computation" * } {
- [ "fpbg ( â¦\83?,?,?â¦\84 >â\89¡[?,?] ⦃?,?,?⦄ )" "fpbg_lift" + "fpbg_fleq" + "fpbg_fpbs" + "fpbg_fpbg" * ]
+ [ "fpbg ( â¦\83?,?,?â¦\84 >â\89\9b[?,?] ⦃?,?,?⦄ )" "fpbg_lift" + "fpbg_fleq" + "fpbg_fpbs" + "fpbg_fpbg" * ]
[ "fpbs ( ⦃?,?,?⦄ ≥[?,?] ⦃?,?,?⦄ )" "fpbs_alt ( ⦃?,?,?⦄ ≥≥[?,?] ⦃?,?,?⦄ )" "fpbs_lift" + "fpbs_aaa" + "fpbs_fpb" + "fpbs_fpbs" * ]
}
]
}
]
[ { "degree-based equivalence on referred entries" * } {
- [ "ffdeq ( â¦\83?,?,?â¦\84 â\89¡[?,?] ⦃?,?,?⦄ )" "ffdeq_fqup" + "ffdeq_ffdeq" * ]
- [ "lfdeq ( ? â\89¡[?,?,?] ? )" "lfdeq_length" + "lfdeq_drops" + "lfdeq_fqup" + "lfdeq_fqus" + "lfdeq_lfdeq" * ]
+ [ "ffdeq ( â¦\83?,?,?â¦\84 â\89\9b[?,?] ⦃?,?,?⦄ )" "ffdeq_fqup" + "ffdeq_ffdeq" * ]
+ [ "lfdeq ( ? â\89\9b[?,?,?] ? )" "lfdeq_length" + "lfdeq_drops" + "lfdeq_fqup" + "lfdeq_fqus" + "lfdeq_lfdeq" * ]
}
]
[ { "generic extension on referred entries" * } {
}
]
[ { "degree-based equivalence" * } {
- [ "tdeq_ext ( ? â\89¡[?,?] ? ) ( ? â\8a¢ ? â\89¡[?,?] ? )" * ]
- [ "tdeq ( ? â\89¡[?,?] ? )" "tdeq_tdeq" * ]
+ [ "tdeq_ext ( ? â\89\9b[?,?] ? ) ( ? â\8a¢ ? â\89\9b[?,?] ? )" * ]
+ [ "tdeq ( ? â\89\9b[?,?] ? )" "tdeq_tdeq" * ]
}
]
[ { "closures" * } {
#!/bin/sh
-for MA in `find -name "*.ma"`; do
+for MA in `find basic_2 -name "*.ma"`; do
#for MA in `find -name "cpg*.ma" -or -name "cpx*.ma"`; do
- echo ${MA}; sed "s!$1!$2!g" ${MA} > ${MA}.new
- if diff ${MA} ${MA}.new > /dev/null;
+ sed "s!$1!$2!g" ${MA} > ${MA}.new
+ if [ ! -s ${MA}.new ] || diff ${MA} ${MA}.new > /dev/null;
then rm -f ${MA}.new;
- else mv -f ${MA} ${MA}.old; mv -f ${MA}.new ${MA};
+ else echo ${MA}; mv -f ${MA} ${MA}.old; mv -f ${MA}.new ${MA};
fi
done
--- /dev/null
+#!/bin/sh
+for MA in `find -name "*.ma"`; do
+ if [ -s ${MA}.old ];
+ then echo ${MA}; mv -f ${MA}.old ${MA};
+ fi
+done
+
+unset MA
projects / helm.git / commitdiff