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/rt_transition/cpm_drops.ma".
16 include "basic_2/rt_transition/cpr.ma".
17 include "apps_2/functional/mf_exteq.ma".
19 (* MULTIPLE FILLING FOR TERMS ***********************************************)
21 (* Properties with relocation ***********************************************)
23 lemma mf_delta_drops (h) (G): ∀K,V1,V2. ❨G,K❩ ⊢ V1 ➡[h,0] V2 →
24 ∀T,L,i. ⇩[i] L ≘ K.ⓓV1 →
25 ∀gv,lv. ❨G,L❩ ⊢ ●[gv,⇡[i←#i]lv]T ➡[h,0] ●[gv,⇡[i←↑[↑i]V2]lv]T.
26 #h #G #K #V1 #V2 #HV #T elim T -T * //
27 [ #i #L #j #HKL #gv #lv
29 elim (lt_or_eq_or_gt i j) #Hj destruct
30 [ >(mf_vpush_lt … Hj) >(mf_vpush_lt … Hj) //
31 | >mf_vpush_eq >mf_vpush_eq
32 /2 width=6 by cpm_delta_drops/
33 | >(mf_vpush_gt … Hj) >(mf_vpush_gt … Hj) //
35 | #p #I #V #T #IHV #IHT #L #j #HLK #gv #lv
37 >(mf_comp … T) in ⊢ (?????%?);
38 [2: @mf_vpush_swap // |4: @exteq_refl |3,5: skip ]
39 >(mf_comp … T) in ⊢ (??????%);
40 [2: @mf_vpush_swap // |4: @exteq_refl |3,5: skip ]
41 >(flifts_lref_uni 1 j) >(flifts_compose_uni 1 (↑j))
42 /4 width=1 by cpm_bind, drops_drop/
43 | #I #V #T #IHV #IHT #L #j #HLK #gv #lv
44 >mf_flat >mf_flat /3 width=1 by cpr_flat/