]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_fpbg.ma
12c72dceb7e4c09444b0d56ccd49a63a5b594a88
[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / rt_computation / fsb_fpbg.ma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||         The HELM team.                                      *)
8 (*      ||A||         http://helm.cs.unibo.it                             *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU General Public License Version 2                  *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 include "basic_2/rt_computation/fpbg_fqup.ma".
16 include "basic_2/rt_computation/fpbg_feqg.ma".
17 include "basic_2/rt_computation/fsb_feqg.ma".
18
19 (* STRONGLY NORMALIZING CLOSURES FOR PARALLEL RST-TRANSITION ****************)
20
21 (* Properties with parallel rst-computation for closures ********************)
22
23 lemma fsb_fpbs_trans:
24       ∀G1,L1,T1. ≥𝐒 ❨G1,L1,T1❩ →
25       ∀G2,L2,T2. ❨G1,L1,T1❩ ≥ ❨G2,L2,T2❩ → ≥𝐒 ❨G2,L2,T2❩.
26 #G1 #L1 #T1 #H @(fsb_ind … H) -G1 -L1 -T1
27 #G1 #L1 #T1 #H1 #IH #G2 #L2 #T2 #H12
28 elim (fpbs_inv_fpbg … H12) -H12
29 [ -IH /2 width=9 by fsb_feqg_trans/
30 | -H1 #H elim (fpbg_inv_fpbc_fpbs … H)
31   /2 width=5 by/
32 ]
33 qed-.
34
35 (* Properties with parallel rst-transition for closures *********************)
36
37 lemma fsb_fpb_trans:
38       ∀G1,L1,T1. ≥𝐒 ❨G1,L1,T1❩ →
39       ∀G2,L2,T2. ❨G1,L1,T1❩ ≽ ❨G2,L2,T2❩ → ≥𝐒 ❨G2,L2,T2❩.
40 /3 width=5 by fsb_fpbs_trans, fpb_fpbs/ qed-.
41
42 (* Properties with proper parallel rst-computation for closures *************)
43
44 lemma fsb_intro_fpbg:
45       ∀G1,L1,T1.
46       (∀G2,L2,T2. ❨G1,L1,T1❩ > ❨G2,L2,T2❩ → ≥𝐒 ❨G2,L2,T2❩) →
47       ≥𝐒 ❨G1,L1,T1❩.
48 /4 width=1 by fsb_intro, fpbc_fpbg/ qed.
49
50 (* Eliminators with proper parallel rst-computation for closures ************)
51
52 lemma fsb_ind_fpbg_fpbs (Q:relation3 …):
53       (∀G1,L1,T1. ≥𝐒 ❨G1,L1,T1❩ →
54         (∀G2,L2,T2. ❨G1,L1,T1❩ > ❨G2,L2,T2❩ → Q G2 L2 T2) →
55         Q G1 L1 T1
56       ) →
57       ∀G1,L1,T1. ≥𝐒 ❨G1,L1,T1❩ →
58       ∀G2,L2,T2. ❨G1,L1,T1❩ ≥ ❨G2,L2,T2❩ → Q G2 L2 T2.
59 #Q #IH1 #G1 #L1 #T1 #H @(fsb_ind … H) -G1 -L1 -T1
60 #G1 #L1 #T1 #H1 #IH #G2 #L2 #T2 #H12
61 @IH1 -IH1
62 [ -IH /2 width=5 by fsb_fpbs_trans/
63 | -H1 #G0 #L0 #T0 #H10
64   lapply (fpbs_fpbg_trans … H12 … H10) -G2 -L2 -T2 #H
65   elim (fpbg_inv_fpbc_fpbs … H) -H #G #L #T #H1 #H0
66   /2 width=5 by/
67 ]
68 qed-.
69
70 lemma fsb_ind_fpbg (Q:relation3 …):
71       (∀G1,L1,T1. ≥𝐒 ❨G1,L1,T1❩ →
72         (∀G2,L2,T2. ❨G1,L1,T1❩ > ❨G2,L2,T2❩ → Q G2 L2 T2) →
73         Q G1 L1 T1
74       ) →
75       ∀G1,L1,T1. ≥𝐒 ❨G1,L1,T1❩ →  Q G1 L1 T1.
76 #Q #IH #G1 #L1 #T1 #H @(fsb_ind_fpbg_fpbs … H) -H
77 /3 width=1 by/
78 qed-.
79
80 (* Inversion lemmas with proper parallel rst-computation for closures *******)
81
82 lemma fsb_fpbg_refl_false (G) (L) (T):
83       ≥𝐒 ❨G,L,T❩ → ❨G,L,T❩ > ❨G,L,T❩ → ⊥.
84 #G #L #T #H
85 @(fsb_ind_fpbg … H) -G -L -T #G1 #L1 #T1 #_ #IH #H
86 /2 width=5 by/
87 qed-.