(**************************************************************************) (* ___ *) (* ||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/notation/relations/btpredalt_8.ma". include "basic_2/reduction/fpb_fleq.ma". include "basic_2/reduction/fpbq.ma". (* "QRST" PARALLEL REDUCTION FOR CLOSURES ***********************************) (* Basic properties *********************************************************) lemma fleq_fpbq: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≡[0] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≽[h, o] ⦃G2, L2, T2⦄. #h #o #G1 #G2 #L1 #L2 #T1 #T2 * /2 width=1 by fpbq_lleq/ qed. lemma fpb_fpbq: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≻[h, o] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≽[h, o] ⦃G2, L2, T2⦄. #h #o #G1 #G2 #L1 #L2 #T1 #T2 * -G2 -L2 -T2 /3 width=1 by fpbq_fquq, fpbq_cpx, fpbq_lpx, fqu_fquq/ qed. (* Advanced eliminators *****************************************************) lemma fpbq_ind_alt: ∀h,o,G1,G2,L1,L2,T1,T2. ∀R:Prop. (⦃G1, L1, T1⦄ ≡[0] ⦃G2, L2, T2⦄ → R) → (⦃G1, L1, T1⦄ ≻[h, o] ⦃G2, L2, T2⦄ → R) → ⦃G1, L1, T1⦄ ≽[h, o] ⦃G2, L2, T2⦄ → R. #h #o #G1 #G2 #L1 #L2 #T1 #T2 #R #HI1 #HI2 #H elim (fpbq_fpbqa … H) /2 width=1 by/ qed-. (* aternative definition of fpb *********************************************) lemma fpb_fpbq_alt: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≻[h, o] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≽[h, o] ⦃G2, L2, T2⦄ ∧ (⦃G1, L1, T1⦄ ≡[0] ⦃G2, L2, T2⦄ → ⊥). /3 width=10 by fpb_fpbq, fpb_inv_fleq, conj/ qed. lemma fpbq_inv_fpb_alt: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≽[h, o] ⦃G2, L2, T2⦄ → (⦃G1, L1, T1⦄ ≡[0] ⦃G2, L2, T2⦄ → ⊥) → ⦃G1, L1, T1⦄ ≻[h, o] ⦃G2, L2, T2⦄. #h #o #G1 #G2 #L1 #L2 #T1 #T2 #H #H0 @(fpbq_ind_alt … H) -H // #H elim H0 -H0 // qed-.