1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "basic_2/dynamic/cnv_cpm_conf.ma".
16 include "basic_2/dynamic/cnv_cpms_teqx_conf.ma".
18 (* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************)
20 (* Sub confluence propery with t-bound rt-computation for terms *************)
22 fact cnv_cpms_conf_lpr_teqx_teqx_aux (h) (a) (G0) (L0) (T0):
23 (∀G,L,T. ❨G0,L0,T0❩ > ❨G,L,T❩ → IH_cnv_cpm_trans_lpr h a G L T) →
24 (∀G,L,T. ❨G0,L0,T0❩ > ❨G,L,T❩ → IH_cnv_cpms_conf_lpr h a G L T) →
26 ∀n1,T1. ❨G0,L0❩ ⊢ T0 ➡*[h,n1] T1 → T0 ≅ T1 →
27 ∀n2,T2. ❨G0,L0❩ ⊢ T0 ➡*[h,n2] T2 → T0 ≅ T2 →
28 ∀L1. ❨G0,L0❩ ⊢ ➡[h,0] L1 → ∀L2. ❨G0,L0❩ ⊢ ➡[h,0] L2 →
29 ∃∃T. ❨G0,L1❩ ⊢ T1 ➡*[h,n2-n1] T & ❨G0,L2❩ ⊢ T2 ➡*[h,n1-n2] T.
30 #h #a #G #L0 #T0 #IH2 #IH1 #HT0
31 #n1 #T1 #H1T01 #H2T01 #n2 #T2 #H1T02 #H2T02
33 elim (cnv_cpms_teqx_conf_lpr_aux … IH2 IH1 … H1T01 … H1T02 … HL01 … HL02) -IH2 -IH1 -H1T01 -H1T02 -HL01 -HL02
34 /2 width=3 by ex2_intro/
37 fact cnv_cpms_conf_lpr_refl_tneqx_sub (h) (a) (G0) (L0) (T0) (m21) (m22):
38 (∀G,L,T. ❨G0,L0,T0❩ > ❨G,L,T❩ → IH_cnv_cpm_trans_lpr h a G L T) →
39 (∀G,L,T. ❨G0,L0,T0❩ > ❨G,L,T❩ → IH_cnv_cpms_conf_lpr h a G L T) →
41 ∀X2. ❨G0,L0❩ ⊢ T0 ➡[h,m21] X2 → (T0 ≅ X2 → ⊥) → ∀T2. ❨G0,L0❩ ⊢ X2 ➡*[h,m22] T2 →
42 ∀L1. ❨G0,L0❩ ⊢ ➡[h,0] L1 → ∀L2. ❨G0,L0❩ ⊢ ➡[h,0] L2 →
43 ∃∃T. ❨G0,L1❩ ⊢ T0 ➡*[h,m21+m22] T& ❨G0,L2❩ ⊢ T2 ➡*[h,0] T.
44 #h #a #G0 #L0 #T0 #m21 #m22 #IH2 #IH1 #H0
45 #X2 #HX02 #HnX02 #T2 #HXT2
47 lapply (cnv_cpm_trans_lpr_aux … IH1 IH2 … HX02 … L0 ?) // #HX2
48 elim (cnv_cpm_conf_lpr_aux … IH2 IH1 … HX02 … 0 T0 … L0 … HL01) //
49 <minus_n_O <minus_O_n #Y1 #HXY1 #HTY1
50 elim (cnv_cpms_strip_lpr_sub … IH1 … HXT2 0 X2 … HL02 L0) [|*: /4 width=3 by fpbc_fpbg, cpm_fwd_fpbc/ ]
51 <minus_n_O <minus_O_n #Y2 #HTY2 #HXY2 -HXT2
52 elim (IH1 … HXY1 … HXY2 … HL01 … HL02) [|*: /4 width=3 by fpbc_fpbg, cpm_fwd_fpbc/ ]
53 -a -L0 -X2 <minus_n_O <minus_O_n #Y #HY1 #HY2
54 lapply (cpms_trans … HTY1 … HY1) -Y1 #HT0Y
55 lapply (cpms_trans … HTY2 … HY2) -Y2 #HT2Y
56 /2 width=3 by ex2_intro/
59 fact cnv_cpms_conf_lpr_step_tneqx_sub (h) (a) (G0) (L0) (T0) (m11) (m12) (m21) (m22):
60 (∀G,L,T. ❨G0,L0,T0❩ > ❨G,L,T❩ → IH_cnv_cpm_trans_lpr h a G L T) →
61 (∀G,L,T. ❨G0,L0,T0❩ > ❨G,L,T❩ → IH_cnv_cpms_conf_lpr h a G L T) →
63 ∀X1. ❨G0,L0❩ ⊢ T0 ➡[h,m11] X1 → T0 ≅ X1 → ∀T1. ❨G0,L0❩ ⊢ X1 ➡*[h,m12] T1 → X1 ≅ T1 →
64 ∀X2. ❨G0,L0❩ ⊢ T0 ➡[h,m21] X2 → (T0 ≅ X2 → ⊥) → ∀T2. ❨G0,L0❩ ⊢ X2 ➡*[h,m22] T2 →
65 ∀L1. ❨G0,L0❩ ⊢ ➡[h,0] L1 → ∀L2. ❨G0,L0❩ ⊢ ➡[h,0] L2 →
66 ((∀G,L,T. ❨G0,L0,X1❩ > ❨G,L,T❩ → IH_cnv_cpm_trans_lpr h a G L T) →
67 (∀G,L,T. ❨G0,L0,X1❩ > ❨G,L,T❩ → IH_cnv_cpms_conf_lpr h a G L T) →
69 ∀X2. ❨G0,L0❩ ⊢ X1 ➡[h,m21] X2 → (X1 ≅ X2 → ⊥) →
70 ∀T2. ❨G0,L0❩ ⊢ X2 ➡*[h,m22] T2 →
71 ∀L1. ❨G0,L0❩ ⊢ ➡[h,0] L1 → ∀L2. ❨G0,L0❩ ⊢ ➡[h,0] L2 →
72 ∃∃T. ❨G0,L1❩ ⊢ T1 ➡*[h,m21+m22-m12] T & ❨G0,L2❩ ⊢ T2 ➡*[h,m12-(m21+m22)]T
74 ∃∃T. ❨G0,L1❩ ⊢ T1 ➡*[h,m21+m22-(m11+m12)] T & ❨G0,L2❩ ⊢ T2 ➡*[h,m11+m12-(m21+m22)] T.
75 #h #a #G0 #L0 #T0 #m11 #m12 #m21 #m22 #IH2 #IH1 #HT0
76 #X1 #H1X01 #H2X01 #T1 #H1XT1 #H2XT1 #X2 #H1X02 #H2X02 #T2 #HXT2
77 #L1 #HL01 #L2 #HL02 #IH
78 lapply (cnv_cpm_trans_lpr_aux … IH1 IH2 … H1X01 … L0 ?) // #HX1
79 lapply (cnv_cpm_trans_lpr_aux … IH1 IH2 … H1X02 … L0 ?) // #HX2
80 elim (cnv_cpm_conf_lpr_aux … IH2 IH1 … H1X01 … H1X02 … L0 … L0) // #Z0 #HXZ10 #HXZ20
81 cut (❨G0, L0, T0❩ > ❨G0, L0, X2❩) [ /4 width=5 by cpms_fwd_fpbs, cpm_fwd_fpbc, fpbc_fpbs_fpbg/ ] #H1fpbg (**) (* cut *)
82 lapply (fpbg_fpbs_trans … H1fpbg G0 L0 Z0 ?) [ /2 width=3 by cpms_fwd_fpbs/ ] #H2fpbg
83 lapply (cnv_cpms_trans_lpr_sub … IH2 … HXZ20 … L0 ?) // #HZ0
84 elim (IH1 … HXT2 … HXZ20 … L2 … L0) [|*: /4 width=2 by fpbc_fpbg, cpm_fwd_fpbc/ ] -HXT2 -HXZ20 #Z2 #HTZ2 #HZ02
85 elim (teqx_dec X1 Z0) #H2XZ
87 elim (cnv_cpms_conf_lpr_teqx_teqx_aux … HX1 … H1XT1 H2XT1 … HXZ10 H2XZ … L1 … L0)
88 [2,3: // |4,5: /4 width=5 by cpm_fwd_fpb, fpb_fpbg_trans/ ]
90 elim (cpms_tneqx_fwd_step_sn_aux … HXZ10 HX1 H2XZ) [|*: /4 width=5 by cpm_fwd_fpb, fpb_fpbg_trans/ ]
91 -HXZ10 -H2XZ #n1 #n2 #X0 #H1X10 #H2X10 #HXZ0 #Hn
92 elim (IH … H1X10 H2X10 … HXZ0 … L1 … L0) [2,3: // |4,5: /4 width=5 by cpm_fwd_fpb, fpb_fpbg_trans/ ]
96 elim (IH1 … HZ01 … HZ02 L1 … L2) // -L0 -T0 -X1 -X2 -Z0 #Z #HZ01 #HZ02
97 lapply (cpms_trans … HTZ1 … HZ01) -Z1 <arith_l4 #HT1Z
98 lapply (cpms_trans … HTZ2 … HZ02) -Z2 <arith_l4 #HT2Z
99 /2 width=3 by ex2_intro/
102 fact cnv_cpms_conf_lpr_teqx_tneqx_aux (h) (a) (G0) (L0) (T0) (n1) (m21) (m22):
103 (∀G,L,T. ❨G0,L0,T0❩ > ❨G,L,T❩ → IH_cnv_cpm_trans_lpr h a G L T) →
104 (∀G,L,T. ❨G0,L0,T0❩ > ❨G,L,T❩ → IH_cnv_cpms_conf_lpr h a G L T) →
105 ❨G0,L0❩ ⊢ T0 ![h,a] →
106 ∀T1. ❨G0,L0❩ ⊢ T0 ➡*[h,n1] T1 → T0 ≅ T1 →
107 ∀X2. ❨G0,L0❩ ⊢ T0 ➡[h,m21] X2 → (T0 ≅ X2 → ⊥) → ∀T2. ❨G0,L0❩ ⊢ X2 ➡*[h,m22] T2 →
108 ∀L1. ❨G0,L0❩ ⊢ ➡[h,0] L1 → ∀L2. ❨G0,L0❩ ⊢ ➡[h,0] L2 →
109 ∃∃T. ❨G0,L1❩ ⊢ T1 ➡*[h,m21+m22-n1] T & ❨G0,L2❩ ⊢ T2 ➡*[h,n1-(m21+m22)] T.
110 #h #a #G0 #L0 #T0 #n1 #m21 #m22 #IH2 #IH1 #HT0
112 generalize in match m22; generalize in match m21; -m21 -m22
113 generalize in match IH1; generalize in match IH2;
114 @(cpms_teqx_ind_sn … H1T01 HT0 H2T01 IH1 IH2) -n1 -T0
115 [ #HT1 #IH2 #IH1 #m21 #m22
116 #X2 #HX02 #HnX02 #T2 #HXT2 #L1 #HL01 #L2 #HL02
117 <minus_O_n <minus_n_O
118 @(cnv_cpms_conf_lpr_refl_tneqx_sub … IH2 IH1) -IH2 -IH1 /2 width=4 by/
119 | #m11 #m12 #T0 #X1 #H1X01 #HT0 #H2X01 #H1XT1 #_ #H2XT1 #IH #IH2 #IH1 #m21 #m22
120 #X2 #HX02 #HnX02 #T2 #HXT2 #L1 #HL01 #L2 #HL02
121 @(cnv_cpms_conf_lpr_step_tneqx_sub … IH2 IH1 … IH) -IH2 -IH1 -IH /2 width=4 by/
125 fact cnv_cpms_conf_lpr_tneqx_tneqx_aux (h) (a) (G0) (L0) (T0) (m11) (m12) (m21) (m22):
126 (∀G,L,T. ❨G0,L0,T0❩ > ❨G,L,T❩ → IH_cnv_cpm_trans_lpr h a G L T) →
127 (∀G,L,T. ❨G0,L0,T0❩ > ❨G,L,T❩ → IH_cnv_cpms_conf_lpr h a G L T) →
128 ❨G0,L0❩ ⊢ T0 ![h,a] →
129 ∀X1. ❨G0,L0❩ ⊢ T0 ➡[h,m11] X1 → (T0 ≅ X1 → ⊥) → ∀T1. ❨G0,L0❩ ⊢ X1 ➡*[h,m12] T1 →
130 ∀X2. ❨G0,L0❩ ⊢ T0 ➡[h,m21] X2 → (T0 ≅ X2 → ⊥) → ∀T2. ❨G0,L0❩ ⊢ X2 ➡*[h,m22] T2 →
131 ∀L1. ❨G0,L0❩ ⊢ ➡[h,0] L1 → ∀L2. ❨G0,L0❩ ⊢ ➡[h,0] L2 →
132 ∃∃T. ❨G0,L1❩ ⊢ T1 ➡*[h,m21+m22-(m11+m12)] T & ❨G0,L2❩ ⊢ T2 ➡*[h,m11+m12-(m21+m22)] T.
133 #h #a #G0 #L0 #T0 #m11 #m12 #m21 #m22 #IH2 #IH1 #H0
134 #X1 #HX01 #HnX01 #T1 #HXT1 #X2 #HX02 #HnX02 #T2 #HXT2
136 lapply (cnv_cpm_trans_lpr_aux … IH1 IH2 … HX01 … L0 ?) // #HX1
137 lapply (cnv_cpm_trans_lpr_aux … IH1 IH2 … HX02 … L0 ?) // #HX2
138 elim (cnv_cpm_conf_lpr_aux … IH2 IH1 … HX01 … HX02 … L0 … L0) // #Z0 #HXZ10 #HXZ20
139 cut (❨G0, L0, T0❩ > ❨G0, L0, X1❩) [ /4 width=5 by cpms_fwd_fpbs, cpm_fwd_fpbc, fpbc_fpbs_fpbg/ ] #H1fpbg (**) (* cut *)
140 lapply (fpbg_fpbs_trans … H1fpbg G0 L0 Z0 ?) [ /2 width=3 by cpms_fwd_fpbs/ ] #H2fpbg
141 lapply (cnv_cpms_trans_lpr_sub … IH2 … HXZ10 … L0 ?) // #HZ0
142 elim (IH1 … HXT1 … HXZ10 … L1 … L0) [|*: /4 width=2 by fpbc_fpbg, cpm_fwd_fpbc/ ] -HXT1 -HXZ10 #Z1 #HTZ1 #HZ01
143 elim (IH1 … HXT2 … HXZ20 … L2 … L0) [|*: /4 width=3 by fpbc_fpbg, cpm_fwd_fpbc/ ] -HXT2 -HXZ20 #Z2 #HTZ2 #HZ02
144 elim (IH1 … HZ01 … HZ02 L1 … L2) // -L0 -T0 -X1 -X2 -Z0 #Z #HZ01 #HZ02
145 lapply (cpms_trans … HTZ1 … HZ01) -Z1 <arith_l4 #HT1Z
146 lapply (cpms_trans … HTZ2 … HZ02) -Z2 <arith_l4 #HT2Z
147 /2 width=3 by ex2_intro/
150 fact cnv_cpms_conf_lpr_aux (h) (a) (G0) (L0) (T0):
151 (∀G,L,T. ❨G0,L0,T0❩ > ❨G,L,T❩ → IH_cnv_cpm_trans_lpr h a G L T) →
152 (∀G,L,T. ❨G0,L0,T0❩ > ❨G,L,T❩ → IH_cnv_cpms_conf_lpr h a G L T) →
153 ∀G,L,T. G0 = G → L0 = L → T0 = T → IH_cnv_cpms_conf_lpr h a G L T.
154 #h #a #G #L #T #IH2 #IH1 #G0 #L0 #T0 #HG #HL #HT
155 #HT0 #n1 #T1 #HT01 #n2 #T2 #HT02 #L1 #HL01 #L2 #HL02 destruct
156 elim (teqx_dec T0 T1) #H2T01
157 elim (teqx_dec T0 T2) #H2T02
158 [ @(cnv_cpms_conf_lpr_teqx_teqx_aux … IH2 IH1) -IH2 -IH1 /2 width=1 by/
159 | elim (cpms_tneqx_fwd_step_sn_aux … HT02 HT0 H2T02 IH1 IH2) -HT02 -H2T02
160 #m21 #m22 #X2 #HX02 #HnX02 #HXT2 #H2 destruct
161 @(cnv_cpms_conf_lpr_teqx_tneqx_aux … IH2 IH1) -IH2 -IH1 /2 width=4 by/
162 | elim (cpms_tneqx_fwd_step_sn_aux … HT01 HT0 H2T01 IH1 IH2) -HT01 -H2T01
163 #m11 #m12 #X1 #HX01 #HnX01 #HXT1 #H1 destruct
164 @ex2_commute @(cnv_cpms_conf_lpr_teqx_tneqx_aux … IH2 IH1) -IH2 -IH1 /2 width=4 by/
165 | elim (cpms_tneqx_fwd_step_sn_aux … HT01 HT0 H2T01 IH1 IH2) -HT01 -H2T01
166 elim (cpms_tneqx_fwd_step_sn_aux … HT02 HT0 H2T02 IH1 IH2) -HT02 -H2T02
167 #m21 #m22 #X2 #HX02 #HnX02 #HXT2 #H2 #m11 #m12 #X1 #HX01 #HnX01 #HXT1 #H1 destruct
168 @(cnv_cpms_conf_lpr_tneqx_tneqx_aux … IH2 IH1) -IH2 -IH1 /2 width=4 by/