1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "static_2/static/feqg_fqus.ma".
16 include "static_2/static/feqg_feqg.ma".
17 include "basic_2/rt_transition/cpx_feqg.ma".
18 include "basic_2/rt_transition/lpx_reqg.ma".
19 include "basic_2/rt_transition/fpb.ma".
21 (* PARALLEL RST-TRANSITION FOR CLOSURES *************************************)
23 (* Propreties with generic equivalence on referred closures *****************)
25 (* Basic_2A1: includes: fleq_fpbq fpbq_lleq *)
26 (* Basic_2A1: uses: fpbq_feqx *)
27 lemma feqg_fpb (S) (G1) (G2) (L1) (L2) (T1) (T2):
28 reflexive … S → symmetric … S →
29 ❨G1,L1,T1❩ ≛[S] ❨G2,L2,T2❩ → ❨G1,L1,T1❩ ≽ ❨G2,L2,T2❩.
30 #S #G1 #G2 #L1 #L2 #T1 #T2 #HS1 #HS2 #H
31 elim (feqg_inv_gen_sn … H) -H #H #HL12 #HT12 destruct
32 /4 width=8 by reqg_rpx, teqg_cpx, fpb_intro/
35 lemma feqg_fpb_trans (S) (G) (L) (T):
36 reflexive … S → symmetric … S → Transitive … S →
37 ∀G1,L1,T1. ❨G1,L1,T1❩ ≛[S] ❨G,L,T❩ →
38 ∀G2,L2,T2. ❨G,L,T❩ ≽ ❨G2,L2,T2❩ → ❨G1,L1,T1❩ ≽ ❨G2,L2,T2❩.
39 #S #G #L #T #H1S #H2S #H3S #G1 #L1 #T1 #H1 #G2 #L2 #T2 #H2
40 elim (fpb_inv_gen … H2) -H2 #L0 #T0 #H0 #HT02 #H
41 elim (rpx_inv_reqg_lpx S … H) -H // #L3 #HL03 #HL32
42 elim (feqg_fquq_trans … H1 … H0) -G -L -T // #G #L #T #H1 #H0
43 lapply (feqg_cpx_trans_cpx … H0 … HT02) // -HT02 #HT2
44 lapply (feqg_reqg_trans … H0 … HL03) -H0 -HL03 // #H
45 elim (feqg_inv_gen_sn … H) -H #H #HL3 #_ destruct -T0
46 /3 width=10 by fpb_intro, reqg_lpx_trans_rpx/