]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpt_fqu.ma
update in ground
[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / rt_transition / cpt_fqu.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 "static_2/s_transition/fqu_weight.ma".
16 include "basic_2/rt_transition/cpt.ma".
17
18 (* T-BOUND CONTEXT-SENSITIVE PARALLEL T-TRANSITION FOR TERMS ****************)
19
20 (* Basic eliminators ********************************************************)
21
22 lemma cpt_ind (h) (Q:relation5 …):
23       (∀I,G,L. Q 0 G L (⓪[I]) (⓪[I])) →
24       (∀G,L,s. Q 1 G L (⋆s) (⋆(⫯[h]s))) →
25       (∀n,G,K,V1,V2,W2. ❪G,K❫ ⊢ V1 ⬆[h,n] V2 → Q n G K V1 V2 →
26         ⇧[1] V2 ≘ W2 → Q n G (K.ⓓV1) (#0) W2
27       ) → (∀n,G,K,V1,V2,W2. ❪G,K❫ ⊢ V1 ⬆[h,n] V2 → Q n G K V1 V2 →
28         ⇧[1] V2 ≘ W2 → Q (↑n) G (K.ⓛV1) (#0) W2
29       ) → (∀n,I,G,K,T,U,i. ❪G,K❫ ⊢ #i ⬆[h,n] T → Q n G K (#i) T →
30         ⇧[1] T ≘ U → Q n G (K.ⓘ[I]) (#↑i) (U)
31       ) → (∀n,p,I,G,L,V1,V2,T1,T2. ❪G,L❫ ⊢ V1 ⬆[h,0] V2 → ❪G,L.ⓑ[I]V1❫ ⊢ T1 ⬆[h,n] T2 →
32         Q 0 G L V1 V2 → Q n G (L.ⓑ[I]V1) T1 T2 → Q n G L (ⓑ[p,I]V1.T1) (ⓑ[p,I]V2.T2)
33       ) → (∀n,G,L,V1,V2,T1,T2. ❪G,L❫ ⊢ V1 ⬆[h,0] V2 → ❪G,L❫ ⊢ T1 ⬆[h,n] T2 →
34         Q 0 G L V1 V2 → Q n G L T1 T2 → Q n G L (ⓐV1.T1) (ⓐV2.T2)
35       ) → (∀n,G,L,V1,V2,T1,T2. ❪G,L❫ ⊢ V1 ⬆[h,n] V2 → ❪G,L❫ ⊢ T1 ⬆[h,n] T2 →
36         Q n G L V1 V2 → Q n G L T1 T2 → Q n G L (ⓝV1.T1) (ⓝV2.T2)
37       ) → (∀n,G,L,V1,V2,T. ❪G,L❫ ⊢ V1 ⬆[h,n] V2 →
38         Q n G L V1 V2 → Q (↑n) G L (ⓝV1.T) V2
39       ) →
40       ∀n,G,L,T1,T2. ❪G,L❫ ⊢ T1 ⬆[h,n] T2 → Q n G L T1 T2.
41 #h #Q #IH1 #IH2 #IH3 #IH4 #IH5 #IH6 #IH7 #IH8 #IH9 #n #G #L #T1
42 generalize in match n; -n
43 @(fqu_wf_ind (Ⓣ) … G L T1) -G -L -T1 #G0 #L0 * [| * [| * ]]
44 [ #I #IH #n #X2 #HX2 -IH6 -IH7 -IH8 -IH9
45   elim (cpt_inv_atom_sn … HX2) -HX2 *
46   [ #H1 #H2 destruct -IH2 -IH3 -IH4 -IH5 //
47   | #s #H1 #H2 #H3 destruct -IH1 -IH3 -IH4 -IH5 //
48   | #K #V1 #V2 #HV12 #HVX2 #H1 #H2 destruct -IH1 -IH2 -IH4 -IH5 /3 width=4 by/
49   | #m #K #W1 #W2 #HW12 #HWX2 #H1 #H2 #H3 destruct -IH1 -IH2 -IH3 -IH5 /3 width=4 by/
50   | #J #K #T2 #i #HT2 #HTX2 #H1 #H2 destruct -IH1 -IH2 -IH3 -IH4 /3 width=4 by/
51   ]
52 | #p #I #V1 #T1 #IH #n #X2 #HX2 -IH1 -IH2 -IH3 -IH4 -IH5 -IH7 -IH8 -IH9
53   elim (cpt_inv_bind_sn … HX2) -HX2 #V2 #T2 #HV12 #HT12 #H destruct
54   /4 width=1 by fqu_bind_dx/
55 | #V1 #T1 #IH #n #X2 #HX2 -IH1 -IH2 -IH3 -IH4 -IH5 -IH6 -IH8 -IH9
56   elim (cpt_inv_appl_sn … HX2) -HX2 #V2 #T2 #HV12 #HT12 #H destruct /3 width=1 by/
57 | #U1 #T1 #IH #n #X2 #HX2 -IH1 -IH2 -IH3 -IH4 -IH5 -IH6 -IH7
58   elim (cpt_inv_cast_sn … HX2) -HX2 *
59   [ #U2 #T2 #HU12 #HT12 #H destruct -IH9 /3 width=1 by/
60   | #m #Hm #H destruct -IH8 /3 width=1 by/
61   ]
62 ]
63 qed-.