From: Ferruccio Guidi Date: Tue, 13 Sep 2016 19:23:02 +0000 (+0000) Subject: more results on cpm ... X-Git-Tag: make_still_working~542 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=6f06bee3eeb4f718b273f0cca5873e9dc5e758b2;p=helm.git more results on cpm ... --- diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/cpr/cpr.etc b/matita/matita/contribs/lambdadelta/basic_2/etc_new/cpr/cpr.etc new file mode 100644 index 000000000..3f30e621f --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc_new/cpr/cpr.etc @@ -0,0 +1,29 @@ +lemma cpr_delift: ∀G,K,V,T1,L,l. ⬇[l] L ≡ (K.ⓓV) → + ∃∃T2,T. ⦃G, L⦄ ⊢ T1 ➡ T2 & ⬆[l, 1] T ≡ T2. +#G #K #V #T1 elim T1 -T1 +[ * /2 width=4 by cpr_atom, lift_sort, lift_gref, ex2_2_intro/ + #i #L #l #HLK elim (lt_or_eq_or_gt i l) + #Hil [1,3: /4 width=4 by lift_lref_ge_minus, lift_lref_lt, ylt_inj, yle_inj, ex2_2_intro/ ] + destruct + elim (lift_total V 0 (i+1)) #W #HVW + elim (lift_split … HVW i i) /3 width=6 by cpr_delta, ex2_2_intro/ +| * [ #a ] #I #W1 #U1 #IHW1 #IHU1 #L #l #HLK + elim (IHW1 … HLK) -IHW1 #W2 #W #HW12 #HW2 + [ elim (IHU1 (L. ⓑ{I}W1) (l+1)) -IHU1 /3 width=9 by drop_drop, cpr_bind, lift_bind, ex2_2_intro/ + | elim (IHU1 … HLK) -IHU1 -HLK /3 width=8 by cpr_flat, lift_flat, ex2_2_intro/ + ] +] +qed-. + +fact lstas_cpr_aux: ∀h,G,L,T1,T2,d. ⦃G, L⦄ ⊢ T1 •*[h, d] T2 → + d = 0 → ⦃G, L⦄ ⊢ T1 ➡ T2. +#h #G #L #T1 #T2 #d #H elim H -G -L -T1 -T2 -d +/3 width=1 by cpr_eps, cpr_flat, cpr_bind/ +[ #G #L #K #V1 #V2 #W2 #i #d #HLK #_ #HVW2 #IHV12 #H destruct + /3 width=6 by cpr_delta/ +| #G #L #K #V1 #V2 #W2 #i #d #_ #_ #_ #_ IHV1 -IHV1 // -HV1 >IHT1 -IHT1 // + | elim (cir_inv_ri2 … H) /2 width=1 by/ + ] +| #G #L #V1 #T1 #T #T2 #_ #_ #_ #H + elim (cir_inv_ri2 … H) /2 width=1 by or_introl/ +| #G #L #V1 #T1 #T2 #_ #_ #H + elim (cir_inv_ri2 … H) /2 width=1 by/ +| #a #G #L #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #_ #_ #H + elim (cir_inv_appl … H) -H #_ #_ #H + elim (simple_inv_bind … H) +| #a #G #L #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #_ #_ #_ #H + elim (cir_inv_appl … H) -H #_ #_ #H + elim (simple_inv_bind … H) +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_cpx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_cpx.ma new file mode 100644 index 000000000..d459fff2a --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_cpx.ma @@ -0,0 +1,26 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/rt_transition/cpx.ma". +include "basic_2/rt_transition/cpm.ma". + +(* T-BOUND CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS ***************) + +(* Forward lemmas with uncounted context-sensitive rt-transition for terms **) + +(* Basic_2A1: includes: cpr_cpx *) +lemma cpm_fwd_cpx: ∀n,h,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[n, h] T2 → ⦃G, L⦄ ⊢ T1 ⬈[h] T2. +#n #h #G #L #T1 #T2 * #c #Hc #H elim H -L -T1 -T2 +/2 width=3 by cpx_theta, cpx_beta, cpx_ee, cpx_eps, cpx_zeta, cpx_flat, cpx_bind, cpx_lref, cpx_delta/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_drops.ma new file mode 100644 index 000000000..786d2f9ce --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_drops.ma @@ -0,0 +1,95 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/rt_transition/cpg_drops.ma". +include "basic_2/rt_transition/cpm.ma". + +(* T-BOUND CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS ***************) + +(* Advanced properties ******************************************************) + +(* Basic_1: includes: pr2_delta1 *) +(* Basic_2A1: includes: cpr_delta *) +lemma cpm_delta_drops: ∀n,h,G,L,K,V,V2,W2,i. + ⬇*[i] L ≡ K.ⓓV → ⦃G, K⦄ ⊢ V ➡[n, h] V2 → + ⬆*[⫯i] V2 ≡ W2 → ⦃G, L⦄ ⊢ #i ➡[n, h] W2. +#n #h #G #L #K #V #V2 #W2 #i #HLK * +/3 width=8 by cpg_delta_drops, ex2_intro/ +qed. + +lemma cpm_ell_drops: ∀n,h,G,L,K,V,V2,W2,i. + ⬇*[i] L ≡ K.ⓛV → ⦃G, K⦄ ⊢ V ➡[n, h] V2 → + ⬆*[⫯i] V2 ≡ W2 → ⦃G, L⦄ ⊢ #i ➡[⫯n, h] W2. +#n #h #G #L #K #V #V2 #W2 #i #HLK * +/3 width=8 by cpg_ell_drops, isrt_succ, ex2_intro/ +qed. + +(* Advanced inversion lemmas ************************************************) + +lemma cpm_inv_atom1_drops: ∀n,h,I,G,L,T2. ⦃G, L⦄ ⊢ ⓪{I} ➡[n, h] T2 → + ∨∨ T2 = ⓪{I} ∧ n = 0 + | ∃∃s. T2 = ⋆(next h s) & I = Sort s & n = 1 + | ∃∃K,V,V2,i. ⬇*[i] L ≡ K.ⓓV & ⦃G, K⦄ ⊢ V ➡[n, h] V2 & + ⬆*[⫯i] V2 ≡ T2 & I = LRef i + | ∃∃m,K,V,V2,i. ⬇*[i] L ≡ K.ⓛV & ⦃G, K⦄ ⊢ V ➡[m, h] V2 & + ⬆*[⫯i] V2 ≡ T2 & I = LRef i & n = ⫯m. +#n #h #I #G #L #T2 * #c #Hc #H elim (cpg_inv_atom1_drops … H) -H * +[ #H1 #H2 destruct lapply (isrt_inv_00 … Hc) -Hc + /3 width=1 by or4_intro0, conj/ +| #s #H1 #H2 #H3 destruct lapply (isrt_inv_01 … Hc) -Hc + /4 width=3 by or4_intro1, ex3_intro, sym_eq/ (**) (* sym_eq *) +| #cV #i #K #V1 #V2 #HLK #HV12 #HVT2 #H1 #H2 destruct + /4 width=8 by ex4_4_intro, ex2_intro, or4_intro2/ +| #cV #i #K #V1 #V2 #HLK #HV12 #HVT2 #H1 #H2 destruct + elim (isrt_inv_plus_SO_dx … Hc) -Hc + /4 width=10 by ex5_5_intro, ex2_intro, or4_intro3/ +] +qed-. + +lemma cpm_inv_lref1_drops: ∀n,h,G,L,T2,i. ⦃G, L⦄ ⊢ #i ➡[n, h] T2 → + ∨∨ T2 = #i ∧ n = 0 + | ∃∃K,V,V2. ⬇*[i] L ≡ K. ⓓV & ⦃G, K⦄ ⊢ V ➡[n, h] V2 & + ⬆*[⫯i] V2 ≡ T2 + | ∃∃m,K,V,V2. ⬇*[i] L ≡ K. ⓛV & ⦃G, K⦄ ⊢ V ➡[m, h] V2 & + ⬆*[⫯i] V2 ≡ T2 & n = ⫯m. +#n #h #G #L #T2 #i * #c #Hc #H elim (cpg_inv_lref1_drops … H) -H * +[ #H1 #H2 destruct lapply (isrt_inv_00 … Hc) -Hc + /3 width=1 by or3_intro0, conj/ +| #cV #K #V1 #V2 #HLK #HV12 #HVT2 #H destruct + /4 width=6 by ex3_3_intro, ex2_intro, or3_intro1/ +| #cV #K #V1 #V2 #HLK #HV12 #HVT2 #H destruct + elim (isrt_inv_plus_SO_dx … Hc) -Hc + /4 width=8 by ex4_4_intro, ex2_intro, or3_intro2/ +] +qed-. + +(* Properties with generic slicing for local environments *******************) + +(* Basic_1: includes: pr0_lift pr2_lift *) +(* Basic_2A1: includes: cpr_lift *) +lemma cpm_lifts: ∀n,h,G. d_liftable2 (cpm n h G). +#n #h #G #K #T1 #T2 * #c #Hc #HT12 #b #f #L #HLK #U1 #HTU1 +elim (cpg_lifts … HT12 … HLK … HTU1) -K -T1 +/3 width=5 by ex2_intro/ +qed-. + +(* Inversion lemmas with generic slicing for local environments *************) + +(* Basic_1: includes: pr0_gen_lift pr2_gen_lift *) +(* Basic_2A1: includes: cpr_inv_lift1 *) +lemma cpm_inv_lifts1: ∀n,h,G. d_deliftable2_sn (cpm n h G). +#n #h #G #L #U1 #U2 * #c #Hc #HU12 #b #f #K #HLK #T1 #HTU1 +elim (cpg_inv_lifts1 … HU12 … HLK … HTU1) -L -U1 +/3 width=5 by ex2_intro/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_lsubr.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_lsubr.ma new file mode 100644 index 000000000..ac03ed30c --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_lsubr.ma @@ -0,0 +1,33 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/rt_transition/cpg_lsubr.ma". +include "basic_2/rt_transition/cpm.ma". + +(* T-BOUND CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS ***************) + +(* Properties with restricted refinement for local environments *************) + +(* Basic_2A1: includes: lsubr_cpr_trans *) +lemma lsubr_cpm_trans: ∀n,h,G. lsub_trans … (cpm n h G) lsubr. +#n #h #G #L1 #T1 #T2 * /3 width=5 by lsubr_cpg_trans, ex2_intro/ +qed-. + +(* Advanced properties ******************************************************) + +(* Basic_1: was by definition: pr2_free *) +(* Basic_2A1: includes: tpr_cpr *) +lemma tpm_cpm: ∀n,h,G,T1,T2. ⦃G, ⋆⦄ ⊢ T1 ➡[n, h] T2 → ∀L. ⦃G, L⦄ ⊢ T1 ➡[n, h] T2. +#n #h #G #T1 #T2 #HT12 #L lapply (lsubr_cpm_trans … HT12 L ?) // +qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_simple.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_simple.ma new file mode 100644 index 000000000..9a37802e6 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_simple.ma @@ -0,0 +1,30 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/rt_transition/cpg_simple.ma". +include "basic_2/rt_transition/cpm.ma". + +(* T-BOUND CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS ***************) + +(* Properties with simple terms *********************************************) + +(* Basic_2A1: includes: cpr_inv_appl1_simple *) +lemma cpm_inv_appl1_simple: ∀n,h,G,L,V1,T1,U. ⦃G, L⦄ ⊢ ⓐV1.T1 ➡[n, h] U → 𝐒⦃T1⦄ → + ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡[h] V2 & ⦃G, L⦄ ⊢ T1 ➡[n, h] T2 & + U = ⓐV2.T2. +#n #h #G #L #V1 #T1 #U * #c #Hc #H #HT1 elim (cpg_inv_appl1_simple … H HT1) -H -HT1 +#cV #cT #V2 #T2 #HV12 #HT12 #H1 #H2 destruct elim (isrt_inv_max … Hc) -Hc +#nV #nT #HnV #HnT #H destruct elim (isrt_inv_shift … HnV) -HnV +#HnV #H destruct /3 width=5 by ex3_2_intro, ex2_intro/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr.etc b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr.etc deleted file mode 100644 index dee79d193..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr.etc +++ /dev/null @@ -1,87 +0,0 @@ -(* Basic_1: includes: pr2_delta1 *) -| cpr_delta: ∀G,L,K,V,V2,W2,i. - ⬇[i] L ≡ K. ⓓV → cpr G K V V2 → - ⬆[0, i + 1] V2 ≡ W2 → cpr G L (#i) W2 - -lemma cpr_cpx: ∀h,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡ T2 → ⦃G, L⦄ ⊢ T1 ➡[h] T2. -#h #o #G #L #T1 #T2 #H elim H -L -T1 -T2 -/2 width=7 by cpx_delta, cpx_bind, cpx_flat, cpx_zeta, cpx_eps, cpx_beta, cpx_theta/ -qed. - -lemma lsubr_cpr_trans: ∀G. lsub_trans … (cpr G) lsubr. -#G #L1 #T1 #T2 #H elim H -G -L1 -T1 -T2 -[ // -| #G #L1 #K1 #V1 #V2 #W2 #i #HLK1 #_ #HVW2 #IHV12 #L2 #HL12 - elim (lsubr_fwd_drop2_abbr … HL12 … HLK1) -L1 * - /3 width=6 by cpr_delta/ -|3,7: /4 width=1 by lsubr_pair, cpr_bind, cpr_beta/ -|4,6: /3 width=1 by cpr_flat, cpr_eps/ -|5,8: /4 width=3 by lsubr_pair, cpr_zeta, cpr_theta/ -] -qed-. - -(* Basic_1: was by definition: pr2_free *) -lemma tpr_cpr: ∀G,T1,T2. ⦃G, ⋆⦄ ⊢ T1 ➡ T2 → ∀L. ⦃G, L⦄ ⊢ T1 ➡ T2. -#G #T1 #T2 #HT12 #L -lapply (lsubr_cpr_trans … HT12 L ?) // -qed. - -lemma cpr_delift: ∀G,K,V,T1,L,l. ⬇[l] L ≡ (K.ⓓV) → - ∃∃T2,T. ⦃G, L⦄ ⊢ T1 ➡ T2 & ⬆[l, 1] T ≡ T2. -#G #K #V #T1 elim T1 -T1 -[ * /2 width=4 by cpr_atom, lift_sort, lift_gref, ex2_2_intro/ - #i #L #l #HLK elim (lt_or_eq_or_gt i l) - #Hil [1,3: /4 width=4 by lift_lref_ge_minus, lift_lref_lt, ylt_inj, yle_inj, ex2_2_intro/ ] - destruct - elim (lift_total V 0 (i+1)) #W #HVW - elim (lift_split … HVW i i) /3 width=6 by cpr_delta, ex2_2_intro/ -| * [ #a ] #I #W1 #U1 #IHW1 #IHU1 #L #l #HLK - elim (IHW1 … HLK) -IHW1 #W2 #W #HW12 #HW2 - [ elim (IHU1 (L. ⓑ{I}W1) (l+1)) -IHU1 /3 width=9 by drop_drop, cpr_bind, lift_bind, ex2_2_intro/ - | elim (IHU1 … HLK) -IHU1 -HLK /3 width=8 by cpr_flat, lift_flat, ex2_2_intro/ - ] -] -qed-. - -fact lstas_cpr_aux: ∀h,G,L,T1,T2,d. ⦃G, L⦄ ⊢ T1 •*[h, d] T2 → - d = 0 → ⦃G, L⦄ ⊢ T1 ➡ T2. -#h #G #L #T1 #T2 #d #H elim H -G -L -T1 -T2 -d -/3 width=1 by cpr_eps, cpr_flat, cpr_bind/ -[ #G #L #K #V1 #V2 #W2 #i #d #HLK #_ #HVW2 #IHV12 #H destruct - /3 width=6 by cpr_delta/ -| #G #L #K #V1 #V2 #W2 #i #d #_ #_ #_ #_ IHV1 -IHV1 // -HV1 >IHT1 -IHT1 // - | elim (cir_inv_ri2 … H) /2 width=1 by/ - ] -| #G #L #V1 #T1 #T #T2 #_ #_ #_ #H - elim (cir_inv_ri2 … H) /2 width=1 by or_introl/ -| #G #L #V1 #T1 #T2 #_ #_ #H - elim (cir_inv_ri2 … H) /2 width=1 by/ -| #a #G #L #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #_ #_ #H - elim (cir_inv_appl … H) -H #_ #_ #H - elim (simple_inv_bind … H) -| #a #G #L #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #_ #_ #_ #H - elim (cir_inv_appl … H) -H #_ #_ #H - elim (simple_inv_bind … H) -] -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr_drops.ma new file mode 100644 index 000000000..48d281e4f --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr_drops.ma @@ -0,0 +1,45 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/rt_transition/cpm_drops.ma". + +(* CONTEXT-SENSITIVE PARALLEL R-TRANSITION FOR TERMS ************************) + +(* Advanced inversion lemmas ************************************************) + +(* Basic_2A1: includes: cpr_inv_atom1 *) +lemma cpr_inv_atom1_drops: ∀h,I,G,L,T2. ⦃G, L⦄ ⊢ ⓪{I} ➡[h] T2 → + T2 = ⓪{I} ∨ + ∃∃K,V,V2,i. ⬇*[i] L ≡ K.ⓓV & ⦃G, K⦄ ⊢ V ➡[h] V2 & + ⬆*[⫯i] V2 ≡ T2 & I = LRef i. +#h #I #G #L #T2 #H elim (cpm_inv_atom1_drops … H) -H * +[ /2 width=1 by or_introl/ +| #s #_ #_ #H destruct +| /3 width=8 by ex4_4_intro, or_intror/ +| #m #K #V1 #V2 #i #_ #_ #_ #_ #H destruct +] +qed-. + +(* Basic_1: includes: pr0_gen_lref pr2_gen_lref *) +(* Basic_2A1: includes: cpr_inv_lref1 *) +lemma cpr_inv_lref1_drops: ∀h,G,L,T2,i. ⦃G, L⦄ ⊢ #i ➡[h] T2 → + T2 = #i ∨ + ∃∃K,V,V2. ⬇*[i] L ≡ K. ⓓV & ⦃G, K⦄ ⊢ V ➡[h] V2 & + ⬆*[⫯i] V2 ≡ T2. +#h #G #L #T2 #i #H elim (cpm_inv_lref1_drops … H) -H * +[ /2 width=1 by or_introl/ +| /3 width=6 by ex3_3_intro, or_intror/ +| #m #K #V1 #V2 #_ #_ #_ #H destruct +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr_lift.ma deleted file mode 100644 index bebe3429f..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr_lift.ma +++ /dev/null @@ -1,112 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "ground_2/ynat/ynat_max.ma". -include "basic_2/substitution/drop_drop.ma". -include "basic_2/reduction/cpr.ma". - -(* CONTEXT-SENSITIVE PARALLEL REDUCTION FOR TERMS ***************************) - -(* Relocation properties ****************************************************) - -(* Basic_1: includes: pr0_lift pr2_lift *) -lemma cpr_lift: ∀G. d_liftable (cpr G). -#G #K #T1 #T2 #H elim H -G -K -T1 -T2 -[ #I #G #K #L #b #l #k #_ #U1 #H1 #U2 #H2 - >(lift_mono … H1 … H2) -H1 -H2 // -| #G #K #KV #V #V2 #W2 #i #HKV #HV2 #HVW2 #IHV2 #L #b #l #k #HLK #U1 #H #U2 #HWU2 - elim (lift_inv_lref1 … H) * #Hil #H destruct - [ elim (lift_trans_ge … HVW2 … HWU2) -W2 /2 width=1 by ylt_fwd_le_succ1/ #W2 #HVW2 #HWU2 - elim (drop_trans_le … HLK … HKV) -K /2 width=2 by ylt_fwd_le/ #X #HLK #H - elim (drop_inv_skip2 … H) -H /2 width=1 by ylt_to_minus/ -Hil - #K #Y #HKV #HVY #H destruct /3 width=9 by cpr_delta/ - | lapply (lift_trans_be … HVW2 … HWU2 ? ?) -W2 /2 width=1 by yle_succ_dx/ >plus_plus_comm_23 #HVU2 - lapply (drop_trans_ge_comm … HLK … HKV ?) -K // -Hil /3 width=6 by cpr_delta, drop_inv_gen/ - ] -| #a #I #G #K #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L #b #l #k #HLK #U1 #H1 #U2 #H2 - elim (lift_inv_bind1 … H1) -H1 #VV1 #TT1 #HVV1 #HTT1 #H1 destruct - elim (lift_inv_bind1 … H2) -H2 #VV2 #TT2 #HVV2 #HTT2 #H2 destruct /4 width=6 by cpr_bind, drop_skip/ -| #I #G #K #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L #b #l #k #HLK #U1 #H1 #U2 #H2 - elim (lift_inv_flat1 … H1) -H1 #VV1 #TT1 #HVV1 #HTT1 #H1 destruct - elim (lift_inv_flat1 … H2) -H2 #VV2 #TT2 #HVV2 #HTT2 #H2 destruct /3 width=6 by cpr_flat/ -| #G #K #V #T1 #T #T2 #_ #HT2 #IHT1 #L #b #l #k #HLK #U1 #H #U2 #HTU2 - elim (lift_inv_bind1 … H) -H #VV1 #TT1 #HVV1 #HTT1 #H destruct - elim (lift_conf_O1 … HTU2 … HT2) -T2 /4 width=6 by cpr_zeta, drop_skip/ -| #G #K #V #T1 #T2 #_ #IHT12 #L #b #l #k #HLK #U1 #H #U2 #HTU2 - elim (lift_inv_flat1 … H) -H #VV1 #TT1 #HVV1 #HTT1 #H destruct /3 width=6 by cpr_eps/ -| #a #G #K #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV12 #IHW12 #IHT12 #L #b #l #k #HLK #X1 #HX1 #X2 #HX2 - elim (lift_inv_flat1 … HX1) -HX1 #V0 #X #HV10 #HX #HX1 destruct - elim (lift_inv_bind1 … HX) -HX #W0 #T0 #HW0 #HT10 #HX destruct - elim (lift_inv_bind1 … HX2) -HX2 #X #T3 #HX #HT23 #HX2 destruct - elim (lift_inv_flat1 … HX) -HX #W3 #V3 #HW23 #HV23 #HX destruct /4 width=6 by cpr_beta, drop_skip/ -| #a #G #K #V1 #V #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV1 #IHW12 #IHT12 #L #b #l #k #HLK #X1 #HX1 #X2 #HX2 - elim (lift_inv_flat1 … HX1) -HX1 #V0 #X #HV10 #HX #HX1 destruct - elim (lift_inv_bind1 … HX) -HX #W0 #T0 #HW0 #HT10 #HX destruct - elim (lift_inv_bind1 … HX2) -HX2 #W3 #X #HW23 #HX #HX2 destruct - elim (lift_inv_flat1 … HX) -HX #V3 #T3 #HV3 #HT23 #HX destruct - elim (lift_trans_ge … HV2 … HV3) -V2 /4 width=6 by cpr_theta, drop_skip/ -] -qed. - -(* Basic_1: includes: pr0_gen_lift pr2_gen_lift *) -lemma cpr_inv_lift1: ∀G. d_deliftable_sn (cpr G). -#G #L #U1 #U2 #H elim H -G -L -U1 -U2 -[ * #i #G #L #K #b #l #k #_ #T1 #H - [ lapply (lift_inv_sort2 … H) -H #H destruct /2 width=3 by ex2_intro/ - | elim (lift_inv_lref2 … H) -H * #Hil #H destruct /3 width=3 by lift_lref_ge_minus, lift_lref_lt, ex2_intro/ - | lapply (lift_inv_gref2 … H) -H #H destruct /2 width=3 by ex2_intro/ - ] -| #G #L #LV #V #V2 #W2 #i #HLV #HV2 #HVW2 #IHV2 #K #b #l #k #HLK #T1 #H - elim (lift_inv_lref2 … H) -H * #Hil #H destruct - [ elim (drop_conf_lt … HLK … HLV) -L // #L #U #HKL #HLV #HUV - elim (IHV2 … HLV … HUV) -V #U2 #HUV2 #HU2 - elim (lift_trans_le … HUV2 … HVW2) -V2 // yplus_SO2 >ymax_pre_sn /3 width=8 by cpr_delta, ylt_fwd_le_succ1, ex2_intro/ - | elim (yle_inv_plus_inj2 … Hil) #Hlim #Hmi - lapply (yle_inv_inj … Hmi) -Hmi #Hmi - lapply (drop_conf_ge … HLK … HLV ?) -L // #HKLV - elim (lift_split … HVW2 l (i - k + 1)) -HVW2 [2,3,4: /2 width=1 by yle_succ_dx, le_S_S/ ] -Hil -Hlim - #V1 #HV1 >plus_minus //