]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/lambdadelta/basic_2/etc_new/cpx/cpx_sta.etc
frees_drops completed!
[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / etc_new / cpx / cpx_sta.etc
1 fact sta_cpx_aux: ∀h,o,G,L,T1,T2,d2,d1. ⦃G, L⦄ ⊢ T1 •*[h, d2] T2 → d2 = 1 →
2                   ⦃G, L⦄ ⊢ T1 ▪[h, o] d1+1 → ⦃G, L⦄ ⊢ T1 ➡[h, o] T2.
3 #h #o #G #L #T1 #T2 #d2 #d1 #H elim H -G -L -T1 -T2 -d2
4 [ #G #L #d2 #s #H0 destruct normalize
5   /3 width=4 by cpx_st, da_inv_sort/
6 | #G #L #K #V1 #V2 #W2 #i #d2 #HLK #_ #HVW2 #IHV12 #H0 #H destruct
7   elim (da_inv_lref … H) -H * #K0 #V0 [| #d0 ] #HLK0
8   lapply (drop_mono … HLK0 … HLK) -HLK0 #H destruct /3 width=7 by cpx_delta/
9 | #G #L #K #V1 #V2 #i #_ #_ #_ #H destruct
10 | #G #L #K #V1 #V2 #W2 #i #d2 #HLK #HV12 #HVW2 #_ #H0 #H
11   lapply (discr_plus_xy_y … H0) -H0 #H0 destruct
12   elim (da_inv_lref … H) -H * #K0 #V0 [| #d0 ] #HLK0
13   lapply (drop_mono … HLK0 … HLK) -HLK0 #H destruct
14   /4 width=7 by cpx_delta, cpr_cpx, lstas_cpr/
15 | /4 width=2 by cpx_bind, da_inv_bind/
16 | /4 width=3 by cpx_flat, da_inv_flat/
17 | /4 width=3 by cpx_eps, da_inv_flat/
18 ]
19 qed-.
20
21 lemma sta_cpx: ∀h,o,G,L,T1,T2,d. ⦃G, L⦄ ⊢ T1 •*[h, 1] T2 →
22                ⦃G, L⦄ ⊢ T1 ▪[h, o] d+1 → ⦃G, L⦄ ⊢ T1 ➡[h, o] T2.
23 /2 width=3 by sta_cpx_aux/ qed.
24
25 lemma fqu_sta_trans: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐ ⦃G2, L2, T2⦄ →
26                      ∀U2. ⦃G2, L2⦄ ⊢ T2 •*[h, 1] U2 →
27                      ∀d. ⦃G2, L2⦄ ⊢ T2 ▪[h, o] d+1 →
28                      ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡[h, o] U1 & ⦃G1, L1, U1⦄ ⊐ ⦃G2, L2, U2⦄.
29 /3 width=5 by fqu_cpx_trans, sta_cpx/ qed-.
30
31 lemma fquq_sta_trans: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐⸮ ⦃G2, L2, T2⦄ →
32                       ∀U2. ⦃G2, L2⦄ ⊢ T2 •*[h, 1] U2 →
33                       ∀d. ⦃G2, L2⦄ ⊢ T2 ▪[h, o] d+1 →
34                       ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡[h, o] U1 & ⦃G1, L1, U1⦄ ⊐⸮ ⦃G2, L2, U2⦄.
35 /3 width=5 by fquq_cpx_trans, sta_cpx/ qed-.
36