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] V2 →
24 ∀T,L,l. ⇩*[l] L ≘ K.ⓓV1 →
25 ∀gv,lv. ⦃G,L⦄ ⊢ ●[gv,⇡[l←#l]lv]T ➡[h] ●[gv,⇡[l←↑[↑l]V2]lv]T.
26 #h #G #K #V1 #V2 #HV #T elim T -T * //
27 [ #i #L #l #HKL #gv #lv
29 elim (lt_or_eq_or_gt i l) #Hl destruct
30 [ >(mf_vpush_lt … Hl) >(mf_vpush_lt … Hl) //
31 | >mf_vpush_eq >mf_vpush_eq
32 /2 width=6 by cpm_delta_drops/
33 | >(mf_vpush_gt … Hl) >(mf_vpush_gt … Hl) //
35 | #p #I #V #T #IHV #IHT #L #l #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 l) >(flifts_compose_uni 1 (↑l))
42 /4 width=1 by cpm_bind, drops_drop/
43 | #I #V #T #IHV #IHT #L #l #HLK #gv #lv
44 >mf_flat >mf_flat /3 width=1 by cpr_flat/