]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/lambdadelta/basic_2/etc/lfpx/lfpx_lreq.etc
update in delayed_updating
[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / etc / lfpx / lfpx_lreq.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/multiple/llor_drop.ma".
16 include "basic_2/multiple/llpx_sn_llor.ma".
17 include "basic_2/multiple/llpx_sn_lpx_sn.ma".
18 include "basic_2/multiple/lleq_lreq.ma".
19 include "basic_2/multiple/lleq_llor.ma".
20 include "basic_2/reduction/cpx_lreq.ma".
21 include "basic_2/reduction/cpx_lleq.ma".
22 include "basic_2/reduction/lpx_frees.ma".
23
24 (* SN EXTENDED PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS ********************)
25
26
27 fact lreq_lpx_trans_lleq_aux: ∀h,o,G,L1,L0,l,k. L1 ⩬[l, k] L0 → k = ∞ →
28                               ∀L2. ⦃G, L0⦄ ⊢ ➡[h, o] L2 →
29                               ∃∃L. L ⩬[l, k] L2 & ⦃G, L1⦄ ⊢ ➡[h, o] L &
30                                    (∀T. L0 ≡[T, l] L2 ↔ L1 ≡[T, l] L).
31 #h #o #G #L1 #L0 #l #k #H elim H -L1 -L0 -l -k
32 [ #l #k #_ #L2 #H >(lpx_inv_atom1 … H) -H
33   /3 width=5 by ex3_intro, conj/
34 | #I1 #I0 #L1 #L0 #V1 #V0 #_ #_ #Hm destruct
35 | #I #L1 #L0 #V1 #k #HL10 #IHL10 #Hm #Y #H
36   elim (lpx_inv_pair1 … H) -H #L2 #V2 #HL02 #HV02 #H destruct
37   lapply (ysucc_inv_Y_dx … Hm) -Hm #Hm
38   elim (IHL10 … HL02) // -IHL10 -HL02 #L #HL2 #HL1 #IH
39   @(ex3_intro … (L.ⓑ{I}V2)) /3 width=3 by lpx_pair, lreq_cpx_trans, lreq_pair/
40   #T elim (IH T) #HL0dx #HL0sn
41   @conj #H @(lleq_lreq_repl … H) -H /3 width=1 by lreq_sym, lreq_pair_O_Y/
42 | #I1 #I0 #L1 #L0 #V1 #V0 #l #k #HL10 #IHL10 #Hm #Y #H
43   elim (lpx_inv_pair1 … H) -H #L2 #V2 #HL02 #HV02 #H destruct
44   elim (IHL10 … HL02) // -IHL10 -HL02 #L #HL2 #HL1 #IH
45   @(ex3_intro … (L.ⓑ{I1}V1)) /3 width=1 by lpx_pair, lreq_succ/
46   #T elim (IH T) #HL0dx #HL0sn
47   @conj #H @(lleq_lreq_repl … H) -H /3 width=1 by lreq_sym, lreq_succ/
48 ]
49 qed-.
50
51 lemma lreq_lpx_trans_lleq: ∀h,o,G,L1,L0,l. L1 ⩬[l, ∞] L0 →
52                            ∀L2. ⦃G, L0⦄ ⊢ ➡[h, o] L2 →
53                            ∃∃L. L ⩬[l, ∞] L2 & ⦃G, L1⦄ ⊢ ➡[h, o] L &
54                                 (∀T. L0 ≡[T, l] L2 ↔ L1 ≡[T, l] L).
55 /2 width=1 by lreq_lpx_trans_lleq_aux/ qed-.