X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fstatic_2%2Fstatic%2Frdeq_fqus.ma;h=bbd8a38212232c4a918cbf637c0a23bbb140f37a;hp=66fd1b7536a2aeb51a76d839e196394522a2eeb3;hb=f308429a0fde273605a2330efc63268b4ac36c99;hpb=87f57ddc367303c33e19c83cd8989cd561f3185b diff --git a/matita/matita/contribs/lambdadelta/static_2/static/rdeq_fqus.ma b/matita/matita/contribs/lambdadelta/static_2/static/rdeq_fqus.ma index 66fd1b753..bbd8a3821 100644 --- a/matita/matita/contribs/lambdadelta/static_2/static/rdeq_fqus.ma +++ b/matita/matita/contribs/lambdadelta/static_2/static/rdeq_fqus.ma @@ -21,9 +21,9 @@ include "static_2/static/rdeq_rdeq.ma". (* Properties with extended structural successor for closures ***************) -lemma fqu_tdeq_conf: ∀b,G1,G2,L1,L2,U1,T1. ⦃G1, L1, U1⦄ ⊐[b] ⦃G2, L2, T1⦄ → +lemma fqu_tdeq_conf: ∀b,G1,G2,L1,L2,U1,T1. ⦃G1,L1,U1⦄ ⊐[b] ⦃G2,L2,T1⦄ → ∀U2. U1 ≛ U2 → - ∃∃L,T2. ⦃G1, L1, U2⦄ ⊐[b] ⦃G2, L, T2⦄ & L2 ≛[T1] L & T1 ≛ T2. + ∃∃L,T2. ⦃G1,L1,U2⦄ ⊐[b] ⦃G2,L,T2⦄ & L2 ≛[T1] L & T1 ≛ T2. #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/ @@ -45,18 +45,18 @@ lemma fqu_tdeq_conf: ∀b,G1,G2,L1,L2,U1,T1. ⦃G1, L1, U1⦄ ⊐[b] ⦃G2, L2, ] qed-. -lemma tdeq_fqu_trans: ∀b,G1,G2,L1,L2,U1,T1. ⦃G1, L1, U1⦄ ⊐[b] ⦃G2, L2, T1⦄ → +lemma tdeq_fqu_trans: ∀b,G1,G2,L1,L2,U1,T1. ⦃G1,L1,U1⦄ ⊐[b] ⦃G2,L2,T1⦄ → ∀U2. U2 ≛ U1 → - ∃∃L,T2. ⦃G1, L1, U2⦄ ⊐[b] ⦃G2, L, T2⦄ & T2 ≛ T1 & L ≛[T1] L2. + ∃∃L,T2. ⦃G1,L1,U2⦄ ⊐[b] ⦃G2,L,T2⦄ & T2 ≛ T1 & L ≛[T1] L2. #b #G1 #G2 #L1 #L2 #U1 #T1 #H12 #U2 #HU21 elim (fqu_tdeq_conf … H12 U2) -H12 /3 width=5 by rdeq_sym, tdeq_sym, ex3_2_intro/ qed-. (* Basic_2A1: uses: lleq_fqu_trans *) -lemma rdeq_fqu_trans: ∀b,G1,G2,L2,K2,T,U. ⦃G1, L2, T⦄ ⊐[b] ⦃G2, K2, U⦄ → +lemma rdeq_fqu_trans: ∀b,G1,G2,L2,K2,T,U. ⦃G1,L2,T⦄ ⊐[b] ⦃G2,K2,U⦄ → ∀L1. L1 ≛[T] L2 → - ∃∃K1,U0. ⦃G1, L1, T⦄ ⊐[b] ⦃G2, K1, U0⦄ & U0 ≛ U & K1 ≛[U] K2. + ∃∃K1,U0. ⦃G1,L1,T⦄ ⊐[b] ⦃G2,K1,U0⦄ & U0 ≛ U & K1 ≛[U] K2. #b #G1 #G2 #L2 #K2 #T #U #H elim H -G1 -G2 -L2 -K2 -T -U [ #I #G #L2 #V2 #L1 #H elim (rdeq_inv_zero_pair_dx … H) -H #K1 #V1 #HV1 #HV12 #H destruct @@ -80,9 +80,9 @@ qed-. (* Properties with optional structural successor for closures ***************) -lemma tdeq_fquq_trans: ∀b,G1,G2,L1,L2,U1,T1. ⦃G1, L1, U1⦄ ⊐⸮[b] ⦃G2, L2, T1⦄ → +lemma tdeq_fquq_trans: ∀b,G1,G2,L1,L2,U1,T1. ⦃G1,L1,U1⦄ ⊐⸮[b] ⦃G2,L2,T1⦄ → ∀U2. U2 ≛ U1 → - ∃∃L,T2. ⦃G1, L1, U2⦄ ⊐⸮[b] ⦃G2, L, T2⦄ & T2 ≛ T1 & L ≛[T1] L2. + ∃∃L,T2. ⦃G1,L1,U2⦄ ⊐⸮[b] ⦃G2,L,T2⦄ & T2 ≛ T1 & L ≛[T1] L2. #b #G1 #G2 #L1 #L2 #U1 #T1 #H elim H -H [ #H #U2 #HU21 elim (tdeq_fqu_trans … H … HU21) -U1 /3 width=5 by fqu_fquq, ex3_2_intro/ @@ -91,9 +91,9 @@ lemma tdeq_fquq_trans: ∀b,G1,G2,L1,L2,U1,T1. ⦃G1, L1, U1⦄ ⊐⸮[b] ⦃G2, qed-. (* Basic_2A1: was just: lleq_fquq_trans *) -lemma rdeq_fquq_trans: ∀b,G1,G2,L2,K2,T,U. ⦃G1, L2, T⦄ ⊐⸮[b] ⦃G2, K2, U⦄ → +lemma rdeq_fquq_trans: ∀b,G1,G2,L2,K2,T,U. ⦃G1,L2,T⦄ ⊐⸮[b] ⦃G2,K2,U⦄ → ∀L1. L1 ≛[T] L2 → - ∃∃K1,U0. ⦃G1, L1, T⦄ ⊐⸮[b] ⦃G2, K1, U0⦄ & U0 ≛ U & K1 ≛[U] K2. + ∃∃K1,U0. ⦃G1,L1,T⦄ ⊐⸮[b] ⦃G2,K1,U0⦄ & U0 ≛ U & K1 ≛[U] K2. #b #G1 #G2 #L2 #K2 #T #U #H elim H -H [ #H #L1 #HL12 elim (rdeq_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/ @@ -103,9 +103,9 @@ qed-. (* Properties with plus-iterated structural successor for closures **********) (* Basic_2A1: was just: lleq_fqup_trans *) -lemma rdeq_fqup_trans: ∀b,G1,G2,L2,K2,T,U. ⦃G1, L2, T⦄ ⊐+[b] ⦃G2, K2, U⦄ → +lemma rdeq_fqup_trans: ∀b,G1,G2,L2,K2,T,U. ⦃G1,L2,T⦄ ⊐+[b] ⦃G2,K2,U⦄ → ∀L1. L1 ≛[T] L2 → - ∃∃K1,U0. ⦃G1, L1, T⦄ ⊐+[b] ⦃G2, K1, U0⦄ & U0 ≛ U & K1 ≛[U] K2. + ∃∃K1,U0. ⦃G1,L1,T⦄ ⊐+[b] ⦃G2,K1,U0⦄ & U0 ≛ U & K1 ≛[U] K2. #b #G1 #G2 #L2 #K2 #T #U #H @(fqup_ind … H) -G2 -K2 -U [ #G2 #K2 #U #HTU #L1 #HL12 elim (rdeq_fqu_trans … HTU … HL12) -L2 /3 width=5 by fqu_fqup, ex3_2_intro/ @@ -118,9 +118,9 @@ lemma rdeq_fqup_trans: ∀b,G1,G2,L2,K2,T,U. ⦃G1, L2, T⦄ ⊐+[b] ⦃G2, K2, ] qed-. -lemma tdeq_fqup_trans: ∀b,G1,G2,L1,L2,U1,T1. ⦃G1, L1, U1⦄ ⊐+[b] ⦃G2, L2, T1⦄ → +lemma tdeq_fqup_trans: ∀b,G1,G2,L1,L2,U1,T1. ⦃G1,L1,U1⦄ ⊐+[b] ⦃G2,L2,T1⦄ → ∀U2. U2 ≛ U1 → - ∃∃L,T2. ⦃G1, L1, U2⦄ ⊐+[b] ⦃G2, L, T2⦄ & T2 ≛ T1 & L ≛[T1] L2. + ∃∃L,T2. ⦃G1,L1,U2⦄ ⊐+[b] ⦃G2,L,T2⦄ & T2 ≛ T1 & L ≛[T1] L2. #b #G1 #G2 #L1 #L2 #U1 #T1 #H @(fqup_ind_dx … H) -G1 -L1 -U1 [ #G1 #L1 #U1 #H #U2 #HU21 elim (tdeq_fqu_trans … H … HU21) -U1 /3 width=5 by fqu_fqup, ex3_2_intro/ @@ -136,9 +136,9 @@ qed-. (* Properties with star-iterated structural successor for closures **********) -lemma tdeq_fqus_trans: ∀b,G1,G2,L1,L2,U1,T1. ⦃G1, L1, U1⦄ ⊐*[b] ⦃G2, L2, T1⦄ → +lemma tdeq_fqus_trans: ∀b,G1,G2,L1,L2,U1,T1. ⦃G1,L1,U1⦄ ⊐*[b] ⦃G2,L2,T1⦄ → ∀U2. U2 ≛ U1 → - ∃∃L,T2. ⦃G1, L1, U2⦄ ⊐*[b] ⦃G2, L, T2⦄ & T2 ≛ T1 & L ≛[T1] L2. + ∃∃L,T2. ⦃G1,L1,U2⦄ ⊐*[b] ⦃G2,L,T2⦄ & T2 ≛ T1 & L ≛[T1] L2. #b #G1 #G2 #L1 #L2 #U1 #T1 #H #U2 #HU21 elim(fqus_inv_fqup … H) -H [ #H elim (tdeq_fqup_trans … H … HU21) -U1 /3 width=5 by fqup_fqus, ex3_2_intro/ | * #HG #HL #HT destruct /2 width=5 by ex3_2_intro/ @@ -146,9 +146,9 @@ lemma tdeq_fqus_trans: ∀b,G1,G2,L1,L2,U1,T1. ⦃G1, L1, U1⦄ ⊐*[b] ⦃G2, L qed-. (* Basic_2A1: was just: lleq_fqus_trans *) -lemma rdeq_fqus_trans: ∀b,G1,G2,L2,K2,T,U. ⦃G1, L2, T⦄ ⊐*[b] ⦃G2, K2, U⦄ → +lemma rdeq_fqus_trans: ∀b,G1,G2,L2,K2,T,U. ⦃G1,L2,T⦄ ⊐*[b] ⦃G2,K2,U⦄ → ∀L1. L1 ≛[T] L2 → - ∃∃K1,U0. ⦃G1, L1, T⦄ ⊐*[b] ⦃G2, K1, U0⦄ & U0 ≛ U & K1 ≛[U] K2. + ∃∃K1,U0. ⦃G1,L1,T⦄ ⊐*[b] ⦃G2,K1,U0⦄ & U0 ≛ U & K1 ≛[U] K2. #b #G1 #G2 #L2 #K2 #T #U #H #L1 #HL12 elim(fqus_inv_fqup … H) -H [ #H elim (rdeq_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/