]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/lambdadelta/basic_2/etc/referred/lfsx_lfsx.etc
update in delayed_updating
[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / etc / referred / lfsx_lfsx.etc
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_transition/lfpx_lfdeq.ma".
16 include "basic_2/rt_computation/lfsx.ma".
17
18 (* STRONGLY NORMALIZING LOCAL ENV.S FOR UNBOUND PARALLEL RT-TRANSITION ******)
19
20 (* Advanced properties ******************************************************)
21
22 (* Basic_2A1: uses: lsx_lleq_trans *)
23 lemma lfsx_lfdeq_trans: āˆ€h,o,G,L1,T. G āŠ¢ ā¬ˆ*[h, o, T] š’ā¦ƒL1ā¦„ ā†’
24                         āˆ€L2. L1 ā‰›[h, o, T] L2 ā†’ G āŠ¢ ā¬ˆ*[h, o, T] š’ā¦ƒL2ā¦„.
25 #h #o #G #L1 #T #H @(lfsx_ind ā€¦ H) -L1
26 #L1 #_ #IHL1 #L2 #HL12 @lfsx_intro
27 #L #HL2 #HnL2 elim (lfdeq_lfpx_trans ā€¦ HL2 ā€¦ HL12) -HL2
28 /4 width=5 by lfdeq_repl/
29 qed-.
30
31 (* Basic_2A1: uses: lsx_lpx_trans *)
32 lemma lfsx_lfpx_trans: āˆ€h,o,G,L1,T. G āŠ¢ ā¬ˆ*[h, o, T] š’ā¦ƒL1ā¦„ ā†’
33                        āˆ€L2. ā¦ƒG, L1ā¦„ āŠ¢ ā¬ˆ[h, T] L2 ā†’ G āŠ¢ ā¬ˆ*[h, o, T] š’ā¦ƒL2ā¦„.
34 #h #o #G #L1 #T #H @(lfsx_ind ā€¦ H) -L1 #L1 #HL1 #IHL1 #L2 #HL12
35 elim (lfdeq_dec h o L1 L2 T) /3 width=4 by lfsx_lfdeq_trans, lfxs_refl/
36 qed-.
37
38 (* Advanced forward lemmas **************************************************)
39
40 (* Basic_2A1: uses: lsx_fwd_pair_sn lsx_fwd_bind_sn lsx_fwd_flat_sn *)
41 lemma lfsx_fwd_pair_sn: āˆ€h,o,I,G,L,V,T. G āŠ¢ ā¬ˆ*[h, o, ā‘”{I}V.T] š’ā¦ƒLā¦„ ā†’
42                         G āŠ¢ ā¬ˆ*[h, o, V] š’ā¦ƒLā¦„.
43 #h #o #I #G #L #V #T #H @(lfsx_ind ā€¦ H) -L
44 #L1 #_ #IHL1 @lfsx_intro
45 #L2 #H #HnL12 elim (lfpx_pair_sn_split ā€¦ H o I T) -H
46 /6 width=3 by lfsx_lfdeq_trans, lfdeq_trans, lfdeq_fwd_pair_sn/
47 qed-.
48
49 (* Basic_2A1: uses: lsx_fwd_flat_dx *)
50 lemma lfsx_fwd_flat_dx: āˆ€h,o,I,G,L,V,T. G āŠ¢ ā¬ˆ*[h, o, ā“•{I}V.T] š’ā¦ƒLā¦„ ā†’
51                         G āŠ¢ ā¬ˆ*[h, o, T] š’ā¦ƒLā¦„.
52 #h #o #I #G #L #V #T #H @(lfsx_ind ā€¦ H) -L
53 #L1 #_ #IHL1 @lfsx_intro
54 #L2 #H #HnL12 elim (lfpx_flat_dx_split ā€¦ H o I V) -H
55 /6 width=3 by lfsx_lfdeq_trans, lfdeq_trans, lfdeq_fwd_flat_dx/
56 qed-.
57
58 (* Basic_2A1: uses: lsx_fwd_bind_dx *)
59 (* Note: the exclusion binder (ā“§) makes this more elegant and much simpler *)
60 lemma lfsx_fwd_bind_dx: āˆ€h,o,p,I,G,L,V,T. G āŠ¢ ā¬ˆ*[h, o, ā“‘{p,I}V.T] š’ā¦ƒLā¦„ ā†’
61                         G āŠ¢ ā¬ˆ*[h, o, T] š’ā¦ƒL.ā“§ā¦„.
62 #h #o #p #I #G #L #V #T #H @(lfsx_ind ā€¦ H) -L
63 #L1 #_ #IH @lfsx_intro
64 #L2 #H #HT elim (lfpx_bind_dx_split_void ā€¦ H o p I V) -H
65 /6 width=5 by lfsx_lfdeq_trans, lfdeq_trans, lfdeq_fwd_bind_dx_void/
66 qed-.
67
68 (* Advanced inversion lemmas ************************************************)
69
70 (* Basic_2A1: uses: lsx_inv_flat *)
71 lemma lfsx_inv_flat: āˆ€h,o,I,G,L,V,T. G āŠ¢ ā¬ˆ*[h, o, ā“•{I}V.T] š’ā¦ƒLā¦„ ā†’
72                      G āŠ¢ ā¬ˆ*[h, o, V] š’ā¦ƒLā¦„ āˆ§ G āŠ¢ ā¬ˆ*[h, o, T] š’ā¦ƒLā¦„.
73 /3 width=3 by lfsx_fwd_pair_sn, lfsx_fwd_flat_dx, conj/ qed-.
74
75 (* Basic_2A1: uses: lsx_inv_bind *)
76 lemma lfsx_inv_bind: āˆ€h,o,p,I,G,L,V,T. G āŠ¢ ā¬ˆ*[h, o, ā“‘{p,I}V.T] š’ā¦ƒLā¦„ ā†’
77                      G āŠ¢ ā¬ˆ*[h, o, V] š’ā¦ƒLā¦„ āˆ§ G āŠ¢ ā¬ˆ*[h, o, T] š’ā¦ƒL.ā“§ā¦„.
78 /3 width=4 by lfsx_fwd_pair_sn, lfsx_fwd_bind_dx, conj/ qed-.