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 "basic_2/rt_transition/fpb_feqg.ma".
16 include "basic_2/rt_transition/fpbc.ma".
18 (* PROPER PARALLEL RST-TRANSITION FOR CLOSURES ******************************)
20 (* Properties with generic equivalence for closures *************************)
22 (* Basic_2A1: uses: teqg_fpb_trans lleq_fpb_trans fleq_fpb_trans *)
23 lemma feqg_fpbc_trans (S) (G) (L) (T):
24 reflexive … S → symmetric … S → Transitive … S →
25 ∀G1,L1,T1. ❨G1,L1,T1❩ ≛[S] ❨G,L,T❩ →
26 ∀G2,L2,T2. ❨G,L,T❩ ≻ ❨G2,L2,T2❩ → ❨G1,L1,T1❩ ≻ ❨G2,L2,T2❩.
27 #S #G #L #T #H1S #H2S #H3S #G1 #L1 #T1 #H1 #G2 #L2 #T2 #H2
28 elim (fpbc_inv_gen sfull … H2) -H2 #H2 #Hn2
29 /6 width=9 by fpbc_intro, feqg_fpb_trans, feqg_canc_sn, feqg_feqx/
32 (* Inversion lemmas with generic equivalence for closures *******************)
34 (* Basic_2A1: uses: fpb_inv_fleq *)
35 lemma fpbc_inv_feqg (S):
36 ∀G1,G2,L1,L2,T1,T2. ❨G1,L1,T1❩ ≻ ❨G2,L2,T2❩ →
37 ❨G1,L1,T1❩ ≛[S] ❨G2,L2,T2❩ → ⊥.
38 #S #G1 #G2 #L1 #L2 #T1 #T2 #H #H12
39 elim (fpbc_inv_gen S … H) -H #_ #Hn2