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_computation/fpbs_fpbc.ma".
16 include "basic_2/rt_computation/fpbg_fpbs.ma".
18 (* PROPER PARALLEL RST-COMPUTATION FOR CLOSURES *****************************)
20 (* Properties with generic equivalence for closures *************************)
22 (* Basic_2A1: uses: fpbg_fleq_trans *)
23 lemma fpbg_feqg_trans (S) (G) (L) (T):
24 reflexive … S → symmetric … S →
25 ∀G1,L1,T1. ❨G1,L1,T1❩ > ❨G,L,T❩ →
26 ∀G2,L2,T2. ❨G,L,T❩ ≛[S] ❨G2,L2,T2❩ → ❨G1,L1,T1❩ > ❨G2,L2,T2❩.
27 /3 width=8 by fpbg_fpb_trans, feqg_fpb/ qed-.
29 (* Basic_2A1: uses: fleq_fpbg_trans *)
30 lemma feqg_fpbg_trans (S) (G) (L) (T):
31 reflexive … S → symmetric … S →
32 ∀G1,L1,T1. ❨G1,L1,T1❩ ≛[S] ❨G,L,T❩ →
33 ∀G2,L2,T2. ❨G,L,T❩ > ❨G2,L2,T2❩ → ❨G1,L1,T1❩ > ❨G2,L2,T2❩.
34 /3 width=8 by fpb_fpbg_trans, feqg_fpb/ qed-.
36 (* Properties with generic equivalence for terms ****************************)
38 lemma fpbg_teqg_div (S):
39 reflexive … S → symmetric … S →
40 ∀G1,G2,L1,L2,T1,T. ❨G1,L1,T1❩ > ❨G2,L2,T❩ →
41 ∀T2. T2 ≛[S] T → ❨G1,L1,T1❩ > ❨G2,L2,T2❩.
42 /4 width=8 by fpbg_feqg_trans, teqg_feqg, teqg_sym/ qed-.
44 (* Advanced inversion lemmas of parallel rst-computation on closures ********)
46 (* Basic_2A1: was: fpbs_fpbg *)
48 ∀G1,G2,L1,L2,T1,T2. ❨G1,L1,T1❩ ≥ ❨G2,L2,T2❩ →
49 ∨∨ ❨G1,L1,T1❩ ≅ ❨G2,L2,T2❩
50 | ❨G1,L1,T1❩ > ❨G2,L2,T2❩.
51 #G1 #G2 #L1 #L2 #T1 #T2 #H
52 elim (fpbs_inv_fpbc_sn … H) -H
53 [ /2 width=1 by or_introl/
55 /3 width=9 by fpbg_intro, or_intror/
59 (* Basic_2A1: this was the definition of fpbg *)
60 lemma fpbg_inv_fpbc_fpbs (G1) (G2) (L1) (L2) (T1) (T2):
61 ❨G1,L1,T1❩ > ❨G2,L2,T2❩ →
62 ∃∃G,L,T. ❨G1,L1,T1❩ ≻ ❨G,L,T❩ & ❨G,L,T❩ ≥ ❨G2,L2,T2❩.
63 #G1 #G2 #L1 #L2 #T1 #T2 #H
64 elim (fpbg_inv_gen … H) -H #G3 #L3 #T3 #G4 #L4 #T4 #H13 #H34 #H42
65 elim (fpbs_inv_fpbc_sn … H13) -H13
66 [ /3 width=9 by feqg_fpbc_trans, ex2_3_intro/
68 /4 width=13 by fpbg_fwd_fpbs,fpbg_intro, ex2_3_intro/
72 (* Advanced properties of parallel rst-computation on closures **************)
75 ∀F1,F2,K1,K2,T1,T2. ❨F1,K1,T1❩ ≥ ❨F2,K2,T2❩ →
76 ∀G2,L2,U2. ❨F2,K2,T2❩ ≻ ❨G2,L2,U2❩ →
77 ∃∃G1,L1,U1. ❨F1,K1,T1❩ ≻ ❨G1,L1,U1❩ & ❨G1,L1,U1❩ ≥ ❨G2,L2,U2❩.
78 #F1 #F2 #K1 #K2 #T1 #T2 #H elim (fpbs_inv_fpbg … H) -H
79 [ #H12 #G2 #L2 #U2 #H22
80 lapply (feqg_fpbc_trans … H12 … H22) -F2 -K2 -T2
81 /3 width=5 by feqg_fpbs, ex2_3_intro/
82 | #H12 #G2 #L2 #U2 #H22
83 elim (fpbg_inv_fpbc_fpbs … H12) -H12 #F #K #T #H1 #H2
84 /4 width=9 by fpbs_strap1, fpbc_fwd_fpb, ex2_3_intro/