From: Ferruccio Guidi Date: Mon, 20 Feb 2017 21:16:13 +0000 (+0000) Subject: csx on the way ... X-Git-Tag: make_still_working~497 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=9080be011a214d5ee98639c2c7c6356a7be3d2d1;p=helm.git csx on the way ... --- diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predtystrong_5.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predtystrong_5.ma new file mode 100644 index 000000000..74444d815 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predtystrong_5.ma @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||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 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 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/sn_5.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/sn_5.ma deleted file mode 100644 index b7ce19c7a..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/sn_5.ma +++ /dev/null @@ -1,19 +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 *) -(* *) -(**************************************************************************) - -(* 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 )" - non associative with precedence 45 - for @{ 'SN $h $o $G $L $T }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx.ma index 0def99568..3ba500020 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx.ma @@ -12,26 +12,27 @@ (* *) (**************************************************************************) -include "basic_2/notation/relations/sn_5.ma". -include "basic_2/reduction/cnx.ma". +include "basic_2/notation/relations/predtystrong_5.ma". +include "basic_2/syntax/tdeq.ma". +include "basic_2/rt_transition/cpx.ma". -(* CONTEXT-SENSITIVE EXTENDED STRONGLY NORMALIZING TERMS ********************) +(* STRONGLY NORMALIZING TERMS FOR UNCOUNTED PARALLEL RT-TRANSITION **********) definition csx: ∀h. sd h → relation3 genv lenv term ≝ - λh,o,G,L. SN … (cpx h o G L) (eq …). + λh,o,G,L. SN … (cpx h G L) (tdeq h o …). interpretation - "context-sensitive extended strong normalization (term)" - 'SN h o G L T = (csx h o G L T). + "strong normalization for uncounted context-sensitive parallel rt-transition (term)" + 'PRedTyStrong h o G L T = (csx h o G L T). (* Basic eliminators ********************************************************) lemma csx_ind: ∀h,o,G,L. ∀R:predicate term. - (∀T1. ⦃G, L⦄ ⊢ ⬊*[h, o] T1 → - (∀T2. ⦃G, L⦄ ⊢ T1 ➡[h, o] T2 → (T1 = T2 → ⊥) → R T2) → + (∀T1. ⦃G, L⦄ ⊢ ⬈[h, o] 𝐒⦃T1⦄ → + (∀T2. ⦃G, L⦄ ⊢ T1 ⬈[h] T2 → (T1 ≡[h, o] T2 → ⊥) → R T2) → R T1 ) → - ∀T. ⦃G, L⦄ ⊢ ⬊*[h, o] T → R T. + ∀T. ⦃G, L⦄ ⊢ ⬈[h, o] 𝐒⦃T⦄ → R T. #h #o #G #L #R #H0 #T1 #H elim H -T1 /5 width=1 by SN_intro/ qed-. @@ -40,89 +41,67 @@ qed-. (* Basic_1: was just: sn3_pr2_intro *) lemma csx_intro: ∀h,o,G,L,T1. - (∀T2. ⦃G, L⦄ ⊢ T1 ➡[h, o] T2 → (T1 = T2 → ⊥) → ⦃G, L⦄ ⊢ ⬊*[h, o] T2) → - ⦃G, L⦄ ⊢ ⬊*[h, o] T1. + (∀T2. ⦃G, L⦄ ⊢ T1 ⬈[h] T2 → (T1 ≡[h, o] T2 → ⊥) → ⦃G, L⦄ ⊢ ⬈[h, o] 𝐒⦃T2⦄) → + ⦃G, L⦄ ⊢ ⬈[h, o] 𝐒⦃T1⦄. /4 width=1 by SN_intro/ qed. -lemma csx_cpx_trans: ∀h,o,G,L,T1. ⦃G, L⦄ ⊢ ⬊*[h, o] T1 → - ∀T2. ⦃G, L⦄ ⊢ T1 ➡[h, o] T2 → ⦃G, L⦄ ⊢ ⬊*[h, o] T2. -#h #o #G #L #T1 #H @(csx_ind … H) -T1 #T1 #HT1 #IHT1 #T2 #HLT12 -elim (eq_term_dec T1 T2) #HT12 destruct /3 width=4 by/ -qed-. - -(* Basic_1: was just: sn3_nf2 *) -lemma cnx_csx: ∀h,o,G,L,T. ⦃G, L⦄ ⊢ ➡[h, o] 𝐍⦃T⦄ → ⦃G, L⦄ ⊢ ⬊*[h, o] T. -/2 width=1 by NF_to_SN/ qed. - -lemma csx_sort: ∀h,o,G,L,s. ⦃G, L⦄ ⊢ ⬊*[h, o] ⋆s. +lemma csx_sort: ∀h,o,G,L,s. ⦃G, L⦄ ⊢ ⬈[h, o] 𝐒⦃⋆s⦄. #h #o #G #L #s elim (deg_total h o s) -#d generalize in match s; -s @(nat_ind_plus … d) -d /3 width=6 by cnx_csx, cnx_sort/ -#d #IHd #s #Hkd lapply (deg_next_SO … Hkd) -Hkd -#Hkd @csx_intro #X #H #HX elim (cpx_inv_sort1 … H) -H -[ #H destruct elim HX // -| -HX * #d0 #_ #H destruct -d0 /2 width=1 by/ -] -qed. - -(* Basic_1: was just: sn3_cast *) -lemma csx_cast: ∀h,o,G,L,W. ⦃G, L⦄ ⊢ ⬊*[h, o] W → - ∀T. ⦃G, L⦄ ⊢ ⬊*[h, o] T → ⦃G, L⦄ ⊢ ⬊*[h, o] ⓝW.T. -#h #o #G #L #W #HW @(csx_ind … HW) -W #W #HW #IHW #T #HT @(csx_ind … HT) -T #T #HT #IHT -@csx_intro #X #H1 #H2 -elim (cpx_inv_cast1 … H1) -H1 -[ * #W0 #T0 #HLW0 #HLT0 #H destruct - elim (eq_false_inv_tpair_sn … H2) -H2 - [ /3 width=3 by csx_cpx_trans/ - | -HLW0 * #H destruct /3 width=1 by/ - ] -|2,3: /3 width=3 by csx_cpx_trans/ +#d generalize in match s; -s elim d -d +[ #s1 #Hs1 @csx_intro #X #H #HX elim HX -HX + elim (cpx_inv_sort1 … H) -H #H destruct // + /3 width=3 by tdeq_sort, deg_next/ +| #d #IH #s #Hsd lapply (deg_next_SO … Hsd) -Hsd + #Hsd @csx_intro #X #H #HX + elim (cpx_inv_sort1 … H) -H #H destruct /2 width=1 by/ + elim HX // ] qed. (* Basic forward lemmas *****************************************************) -fact csx_fwd_pair_sn_aux: ∀h,o,G,L,U. ⦃G, L⦄ ⊢ ⬊*[h, o] U → - ∀I,V,T. U = ②{I}V.T → ⦃G, L⦄ ⊢ ⬊*[h, o] V. +fact csx_fwd_pair_sn_aux: ∀h,o,G,L,U. ⦃G, L⦄ ⊢ ⬈[h, o] 𝐒⦃U⦄ → + ∀I,V,T. U = ②{I}V.T → ⦃G, L⦄ ⊢ ⬈[h, o] 𝐒⦃V⦄. #h #o #G #L #U #H elim H -H #U0 #_ #IH #I #V #T #H destruct @csx_intro #V2 #HLV2 #HV2 @(IH (②{I}V2.T)) -IH /2 width=3 by cpx_pair_sn/ -HLV2 -#H destruct /2 width=1 by/ +#H elim (tdeq_inv_pair … H) -H /2 width=1 by/ qed-. (* Basic_1: was just: sn3_gen_head *) -lemma csx_fwd_pair_sn: ∀h,o,I,G,L,V,T. ⦃G, L⦄ ⊢ ⬊*[h, o] ②{I}V.T → ⦃G, L⦄ ⊢ ⬊*[h, o] V. +lemma csx_fwd_pair_sn: ∀h,o,I,G,L,V,T. ⦃G, L⦄ ⊢ ⬈[h, o] 𝐒⦃②{I}V.T⦄ → ⦃G, L⦄ ⊢ ⬈[h, o] 𝐒⦃V⦄. /2 width=5 by csx_fwd_pair_sn_aux/ qed-. -fact csx_fwd_bind_dx_aux: ∀h,o,G,L,U. ⦃G, L⦄ ⊢ ⬊*[h, o] U → - ∀a,I,V,T. U = ⓑ{a,I}V.T → ⦃G, L.ⓑ{I}V⦄ ⊢ ⬊*[h, o] T. -#h #o #G #L #U #H elim H -H #U0 #_ #IH #a #I #V #T #H destruct +fact csx_fwd_bind_dx_aux: ∀h,o,G,L,U. ⦃G, L⦄ ⊢ ⬈[h, o] 𝐒⦃U⦄ → + ∀p,I,V,T. U = ⓑ{p,I}V.T → ⦃G, L.ⓑ{I}V⦄ ⊢ ⬈[h, o] 𝐒⦃T⦄. +#h #o #G #L #U #H elim H -H #U0 #_ #IH #p #I #V #T #H destruct @csx_intro #T2 #HLT2 #HT2 -@(IH (ⓑ{a,I}V.T2)) -IH /2 width=3 by cpx_bind/ -HLT2 -#H destruct /2 width=1 by/ +@(IH (ⓑ{p,I}V.T2)) -IH /2 width=3 by cpx_bind/ -HLT2 +#H elim (tdeq_inv_pair … H) -H /2 width=1 by/ qed-. (* Basic_1: was just: sn3_gen_bind *) -lemma csx_fwd_bind_dx: ∀h,o,a,I,G,L,V,T. ⦃G, L⦄ ⊢ ⬊*[h, o] ⓑ{a,I}V.T → ⦃G, L.ⓑ{I}V⦄ ⊢ ⬊*[h, o] T. +lemma csx_fwd_bind_dx: ∀h,o,p,I,G,L,V,T. ⦃G, L⦄ ⊢ ⬈[h, o] 𝐒⦃ⓑ{p,I}V.T⦄ → ⦃G, L.ⓑ{I}V⦄ ⊢ ⬈[h, o] 𝐒⦃T⦄. /2 width=4 by csx_fwd_bind_dx_aux/ qed-. -fact csx_fwd_flat_dx_aux: ∀h,o,G,L,U. ⦃G, L⦄ ⊢ ⬊*[h, o] U → - ∀I,V,T. U = ⓕ{I}V.T → ⦃G, L⦄ ⊢ ⬊*[h, o] T. +fact csx_fwd_flat_dx_aux: ∀h,o,G,L,U. ⦃G, L⦄ ⊢ ⬈[h, o] 𝐒⦃U⦄ → + ∀I,V,T. U = ⓕ{I}V.T → ⦃G, L⦄ ⊢ ⬈[h, o] 𝐒⦃T⦄. #h #o #G #L #U #H elim H -H #U0 #_ #IH #I #V #T #H destruct @csx_intro #T2 #HLT2 #HT2 @(IH (ⓕ{I}V.T2)) -IH /2 width=3 by cpx_flat/ -HLT2 -#H destruct /2 width=1 by/ +#H elim (tdeq_inv_pair … H) -H /2 width=1 by/ qed-. (* Basic_1: was just: sn3_gen_flat *) -lemma csx_fwd_flat_dx: ∀h,o,I,G,L,V,T. ⦃G, L⦄ ⊢ ⬊*[h, o] ⓕ{I}V.T → ⦃G, L⦄ ⊢ ⬊*[h, o] T. +lemma csx_fwd_flat_dx: ∀h,o,I,G,L,V,T. ⦃G, L⦄ ⊢ ⬈[h, o] 𝐒⦃ⓕ{I}V.T⦄ → ⦃G, L⦄ ⊢ ⬈[h, o] 𝐒⦃T⦄. /2 width=5 by csx_fwd_flat_dx_aux/ qed-. -lemma csx_fwd_bind: ∀h,o,a,I,G,L,V,T. ⦃G, L⦄ ⊢ ⬊*[h, o] ⓑ{a,I}V.T → - ⦃G, L⦄ ⊢ ⬊*[h, o] V ∧ ⦃G, L.ⓑ{I}V⦄ ⊢ ⬊*[h, o] T. +lemma csx_fwd_bind: ∀h,o,p,I,G,L,V,T. ⦃G, L⦄ ⊢ ⬈[h, o] 𝐒⦃ⓑ{p,I}V.T⦄ → + ⦃G, L⦄ ⊢ ⬈[h, o] 𝐒⦃V⦄ ∧ ⦃G, L.ⓑ{I}V⦄ ⊢ ⬈[h, o] 𝐒⦃T⦄. /3 width=3 by csx_fwd_pair_sn, csx_fwd_bind_dx, conj/ qed-. -lemma csx_fwd_flat: ∀h,o,I,G,L,V,T. ⦃G, L⦄ ⊢ ⬊*[h, o] ⓕ{I}V.T → - ⦃G, L⦄ ⊢ ⬊*[h, o] V ∧ ⦃G, L⦄ ⊢ ⬊*[h, o] T. +lemma csx_fwd_flat: ∀h,o,I,G,L,V,T. ⦃G, L⦄ ⊢ ⬈[h, o] 𝐒⦃ⓕ{I}V.T⦄ → + ⦃G, L⦄ ⊢ ⬈[h, o] 𝐒⦃V⦄ ∧ ⦃G, L⦄ ⊢ ⬈[h, o] 𝐒⦃T⦄. /3 width=3 by csx_fwd_pair_sn, csx_fwd_flat_dx, conj/ qed-. (* Basic_1: removed theorems 14: diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_cnx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_cnx.ma new file mode 100644 index 000000000..17d8633dc --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_cnx.ma @@ -0,0 +1,24 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* STRONGLY NORMALIZING TERMS FOR UNCOUNTED PARALLEL RT-TRANSITION **********) + +include "basic_2/rt_transition/cnx.ma". +include "basic_2/rt_computation/csx.ma". + +(* Properties with normal terms for uncounted parallel rt-transition ********) + +(* Basic_1: was just: sn3_nf2 *) +lemma cnx_csx: ∀h,o,G,L,T. ⦃G, L⦄ ⊢ ⬈[h, o] 𝐍⦃T⦄ → ⦃G, L⦄ ⊢ ⬈[h, o] 𝐒⦃T⦄. +/2 width=1 by NF_to_SN/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_main.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_main.ma new file mode 100644 index 000000000..d3556cef5 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_main.ma @@ -0,0 +1,34 @@ +(* +lemma csx_tdeq_trans: ∀h,o,G,L,T1. ⦃G, L⦄ ⊢ ⬈[h, o] 𝐒⦃T1⦄ → + ∀T2. T1 ≡[h, o] T2 → ⦃G, L⦄ ⊢ ⬈[h, o] 𝐒⦃T2⦄. +#h #o #G #L #T1 #H @(csx_ind … H) -H #T #HT #IH #T2 #HT2 +@csx_intro #T0 #HT20 #HnT20 + +lemma csx_tdeq_trans: ∀h,o,T1,T2. T1 ≡[h, o] T2 → + ∀G,L. ⦃G, L⦄ ⊢ ⬈[h, o] 𝐒⦃T1⦄ → ⦃G, L⦄ ⊢ ⬈[h, o] 𝐒⦃T2⦄. +#h #o #T1 #T2 #H elim H -T1 -T2 // +[ #s1 #s2 #d #Hs1 #Hs2 #G #L #H +| #I #V1 #V2 #T1 #T2 #_ #_ #IHV #IHT #G #L #H + +lemma csx_cpx_trans: ∀h,o,G,L,T1. ⦃G, L⦄ ⊢ ⬈[h, o] 𝐒⦃T1⦄ → + ∀T2. ⦃G, L⦄ ⊢ T1 ⬈[h] T2 → ⦃G, L⦄ ⊢ ⬈[h, o] 𝐒⦃T2⦄. +#h #o #G #L #T1 #H @(csx_ind … H) -T1 #T1 #HT1 #IHT1 #T2 #HLT12 +elim (tdeq_dec h o T1 T2) #HT12 /3 width=4 by/ -IHT1 -HLT12 +qed-. + +(* Basic_1: was just: sn3_cast *) +lemma csx_cast: ∀h,o,G,L,W. ⦃G, L⦄ ⊢ ⬈[h, o] 𝐒⦃W → + ∀T. ⦃G, L⦄ ⊢ ⬈[h, o] 𝐒⦃T → ⦃G, L⦄ ⊢ ⬈[h, o] 𝐒⦃ⓝW.T. +#h #o #G #L #W #HW @(csx_ind … HW) -W #W #HW #IHW #T #HT @(csx_ind … HT) -T #T #HT #IHT +@csx_intro #X #H1 #H2 +elim (cpx_inv_cast1 … H1) -H1 +[ * #W0 #T0 #HLW0 #HLT0 #H destruct + elim (eq_false_inv_tpair_sn … H2) -H2 + [ /3 width=3 by csx_cpx_trans/ + | -HLW0 * #H destruct /3 width=1 by/ + ] +|2,3: /3 width=3 by csx_cpx_trans/ +] +qed. + +*) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt index 41a6c9556..fb8f2ebf9 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt @@ -1 +1,2 @@ cpxs.ma +csx.ma csx_cnx.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/syntax/tdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/syntax/tdeq.ma index c79c1940c..4e5e41b4d 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/syntax/tdeq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/syntax/tdeq.ma @@ -32,19 +32,6 @@ interpretation definition cdeq: ∀h. sd h → relation3 lenv term term ≝ λh,o,L. tdeq h o. -(* Basic properties *********************************************************) - -lemma tdeq_refl: ∀h,o. reflexive … (tdeq h o). -#h #o #T elim T -T /2 width=1 by tdeq_pair/ -* /2 width=1 by tdeq_lref, tdeq_gref/ -#s elim (deg_total h o s) /2 width=3 by tdeq_sort/ -qed. - -lemma tdeq_sym: ∀h,o. symmetric … (tdeq h o). -#h #o #T1 #T2 #H elim H -T1 -T2 -/2 width=3 by tdeq_sort, tdeq_lref, tdeq_gref, tdeq_pair/ -qed-. - (* Basic inversion lemmas ***************************************************) fact tdeq_inv_sort1_aux: ∀h,o,X,Y. X ≡[h, o] Y → ∀s1. X = ⋆s1 → @@ -100,7 +87,15 @@ lemma tdeq_inv_pair1: ∀h,o,I,V1,T1,Y. ②{I}V1.T1 ≡[h, o] Y → lemma tdeq_inv_sort1_deg: ∀h,o,Y,s1. ⋆s1 ≡[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/ +#s2 #x #Hx <(deg_mono h o … Hx … Hs1) -s1 -d /2 width=3 by ex2_intro/ +qed-. + +lemma tdeq_inv_sort_deg: ∀h,o,s1,s2. ⋆s1 ≡[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 +elim (tdeq_inv_sort1_deg … H … Hs1) -s1 #s2 #Hs2 #H destruct +<(deg_mono h o … Hy … Hs2) -s2 -d1 // qed-. lemma tdeq_inv_pair: ∀h,o,I1,I2,V1,V2,T1,T2. ②{I1}V1.T1 ≡[h, o] ②{I2}V2.T2 → @@ -122,3 +117,54 @@ lemma tdeq_fwd_atom1: ∀h,o,I,Y. ⓪{I} ≡[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-. + +(* Basic properties *********************************************************) + +lemma tdeq_refl: ∀h,o. reflexive … (tdeq h o). +#h #o #T elim T -T /2 width=1 by tdeq_pair/ +* /2 width=1 by tdeq_lref, tdeq_gref/ +#s elim (deg_total h o s) /2 width=3 by tdeq_sort/ +qed. + +lemma tdeq_sym: ∀h,o. symmetric … (tdeq h o). +#h #o #T1 #T2 #H elim H -T1 -T2 +/2 width=3 by tdeq_sort, tdeq_lref, tdeq_gref, tdeq_pair/ +qed-. + +lemma tdeq_dec: ∀h,o,T1,T2. Decidable (tdeq h o T1 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 + elim (eq_nat_dec d1 d2) #Hd12 destruct /3 width=3 by tdeq_sort, or_introl/ + @or_intror #H + lapply (tdeq_inv_sort_deg … H … H1 H2) -H -H1 -H2 /2 width=1 by/ +|2,3,13: + @or_intror #H + elim (tdeq_inv_sort1 … H) -H #x1 #x2 #_ #_ #H destruct +|4,6,14: + @or_intror #H + lapply (tdeq_inv_lref1 … H) -H #H destruct +|5: + elim (eq_nat_dec s1 s2) #Hs12 destruct /2 width=1 by or_introl/ + @or_intror #H + lapply (tdeq_inv_lref1 … H) -H #H destruct /2 width=1 by/ +|7,8,15: + @or_intror #H + lapply (tdeq_inv_gref1 … H) -H #H destruct +|9: + elim (eq_nat_dec s1 s2) #Hs12 destruct /2 width=1 by or_introl/ + @or_intror #H + lapply (tdeq_inv_gref1 … H) -H #H destruct /2 width=1 by/ +|10,11,12: + @or_intror #H + elim (tdeq_inv_pair1 … H) -H #X1 #X2 #_ #_ #H destruct +|16: + elim (eq_item2_dec I1 I2) #HI12 destruct + [ elim (IHV V2) -IHV #HV12 + elim (IHT T2) -IHT #HT12 + [ /3 width=1 by tdeq_pair, or_introl/ ] + ] + @or_intror #H + elim (tdeq_inv_pair … H) -H /2 width=1 by/ +] +qed-.