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/unfold/ltpss_tps.ma".
16 include "basic_2/unfold/ltpsss.ma".
18 (* ITERATED PARTIAL UNFOLD ON LOCAL ENVIRONMENTS ****************************)
20 (* Properties concerning partial substitution on terms **********************)
22 lemma ltpsss_tps_trans_ge: ∀L1,L0,d1,e1. L1 [d1, e1] ▶** L0 →
23 ∀T2,U2,d2,e2. L0 ⊢ T2 [d2, e2] ▶ U2 →
24 d1 + e1 ≤ d2 → L1 ⊢ T2 [d2, e2] ▶ U2.
25 #L1 #L0 #d1 #e1 #H @(ltpsss_ind … H) -L0 //
26 #L #L0 #_ #HL0 #IHL #T2 #U2 #d2 #e2 #HTU2 #Hde1d2
27 lapply (ltpss_tps_trans_ge … HTU2 … HL0 ?) -HL0 -HTU2 // /2 width=1/
30 lemma ltpsss_tps_conf_ge: ∀L0,L1,T2,U2,d1,e1,d2,e2. d1 + e1 ≤ d2 →
31 L0 ⊢ T2 [d2, e2] ▶ U2 → L0 [d1, e1] ▶** L1 →
32 L1 ⊢ T2 [d2, e2] ▶ U2.
33 #L0 #L1 #T2 #U2 #d1 #e1 #d2 #e2 #Hde1d2 #HTU2 #H @(ltpsss_ind … H) -L1 //
34 -HTU2 #L #L1 #_ #HL1 #IHL
35 lapply (ltpss_tps_conf_ge … IHL … HL1 ?) -HL1 -IHL //