interpretation "uniform functional relocation (term)"
'UpArrow i T = (flifts (uni i) T).
+(* Basic properties *********************************************************)
+
+lemma flifts_lref (f) (i): ↑*[f](#i) = #(f@❴i❵).
+// qed.
+
+lemma flifts_bind (f) (p) (I) (V) (T): ↑*[f](ⓑ{p,I}V.T) = ⓑ{p,I}↑*[f]V.↑*[⫯f]T.
+// qed.
+
+lemma flifts_flat (f) (I) (V) (T): ↑*[f](ⓕ{I}V.T) = ⓕ{I}↑*[f]V.↑*[f]T.
+// qed.
+
(* Main properties **********************************************************)
theorem flifts_lifts: ∀T,f. ⬆*[f]T ≘ ↑*[f]T.
(* Derived properties *******************************************************)
+lemma flifts_comp: ∀f1,f2. f1 ≡ f2 → ∀T. ↑*[f1]T = ↑*[f2]T.
+/3 width=3 by flifts_inv_lifts, lifts_eq_repl_fwd/ qed.
+
+(* Derived properties with uniform relocation *******************************)
+
lemma flifts_lref_uni: ∀l,i. ↑[l](#i) = #(l+i).
/3 width=1 by flifts_inv_lifts, lifts_lref_uni/ qed.
-(*
-lemma flift_join: ∀e1,e2,T. ⬆[e1, e2] ↑[0, e1] T ≡ ↑[0, e1 + e2] T.
-#e1 #e2 #T
-lapply (flift_lift T 0 (e1+e2)) #H
-elim (lift_split … H e1 e1) -H // #U #H
->(flift_inv_lift … H) -H //
-qed.
-*)
(* *)
(**************************************************************************)
-include "ground_2/relocation/rtmap_basic.ma".
+include "ground_2/relocation/nstream_basic.ma".
include "apps_2/functional/flifts.ma".
include "apps_2/notation/functional/uparrow_3.ma".
-(* GENERIC FUNCTIONAL RELOCATION ********************************************)
+(* BASIC FUNCTIONAL RELOCATION **********************************************)
interpretation "basic functional relocation (term)"
'UpArrow d h T = (flifts (basic d h) T).
+
+(* Basic properties *********************************************************)
+
+lemma flifts_basic_lref_ge (i) (d) (h): d ≤ i → ↑[d,h](#i) = #(h+i).
+#i #d #h #Hdi
+/4 width=1 by apply_basic_ge, (* 2x *) eq_f/
+qed-.
+
+lemma flifts_basic_bind (p) (I) (V) (T) (d) (h): ↑[d,h](ⓑ{p,I}V.T) = ⓑ{p,I}(↑[d,h]V).(↑[↑d,h]T).
+// qed.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "static_2/relocation/lifts_lifts.ma".
+include "apps_2/functional/flifts.ma".
+
+(* GENERIC FUNCTIONAL RELOCATION ********************************************)
+
+(* Main derived properties **************************************************)
+
+theorem flifts_compose (f2) (f1) (T): ↑*[f2]↑*[f1]T = ↑*[f2∘f1]T.
+#f2 #f1 #T
+elim (lifts_total T f1) #U #HTU
+>(flifts_inv_lifts … HTU)
+/4 width=6 by flifts_inv_lifts, lifts_trans, sym_eq/
+qed.
+
+(* Main derived properties with uniform relocation **************************)
+
+theorem flifts_compose_uni (l2) (l1) (T): ↑[l2]↑[l1]T = ↑[l2+l1]T.
+#l2 #l1 #T >flifts_compose
+/4 width=1 by flifts_inv_lifts, lifts_uni, sym_eq/ qed.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "apps_2/functional/flifts_flifts.ma".
+include "apps_2/functional/flifts_basic.ma".
+
+(* BASIC FUNCTIONAL RELOCATION **********************************************)
+
+(* Main properties **********************************************************)
+
+theorem flifts_basic_swap (T) (d1) (d2) (h1) (h2):
+ d2 ≤ d1 → ↑[d2,h2]↑[d1,h1]T = ↑[h2+d1,h1]↑[d2,h2]T.
+/3 width=1 by flifts_comp, basic_swap/ qed-.
+(*
+lemma flift_join: ∀e1,e2,T. ⬆[e1, e2] ↑[0, e1] T ≡ ↑[0, e1 + e2] T.
+#e1 #e2 #T
+lapply (flift_lift T 0 (e1+e2)) #H
+elim (lift_split … H e1 e1) -H // #U #H
+>(flift_inv_lift … H) -H //
+qed.
+*)
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "apps_2/notation/functional/blackcircle_3.ma".
+include "apps_2/functional/mf_vlift.ma".
+include "apps_2/functional/mf_vpush.ma".
+
+(* MULTIPLE FILLING FOR TERMS ***********************************************)
+
+rec definition mf gv lv T on T ≝ match T with
+[ TAtom I ⇒ match I with
+ [ Sort _ ⇒ T
+ | LRef i ⇒ lv i
+ | GRef l ⇒ gv l
+ ]
+| TPair I V T ⇒ match I with
+ [ Bind2 _ _ ⇒ TPair I (mf gv lv V) (mf (⇡[0]gv) (⇡[0←#0]lv) T)
+ | Flat2 _ ⇒ TPair I (mf gv lv V) (mf gv lv T)
+ ]
+].
+
+interpretation "term filling (multiple filling)"
+ 'BlackCircle gv lv T = (mf gv lv T).
+
+(* Basic Properties *********************************************************)
+
+lemma mf_sort: ∀gv,lv,s. ●[gv,lv]⋆s = ⋆s.
+// qed.
+
+lemma mf_lref: ∀gv,lv,i. ●[gv,lv]#i = lv i.
+// qed.
+
+lemma mf_gref: ∀gv,lv,l. ●[gv,lv]§l = gv l.
+// qed.
+
+lemma mf_bind (p) (I): ∀gv,lv,V,T.
+ ●[gv,lv]ⓑ{p,I}V.T = ⓑ{p,I}●[gv,lv]V.●[⇡[0]gv,⇡[0←#0]lv]T.
+// qed.
+
+lemma mf_flat (I): ∀gv,lv,V,T.
+ ●[gv,lv]ⓕ{I}V.T = ⓕ{I}●[gv,lv]V.●[gv,lv]T.
+// qed.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/rt_transition/cpm_drops.ma".
+include "basic_2/rt_transition/cpr.ma".
+include "apps_2/functional/mf_exteq.ma".
+
+(* MULTIPLE FILLING FOR TERMS ***********************************************)
+
+(* Properties with relocation ***********************************************)
+
+lemma mf_delta_drops (h) (G): ∀K,V1,V2. ⦃G, K⦄ ⊢ V1 ➡[h] V2 →
+ ∀T,L,l. ⬇*[l] L ≘ K.ⓓV1 →
+ ∀gv,lv. ⦃G, L⦄ ⊢ ●[gv,⇡[l←#l]lv]T ➡[h] ●[gv,⇡[l←↑[↑l]V2]lv]T.
+#h #G #K #V1 #V2 #HV #T elim T -T * //
+[ #i #L #l #HKL #gv #lv
+ >mf_lref >mf_lref
+ elim (lt_or_eq_or_gt i l) #Hl destruct
+ [ >(mf_vpush_lt … Hl) >(mf_vpush_lt … Hl) //
+ | >mf_vpush_eq >mf_vpush_eq
+ /2 width=6 by cpm_delta_drops/
+ | >(mf_vpush_gt … Hl) >(mf_vpush_gt … Hl) //
+ ]
+| #p #I #V #T #IHV #IHT #L #l #HLK #gv #lv
+ >mf_bind >mf_bind
+ >(mf_comp … T) in ⊢ (?????%?);
+ [2: @mf_vpush_swap // |4: @exteq_refl |3,5: skip ]
+ >(mf_comp … T) in ⊢ (??????%);
+ [2: @mf_vpush_swap // |4: @exteq_refl |3,5: skip ]
+ >(flifts_lref_uni 1 l) >(flifts_compose_uni 1 (↑l))
+ /4 width=1 by cpm_bind, drops_drop/
+| #I #V #T #IHV #IHT #L #l #HLK #gv #lv
+ >mf_flat >mf_flat /3 width=1 by cpr_flat/
+]
+qed.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "apps_2/functional/mf_vlift_exteq.ma".
+include "apps_2/functional/mf_vpush_exteq.ma".
+include "apps_2/functional/mf.ma".
+
+(* MULTIPLE FILLING FOR TERMS ***********************************************)
+
+(* Properties with extensional equivalence **********************************)
+
+lemma mf_comp (T): compatible_3 … (λgv,lv.●[gv,lv]T) (exteq …) (exteq …) (eq …).
+#T elim T -T *
+[ //
+| #i #gv1 #gv2 #Hgv #lv1 #lv2 #Hlv
+ whd in ⊢ (??%%); //
+| #i #gv1 #gv2 #Hgv #lv1 #lv2 #Hlv
+ whd in ⊢ (??%%); //
+| #p #I #V #T #IHV #IHT #gv1 #gv2 #Hgv #lv1 #lv2 #Hlv
+ whd in ⊢ (??%%); /4 width=1 by mf_vlift_comp, mf_vpush_comp, eq_f3/
+| #I #V #T #IHV #IHT #gv1 #gv2 #Hgv #lv1 #lv2 #Hlv
+ whd in ⊢ (??%%); /3 width=1 by eq_f3/
+]
+qed-.
+
+(* Advanced properties ******************************************************)
+
+lemma mf_id (T): ●[mf_gi,mf_li]T = T.
+#T elim T -T * //
+[ #p #I #V #T #IHV #IHT
+ <IHV in ⊢ (???%); <IHT in ⊢ (???%); -IHV -IHT
+ whd in ⊢ (??%?); /3 width=1 by mf_comp, eq_f3/
+| #I #V #T #IHV #IHT
+ <IHV in ⊢ (???%); <IHT in ⊢ (???%); -IHV -IHT //
+]
+qed.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "apps_2/functional/mf_vpush_vlift.ma".
+include "apps_2/functional/mf_exteq.ma".
+
+(* MULTIPLE FILLING FOR TERMS ***********************************************)
+
+(* Properties with relocation ***********************************************)
+
+lemma mf_lifts_basic_SO_dx (T) (j): ∀gv,lv. ↑[j,1]●[gv,lv]T = ●[⇡[j]gv,⇡[j]lv]T.
+#T elim T -T * //
+[ #p #I #V #T #IHV #IHT #j #gv #lv
+ >mf_bind >mf_bind >flifts_basic_bind
+ /4 width=1 by mf_comp, mf_vlift_swap, eq_f2/
+| #I #V #T #IHV #IHT #j #gv #lv
+ >mf_flat >mf_flat >flifts_flat
+ //
+]
+qed.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "static_2/syntax/term.ma".
+
+(* MULTIPLE FILLING EVALUATION **********************************************)
+
+definition mf_evaluation ≝ nat → term.
+
+definition mf_li: mf_evaluation ≝ λi.#i.
+
+definition mf_gi: mf_evaluation ≝ λl.§l.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "apps_2/notation/functional/dotteduparrow_2.ma".
+include "apps_2/functional/flifts_basic.ma".
+include "apps_2/functional/mf_v.ma".
+
+(* MULTIPLE EVALUATION LIFT *************************************************)
+
+definition mf_vlift (j) (gv): mf_evaluation ≝ λi. ↑[j,1](gv i).
+
+interpretation "lift (multiple_filling)"
+ 'DottedUpArrow i gv = (mf_vlift i gv).
+
+(* Basic properties *********************************************************)
+
+lemma mf_vlift_rw (j) (gv): ∀i. (⇡[j]gv) i = ↑[j,1](gv i).
+// qed.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "ground_2/lib/functions.ma".
+include "ground_2/lib/exteq.ma".
+include "apps_2/functional/flifts_flifts_basic.ma".
+include "apps_2/functional/mf_vlift.ma".
+
+(* MULTIPLE EVALUATION LIFT *************************************************)
+
+(* Properties with extensional equivalence **********************************)
+
+lemma mf_gc_id: ∀j. ⇡[j]mf_gi ≐ mf_gi.
+// qed.
+
+lemma mf_vlift_comp (l): compatible_2 … (mf_vlift l) (exteq …) (exteq …).
+#l #gv1 #gv2 #Hgv #i
+>mf_vlift_rw >mf_vlift_rw //
+qed.
+
+(* Main properties with extensional equivalence *****************************)
+
+theorem mf_vlift_swap: ∀l1,l2. l2 ≤ l1 → ∀v. ⇡[l2]⇡[l1]v ≐ ⇡[↑l1]⇡[l2]v.
+/2 width=1 by flifts_basic_swap/ qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "apps_2/notation/functional/dotteduparrow_3.ma".
+include "apps_2/functional/flifts_basic.ma".
+include "apps_2/functional/mf_v.ma".
+
+(* MULTIPLE FILLING PUSH ****************************************************)
+
+definition mf_vpush (j) (T) (lv): mf_evaluation ≝
+ λi. tri … i j (lv i) T (↑[j,1](lv (↓i))).
+
+interpretation "push (multiple filling)"
+ 'DottedUpArrow i d lv = (mf_vpush i d lv).
+
+(* Basic properties *********************************************************)
+
+lemma mf_vpush_lt (lv) (j) (T): ∀i. i < j → (⇡[j←T]lv) i = lv i.
+/2 width=1 by tri_lt/ qed-.
+
+lemma mf_vpush_eq: ∀lv,T,i. (⇡[i←T]lv) i = T.
+/2 width=1 by tri_eq/ qed.
+
+lemma mf_vpush_gt: ∀lv,T,j,i. j < i → (⇡[j←T]lv) i = ↑[j,1](lv (↓i)).
+/2 width=1 by tri_gt/ qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "ground_2/lib/functions.ma".
+include "ground_2/lib/exteq.ma".
+include "apps_2/functional/flifts_flifts_basic.ma".
+include "apps_2/functional/mf_vpush.ma".
+
+(* MULTIPLE FILLING PUSH ****************************************************)
+
+(* Properties with extensional equivalence **********************************)
+
+lemma mf_lc_id: ⇡[0←#0]mf_li ≐ mf_li.
+#i elim (eq_or_gt i) #Hi destruct //
+>mf_vpush_gt // >(flifts_lref_uni 1) <(S_pred … Hi) in ⊢ (???%); -Hi //
+qed.
+
+lemma mf_vpush_comp (i): compatible_3 … (mf_vpush i) (eq …) (exteq …) (exteq …).
+#i #T1 #T2 #HT12 #lv1 #lv2 #Hlv #j
+elim (lt_or_eq_or_gt j i) #Hij destruct
+[ >mf_vpush_lt // >mf_vpush_lt //
+| >mf_vpush_eq >mf_vpush_eq //
+| >mf_vpush_gt // >mf_vpush_gt //
+]
+qed-.
+
+(* Main properties with extensional equivalence *****************************)
+
+theorem mf_vpush_swap: ∀l1,l2. l2 ≤ l1 →
+ ∀v,T1,T2. ⇡[l2←T2]⇡[l1←T1]v ≐ ⇡[↑l1←↑[l2,1]T1]⇡[l2←T2]v.
+#l1 #l2 #Hl21 #v #T1 #T2 #i
+elim (lt_or_eq_or_gt i l2) #Hl2 destruct
+[ lapply (lt_to_le_to_lt … Hl2 Hl21) #Hl1
+ >mf_vpush_lt // >mf_vpush_lt // >mf_vpush_lt /2 width=1 by lt_S/ >mf_vpush_lt //
+| >mf_vpush_eq >mf_vpush_lt /2 width=1 by monotonic_le_plus_l/
+| >mf_vpush_gt // elim (lt_or_eq_or_gt (↓i) l1) #Hl1 destruct
+ [ >mf_vpush_lt // >mf_vpush_lt /2 width=1 by lt_minus_to_plus/ >mf_vpush_gt //
+ | >mf_vpush_eq <(lt_succ_pred … Hl2) >mf_vpush_eq //
+ | lapply (le_to_lt_to_lt … Hl21 Hl1) -Hl2 #Hl2
+ >mf_vpush_gt // >mf_vpush_gt /2 width=1 by lt_minus_to_plus_r/ >mf_vpush_gt //
+ /2 width=1 by flifts_basic_swap/
+ ]
+]
+qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "apps_2/functional/mf_vlift_exteq.ma".
+include "apps_2/functional/mf_vpush.ma".
+
+(* MULTIPLE FILLING PUSH ****************************************************)
+
+(* Properties with multiple filling lift ************************************)
+
+lemma mf_vpush_vlift_swap_O (v) (T) (l): ⇡[0←↑[↑l,1]T]⇡[l]v ≐⇡[↑l]⇡[0←T]v.
+#v #T #l #i
+elim (eq_or_gt i) #Hi destruct
+[ >mf_vpush_eq >mf_vlift_rw >mf_vpush_eq //
+| >(mf_vpush_gt … Hi) >mf_vlift_rw >mf_vlift_rw >(mf_vpush_gt … Hi)
+ @mf_vlift_swap //
+]
+qed.
+
+lemma mf_vpush_vlift_swap_O_lref_O (v) (l): ⇡[0←#0]⇡[l]v ≐⇡[↑l]⇡[0←#0]v.
+#v #l @(mf_vpush_vlift_swap_O … (#0))
+qed.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "ground_2/lib/functions.ma".
-include "ground_2/lib/exteq.ma".
-include "apps_2/models/tm.ma".
-
-(* TERM MODEL ***************************************************************)
-
-(* Properties with extensional equivalencs of evaluations *******************)
-
-lemma tm_gc_id: ∀j. ⇡[j]tm_gc ≐ tm_gc.
-// qed.
-
-lemma tm_lc_id: ⇡[0←#0]tm_lc ≐ tm_lc.
-#i elim (eq_or_gt i) #Hi destruct //
->tm_vpush_gt // >(flifts_lref_uni 1) <(S_pred … Hi) in ⊢ (???%); -Hi //
-qed.
-
-lemma tm_vlift_comp (l): compatible_2 … (tm_vlift l) (exteq …) (exteq …).
-#l #gv1 #gv2 #Hgv #i
->tm_vlift_rw >tm_vlift_rw //
-qed.
-
-lemma tm_vpush_comp (i): compatible_3 … (tm_vpush i) (eq …) (exteq …) (exteq …).
-#i #T1 #T2 #HT12 #lv1 #lv2 #Hlv #j
-elim (lt_or_eq_or_gt j i) #Hij destruct
-[ >tm_vpush_lt // >tm_vpush_lt //
-| >tm_vpush_eq >tm_vpush_eq //
-| >tm_vpush_gt // >tm_vpush_gt //
-]
-qed-.
-
-lemma tm_ti_comp (T): compatible_3 … (λgv,lv.tm_ti gv lv T) (exteq …) (exteq …) (eq …).
-#T elim T -T *
-[ //
-| #i #gv1 #gv2 #Hgv #lv1 #lv2 #Hlv
- whd in ⊢ (??%%); //
-| #i #gv1 #gv2 #Hgv #lv1 #lv2 #Hlv
- whd in ⊢ (??%%); //
-| #p #I #V #T #IHV #IHT #gv1 #gv2 #Hgv #lv1 #lv2 #Hlv
- whd in ⊢ (??%%); /4 width=1 by tm_vlift_comp, tm_vpush_comp, eq_f3/
-| #I #V #T #IHV #IHT #gv1 #gv2 #Hgv #lv1 #lv2 #Hlv
- whd in ⊢ (??%%); /3 width=1 by eq_f3/
-]
-qed-.
-
-lemma tm_ti_eq (T): tm_ti tm_gc tm_lc T = T.
-#T elim T -T * //
-[ #p #I #V #T #IHV #IHT
- <IHV in ⊢ (???%); <IHT in ⊢ (???%); -IHV -IHT
- whd in ⊢ (??%?); /3 width=1 by tm_ti_comp, eq_f3/
-| #I #V #T #IHV #IHT
- <IHV in ⊢ (???%); <IHT in ⊢ (???%); -IHV -IHT //
-]
-qed.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* NOTATION FOR THE "models" COMPONENT **************************************)
+
+notation "hvbox( ●[ term 46 gv, break term 46 lv ] break term 46 T )"
+ non associative with precedence 46
+ for @{ 'BlackCircle $gv $lv $T }.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* NOTATION FOR THE "models" COMPONENT **************************************)
+
+notation "hvbox( ⇡[ term 46 i ] break term 46 gv )"
+ non associative with precedence 46
+ for @{ 'DottedUpArrow $i $gv }.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* NOTATION FOR THE "models" COMPONENT **************************************)
+
+notation "hvbox( ⇡[ term 46 i ← break term 46 d ] break term 46 lv )"
+ non associative with precedence 46
+ for @{ 'DottedUpArrow $i $d $lv }.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-(* NOTATION FOR THE "models" COMPONENT **************************************)
-
-notation "hvbox( ⇡[ term 46 i ] break term 46 gv )"
- non associative with precedence 46
- for @{ 'DottedUpArrow $i $gv }.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-(* NOTATION FOR THE "models" COMPONENT **************************************)
-
-notation "hvbox( ⇡[ term 46 i ← break term 46 d ] break term 46 lv )"
- non associative with precedence 46
- for @{ 'DottedUpArrow $i $d $lv }.
class "yellow"
[ { "models" * } {
[ { "term model" * } {
- [ "tm" + "( ⇡[?]? )" + "( ⇡[?←?]? )"
- "tm_exteq"
- * ]
+ [ "tm" * ]
}
]
[ { "denotational equivalence" * } {
*)
class "orange"
[ { "functional" * } {
-(*
- [ { "reduction and type machine" * } {
- [ "rtm" "rtm_step ( ? ⇨ ? )" * ]
+ [ { "multiple filling" * } {
+ [ "mf" + "( ●[?,?]? )" "mf_exeq" "mf_lifts" "mf_cpr" *]
+ [ "mf_vpush" + "( ⇡[?←?]? )" "mf_vpush_exteq" "mf_vpush_vlift" * ]
+ [ "mf_vlift" + "( ⇡[?]? )" "mf_vlift_exteq" * ]
+ [ "mf_v" * ]
}
]
-*)
[ { "relocation" * } {
- [ "flifts" + "( ↑*[?]? )" + "( ↑[?]? )"
- "flifts_basic" + "( ↑[?,?]? )"
- * ]
+ [ "flifts_basic" + "( ↑[?,?]? )" "flifts_flifts_basic" * ]
+ [ "flifts" + "( ↑*[?]? )" + "( ↑[?]? )" "flifts_flifts" * ]
}
]
}
[ "vdrop" + "( ⫰{?}? )" + "( ⫰{?}[?]? )" "vdrop_vlift" * ]
}
]
+ [ { "reduction and type machine" * } {
+ [ "rtm" "rtm_step ( ? ⇨ ? )" * ]
+ }
+ ]
*)
["M"; "ℳ"; "𝕄"; "𝐌"; "Ⓜ"; ] ;
["n"; "𝕟"; "𝐧"; "𝛈"; "ⓝ"; ] ;
["N"; "ℕ"; "№"; "𝐍"; "Ⓝ"; ] ;
- ["o"; "θ"; "ϑ"; "𝕠"; "∘"; "⊚"; "ø"; "○"; "𝐨"; "𝛉"; "ⓞ"; ] ;
+ ["o"; "θ"; "ϑ"; "𝕠"; "∘"; "⊚"; "ø"; "○"; "●"; "𝐨"; "𝛉"; "ⓞ"; ] ;
["O"; "Θ"; "𝕆"; "𝐎"; "𝚯"; "𝚹"; "Ⓞ"; ] ;
["p"; "π"; "𝕡"; "𝐩"; "𝛑"; "ⓟ"; ] ;
["P"; "Π"; "℘"; "ℙ"; "𝐏"; "𝚷"; "Ⓟ"; ] ;
projects / helm.git / commitdiff