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/fpbg_fpbs.ma".
16 include "basic_2/rt_computation/fsb_feqx.ma".
18 (* STRONGLY NORMALIZING CLOSURES FOR PARALLEL RST-TRANSITION ****************)
20 (* Properties with parallel rst-computation for closures ********************)
23 ∀G1,L1,T1. ≥𝐒 ❪G1,L1,T1❫ →
24 ∀G2,L2,T2. ❪G1,L1,T1❫ ≥ ❪G2,L2,T2❫ → ≥𝐒 ❪G2,L2,T2❫.
25 #G1 #L1 #T1 #H @(fsb_ind_alt … H) -G1 -L1 -T1
26 #G1 #L1 #T1 #H1 #IH #G2 #L2 #T2 #H12
27 elim (fpbs_inv_fpbg … H12) -H12
28 [ -IH /2 width=5 by fsb_feqx_trans/
29 | -H1 * /2 width=5 by/
33 (* Properties with proper parallel rst-computation for closures *************)
37 (∀G2,L2,T2. ❪G1,L1,T1❫ > ❪G2,L2,T2❫ → ≥𝐒 ❪G2,L2,T2❫) →
39 /4 width=1 by fsb_intro, fpb_fpbg/ qed.
41 (* Eliminators with proper parallel rst-computation for closures ************)
43 lemma fsb_ind_fpbg_fpbs (Q:relation3 …):
44 (∀G1,L1,T1. ≥𝐒 ❪G1,L1,T1❫ →
45 (∀G2,L2,T2. ❪G1,L1,T1❫ > ❪G2,L2,T2❫ → Q G2 L2 T2) →
48 ∀G1,L1,T1. ≥𝐒 ❪G1,L1,T1❫ →
49 ∀G2,L2,T2. ❪G1,L1,T1❫ ≥ ❪G2,L2,T2❫ → Q G2 L2 T2.
50 #Q #IH1 #G1 #L1 #T1 #H @(fsb_ind_alt … H) -G1 -L1 -T1
51 #G1 #L1 #T1 #H1 #IH #G2 #L2 #T2 #H12
53 [ -IH /2 width=5 by fsb_fpbs_trans/
54 | -H1 #G0 #L0 #T0 #H10
55 elim (fpbs_fpbg_trans … H12 … H10) -G2 -L2 -T2
60 lemma fsb_ind_fpbg (Q:relation3 …):
61 (∀G1,L1,T1. ≥𝐒 ❪G1,L1,T1❫ →
62 (∀G2,L2,T2. ❪G1,L1,T1❫ > ❪G2,L2,T2❫ → Q G2 L2 T2) →
65 ∀G1,L1,T1. ≥𝐒 ❪G1,L1,T1❫ → Q G1 L1 T1.
66 #Q #IH #G1 #L1 #T1 #H @(fsb_ind_fpbg_fpbs … H) -H
70 (* Inversion lemmas with proper parallel rst-computation for closures *******)
72 lemma fsb_fpbg_refl_false (G) (L) (T):
73 ≥𝐒 ❪G,L,T❫ → ❪G,L,T❫ > ❪G,L,T❫ → ⊥.
75 @(fsb_ind_fpbg … H) -G -L -T #G1 #L1 #T1 #_ #IH #H