From b3c3ea1c87cbd7a87c8c29a276fc16f9ebbfb5bd Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sat, 26 Oct 2013 17:47:20 +0000 Subject: [PATCH] - bug fix in the connection between global and restricted big-tree proper computation - one file was not committed :( --- .../basic_2/computation/cpxs_lift.ma | 51 ++++++++++--------- .../lambdadelta/basic_2/computation/fpbg.ma | 19 +------ .../basic_2/computation/fpbg_fpbg.ma | 36 +++++++++++++ .../lambdadelta/basic_2/computation/fpbr.ma | 14 ++--- .../basic_2/computation/fpbr_fpbr.ma | 7 +++ .../basic_2/computation/fpbs_alt.ma | 4 +- .../basic_2/computation/lpxs_cpxs.ma | 2 +- .../lambdadelta/basic_2/reduction/cpx_lift.ma | 21 ++++++++ 8 files changed, 102 insertions(+), 52 deletions(-) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/computation/fpbg_fpbg.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_lift.ma index 8028270d6..0c9cfe1e7 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_lift.ma @@ -71,31 +71,43 @@ qed-. (* Properties on supclosure *************************************************) +lemma fqu_cpxs_trans: ∀h,g,G1,G2,L1,L2,T2,U2. ⦃G2, L2⦄ ⊢ T2 ➡*[h, g] U2 → + ∀T1. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ → + ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] U1 & ⦃G1, L1, U1⦄ ⊃ ⦃G2, L2, U2⦄. +#h #g #G1 #G2 #L1 #L2 #T2 #U2 #H @(cpxs_ind_dx … H) -T2 /2 width=3 by ex2_intro/ +#T #T2 #HT2 #_ #IHTU2 #T1 #HT1 elim (fqu_cpx_trans … HT1 … HT2) -T +#T #HT1 #HT2 elim (IHTU2 … HT2) -T2 /3 width=3 by cpxs_strap2, ex2_intro/ +qed-. + lemma fquq_cpxs_trans: ∀h,g,G1,G2,L1,L2,T2,U2. ⦃G2, L2⦄ ⊢ T2 ➡*[h, g] U2 → ∀T1. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ → - ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] U1 & ⦃G1, L1, U1⦄ ⊃* ⦃G2, L2, U2⦄. -#h #g #G1 #G2 #L1 #L2 #T2 #U2 #H @(cpxs_ind_dx … H) -T2 -[ /3 width=3 by fquq_fqus, ex2_intro/ -| #T #T2 #HT2 #_ #IHTU2 #T1 #HT1 - elim (fquq_cpx_trans … HT1 … HT2) -T #T #HT1 #HT2 - elim (IHTU2 … HT2) -T2 /3 width=3 by cpxs_strap2, ex2_intro/ + ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] U1 & ⦃G1, L1, U1⦄ ⊃⸮ ⦃G2, L2, U2⦄. +#h #g #G1 #G2 #L1 #L2 #T2 #U2 #HTU2 #T1 #H elim (fquq_inv_gen … H) -H +[ #HT12 elim (fqu_cpxs_trans … HTU2 … HT12) /3 width=3 by fqu_fquq, ex2_intro/ +| * #H1 #H2 #H3 destruct /2 width=3 by ex2_intro/ ] qed-. lemma fquq_lsstas_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ → ∀U2,l1. ⦃G2, L2⦄ ⊢ T2 •*[h, g, l1] U2 → ∀l2. ⦃G2, L2⦄ ⊢ T2 ▪ [h, g] l2 → l1 ≤ l2 → - ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] U1 & ⦃G1, L1, U1⦄ ⊃* ⦃G2, L2, U2⦄. + ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] U1 & ⦃G1, L1, U1⦄ ⊃⸮ ⦃G2, L2, U2⦄. /3 width=5 by fquq_cpxs_trans, lsstas_cpxs/ qed-. -lemma fqus_cpxs_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ → - ∀U2. ⦃G2, L2⦄ ⊢ T2 ➡*[h, g] U2 → +lemma fqup_cpxs_trans: ∀h,g,G1,G2,L1,L2,T2,U2. ⦃G2, L2⦄ ⊢ T2 ➡*[h, g] U2 → + ∀T1. ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄ → + ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] U1 & ⦃G1, L1, U1⦄ ⊃+ ⦃G2, L2, U2⦄. +#h #g #G1 #G2 #L1 #L2 #T2 #U2 #H @(cpxs_ind_dx … H) -T2 /2 width=3 by ex2_intro/ +#T #T2 #HT2 #_ #IHTU2 #T1 #HT1 elim (fqup_cpx_trans … HT1 … HT2) -T +#U1 #HTU1 #H2 elim (IHTU2 … H2) -T2 /3 width=3 by cpxs_strap2, ex2_intro/ +qed-. + +lemma fqus_cpxs_trans: ∀h,g,G1,G2,L1,L2,T2,U2. ⦃G2, L2⦄ ⊢ T2 ➡*[h, g] U2 → + ∀T1. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ → ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] U1 & ⦃G1, L1, U1⦄ ⊃* ⦃G2, L2, U2⦄. -#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqus_ind … H) -G2 -L2 -T2 -[ /2 width=3 by ex2_intro/ -| #G #G2 #L #L2 #T #T2 #_ #HT2 #IHT1 #U2 #HTU2 - elim (fquq_cpxs_trans … HTU2 … HT2) -T2 #T2 #HT2 #HTU2 - elim (IHT1 … HT2) -T /3 width=7 by fqus_trans, ex2_intro/ +#h #g #G1 #G2 #L1 #L2 #T2 #U2 #HTU2 #T1 #H elim (fqus_inv_gen … H) -H +[ #HT12 elim (fqup_cpxs_trans … HTU2 … HT12) /3 width=3 by fqup_fqus, ex2_intro/ +| * #H1 #H2 #H3 destruct /2 width=3 by ex2_intro/ ] qed-. @@ -104,14 +116,3 @@ lemma fqus_lsstas_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, ∀l2. ⦃G2, L2⦄ ⊢ T2 ▪ [h, g] l2 → l1 ≤ l2 → ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] U1 & ⦃G1, L1, U1⦄ ⊃* ⦃G2, L2, U2⦄. /3 width=7 by fqus_cpxs_trans, lsstas_cpxs/ qed-. - -lemma fqus_cpx_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ → - ∀U2. ⦃G2, L2⦄ ⊢ T2 ➡[h, g] U2 → - ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡[h, g] U1 & ⦃G1, L1, U1⦄ ⊃* ⦃G2, L2, U2⦄. -#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqus_ind … H) -G2 -L2 -T2 -[ /2 width=3 by ex2_intro/ -| #G #G2 #L #L2 #T #T2 #_ #HT2 #IHT1 #U2 #HTU2 - elim (fquq_cpx_trans … HT2 … HTU2) -T2 #T2 #HT2 #HTU2 - elim (IHT1 … HT2) -T /3 width=7 by fqus_strap1, ex2_intro/ -] -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg.ma index 29cbd8d5d..faf5dd7d9 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg.ma @@ -18,6 +18,7 @@ include "basic_2/computation/fpbs.ma". (* GENEARAL "BIG TREE" PROPER PARALLEL COMPUTATION FOR CLOSURES *************) +(* Note: this is not transitive *) inductive fpbg (h) (g) (G1) (L1) (T1): relation3 genv lenv term ≝ | fpbg_cpxs: ∀L2,T2. ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] T2 → (T1 = T2 → ⊥) → ⦃G1, L1⦄ ⊢ ➡*[h, g] L2 → fpbg h g G1 L1 T1 G1 L2 T2 @@ -35,21 +36,3 @@ lemma fpbc_fpbg: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, L2, #h #g #G1 #G2 #L1 #L2 #T1 #T2 * -G2 -L2 -T2 /3 width=5 by fpbg_cpxs, fpbg_fqup, fqu_fqup, cpx_cpxs/ qed. - -axiom fpbg_strap1: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ >[h, g] ⦃G, L, T⦄ → - ⦃G, L, T⦄ ≽[h, g] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ >[h, g] ⦃G2, L2, T2⦄. - -axiom fpbg_strap2: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ ≽[h, g] ⦃G, L, T⦄ → - ⦃G, L, T⦄ >[h, g] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ >[h, g] ⦃G2, L2, T2⦄. - -lemma fpbg_fpbs_trans: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ >[h, g] ⦃G, L, T⦄ → - ⦃G, L, T⦄ ≥[h, g] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ >[h, g] ⦃G2, L2, T2⦄. -#h #g #G1 #G #G2 #L1 #L #L2 #T1 #T #T2 #H1 #H @(fpbs_ind … H) -G2 -L2 -T2 -/2 width=5 by fpbg_strap1/ -qed-. - -lemma fpbs_fpbg_trans: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G, L, T⦄ → - ⦃G, L, T⦄ >[h, g] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ >[h, g] ⦃G2, L2, T2⦄. -#h #g #G1 #G #G2 #L1 #L #L2 #T1 #T #T2 #H @(fpbs_ind_dx … H) -G1 -L1 -T1 -/3 width=5 by fpbg_strap2/ -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg_fpbg.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg_fpbg.ma new file mode 100644 index 000000000..047aee3d4 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg_fpbg.ma @@ -0,0 +1,36 @@ +(**************************************************************************) +(* ___ *) +(* ||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/computation/fpbs_alt.ma". +include "basic_2/computation/fpbs_fpbs.ma". +include "basic_2/computation/fpbg.ma". + +(* GENERAL "BIG TREE" PROPER PARALLEL COMPUTATION FOR CLOSURES **************) + +(* Advanced forward lemmas **************************************************) + +lemma fpbg_fwd_fpbs: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ >[h, g] ⦃G2, L2, T2⦄ → + ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄. +#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G2 -L2 -T2 +/3 width=5 by cpxs_fqup_fpbs, fpbs_trans, lpxs_fpbs, cpxs_fpbs/ +qed-. + +(* Advanced properties ******************************************************) + +lemma fqu_fpbs_fpbg: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G, L, T⦄ → + ⦃G, L, T⦄ ≥[h, g] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ >[h, g] ⦃G2, L2, T2⦄. +#h #g #G1 #G #G2 #L1 #L #L2 #T1 #T #T2 #H1 #H elim(fpbs_fpbsa … H) -H +#L0 #T0 #HT0 #HT02 #HL02 elim (fqu_cpxs_trans … HT0 … H1) -T +/3 width=7 by fpbg_fqup, fqus_strap2_fqu/ +qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbr.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbr.ma index 099567d41..04f0e2309 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbr.ma @@ -13,7 +13,7 @@ (**************************************************************************) include "basic_2/notation/relations/btpredstarrestricted_8.ma". -include "basic_2/computation/fpbg.ma". +include "basic_2/computation/fpbs.ma". (* RESTRICTED "BIG TREE" PROPER PARALLEL COMPUTATION FOR CLOSURES ***********) @@ -26,14 +26,16 @@ inductive fpbr (h) (g) (G1) (L1) (T1): relation3 genv lenv term ≝ interpretation "restricted 'big tree' proper parallel computation (closure)" 'BTPRedStarRestricted h g G1 L1 T1 G2 L2 T2 = (fpbr h g G1 L1 T1 G2 L2 T2). -(* Basic forward lemmas *****************************************************) +(* Basic inversion lemmas ***************************************************) -lemma fpbr_fwd_fpbg: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃≥[h, g] ⦃G2, L2, T2⦄ → - ⦃G1, L1, T1⦄ >[h, g] ⦃G2, L2, T2⦄. -#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G2 -L2 -T2 -/3 width=5 by fpbg_strap1, fpbc_fpbg, fpbc_fqu/ +lemma fpbr_inv_fqu_fpbs: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃≥[h, g] ⦃G2, L2, T2⦄ → + ∃∃G,L,T. ⦃G1, L1, T1⦄ ⊃ ⦃G, L, T⦄ & ⦃G, L, T⦄ ≥[h, g] ⦃G2, L2, T2⦄. +#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G2 -L2 -T2 [ /2 width=5 by ex2_3_intro/ ] (**) (* auto fails without brackets *) +#G #G2 #L #L2 #T #T2 #_ #HT2 * /3 width=9 by fpbs_strap1, ex2_3_intro/ qed-. +(* Basic forward lemmas *****************************************************) + lemma fpbr_fwd_fpbs: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃≥[h, g] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄. #h #g #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G2 -L2 -T2 diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbr_fpbr.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbr_fpbr.ma index 786030aff..f0d79dc33 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbr_fpbr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbr_fpbr.ma @@ -18,6 +18,13 @@ include "basic_2/computation/fpbr.ma". (* RESTRICTED "BIG TREE" ORDER FOR CLOSURES *********************************) (* Advanced forward lemmas **************************************************) + +lemma fpbr_fwd_fpbg: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃≥[h, g] ⦃G2, L2, T2⦄ → + ⦃G1, L1, T1⦄ >[h, g] ⦃G2, L2, T2⦄. +#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H elim (fpbr_inv_fqu_fpbs … H) -H +/2 width=5 by fqu_fpbs_fpbg/ +qed-. + lemma fpbr_fwd_fpbs: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃≥[h, g] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄. /3 width=5 by fpbr_fwd_fpbg, fpbg_fwd_fpbs/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_alt.ma index 9e5336c04..36fc55264 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_alt.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_alt.ma @@ -32,10 +32,10 @@ interpretation "'big tree' parallel computation (closure) alternative" lemma fpb_fpbsa_trans: ∀h,g,G1,G,L1,L,T1,T. ⦃G1, L1, T1⦄ ≽[h, g] ⦃G, L, T⦄ → ∀G2,L2,T2. ⦃G, L, T⦄ ≥≥[h, g] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≥≥[h, g] ⦃G2, L2, T2⦄. -#h #g #G1 #G #L1 #L #T1 #T * -G -L -T [ #G #L #T #HG1 | #T #HT1 | #L #HL1 ] +#h #g #G1 #G #L1 #L #T1 #T * -G -L -T [ #G #L #T #HG1 | #T #HT1 | #L #HL1 ] #G2 #L2 #T2 * #L0 #T0 #HT0 #HG2 #HL02 [ elim (fquq_cpxs_trans … HT0 … HG1) -T - /3 width=7 by fqus_trans, ex3_2_intro/ + /3 width=7 by fqus_strap2, ex3_2_intro/ | /3 width=5 by cpxs_strap2, ex3_2_intro/ | lapply (lpx_cpxs_trans … HT0 … HL1) -HT0 elim (lpx_fqus_trans … HG2 … HL1) -L diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_cpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_cpxs.ma index 2d197c95b..10600383a 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_cpxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_cpxs.ma @@ -107,7 +107,7 @@ lemma lpxs_fqus_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2 #h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqus_ind … H) -G2 -L2 -T2 /2 width=5 by ex3_2_intro/ #G #G2 #L #L2 #T #T2 #_ #H2 #IH1 #K1 #HLK1 elim (IH1 … HLK1) -L1 #L0 #T0 #HT10 #HT0 #HL0 elim (lpxs_fquq_trans … H2 … HL0) -L -#L #T3 #HT3 #HT32 #HL2 elim (fqus_cpxs_trans … HT0 … HT3) -T +#L #T3 #HT3 #HT32 #HL2 elim (fqus_cpxs_trans … HT3 … HT0) -T /3 width=7 by cpxs_trans, fqus_strap1, ex3_2_intro/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lift.ma index eeb23f7b5..505eabf1a 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lift.ma @@ -173,6 +173,27 @@ lemma fquq_ssta_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡[h, g] U1 & ⦃G1, L1, U1⦄ ⊃⸮ ⦃G2, L2, U2⦄. /3 width=5 by fquq_cpx_trans, ssta_cpx/ qed-. +lemma fqup_cpx_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄ → + ∀U2. ⦃G2, L2⦄ ⊢ T2 ➡[h, g] U2 → + ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡[h, g] U1 & ⦃G1, L1, U1⦄ ⊃+ ⦃G2, L2, U2⦄. +#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind … H) -G2 -L2 -T2 +[ #G2 #L2 #T2 #H12 #U2 #HTU2 elim (fqu_cpx_trans … H12 … HTU2) -T2 + /3 width=3 by fqu_fqup, ex2_intro/ +| #G #G2 #L #L2 #T #T2 #_ #HT2 #IHT1 #U2 #HTU2 + elim (fqu_cpx_trans … HT2 … HTU2) -T2 #T2 #HT2 #HTU2 + elim (IHT1 … HT2) -T /3 width=7 by fqup_strap1, ex2_intro/ +] +qed-. + +lemma fqus_cpx_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ → + ∀U2. ⦃G2, L2⦄ ⊢ T2 ➡[h, g] U2 → + ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡[h, g] U1 & ⦃G1, L1, U1⦄ ⊃* ⦃G2, L2, U2⦄. +#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H #U2 #HTU2 elim (fqus_inv_gen … H) -H +[ #HT12 elim (fqup_cpx_trans … HT12 … HTU2) /3 width=3 by fqup_fqus, ex2_intro/ +| * #H1 #H2 #H3 destruct /2 width=3 by ex2_intro/ +] +qed-. + lemma fqu_cpx_trans_neq: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ → ∀U2. ⦃G2, L2⦄ ⊢ T2 ➡[h, g] U2 → (T2 = U2 → ⊥) → ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡[h, g] U1 & T1 = U1 → ⊥ & ⦃G1, L1, U1⦄ ⊃ ⦃G2, L2, U2⦄. -- 2.39.2