]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_preterm_fsubst.ma
projects / helm.git / blob
? search:


ecf0eaf0f7d1b131fd80decb6a63ebc9fb39c545
[helm.git] / matita / matita / contribs / lambdadelta / delayed_updating / unwind / unwind2_preterm_fsubst.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 "delayed_updating/unwind/unwind2_prototerm_eq.ma".
16 include "delayed_updating/unwind/unwind2_path_append.ma".
17 include "delayed_updating/substitution/fsubst.ma".
18 include "delayed_updating/syntax/preterm.ma".
19 include "delayed_updating/syntax/prototerm_proper.ma".
20
21 (* TAILED UNWIND FOR PRETERM ************************************************)
22
23 (* Constructions with fsubst and pic ****************************************)
24
25 lemma unwind2_term_fsubst_pic_sn (f) (t) (u) (p): p Ļµ šˆ ā†’
26       (ā–¼[f]t)[ā‹”(āŠ—p)ā†ā–¼[ā–¶[f]p]u] āŠ† ā–¼[f](t[ā‹”pā†u]).
27 #f #t #u #p #Hp #ql * *
28 [ #rl * #r #Hr #H1 #H2 destruct
29   >unwind2_path_append_pic_sn
30   /4 width=3 by in_comp_unwind2_path_term, or_introl, ex2_intro/
31 | * #q #Hq #H1 #H0
32   @(ex2_intro ā€¦ H1) @or_intror @conj // *
33   [ <list_append_empty_sn #H2 destruct
34     elim (unwind2_path_root f q) #r #_ #Hr /2 width=2 by/
35   | #l #r #H2 destruct
36     /3 width=2 by unwind2_path_append_pic_sn/
37   ]
38 ]
39 qed-.
40
41 lemma unwind2_term_fsubst_pic_dx (f) (t) (u) (p): p Ļµ šˆ ā†’ p Ļµ ā–µt ā†’ t Ļµ š“ ā†’
42       ā–¼[f](t[ā‹”pā†u]) āŠ† (ā–¼[f]t)[ā‹”(āŠ—p)ā†ā–¼[ā–¶[f]p]u].
43 #f #t #u #p #Hp #H1p #H2p #ql * #q * *
44 [ #r #Hu #H1 #H2 destruct
45   /5 width=3 by unwind2_path_append_pic_sn, ex2_intro, or_introl/
46 | #Hq #H0 #H1 destruct
47   @or_intror @conj [ /2 width=1 by in_comp_unwind2_path_term/ ] *
48   [ <list_append_empty_sn #Hr @(H0 ā€¦ (šž)) -H0
49     <list_append_empty_sn @H2p -H2p
50     /2 width=2 by unwind2_path_des_structure, prototerm_in_comp_root/
51   | #l #r #Hr
52     elim (unwind2_path_inv_append_ppc_dx ā€¦ Hr) -Hr // #s1 #s2 #Hs1 #_ #H1 destruct
53     lapply (H2p ā€¦ Hs1) -H2p -Hs1 /2 width=2 by ex_intro/
54   ]
55 ]
56 qed-.
57
58 lemma unwind2_term_fsubst_pic (f) (t) (u) (p): p Ļµ šˆ ā†’ p Ļµ ā–µt ā†’ t Ļµ š“ ā†’
59       (ā–¼[f]t)[ā‹”(āŠ—p)ā†ā–¼[ā–¶[f]p]u] ā‡” ā–¼[f](t[ā‹”pā†u]).
60 /4 width=3 by unwind2_term_fsubst_pic_sn, conj, unwind2_term_fsubst_pic_dx/ qed.
61
62 (* Constructions with fsubst and ppc ****************************************)
63
64 lemma unwind2_term_fsubst_ppc_sn (f) (t) (u) (p): u Ļµ š ā†’
65       (ā–¼[f]t)[ā‹”(āŠ—p)ā†ā–¼[ā–¶[f]p]u] āŠ† ā–¼[f](t[ā‹”pā†u]).
66 #f #t #u #p #Hu #ql * *
67 [ #rl * #r #Hr #H1 #H2 destruct
68   >unwind2_path_append_ppc_dx
69   /4 width=5 by in_comp_unwind2_path_term, in_comp_tpc_trans, or_introl, ex2_intro/
70 | * #q #Hq #H1 #H0
71   @(ex2_intro ā€¦ H1) @or_intror @conj // *
72   [ <list_append_empty_sn #H2 destruct
73     elim (unwind2_path_root f q) #r #_ #Hr /2 width=2 by/
74   | #l #r #H2 destruct
75     @H0 -H0 [| <unwind2_path_append_ppc_dx /2 width=3 by ppc_rcons/ ]
76   ]
77 ]
78 qed-.
79
80 lemma unwind2_term_fsubst_ppc_dx (f) (t) (u) (p): u Ļµ š ā†’ p Ļµ ā–µt ā†’ t Ļµ š“ ā†’
81       ā–¼[f](t[ā‹”pā†u]) āŠ† (ā–¼[f]t)[ā‹”(āŠ—p)ā†ā–¼[ā–¶[f]p]u].
82 #f #t #u #p #Hu #H1p #H2p #ql * #q * *
83 [ #r #Hu #H1 #H2 destruct
84   @or_introl @ex2_intro
85   [|| <unwind2_path_append_ppc_dx /2 width=5 by in_comp_tpc_trans/ ]
86   /2 width=3 by ex2_intro/
87 | #Hq #H0 #H1 destruct
88   @or_intror @conj [ /2 width=1 by in_comp_unwind2_path_term/ ] *
89   [ <list_append_empty_sn #Hr @(H0 ā€¦ (šž)) -H0
90     <list_append_empty_sn @H2p -H2p
91     /2 width=2 by unwind2_path_des_structure, prototerm_in_comp_root/
92   | #l #r #Hr
93     elim (unwind2_path_inv_append_ppc_dx ā€¦ Hr) -Hr // #s1 #s2 #Hs1 #_ #H1 destruct
94     lapply (H2p ā€¦ Hs1) -H2p -Hs1 /2 width=2 by ex_intro/
95   ]
96 ]
97 qed-.
98
99 lemma unwind2_term_fsubst_ppc (f) (t) (u) (p): u Ļµ š ā†’ p Ļµ ā–µt ā†’ t Ļµ š“ ā†’
100       (ā–¼[f]t)[ā‹”(āŠ—p)ā†ā–¼[ā–¶[f]p]u] ā‡” ā–¼[f](t[ā‹”pā†u]).
101 /4 width=3 by unwind2_term_fsubst_ppc_sn, conj, unwind2_term_fsubst_ppc_dx/ qed.
Unnamed repository; edit this file 'description' to name the repository.