From 04cd2181640b3828b3d193a8e819c849ef574236 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sat, 26 Nov 2011 22:52:35 +0000 Subject: [PATCH] component "reducibility" updated to new syntax! --- .../lambda_delta/Basic_2/reducibility/cpr.ma | 14 +-- .../Basic_2/reducibility/cpr_cpr.ma | 6 +- .../Basic_2/reducibility/cpr_lift.ma | 14 +-- .../Basic_2/reducibility/cpr_ltpr.ma | 10 +- .../lambda_delta/Basic_2/reducibility/lcpr.ma | 2 +- .../lambda_delta/Basic_2/reducibility/ltpr.ma | 24 ++-- .../Basic_2/reducibility/ltpr_ldrop.ma | 26 ++--- .../lambda_delta/Basic_2/reducibility/tnf.ma | 34 +++--- .../lambda_delta/Basic_2/reducibility/tpr.ma | 41 ++++--- .../Basic_2/reducibility/tpr_lift.ma | 106 +++++++++--------- .../Basic_2/reducibility/tpr_tpr.ma | 104 ++++++++--------- .../Basic_2/reducibility/tpr_tpss.ma | 78 ++++++------- .../lambda_delta/Basic_2/reducibility/trf.ma | 34 +++--- .../Basic_2/reducibility/twhnf.ma | 12 +- 14 files changed, 252 insertions(+), 253 deletions(-) diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/cpr.ma b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/cpr.ma index 90bd96d4d..3b05c3ea6 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/cpr.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/cpr.ma @@ -30,13 +30,13 @@ interpretation (* Basic_1: was by definition: pr2_free *) lemma cpr_pr: ∀T1,T2. T1 ⇒ T2 → ∀L. L ⊢ T1 ⇒ T2. -/2/ qed. +/2 width=3/ qed. lemma cpr_tpss: ∀L,T1,T2,d,e. L ⊢ T1 [d, e] ≫* T2 → L ⊢ T1 ⇒ T2. /3 width=5/ qed. lemma cpr_refl: ∀L,T. L ⊢ T ⇒ T. -/2/ qed. +/2 width=1/ qed. (* Note: new property *) (* Basic_1: was only: pr2_thin_dx *) @@ -47,7 +47,7 @@ qed. lemma cpr_cast: ∀L,V,T1,T2. L ⊢ T1 ⇒ T2 → L ⊢ 𝕔{Cast} V. T1 ⇒ T2. -#L #V #T1 #T2 * /3/ +#L #V #T1 #T2 * /3 width=3/ qed. (* Note: it does not hold replacing |L1| with |L2| *) @@ -55,7 +55,7 @@ qed. lemma cpr_lsubs_conf: ∀L1,T1,T2. L1 ⊢ T1 ⇒ T2 → ∀L2. L1 [0, |L1|] ≼ L2 → L2 ⊢ T1 ⇒ T2. #L1 #T1 #T2 * #T #HT1 #HT2 #L2 #HL12 -lapply (tpss_lsubs_conf … HT2 … HL12) -HT2 HL12 /3/ +lapply (tpss_lsubs_conf … HT2 … HL12) -HT2 -HL12 /3 width=4/ qed. (* Basic inversion lemmas ***************************************************) @@ -79,9 +79,9 @@ lemma cpr_inv_cast1: ∀L,V1,T1,U2. L ⊢ 𝕔{Cast} V1. T1 ⇒ U2 → ( U2 = 𝕔{Cast} V2. T2 ) ∨ L ⊢ T1 ⇒ U2. #L #V1 #T1 #U2 * #X #H #HU2 -elim (tpr_inv_cast1 … H) -H /3/ -* #V #T #HV1 #HT1 #H destruct -X; -elim (tpss_inv_flat1 … HU2) -HU2 #V2 #T2 #HV2 #HT2 #H destruct -U2 /4 width=5/ +elim (tpr_inv_cast1 … H) -H /3 width=3/ +* #V #T #HV1 #HT1 #H destruct +elim (tpss_inv_flat1 … HU2) -HU2 #V2 #T2 #HV2 #HT2 #H destruct /4 width=5/ qed-. (* Basic_1: removed theorems 5: diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/cpr_cpr.ma b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/cpr_cpr.ma index 005e9b0d4..5ac57a614 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/cpr_cpr.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/cpr_cpr.ma @@ -22,7 +22,7 @@ include "Basic_2/reducibility/cpr.ma". lemma cpr_bind_sn: ∀I,L,V1,V2,T1,T2. L ⊢ V1 ⇒ V2 → T1 ⇒ T2 → L ⊢ 𝕓{I} V1. T1 ⇒ 𝕓{I} V2. T2. #I #L #V1 #V2 #T1 #T2 * #V #HV1 #HV2 #HT12 -@ex2_1_intro [2: @(tpr_delta … HV1 HT12) | skip ] /2/ (* /3 width=5/ is too slow *) +@ex2_1_intro [2: @(tpr_delta … HV1 HT12) | skip ] /2 width=3/ (* /3 width=5/ is too slow *) qed. (* Basic_1: was only: pr2_gen_cbind *) @@ -30,9 +30,9 @@ lemma cpr_bind_dx: ∀I,L,V1,V2,T1,T2. V1 ⇒ V2 → L. 𝕓{I} V2 ⊢ T1 ⇒ T2 L ⊢ 𝕓{I} V1. T1 ⇒ 𝕓{I} V2. T2. #I #L #V1 #V2 #T1 #T2 #HV12 * #T #HT1 normalize #HT2 elim (tpss_split_up … HT2 1 ? ?) -HT2 // #T0 (tpr_inv_atom1 … H) -H #H -elim (tpss_inv_lref1 … H) -H /2/ +elim (tpss_inv_lref1 … H) -H /2 width=1/ * /3 width=6/ qed-. (* Basic_1: was: pr2_gen_abst *) lemma cpr_inv_abst1: ∀V1,T1,U2. 𝕔{Abst} V1. T1 ⇒ U2 → ∃∃V2,T2. V1 ⇒ V2 & T1 ⇒ T2 & U2 = 𝕔{Abst} V2. T2. -/2/ qed-. +/2 width=3/ qed-. (* Relocation properties ****************************************************) @@ -58,8 +58,8 @@ lemma cpr_lift: ∀L,K,d,e. ↓[d, e] L ≡ K → elim (lift_total T d e) #U #HTU lapply (tpr_lift … HT1 … HTU1 … HTU) -T1 #HU1 elim (lt_or_ge (|K|) d) #HKd -[ lapply (tpss_lift_le … HT2 … HLK HTU … HTU2) -T2 T HLK [ /2/ | /3/ ] -| lapply (tpss_lift_be … HT2 … HLK HTU … HTU2) -T2 T HLK // /3/ +[ lapply (tpss_lift_le … HT2 … HLK HTU … HTU2) -T2 -T -HLK [ /2 width=1/ | /3 width=4/ ] +| lapply (tpss_lift_be … HT2 … HLK HTU … HTU2) -T2 -T -HLK // /3 width=4/ ] qed. @@ -70,10 +70,10 @@ lemma cpr_inv_lift: ∀L,K,d,e. ↓[d, e] L ≡ K → #L #K #d #e #HLK #T1 #U1 #HTU1 #U2 * #U #HU1 #HU2 elim (tpr_inv_lift … HU1 … HTU1) -U1 #T #HTU #T1 elim (lt_or_ge (|L|) d) #HLd -[ elim (tpss_inv_lift1_le … HU2 … HLK … HTU ?) -U HLK [ /5/ | /2/ ] +[ elim (tpss_inv_lift1_le … HU2 … HLK … HTU ?) -U -HLK [ /5 width=4/ | /2 width=1/ ] | elim (lt_or_ge (|L|) (d + e)) #HLde - [ elim (tpss_inv_lift1_be_up … HU2 … HLK … HTU ? ?) -U HLK // [ /5/ | /2/ ] - | elim (tpss_inv_lift1_be … HU2 … HLK … HTU ? ?) -U HLK // /5/ + [ elim (tpss_inv_lift1_be_up … HU2 … HLK … HTU ? ?) -U -HLK // [ /5 width=4/ | /2 width=1/ ] + | elim (tpss_inv_lift1_be … HU2 … HLK … HTU ? ?) -U -HLK // /5 width=4/ ] ] qed. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/cpr_ltpr.ma b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/cpr_ltpr.ma index 486c12ee0..1311e5290 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/cpr_ltpr.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/cpr_ltpr.ma @@ -25,15 +25,15 @@ lemma cpr_tpss_ltpr: ∀L1,L2. L1 ⇒ L2 → ∀T1,T2. L2 ⊢ T1 ⇒ T2 → ∀d,e,U1. L1 ⊢ T1 [d, e] ≫* U1 → ∃∃U2. L2 ⊢ U1 ⇒ U2 & L2 ⊢ T2 [d, e] ≫* U2. #L1 #L2 #HL12 #T1 #T2 * #T #HT1 #HT2 #d #e #U1 #HTU1 -elim (tpr_tpss_ltpr … HL12 … HT1 … HTU1) -L1 HT1 #U #HU1 #HTU -elim (tpss_conf_eq … HT2 … HTU) -T /3/ +elim (tpr_tpss_ltpr … HL12 … HT1 … HTU1) -L1 -HT1 #U #HU1 #HTU +elim (tpss_conf_eq … HT2 … HTU) -T /3 width=3/ qed. lemma cpr_ltpr_conf_eq: ∀L1,T1,T2. L1 ⊢ T1 ⇒ T2 → ∀L2. L1 ⇒ L2 → ∃∃T. L2 ⊢ T1 ⇒ T & T2 ⇒ T. #L1 #T1 #T2 * #T #HT1 #HT2 #L2 #HL12 ->(ltpr_fwd_length … HL12) in HT2 #HT2 -elim (tpr_tpss_ltpr … HL12 … HT2) -L1 HT2 /3/ +>(ltpr_fwd_length … HL12) in HT2; #HT2 +elim (tpr_tpss_ltpr … HL12 … HT2) -L1 /3 width=3/ qed. lemma cpr_ltpr_conf_tpss: ∀L1,L2. L1 ⇒ L2 → ∀T1,T2. L1 ⊢ T1 ⇒ T2 → @@ -41,6 +41,6 @@ lemma cpr_ltpr_conf_tpss: ∀L1,L2. L1 ⇒ L2 → ∀T1,T2. L1 ⊢ T1 ⇒ T2 → ∃∃U2. L2 ⊢ U1 ⇒ U2 & L2 ⊢ T2 ⇒ U2. #L1 #L2 #HL12 #T1 #T2 #HT12 #d #e #U1 #HTU1 elim (cpr_ltpr_conf_eq … HT12 … HL12) -HT12 #T #HT1 #HT2 -elim (cpr_tpss_ltpr … HL12 … HT1 … HTU1) -L1 HT1 #U2 #HU12 #HTU2 +elim (cpr_tpss_ltpr … HL12 … HT1 … HTU1) -L1 -HT1 #U2 #HU12 #HTU2 lapply (tpss_weak_all … HTU2) -HTU2 #HTU2 /3 width=5/ (**) (* /4 width=5/ is too slow *) qed. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/lcpr.ma b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/lcpr.ma index 13545ad84..30df056e0 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/lcpr.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/lcpr.ma @@ -28,7 +28,7 @@ interpretation (* Basic properties *********************************************************) lemma lcpr_refl: ∀L. L ⊢ ⇒ L. -/2/ qed. +/2 width=3/ qed. (* Basic inversion lemmas ***************************************************) diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/ltpr.ma b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/ltpr.ma index b3ba2ff44..2208557a7 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/ltpr.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/ltpr.ma @@ -29,13 +29,13 @@ interpretation (* Basic properties *********************************************************) lemma ltpr_refl: ∀L:lenv. L ⇒ L. -#L elim L -L /2/ +#L elim L -L // /2 width=1/ qed. (* Basic inversion lemmas ***************************************************) fact ltpr_inv_atom1_aux: ∀L1,L2. L1 ⇒ L2 → L1 = ⋆ → L2 = ⋆. -#L1 #L2 * -L1 L2 +#L1 #L2 * -L1 -L2 [ // | #K1 #K2 #I #V1 #V2 #_ #_ #H destruct ] @@ -43,47 +43,47 @@ qed. (* Basic_1: was: wcpr0_gen_sort *) lemma ltpr_inv_atom1: ∀L2. ⋆ ⇒ L2 → L2 = ⋆. -/2/ qed-. +/2 width=3/ qed-. fact ltpr_inv_pair1_aux: ∀L1,L2. L1 ⇒ L2 → ∀K1,I,V1. L1 = K1. 𝕓{I} V1 → ∃∃K2,V2. K1 ⇒ K2 & V1 ⇒ V2 & L2 = K2. 𝕓{I} V2. -#L1 #L2 * -L1 L2 +#L1 #L2 * -L1 -L2 [ #K1 #I #V1 #H destruct -| #K1 #K2 #I #V1 #V2 #HK12 #HV12 #L #J #W #H destruct - K1 I V1 /2 width=5/ +| #K1 #K2 #I #V1 #V2 #HK12 #HV12 #L #J #W #H destruct /2 width=5/ ] qed. (* Basic_1: was: wcpr0_gen_head *) lemma ltpr_inv_pair1: ∀K1,I,V1,L2. K1. 𝕓{I} V1 ⇒ L2 → ∃∃K2,V2. K1 ⇒ K2 & V1 ⇒ V2 & L2 = K2. 𝕓{I} V2. -/2/ qed-. +/2 width=3/ qed-. fact ltpr_inv_atom2_aux: ∀L1,L2. L1 ⇒ L2 → L2 = ⋆ → L1 = ⋆. -#L1 #L2 * -L1 L2 +#L1 #L2 * -L1 -L2 [ // | #K1 #K2 #I #V1 #V2 #_ #_ #H destruct ] qed. lemma ltpr_inv_atom2: ∀L1. L1 ⇒ ⋆ → L1 = ⋆. -/2/ qed-. +/2 width=3/ qed-. fact ltpr_inv_pair2_aux: ∀L1,L2. L1 ⇒ L2 → ∀K2,I,V2. L2 = K2. 𝕓{I} V2 → ∃∃K1,V1. K1 ⇒ K2 & V1 ⇒ V2 & L1 = K1. 𝕓{I} V1. -#L1 #L2 * -L1 L2 +#L1 #L2 * -L1 -L2 [ #K2 #I #V2 #H destruct -| #K1 #K2 #I #V1 #V2 #HK12 #HV12 #K #J #W #H destruct -K2 I V2 /2 width=5/ +| #K1 #K2 #I #V1 #V2 #HK12 #HV12 #K #J #W #H destruct /2 width=5/ ] qed. lemma ltpr_inv_pair2: ∀L1,K2,I,V2. L1 ⇒ K2. 𝕓{I} V2 → ∃∃K1,V1. K1 ⇒ K2 & V1 ⇒ V2 & L1 = K1. 𝕓{I} V1. -/2/ qed-. +/2 width=3/ qed-. (* Basic forward lemmas *****************************************************) lemma ltpr_fwd_length: ∀L1,L2. L1 ⇒ L2 → |L1| = |L2|. -#L1 #L2 #H elim H -H L1 L2; normalize // +#L1 #L2 #H elim H -L1 -L2 normalize // qed-. (* Basic_1: removed theorems 2: wcpr0_getl wcpr0_getl_back *) diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/ltpr_ldrop.ma b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/ltpr_ldrop.ma index b24c0bad2..38e7858dc 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/ltpr_ldrop.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/ltpr_ldrop.ma @@ -20,33 +20,33 @@ include "Basic_2/reducibility/ltpr.ma". (* Basic_1: was: wcpr0_ldrop *) lemma ltpr_ldrop_conf: ∀L1,K1,d,e. ↓[d, e] L1 ≡ K1 → ∀L2. L1 ⇒ L2 → ∃∃K2. ↓[d, e] L2 ≡ K2 & K1 ⇒ K2. -#L1 #K1 #d #e #H elim H -H L1 K1 d e -[ #d #e #X #H >(ltpr_inv_atom1 … H) -H /2/ +#L1 #K1 #d #e #H elim H -L1 -K1 -d -e +[ #d #e #X #H >(ltpr_inv_atom1 … H) -H /2 width=3/ | #K1 #I #V1 #X #H elim (ltpr_inv_pair1 … H) -H #L2 #V2 #HL12 #HV12 #H destruct /3 width=5/ | #L1 #K1 #I #V1 #e #_ #IHLK1 #X #H - elim (ltpr_inv_pair1 … H) -H #L2 #V2 #HL12 #HV12 #H destruct -X; - elim (IHLK1 … HL12) -IHLK1 HL12 /3/ + elim (ltpr_inv_pair1 … H) -H #L2 #V2 #HL12 #HV12 #H destruct + elim (IHLK1 … HL12) -L1 /3 width=3/ | #L1 #K1 #I #V1 #W1 #d #e #_ #HWV1 #IHLK1 #X #H - elim (ltpr_inv_pair1 … H) -H #L2 #V2 #HL12 #HV12 #H destruct -X; - elim (tpr_inv_lift … HV12 … HWV1) -HV12 HWV1; - elim (IHLK1 … HL12) -IHLK1 HL12 /3 width=5/ + elim (ltpr_inv_pair1 … H) -H #L2 #V2 #HL12 #HV12 #H destruct + elim (tpr_inv_lift … HV12 … HWV1) -V1 + elim (IHLK1 … HL12) -L1 /3 width=5/ ] qed. (* Basic_1: was: wcpr0_ldrop_back *) lemma ltpr_ldrop_trans: ∀L1,K1,d,e. ↓[d, e] L1 ≡ K1 → ∀K2. K1 ⇒ K2 → ∃∃L2. ↓[d, e] L2 ≡ K2 & L1 ⇒ L2. -#L1 #K1 #d #e #H elim H -H L1 K1 d e -[ #d #e #X #H >(ltpr_inv_atom1 … H) -H /2/ +#L1 #K1 #d #e #H elim H -L1 -K1 -d -e +[ #d #e #X #H >(ltpr_inv_atom1 … H) -H /2 width=3/ | #K1 #I #V1 #X #H elim (ltpr_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct /3 width=5/ | #L1 #K1 #I #V1 #e #_ #IHLK1 #K2 #HK12 - elim (IHLK1 … HK12) -IHLK1 HK12 /3 width=5/ + elim (IHLK1 … HK12) -K1 /3 width=5/ | #L1 #K1 #I #V1 #W1 #d #e #_ #HWV1 #IHLK1 #X #H - elim (ltpr_inv_pair1 … H) -H #K2 #W2 #HK12 #HW12 #H destruct -X; + elim (ltpr_inv_pair1 … H) -H #K2 #W2 #HK12 #HW12 #H destruct elim (lift_total W2 d e) #V2 #HWV2 - lapply (tpr_lift … HW12 … HWV1 … HWV2) -HW12 HWV1; - elim (IHLK1 … HK12) -IHLK1 HK12 /3 width=5/ + lapply (tpr_lift … HW12 … HWV1 … HWV2) -W1 + elim (IHLK1 … HK12) -K1 /3 width=5/ ] qed. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tnf.ma b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tnf.ma index 5772e7626..1353c7f06 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tnf.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tnf.ma @@ -28,30 +28,30 @@ interpretation lemma tnf_inv_abst: ∀V,T. ℕ[𝕔{Abst}V.T] → ℕ[V] ∧ ℕ[T]. #V1 #T1 #HVT1 @conj -[ #V2 #HV2 lapply (HVT1 (𝕔{Abst}V2.T1) ?) -HVT1 /2/ -HV2 #H destruct -V1 T1 // -| #T2 #HT2 lapply (HVT1 (𝕔{Abst}V1.T2) ?) -HVT1 /2/ -HT2 #H destruct -V1 T1 // +[ #V2 #HV2 lapply (HVT1 (𝕔{Abst}V2.T1) ?) -HVT1 /2 width=1/ -HV2 #H destruct // +| #T2 #HT2 lapply (HVT1 (𝕔{Abst}V1.T2) ?) -HVT1 /2 width=1/ -HT2 #H destruct // ] qed-. lemma tnf_inv_appl: ∀V,T. ℕ[𝕔{Appl}V.T] → ∧∧ ℕ[V] & ℕ[T] & 𝕊[T]. #V1 #T1 #HVT1 @and3_intro -[ #V2 #HV2 lapply (HVT1 (𝕔{Appl}V2.T1) ?) -HVT1 /2/ -HV2 #H destruct -V1 T1 // -| #T2 #HT2 lapply (HVT1 (𝕔{Appl}V1.T2) ?) -HVT1 /2/ -HT2 #H destruct -V1 T1 // -| generalize in match HVT1 -HVT1; elim T1 -T1 * // * #W1 #U1 #_ #_ #H +[ #V2 #HV2 lapply (HVT1 (𝕔{Appl}V2.T1) ?) -HVT1 /2 width=1/ -HV2 #H destruct // +| #T2 #HT2 lapply (HVT1 (𝕔{Appl}V1.T2) ?) -HVT1 /2 width=1/ -HT2 #H destruct // +| generalize in match HVT1; -HVT1 elim T1 -T1 * // * #W1 #U1 #_ #_ #H [ elim (lift_total V1 0 1) #V2 #HV12 - lapply (H (𝕔{Abbr}W1.𝕔{Appl}V2.U1) ?) -H /2/ -HV12 #H destruct - | lapply (H (𝕔{Abbr}V1.U1) ?) -H /2/ #H destruct + lapply (H (𝕔{Abbr}W1.𝕔{Appl}V2.U1) ?) -H /2 width=3/ -HV12 #H destruct + | lapply (H (𝕔{Abbr}V1.U1) ?) -H /2 width=1/ #H destruct ] qed-. lemma tnf_inv_abbr: ∀V,T. ℕ[𝕔{Abbr}V.T] → False. #V #T #H elim (is_lift_dec T 0 1) [ * #U #HTU - lapply (H U ?) -H /2 width=3/ #H destruct -U; + lapply (H U ?) -H /2 width=3/ #H destruct elim (lift_inv_pair_xy_y … HTU) | #HT elim (tps_full (⋆) V T (⋆. 𝕓{Abbr} V) 0 ?) // #T2 #T1 #HT2 #HT12 - lapply (H (𝕓{Abbr}V.T2) ?) -H /2/ -HT2 #H destruct -T /3 width=2/ + lapply (H (𝕓{Abbr}V.T2) ?) -H /2 width=3/ -HT2 #H destruct /3 width=2/ ] qed. @@ -63,7 +63,7 @@ qed-. (* Basic properties *********************************************************) lemma tpr_tif_eq: ∀T1,T2. T1 ⇒ T2 → 𝕀[T1] → T1 = T2. -#T1 #T2 #H elim H -T1 T2 +#T1 #T2 #H elim H -T1 -T2 [ // | * #V1 #V2 #T1 #T2 #_ #_ #IHV1 #IHT1 #H [ elim (tif_inv_appl … H) -H #HV1 #HT1 #_ @@ -74,7 +74,7 @@ lemma tpr_tif_eq: ∀T1,T2. T1 ⇒ T2 → 𝕀[T1] → T1 = T2. elim (tif_inv_appl … H) -H #_ #_ #H elim (simple_inv_bind … H) | * #V1 #V2 #T1 #T #T2 #_ #_ #HT2 #IHV1 #IHT1 #H - [ -HT2 IHV1 IHT1; elim (tif_inv_abbr … H) + [ -HT2 -IHV1 -IHT1 elim (tif_inv_abbr … H) | <(tps_inv_refl_SO2 … HT2 ?) -HT2 // elim (tif_inv_abst … H) -H #HV1 #HT1 >IHV1 -IHV1 // -HV1 >IHT1 -IHT1 // @@ -90,15 +90,15 @@ lemma tpr_tif_eq: ∀T1,T2. T1 ⇒ T2 → 𝕀[T1] → T1 = T2. qed. theorem tif_tnf: ∀T1. 𝕀[T1] → ℕ[T1]. -/2/ qed. +/2 width=1/ qed. (* Note: this property is unusual *) theorem tnf_trf_false: ∀T1. ℝ[T1] → ℕ[T1] → False. #T1 #H elim H -T1 -[ #V #T #_ #IHV #H elim (tnf_inv_abst … H) -H /2/ -| #V #T #_ #IHT #H elim (tnf_inv_abst … H) -H /2/ -| #V #T #_ #IHV #H elim (tnf_inv_appl … H) -H /2/ -| #V #T #_ #IHV #H elim (tnf_inv_appl … H) -H /2/ +[ #V #T #_ #IHV #H elim (tnf_inv_abst … H) -H /2 width=1/ +| #V #T #_ #IHT #H elim (tnf_inv_abst … H) -H /2 width=1/ +| #V #T #_ #IHV #H elim (tnf_inv_appl … H) -H /2 width=1/ +| #V #T #_ #IHV #H elim (tnf_inv_appl … H) -H /2 width=1/ | #V #T #H elim (tnf_inv_abbr … H) | #V #T #H elim (tnf_inv_cast … H) | #V #W #T #H elim (tnf_inv_appl … H) -H #_ #_ #H @@ -107,7 +107,7 @@ theorem tnf_trf_false: ∀T1. ℝ[T1] → ℕ[T1] → False. qed. theorem tnf_tif: ∀T1. ℕ[T1] → 𝕀[T1]. -/2/ qed. +/2 width=3/ qed. lemma tnf_abst: ∀V,T. ℕ[V] → ℕ[T] → ℕ[𝕔{Abst}V.T]. /4 width=1/ qed. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tpr.ma b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tpr.ma index f2818ea72..cf0c7cae2 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tpr.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tpr.ma @@ -44,18 +44,18 @@ interpretation lemma tpr_bind: ∀I,V1,V2,T1,T2. V1 ⇒ V2 → T1 ⇒ T2 → 𝕓{I} V1. T1 ⇒ 𝕓{I} V2. T2. -/2/ qed. +/2 width=3/ qed. (* Basic_1: was by definition: pr0_refl *) lemma tpr_refl: ∀T. T ⇒ T. #T elim T -T // -#I elim I -I /2/ +#I elim I -I /2 width=1/ qed. (* Basic inversion lemmas ***************************************************) fact tpr_inv_atom1_aux: ∀U1,U2. U1 ⇒ U2 → ∀I. U1 = 𝕒{I} → U2 = 𝕒{I}. -#U1 #U2 * -U1 U2 +#U1 #U2 * -U1 -U2 [ // | #I #V1 #V2 #T1 #T2 #_ #_ #k #H destruct | #V1 #V2 #W #T1 #T2 #_ #_ #k #H destruct @@ -68,7 +68,7 @@ qed. (* Basic_1: was: pr0_gen_sort pr0_gen_lref *) lemma tpr_inv_atom1: ∀I,U2. 𝕒{I} ⇒ U2 → U2 = 𝕒{I}. -/2/ qed-. +/2 width=3/ qed-. fact tpr_inv_bind1_aux: ∀U1,U2. U1 ⇒ U2 → ∀I,V1,T1. U1 = 𝕓{I} V1. T1 → (∃∃V2,T2,T. V1 ⇒ V2 & T1 ⇒ T2 & @@ -76,13 +76,13 @@ fact tpr_inv_bind1_aux: ∀U1,U2. U1 ⇒ U2 → ∀I,V1,T1. U1 = 𝕓{I} V1. T1 U2 = 𝕓{I} V2. T ) ∨ ∃∃T. ↑[0,1] T ≡ T1 & T ⇒ U2 & I = Abbr. -#U1 #U2 * -U1 U2 +#U1 #U2 * -U1 -U2 [ #J #I #V #T #H destruct | #I1 #V1 #V2 #T1 #T2 #_ #_ #I #V #T #H destruct | #V1 #V2 #W #T1 #T2 #_ #_ #I #V #T #H destruct -| #I1 #V1 #V2 #T1 #T2 #T #HV12 #HT12 #HT2 #I0 #V0 #T0 #H destruct -I1 V1 T1 /3 width=7/ +| #I1 #V1 #V2 #T1 #T2 #T #HV12 #HT12 #HT2 #I0 #V0 #T0 #H destruct /3 width=7/ | #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #I0 #V0 #T0 #H destruct -| #V #T #T1 #T2 #HT1 #HT12 #I0 #V0 #T0 #H destruct -V T /3/ +| #V #T #T1 #T2 #HT1 #HT12 #I0 #V0 #T0 #H destruct /3 width=3/ | #V #T1 #T2 #_ #I0 #V0 #T0 #H destruct ] qed. @@ -93,7 +93,7 @@ lemma tpr_inv_bind1: ∀V1,T1,U2,I. 𝕓{I} V1. T1 ⇒ U2 → U2 = 𝕓{I} V2. T ) ∨ ∃∃T. ↑[0,1] T ≡ T1 & T ⇒ U2 & I = Abbr. -/2/ qed-. +/2 width=3/ qed-. (* Basic_1: was pr0_gen_abbr *) lemma tpr_inv_abbr1: ∀V1,T1,U2. 𝕓{Abbr} V1. T1 ⇒ U2 → @@ -118,15 +118,14 @@ fact tpr_inv_flat1_aux: ∀U1,U2. U1 ⇒ U2 → ∀I,V1,U0. U1 = 𝕗{I} V1. U0 U2 = 𝕔{Abbr} W2. 𝕔{Appl} V. T2 & I = Appl | (U0 ⇒ U2 ∧ I = Cast). -#U1 #U2 * -U1 U2 +#U1 #U2 * -U1 -U2 [ #I #J #V #T #H destruct -| #I #V1 #V2 #T1 #T2 #HV12 #HT12 #J #V #T #H destruct -I V1 T1 /3 width=5/ -| #V1 #V2 #W #T1 #T2 #HV12 #HT12 #J #V #T #H destruct -J V1 T /3 width=8/ +| #I #V1 #V2 #T1 #T2 #HV12 #HT12 #J #V #T #H destruct /3 width=5/ +| #V1 #V2 #W #T1 #T2 #HV12 #HT12 #J #V #T #H destruct /3 width=8/ | #I #V1 #V2 #T1 #T2 #T #_ #_ #_ #J #V0 #T0 #H destruct -| #V #V1 #V2 #W1 #W2 #T1 #T2 #HV12 #HV2 #HW12 #HT12 #J #V0 #T0 #H - destruct -J V1 T0 /3 width=12/ +| #V #V1 #V2 #W1 #W2 #T1 #T2 #HV12 #HV2 #HW12 #HT12 #J #V0 #T0 #H destruct /3 width=12/ | #V #T #T1 #T2 #_ #_ #J #V0 #T0 #H destruct -| #V #T1 #T2 #HT12 #J #V0 #T0 #H destruct -J V T1 /3/ +| #V #T1 #T2 #HT12 #J #V0 #T0 #H destruct /3 width=1/ ] qed. @@ -142,7 +141,7 @@ lemma tpr_inv_flat1: ∀V1,U0,U2,I. 𝕗{I} V1. U0 ⇒ U2 → U2 = 𝕔{Abbr} W2. 𝕔{Appl} V. T2 & I = Appl | (U0 ⇒ U2 ∧ I = Cast). -/2/ qed-. +/2 width=3/ qed-. (* Basic_1: was pr0_gen_appl *) lemma tpr_inv_appl1: ∀V1,U0,U2. 𝕔{Appl} V1. U0 ⇒ U2 → @@ -166,9 +165,9 @@ lemma tpr_inv_appl1_simple: ∀V1,T1,U. 𝕔{Appl} V1. T1 ⇒ U → 𝕊[T1] → #V1 #T1 #U #H #HT1 elim (tpr_inv_appl1 … H) -H * [ /2 width=5/ -| #V2 #W #W1 #W2 #_ #_ #H #_ destruct -T1; +| #V2 #W #W1 #W2 #_ #_ #H #_ destruct elim (simple_inv_bind … HT1) -| #V2 #V #W1 #W2 #U1 #U2 #_ #_ #_ #_ #H #_ destruct -T1; +| #V2 #V #W1 #W2 #U1 #U2 #_ #_ #_ #_ #H #_ destruct elim (simple_inv_bind … HT1) ] qed-. @@ -189,14 +188,14 @@ fact tpr_inv_lref2_aux: ∀T1,T2. T1 ⇒ T2 → ∀i. T2 = #i → | ∃∃V,T,T0. ↑[O,1] T0 ≡ T & T0 ⇒ #i & T1 = 𝕔{Abbr} V. T | ∃∃V,T. T ⇒ #i & T1 = 𝕔{Cast} V. T. -#T1 #T2 * -T1 T2 -[ #I #i #H destruct /2/ +#T1 #T2 * -T1 -T2 +[ #I #i #H destruct /2 width=1/ | #I #V1 #V2 #T1 #T2 #_ #_ #i #H destruct | #V1 #V2 #W #T1 #T2 #_ #_ #i #H destruct | #I #V1 #V2 #T1 #T2 #T #_ #_ #_ #i #H destruct | #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #i #H destruct | #V #T #T1 #T2 #HT1 #HT12 #i #H destruct /3 width=6/ -| #V #T1 #T2 #HT12 #i #H destruct /3/ +| #V #T1 #T2 #HT12 #i #H destruct /3 width=4/ ] qed. @@ -205,7 +204,7 @@ lemma tpr_inv_lref2: ∀T1,i. T1 ⇒ #i → | ∃∃V,T,T0. ↑[O,1] T0 ≡ T & T0 ⇒ #i & T1 = 𝕔{Abbr} V. T | ∃∃V,T. T ⇒ #i & T1 = 𝕔{Cast} V. T. -/2/ qed-. +/2 width=3/ qed-. (* Basic_1: removed theorems 3: pr0_subst0_back pr0_subst0_fwd pr0_subst0 diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tpr_lift.ma b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tpr_lift.ma index a30dcddac..d9d9c549a 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tpr_lift.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tpr_lift.ma @@ -22,37 +22,37 @@ include "Basic_2/reducibility/tpr.ma". (* Basic_1: was: pr0_lift *) lemma tpr_lift: ∀T1,T2. T1 ⇒ T2 → ∀d,e,U1. ↑[d, e] T1 ≡ U1 → ∀U2. ↑[d, e] T2 ≡ U2 → U1 ⇒ U2. -#T1 #T2 #H elim H -H T1 T2 +#T1 #T2 #H elim H -T1 -T2 [ * #i #d #e #U1 #HU1 #U2 #HU2 - lapply (lift_mono … HU1 … HU2) -HU1 #H destruct -U1 - [ lapply (lift_inv_sort1 … HU2) -HU2 #H destruct -U2 // - | lapply (lift_inv_lref1 … HU2) * * #Hid #H destruct -U2 // - | lapply (lift_inv_gref1 … HU2) -HU2 #H destruct -U2 // + lapply (lift_mono … HU1 … HU2) -HU1 #H destruct + [ lapply (lift_inv_sort1 … HU2) -HU2 #H destruct // + | lapply (lift_inv_lref1 … HU2) * * #Hid #H destruct // + | lapply (lift_inv_gref1 … HU2) -HU2 #H destruct // ] | #I #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #d #e #X1 #HX1 #X2 #HX2 - elim (lift_inv_flat1 … HX1) -HX1 #W1 #U1 #HVW1 #HTU1 #HX1 destruct -X1; - elim (lift_inv_flat1 … HX2) -HX2 #W2 #U2 #HVW2 #HTU2 #HX2 destruct -X2 /3/ + elim (lift_inv_flat1 … HX1) -HX1 #W1 #U1 #HVW1 #HTU1 #HX1 destruct + elim (lift_inv_flat1 … HX2) -HX2 #W2 #U2 #HVW2 #HTU2 #HX2 destruct /3 width=4/ | #V1 #V2 #W #T1 #T2 #_ #_ #IHV12 #IHT12 #d #e #X1 #HX1 #X2 #HX2 - elim (lift_inv_flat1 … HX1) -HX1 #V0 #X #HV10 #HX #HX1 destruct -X1; - elim (lift_inv_bind1 … HX) -HX #W0 #T0 #HW0 #HT10 #HX destruct -X; - elim (lift_inv_bind1 … HX2) -HX2 #V3 #T3 #HV23 #HT23 #HX2 destruct -X2 /3/ + 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 #V3 #T3 #HV23 #HT23 #HX2 destruct /3 width=4/ | #I #V1 #V2 #T1 #T2 #T0 #HV12 #HT12 #HT2 #IHV12 #IHT12 #d #e #X1 #HX1 #X2 #HX2 - elim (lift_inv_bind1 … HX1) -HX1 #W1 #U1 #HVW1 #HTU1 #HX1 destruct -X1; - elim (lift_inv_bind1 … HX2) -HX2 #W2 #U0 #HVW2 #HTU0 #HX2 destruct -X2; + elim (lift_inv_bind1 … HX1) -HX1 #W1 #U1 #HVW1 #HTU1 #HX1 destruct + elim (lift_inv_bind1 … HX2) -HX2 #W2 #U0 #HVW2 #HTU0 #HX2 destruct elim (lift_total T2 (d + 1) e) #U2 #HTU2 @tpr_delta - [4: @(tps_lift_le … HT2 … HTU2 HTU0 ?) /2/ |1: skip |2: /2/ |3: /2/ ] (**) (*/3. is too slow *) + [4: @(tps_lift_le … HT2 … HTU2 HTU0 ?) /2 width=1/ |1: skip |2: /2 width=4/ |3: /2 width=4/ ] (**) (*/3. is too slow *) | #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV12 #IHW12 #IHT12 #d #e #X1 #HX1 #X2 #HX2 - elim (lift_inv_flat1 … HX1) -HX1 #V0 #X #HV10 #HX #HX1 destruct -X1; - elim (lift_inv_bind1 … HX) -HX #W0 #T0 #HW0 #HT10 #HX destruct -X; - elim (lift_inv_bind1 … HX2) -HX2 #W3 #X #HW23 #HX #HX2 destruct -X2; - elim (lift_inv_flat1 … HX) -HX #V3 #T3 #HV3 #HT23 #HX destruct -X; - elim (lift_trans_ge … HV2 … HV3 ?) -HV2 HV3 V // /3/ + 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 ?) -V // /3 width=4/ | #V #T #T1 #T2 #HT1 #_ #IHT12 #d #e #X #HX #T0 #HT20 - elim (lift_inv_bind1 … HX) -HX #V3 #T3 #_ #HT3 #HX destruct -X; - elim (lift_trans_ge … HT1 … HT3 ?) -HT1 HT3 T // /3 width=6/ + elim (lift_inv_bind1 … HX) -HX #V3 #T3 #_ #HT3 #HX destruct + elim (lift_trans_ge … HT1 … HT3 ?) -T // /3 width=6/ | #V #T1 #T2 #_ #IHT12 #d #e #X #HX #T #HT2 - elim (lift_inv_flat1 … HX) -HX #V0 #T0 #_ #HT0 #HX destruct -X /3/ + elim (lift_inv_flat1 … HX) -HX #V0 #T0 #_ #HT0 #HX destruct /3 width=4/ ] qed. @@ -60,42 +60,42 @@ qed. lemma tpr_inv_lift: ∀T1,T2. T1 ⇒ T2 → ∀d,e,U1. ↑[d, e] U1 ≡ T1 → ∃∃U2. ↑[d, e] U2 ≡ T2 & U1 ⇒ U2. -#T1 #T2 #H elim H -H T1 T2 +#T1 #T2 #H elim H -T1 -T2 [ * #i #d #e #U1 #HU1 - [ lapply (lift_inv_sort2 … HU1) -HU1 #H destruct -U1 /2/ - | lapply (lift_inv_lref2 … HU1) -HU1 * * #Hid #H destruct -U1 /3/ - | lapply (lift_inv_gref2 … HU1) -HU1 #H destruct -U1 /2/ + [ lapply (lift_inv_sort2 … HU1) -HU1 #H destruct /2 width=3/ + | lapply (lift_inv_lref2 … HU1) -HU1 * * #Hid #H destruct /3 width=3/ + | lapply (lift_inv_gref2 … HU1) -HU1 #H destruct /2 width=3/ ] | #I #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #d #e #X #HX - elim (lift_inv_flat2 … HX) -HX #V0 #T0 #HV01 #HT01 #HX destruct -X; - elim (IHV12 … HV01) -IHV12 HV01; - elim (IHT12 … HT01) -IHT12 HT01 /3 width=5/ + elim (lift_inv_flat2 … HX) -HX #V0 #T0 #HV01 #HT01 #HX destruct + elim (IHV12 … HV01) -V1 + elim (IHT12 … HT01) -T1 /3 width=5/ | #V1 #V2 #W1 #T1 #T2 #_ #_ #IHV12 #IHT12 #d #e #X #HX - elim (lift_inv_flat2 … HX) -HX #V0 #Y #HV01 #HY #HX destruct -X; - elim (lift_inv_bind2 … HY) -HY #W0 #T0 #HW01 #HT01 #HY destruct -Y; - elim (IHV12 … HV01) -IHV12 HV01; - elim (IHT12 … HT01) -IHT12 HT01 /3 width=5/ + elim (lift_inv_flat2 … HX) -HX #V0 #Y #HV01 #HY #HX destruct + elim (lift_inv_bind2 … HY) -HY #W0 #T0 #HW01 #HT01 #HY destruct + elim (IHV12 … HV01) -V1 + elim (IHT12 … HT01) -T1 /3 width=5/ | #I #V1 #V2 #T1 #T2 #T0 #_ #_ #HT20 #IHV12 #IHT12 #d #e #X #HX - elim (lift_inv_bind2 … HX) -HX #W1 #U1 #HWV1 #HUT1 #HX destruct -X; - elim (IHV12 … HWV1) -IHV12 HWV1 #W2 #HWV2 #HW12 - elim (IHT12 … HUT1) -IHT12 HUT1 #U2 #HUT2 #HU12 - elim (tps_inv_lift1_le … HT20 … HUT2 ?) -HT20 HUT2 // [3: /2 width=5/ |2: skip ] #U0 #HU20 #HUT0 - @ex2_1_intro [2: /2/ |1: skip |3: /2/ ] (**) (* /3 width=5/ is slow *) + elim (lift_inv_bind2 … HX) -HX #W1 #U1 #HWV1 #HUT1 #HX destruct + elim (IHV12 … HWV1) -V1 #W2 #HWV2 #HW12 + elim (IHT12 … HUT1) -T1 #U2 #HUT2 #HU12 + elim (tps_inv_lift1_le … HT20 … HUT2 ?) -T2 // [3: /2 width=5/ |2: skip ] #U0 #HU20 #HUT0 + @ex2_1_intro [2: /2 width=2/ |1: skip |3: /2 width=3/ ] (**) (* /3 width=5/ is slow *) | #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV12 #IHW12 #IHT12 #d #e #X #HX - elim (lift_inv_flat2 … HX) -HX #V0 #Y #HV01 #HY #HX destruct -X; - elim (lift_inv_bind2 … HY) -HY #W0 #T0 #HW01 #HT01 #HY destruct -Y; - elim (IHV12 … HV01) -IHV12 HV01 #V3 #HV32 #HV03 - elim (IHW12 … HW01) -IHW12 HW01 #W3 #HW32 #HW03 - elim (IHT12 … HT01) -IHT12 HT01 #T3 #HT32 #HT03 - elim (lift_trans_le … HV32 … HV2 ?) -HV32 HV2 V2 // #V2 #HV32 #HV2 - @ex2_1_intro [2: /3/ |1: skip |3: /2/ ] (**) (* /4 width=5/ is slow *) + elim (lift_inv_flat2 … HX) -HX #V0 #Y #HV01 #HY #HX destruct + elim (lift_inv_bind2 … HY) -HY #W0 #T0 #HW01 #HT01 #HY destruct + elim (IHV12 … HV01) -V1 #V3 #HV32 #HV03 + elim (IHW12 … HW01) -W1 #W3 #HW32 #HW03 + elim (IHT12 … HT01) -T1 #T3 #HT32 #HT03 + elim (lift_trans_le … HV32 … HV2 ?) -V2 // #V2 #HV32 #HV2 + @ex2_1_intro [2: /3 width=2/ |1: skip |3: /2 width=3/ ] (**) (* /4 width=5/ is slow *) | #V #T #T1 #T2 #HT1 #_ #IHT12 #d #e #X #HX - elim (lift_inv_bind2 … HX) -HX #V0 #T0 #_ #HT0 #H destruct -X; - elim (lift_div_le … HT1 … HT0 ?) -HT1 HT0 T // #T #HT0 #HT1 - elim (IHT12 … HT1) -IHT12 HT1 /3 width=5/ + elim (lift_inv_bind2 … HX) -HX #V0 #T0 #_ #HT0 #H destruct + elim (lift_div_le … HT1 … HT0 ?) -T // #T #HT0 #HT1 + elim (IHT12 … HT1) -T1 /3 width=5/ | #V #T1 #T2 #_ #IHT12 #d #e #X #HX - elim (lift_inv_flat2 … HX) -HX #V0 #T0 #_ #HT01 #H destruct -X; - elim (IHT12 … HT01) -IHT12 HT01 /3/ + elim (lift_inv_flat2 … HX) -HX #V0 #T0 #_ #HT01 #H destruct + elim (IHT12 … HT01) -T1 /3 width=3/ ] qed. @@ -103,12 +103,12 @@ qed. fact tpr_inv_abst1_aux: ∀U1,U2. U1 ⇒ U2 → ∀V1,T1. U1 = 𝕔{Abst} V1. T1 → ∃∃V2,T2. V1 ⇒ V2 & T1 ⇒ T2 & U2 = 𝕔{Abst} V2. T2. -#U1 #U2 * -U1 U2 +#U1 #U2 * -U1 -U2 [ #I #V #T #H destruct | #I #V1 #V2 #T1 #T2 #_ #_ #V #T #H destruct | #V1 #V2 #W #T1 #T2 #_ #_ #V #T #H destruct -| #I #V1 #V2 #T1 #T2 #T #HV12 #HT12 #HT2 #V0 #T0 #H destruct -I V1 T1; - <(tps_inv_refl_SO2 … HT2 ? ? ?) -HT2 T /2 width=5/ +| #I #V1 #V2 #T1 #T2 #T #HV12 #HT12 #HT2 #V0 #T0 #H destruct + <(tps_inv_refl_SO2 … HT2 ? ? ?) -T /2 width=5/ | #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #V0 #T0 #H destruct | #V #T #T1 #T2 #_ #_ #V0 #T0 #H destruct | #V #T1 #T2 #_ #V0 #T0 #H destruct @@ -118,4 +118,4 @@ qed. (* Basic_1: was pr0_gen_abst *) lemma tpr_inv_abst1: ∀V1,T1,U2. 𝕔{Abst} V1. T1 ⇒ U2 → ∃∃V2,T2. V1 ⇒ V2 & T1 ⇒ T2 & U2 = 𝕔{Abst} V2. T2. -/2/ qed-. +/2 width=3/ qed-. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tpr_tpr.ma b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tpr_tpr.ma index 4217ced9a..332575c21 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tpr_tpr.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tpr_tpr.ma @@ -19,7 +19,7 @@ include "Basic_2/reducibility/tpr_tpss.ma". (* Confluence lemmas ********************************************************) fact tpr_conf_atom_atom: ∀I. ∃∃X. 𝕒{I} ⇒ X & 𝕒{I} ⇒ X. -/2/ qed. +/2 width=3/ qed. fact tpr_conf_flat_flat: ∀I,V0,V1,T0,T1,V2,T2. ( @@ -30,8 +30,8 @@ fact tpr_conf_flat_flat: V0 ⇒ V1 → V0 ⇒ V2 → T0 ⇒ T1 → T0 ⇒ T2 → ∃∃T0. 𝕗{I} V1. T1 ⇒ T0 & 𝕗{I} V2. T2 ⇒ T0. #I #V0 #V1 #T0 #T1 #V2 #T2 #IH #HV01 #HV02 #HT01 #HT02 -elim (IH … HV01 … HV02) -HV01 HV02 // #V #HV1 #HV2 -elim (IH … HT01 … HT02) -HT01 HT02 /3 width=5/ +elim (IH … HV01 … HV02) -HV01 -HV02 // #V #HV1 #HV2 +elim (IH … HT01 … HT02) -HT01 -HT02 -IH // /3 width=5/ qed. fact tpr_conf_flat_beta: @@ -44,9 +44,9 @@ fact tpr_conf_flat_beta: U0 ⇒ T2 → 𝕔{Abst} W0. U0 ⇒ T1 → ∃∃X. 𝕔{Appl} V1. T1 ⇒ X & 𝕔{Abbr} V2. T2 ⇒ X. #V0 #V1 #T1 #V2 #W0 #U0 #T2 #IH #HV01 #HV02 #HT02 #H -elim (tpr_inv_abst1 … H) -H #W1 #U1 #HW01 #HU01 #H destruct -T1; -elim (IH … HV01 … HV02) -HV01 HV02 // #V #HV1 #HV2 -elim (IH … HT02 … HU01) -HT02 HU01 IH /3 width=5/ +elim (tpr_inv_abst1 … H) -H #W1 #U1 #HW01 #HU01 #H destruct +elim (IH … HV01 … HV02) -HV01 -HV02 // #V #HV1 #HV2 +elim (IH … HT02 … HU01) -HT02 -HU01 -IH // /3 width=5/ qed. (* basic-1: was: @@ -63,25 +63,25 @@ fact tpr_conf_flat_theta: W0 ⇒ W2 → U0 ⇒ U2 → 𝕔{Abbr} W0. U0 ⇒ T1 → ∃∃X. 𝕔{Appl} V1. T1 ⇒ X & 𝕔{Abbr} W2. 𝕔{Appl} V. U2 ⇒ X. #V0 #V1 #T1 #V2 #V #W0 #W2 #U0 #U2 #IH #HV01 #HV02 #HV2 #HW02 #HU02 #H -elim (IH … HV01 … HV02) -HV01 HV02 // #VV #HVV1 #HVV2 +elim (IH … HV01 … HV02) -HV01 -HV02 // #VV #HVV1 #HVV2 elim (lift_total VV 0 1) #VVV #HVV lapply (tpr_lift … HVV2 … HV2 … HVV) #HVVV elim (tpr_inv_abbr1 … H) -H * (* case 1: delta *) -[ -HV2 HVV2 #WW2 #UU2 #UU #HWW2 #HUU02 #HUU2 #H destruct -T1; - elim (IH … HW02 … HWW2) -HW02 HWW2 // #W #HW02 #HWW2 - elim (IH … HU02 … HUU02) -HU02 HUU02 IH // #U #HU2 #HUUU2 - elim (tpr_tps_bind … HWW2 HUUU2 … HUU2) -HUU2 HUUU2 #UUU #HUUU2 #HUUU1 +[ -HV2 -HVV2 #WW2 #UU2 #UU #HWW2 #HUU02 #HUU2 #H destruct + elim (IH … HW02 … HWW2) -HW02 -HWW2 // #W #HW02 #HWW2 + elim (IH … HU02 … HUU02) -HU02 -HUU02 -IH // #U #HU2 #HUUU2 + elim (tpr_tps_bind … HWW2 HUUU2 … HUU2) -UU2 #UUU #HUUU2 #HUUU1 @ex2_1_intro [2: @tpr_theta [6: @HVV |7: @HWW2 |8: @HUUU2 |1,2,3,4: skip | // ] |1:skip |3: @tpr_delta [3: @tpr_flat |1: skip ] /2 width=5/ ] (**) (* /5 width=14/ is too slow *) (* case 3: zeta *) -| -HW02 HVV HVVV #UU1 #HUU10 #HUUT1 +| -HW02 -HVV -HVVV #UU1 #HUU10 #HUUT1 elim (tpr_inv_lift … HU02 … HUU10) -HU02 #UU #HUU2 #HUU1 lapply (tw_lift … HUU10) -HUU10 #HUU10 - elim (IH … HUUT1 … HUU1) -HUUT1 HUU1 IH // -HUU10 #U #HU2 #HUUU2 + elim (IH … HUUT1 … HUU1) -HUUT1 -HUU1 -IH // -HUU10 #U #HU2 #HUUU2 @ex2_1_intro [2: @tpr_flat |1: skip @@ -99,7 +99,7 @@ fact tpr_conf_flat_cast: V0 ⇒ V1 → T0 ⇒ T1 → T0 ⇒ X2 → ∃∃X. 𝕔{Cast} V1. T1 ⇒ X & X2 ⇒ X. #X2 #V0 #V1 #T0 #T1 #IH #_ #HT01 #HT02 -elim (IH … HT01 … HT02) -HT01 HT02 IH /3/ +elim (IH … HT01 … HT02) -HT01 -HT02 -IH // /3 width=3/ qed. fact tpr_conf_beta_beta: @@ -111,8 +111,8 @@ fact tpr_conf_beta_beta: V0 ⇒ V1 → V0 ⇒ V2 → T0 ⇒ T1 → T0 ⇒ T2 → ∃∃X. 𝕔{Abbr} V1. T1 ⇒X & 𝕔{Abbr} V2. T2 ⇒ X. #W0 #V0 #V1 #T0 #T1 #V2 #T2 #IH #HV01 #HV02 #HT01 #HT02 -elim (IH … HV01 … HV02) -HV01 HV02 // -elim (IH … HT01 … HT02) -HT01 HT02 IH /3 width=5/ +elim (IH … HV01 … HV02) -HV01 -HV02 // +elim (IH … HT01 … HT02) -HT01 -HT02 -IH // /3 width=5/ qed. (* Basic_1: was: pr0_cong_delta pr0_delta_delta *) @@ -127,11 +127,11 @@ fact tpr_conf_delta_delta: ⋆. 𝕓{I1} V2 ⊢ T2 [O, 1] ≫ TT2 → ∃∃X. 𝕓{I1} V1. TT1 ⇒ X & 𝕓{I1} V2. TT2 ⇒ X. #I1 #V0 #V1 #T0 #T1 #TT1 #V2 #T2 #TT2 #IH #HV01 #HV02 #HT01 #HT02 #HTT1 #HTT2 -elim (IH … HV01 … HV02) -HV01 HV02 // #V #HV1 #HV2 -elim (IH … HT01 … HT02) -HT01 HT02 IH // #T #HT1 #HT2 -elim (tpr_tps_bind … HV1 HT1 … HTT1) -HT1 HTT1 #U1 #TTU1 #HTU1 -elim (tpr_tps_bind … HV2 HT2 … HTT2) -HT2 HTT2 #U2 #TTU2 #HTU2 -elim (tps_conf_eq … HTU1 … HTU2) -HTU1 HTU2 #U #HU1 #HU2 +elim (IH … HV01 … HV02) -HV01 -HV02 // #V #HV1 #HV2 +elim (IH … HT01 … HT02) -HT01 -HT02 -IH // #T #HT1 #HT2 +elim (tpr_tps_bind … HV1 HT1 … HTT1) -T1 #U1 #TTU1 #HTU1 +elim (tpr_tps_bind … HV2 HT2 … HTT2) -T2 #U2 #TTU2 #HTU2 +elim (tps_conf_eq … HTU1 … HTU2) -T #U #HU1 #HU2 @ex2_1_intro [2,3: @tpr_delta |1: skip ] /width=10/ (**) (* /3 width=10/ is too slow *) qed. @@ -146,9 +146,9 @@ fact tpr_conf_delta_zeta: ∃∃X. 𝕓{Abbr} V1. TT1 ⇒ X & X2 ⇒ X. #X2 #V0 #V1 #T0 #T1 #TT1 #T2 #IH #_ #HT01 #HTT1 #HTX2 #HTT20 elim (tpr_inv_lift … HT01 … HTT20) -HT01 #TT2 #HTT21 #HTT2 -lapply (tps_inv_lift1_eq … HTT1 … HTT21) -HTT1 #HTT1 destruct -T1; +lapply (tps_inv_lift1_eq … HTT1 … HTT21) -HTT1 #HTT1 destruct lapply (tw_lift … HTT20) -HTT20 #HTT20 -elim (IH … HTX2 … HTT2) -HTX2 HTT2 IH /3/ +elim (IH … HTX2 … HTT2) -HTX2 -HTT2 -IH // /3 width=3/ qed. (* Basic_1: was: pr0_upsilon_upsilon *) @@ -162,12 +162,12 @@ fact tpr_conf_theta_theta: ↑[O, 1] V1 ≡ VV1 → ↑[O, 1] V2 ≡ VV2 → ∃∃X. 𝕔{Abbr} W1. 𝕔{Appl} VV1. T1 ⇒ X & 𝕔{Abbr} W2. 𝕔{Appl} VV2. T2 ⇒ X. #VV1 #V0 #V1 #W0 #W1 #T0 #T1 #V2 #VV2 #W2 #T2 #IH #HV01 #HV02 #HW01 #HW02 #HT01 #HT02 #HVV1 #HVV2 -elim (IH … HV01 … HV02) -HV01 HV02 // #V #HV1 #HV2 -elim (IH … HW01 … HW02) -HW01 HW02 // #W #HW1 #HW2 -elim (IH … HT01 … HT02) -HT01 HT02 IH // #T #HT1 #HT2 +elim (IH … HV01 … HV02) -HV01 -HV02 // #V #HV1 #HV2 +elim (IH … HW01 … HW02) -HW01 -HW02 // #W #HW1 #HW2 +elim (IH … HT01 … HT02) -HT01 -HT02 -IH // #T #HT1 #HT2 elim (lift_total V 0 1) #VV #HVV -lapply (tpr_lift … HV1 … HVV1 … HVV) -HV1 HVV1 #HVV1 -lapply (tpr_lift … HV2 … HVV2 … HVV) -HV2 HVV2 HVV #HVV2 +lapply (tpr_lift … HV1 … HVV1 … HVV) -V1 #HVV1 +lapply (tpr_lift … HV2 … HVV2 … HVV) -V2 -HVV #HVV2 @ex2_1_intro [2,3: @tpr_bind |1:skip ] /2 width=5/ (**) (* /4 width=5/ is too slow *) qed. @@ -181,9 +181,9 @@ fact tpr_conf_zeta_zeta: ↑[O, 1] T0 ≡ TT0 → ↑[O, 1] T2 ≡ TT0 → ∃∃X. T1 ⇒ X & X2 ⇒ X. #V0 #X2 #TT0 #T0 #T1 #T2 #IH #HT01 #HTX2 #HTT0 #HTT20 -lapply (lift_inj … HTT0 … HTT20) -HTT0 #H destruct -T0; +lapply (lift_inj … HTT0 … HTT20) -HTT0 #H destruct lapply (tw_lift … HTT20) -HTT20 #HTT20 -elim (IH … HT01 … HTX2) -HT01 HTX2 IH /2/ +elim (IH … HT01 … HTX2) -HT01 -HTX2 -IH // /2 width=3/ qed. fact tpr_conf_tau_tau: @@ -195,7 +195,7 @@ fact tpr_conf_tau_tau: T0 ⇒ T1 → T0 ⇒ X2 → ∃∃X. T1 ⇒ X & X2 ⇒ X. #V0 #T0 #X2 #T1 #IH #HT01 #HT02 -elim (IH … HT01 … HT02) -HT01 HT02 IH /2/ +elim (IH … HT01 … HT02) -HT01 -HT02 -IH // /2 width=3/ qed. (* Confluence ***************************************************************) @@ -208,70 +208,70 @@ fact tpr_conf_aux: ) → ∀X0,X1,X2. X0 ⇒ X1 → X0 ⇒ X2 → X0 = Y0 → ∃∃X. X1 ⇒ X & X2 ⇒ X. -#Y0 #IH #X0 #X1 #X2 * -X0 X1 -[ #I1 #H1 #H2 destruct -Y0; +#Y0 #IH #X0 #X1 #X2 * -X0 -X1 +[ #I1 #H1 #H2 destruct lapply (tpr_inv_atom1 … H1) -H1 (* case 1: atom, atom *) - #H1 destruct -X2 // -| #I #V0 #V1 #T0 #T1 #HV01 #HT01 #H1 #H2 destruct -Y0; + #H1 destruct // +| #I #V0 #V1 #T0 #T1 #HV01 #HT01 #H1 #H2 destruct elim (tpr_inv_flat1 … H1) -H1 * (* case 2: flat, flat *) - [ #V2 #T2 #HV02 #HT02 #H destruct -X2 + [ #V2 #T2 #HV02 #HT02 #H destruct /3 width=7 by tpr_conf_flat_flat/ (**) (* /3 width=7/ is too slow *) (* case 3: flat, beta *) - | #V2 #W #U0 #T2 #HV02 #HT02 #H1 #H2 #H3 destruct -T0 X2 I + | #V2 #W #U0 #T2 #HV02 #HT02 #H1 #H2 #H3 destruct /3 width=8 by tpr_conf_flat_beta/ (**) (* /3 width=8/ is too slow *) (* case 4: flat, theta *) - | #V2 #V #W0 #W2 #U0 #U2 #HV02 #HW02 #HT02 #HV2 #H1 #H2 #H3 destruct -T0 X2 I + | #V2 #V #W0 #W2 #U0 #U2 #HV02 #HW02 #HT02 #HV2 #H1 #H2 #H3 destruct /3 width=11 by tpr_conf_flat_theta/ (**) (* /3 width=11/ is too slow *) (* case 5: flat, tau *) - | #HT02 #H destruct -I + | #HT02 #H destruct /3 width=6 by tpr_conf_flat_cast/ (**) (* /3 width=6/ is too slow *) ] -| #V0 #V1 #W0 #T0 #T1 #HV01 #HT01 #H1 #H2 destruct -Y0; +| #V0 #V1 #W0 #T0 #T1 #HV01 #HT01 #H1 #H2 destruct elim (tpr_inv_appl1 … H1) -H1 * (* case 6: beta, flat (repeated) *) - [ #V2 #T2 #HV02 #HT02 #H destruct -X2 + [ #V2 #T2 #HV02 #HT02 #H destruct @ex2_1_comm /3 width=8 by tpr_conf_flat_beta/ (* case 7: beta, beta *) - | #V2 #WW0 #TT0 #T2 #HV02 #HT02 #H1 #H2 destruct -W0 T0 X2 + | #V2 #WW0 #TT0 #T2 #HV02 #HT02 #H1 #H2 destruct /3 width=8 by tpr_conf_beta_beta/ (**) (* /3 width=8/ is too slow *) (* case 8, beta, theta (excluded) *) | #V2 #VV2 #WW0 #W2 #TT0 #T2 #_ #_ #_ #_ #H destruct ] -| #I1 #V0 #V1 #T0 #T1 #TT1 #HV01 #HT01 #HTT1 #H1 #H2 destruct -Y0; +| #I1 #V0 #V1 #T0 #T1 #TT1 #HV01 #HT01 #HTT1 #H1 #H2 destruct elim (tpr_inv_bind1 … H1) -H1 * (* case 9: delta, delta *) - [ #V2 #T2 #TT2 #HV02 #HT02 #HTT2 #H destruct -X2 + [ #V2 #T2 #TT2 #HV02 #HT02 #HTT2 #H destruct /3 width=11 by tpr_conf_delta_delta/ (**) (* /3 width=11/ is too slow *) (* case 10: delta, zata *) - | #T2 #HT20 #HTX2 #H destruct -I1; + | #T2 #HT20 #HTX2 #H destruct /3 width=10 by tpr_conf_delta_zeta/ (**) (* /3 width=10/ is too slow *) ] -| #VV1 #V0 #V1 #W0 #W1 #T0 #T1 #HV01 #HVV1 #HW01 #HT01 #H1 #H2 destruct -Y0; +| #VV1 #V0 #V1 #W0 #W1 #T0 #T1 #HV01 #HVV1 #HW01 #HT01 #H1 #H2 destruct elim (tpr_inv_appl1 … H1) -H1 * (* case 11: theta, flat (repeated) *) - [ #V2 #T2 #HV02 #HT02 #H destruct -X2 + [ #V2 #T2 #HV02 #HT02 #H destruct @ex2_1_comm /3 width=11 by tpr_conf_flat_theta/ (* case 12: theta, beta (repeated) *) | #V2 #WW0 #TT0 #T2 #_ #_ #H destruct (* case 13: theta, theta *) - | #V2 #VV2 #WW0 #W2 #TT0 #T2 #V02 #HW02 #HT02 #HVV2 #H1 #H2 destruct -W0 T0 X2 + | #V2 #VV2 #WW0 #W2 #TT0 #T2 #V02 #HW02 #HT02 #HVV2 #H1 #H2 destruct /3 width=14 by tpr_conf_theta_theta/ (**) (* /3 width=14/ is too slow *) ] -| #V0 #TT0 #T0 #T1 #HTT0 #HT01 #H1 #H2 destruct -Y0; +| #V0 #TT0 #T0 #T1 #HTT0 #HT01 #H1 #H2 destruct elim (tpr_inv_abbr1 … H1) -H1 * (* case 14: zeta, delta (repeated) *) - [ #V2 #T2 #TT2 #HV02 #HT02 #HTT2 #H destruct -X2 + [ #V2 #T2 #TT2 #HV02 #HT02 #HTT2 #H destruct @ex2_1_comm /3 width=10 by tpr_conf_delta_zeta/ (* case 15: zeta, zeta *) | #T2 #HTT20 #HTX2 /3 width=9 by tpr_conf_zeta_zeta/ (**) (* /3 width=9/ is too slow *) ] -| #V0 #T0 #T1 #HT01 #H1 #H2 destruct -Y0; +| #V0 #T0 #T1 #HT01 #H1 #H2 destruct elim (tpr_inv_cast1 … H1) -H1 (* case 16: tau, flat (repeated) *) - [ * #V2 #T2 #HV02 #HT02 #H destruct -X2 + [ * #V2 #T2 #HV02 #HT02 #H destruct @ex2_1_comm /3 width=6 by tpr_conf_flat_cast/ (* case 17: tau, tau *) | #HT02 diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tpr_tpss.ma b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tpr_tpss.ma index f640d1326..e043031bd 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tpr_tpss.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tpr_tpss.ma @@ -24,54 +24,54 @@ lemma tpr_tps_ltpr: ∀T1,T2. T1 ⇒ T2 → ∀L1,d,e,U1. L1 ⊢ T1 [d, e] ≫ U1 → ∀L2. L1 ⇒ L2 → ∃∃U2. U1 ⇒ U2 & L2 ⊢ T2 [d, e] ≫* U2. -#T1 #T2 #H elim H -H T1 T2 +#T1 #T2 #H elim H -T1 -T2 [ #I #L1 #d #e #X #H elim (tps_inv_atom1 … H) -H - [ #H destruct -X /2/ - | * #K1 #V1 #i #Hdi #Hide #HLK1 #HVU1 #H #L2 #HL12 destruct -I; - elim (ltpr_ldrop_conf … HLK1 … HL12) -HLK1 HL12 #X #HLK2 #H - elim (ltpr_inv_pair1 … H) -H #K2 #V2 #_ #HV12 #H destruct -X; + [ #H destruct /2 width=3/ + | * #K1 #V1 #i #Hdi #Hide #HLK1 #HVU1 #H #L2 #HL12 destruct + elim (ltpr_ldrop_conf … HLK1 … HL12) -L1 #X #HLK2 #H + elim (ltpr_inv_pair1 … H) -H #K2 #V2 #_ #HV12 #H destruct elim (lift_total V2 0 (i+1)) #U2 #HVU2 - lapply (tpr_lift … HV12 … HVU1 … HVU2) -HV12 HVU1 #HU12 - @ex2_1_intro [2: @HU12 | skip | /3/ ] (**) (* /4 width=6/ is too slow *) + lapply (tpr_lift … HV12 … HVU1 … HVU2) -V1 #HU12 + @ex2_1_intro [2: @HU12 | skip | /3 width=4/ ] (**) (* /4 width=6/ is too slow *) ] | #I #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L1 #d #e #X #H #L2 #HL12 - elim (tps_inv_flat1 … H) -H #W1 #U1 #HVW1 #HTU1 #H destruct -X; - elim (IHV12 … HVW1 … HL12) -IHV12 HVW1; - elim (IHT12 … HTU1 … HL12) -IHT12 HTU1 HL12 /3 width=5/ + elim (tps_inv_flat1 … H) -H #W1 #U1 #HVW1 #HTU1 #H destruct + elim (IHV12 … HVW1 … HL12) -V1 + elim (IHT12 … HTU1 … HL12) -T1 -HL12 /3 width=5/ | #V1 #V2 #W #T1 #T2 #_ #_ #IHV12 #IHT12 #L1 #d #e #X #H #L2 #HL12 - elim (tps_inv_flat1 … H) -H #VV1 #Y #HVV1 #HY #HX destruct -X; - elim (tps_inv_bind1 … HY) -HY #WW #TT1 #_ #HTT1 #H destruct -Y; - elim (IHV12 … HVV1 … HL12) -IHV12 HVV1 #VV2 #HVV12 #HVV2 - elim (IHT12 … HTT1 (L2. 𝕓{Abst} WW) ?) -IHT12 HTT1 /2/ -HL12 #TT2 #HTT12 #HTT2 + elim (tps_inv_flat1 … H) -H #VV1 #Y #HVV1 #HY #HX destruct + elim (tps_inv_bind1 … HY) -HY #WW #TT1 #_ #HTT1 #H destruct + elim (IHV12 … HVV1 … HL12) -V1 #VV2 #HVV12 #HVV2 + elim (IHT12 … HTT1 (L2. 𝕓{Abst} WW) ?) -T1 /2 width=1/ -HL12 #TT2 #HTT12 #HTT2 lapply (tpss_lsubs_conf … HTT2 (L2. 𝕓{Abbr} VV2) ?) -HTT2 /3 width=5/ | #I #V1 #V2 #T1 #T2 #U2 #HV12 #_ #HTU2 #IHV12 #IHT12 #L1 #d #e #X #H #L2 #HL12 - elim (tps_inv_bind1 … H) -H #VV1 #TT1 #HVV1 #HTT1 #H destruct -X; - elim (IHV12 … HVV1 … HL12) -IHV12 HVV1 #VV2 #HVV12 #HVV2 - elim (IHT12 … HTT1 (L2. 𝕓{I} VV2) ?) -IHT12 HTT1 /2/ -HL12 #TT2 #HTT12 #HTT2 - elim (tpss_strip_neq … HTT2 … HTU2 ?) -HTT2 HTU2 T2 /2/ #T2 #HTT2 #HUT2 - lapply (tps_lsubs_conf … HTT2 (L2. 𝕓{I} V2) ?) -HTT2 /2/ #HTT2 - elim (ltpss_tps_conf … HTT2 (L2. 𝕓{I} VV2) (d + 1) e ?) -HTT2 /2/ #W2 #HTTW2 #HTW2 - lapply (tpss_lsubs_conf … HTTW2 (⋆. 𝕓{I} VV2) ?) -HTTW2 /2/ #HTTW2 + elim (tps_inv_bind1 … H) -H #VV1 #TT1 #HVV1 #HTT1 #H destruct + elim (IHV12 … HVV1 … HL12) -V1 #VV2 #HVV12 #HVV2 + elim (IHT12 … HTT1 (L2. 𝕓{I} VV2) ?) -T1 /2 width=1/ -HL12 #TT2 #HTT12 #HTT2 + elim (tpss_strip_neq … HTT2 … HTU2 ?) -T2 /2 width=1/ #T2 #HTT2 #HUT2 + lapply (tps_lsubs_conf … HTT2 (L2. 𝕓{I} V2) ?) -HTT2 /2 width=1/ #HTT2 + elim (ltpss_tps_conf … HTT2 (L2. 𝕓{I} VV2) (d + 1) e ?) -HTT2 /2 width=1/ #W2 #HTTW2 #HTW2 + lapply (tpss_lsubs_conf … HTTW2 (⋆. 𝕓{I} VV2) ?) -HTTW2 /2 width=1/ #HTTW2 lapply (tpss_tps … HTTW2) -HTTW2 #HTTW2 - lapply (tpss_lsubs_conf … HTW2 (L2. 𝕓{I} VV2) ?) -HTW2 /2/ #HTW2 - lapply (tpss_trans_eq … HUT2 … HTW2) -HUT2 HTW2 /3 width=5/ + lapply (tpss_lsubs_conf … HTW2 (L2. 𝕓{I} VV2) ?) -HTW2 /2 width=1/ #HTW2 + lapply (tpss_trans_eq … HUT2 … HTW2) -T2 /3 width=5/ | #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV12 #IHW12 #IHT12 #L1 #d #e #X #H #L2 #HL12 - elim (tps_inv_flat1 … H) -H #VV1 #Y #HVV1 #HY #HX destruct -X; - elim (tps_inv_bind1 … HY) -HY #WW1 #TT1 #HWW1 #HTT1 #H destruct -Y; - elim (IHV12 … HVV1 … HL12) -IHV12 HVV1 #VV2 #HVV12 #HVV2 - elim (IHW12 … HWW1 … HL12) -IHW12 HWW1 #WW2 #HWW12 #HWW2 - elim (IHT12 … HTT1 (L2. 𝕓{Abbr} WW2) ?) -IHT12 HTT1 /2/ -HL12 #TT2 #HTT12 #HTT2 + elim (tps_inv_flat1 … H) -H #VV1 #Y #HVV1 #HY #HX destruct + elim (tps_inv_bind1 … HY) -HY #WW1 #TT1 #HWW1 #HTT1 #H destruct + elim (IHV12 … HVV1 … HL12) -V1 #VV2 #HVV12 #HVV2 + elim (IHW12 … HWW1 … HL12) -W1 #WW2 #HWW12 #HWW2 + elim (IHT12 … HTT1 (L2. 𝕓{Abbr} WW2) ?) -T1 /2 width=1/ -HL12 #TT2 #HTT12 #HTT2 elim (lift_total VV2 0 1) #VV #H2VV - lapply (tpss_lift_ge … HVV2 (L2. 𝕓{Abbr} WW2) … HV2 … H2VV) -HVV2 HV2 /2/ #HVV + lapply (tpss_lift_ge … HVV2 (L2. 𝕓{Abbr} WW2) … HV2 … H2VV) -V2 /2 width=1/ #HVV @ex2_1_intro [2: @tpr_theta |1: skip |3: @tpss_bind [2: @tpss_flat ] ] /width=11/ (**) (* /4 width=11/ is too slow *) -| #V1 #TT1 #T1 #T2 #HT1 #_ #IHT12 #L1 #d #e #X #H #L2 #HL12 - elim (tps_inv_bind1 … H) -H #V2 #TT2 #HV12 #HTT12 #H destruct -X; - elim (tps_inv_lift1_ge … HTT12 L1 … HT1 ?) -HTT12 HT1 /2/ #T2 #HT12 #HTT2 - elim (IHT12 … HT12 … HL12) -IHT12 HT12 HL12