(* Basic Properties *********************************************************)
-lemma mf_sort: â\88\80gv,lv,s. â\97\8f[gv,lv]⋆s = ⋆s.
+lemma mf_sort: â\88\80gv,lv,s. â\96 [gv,lv]⋆s = ⋆s.
// qed.
-lemma mf_lref: â\88\80gv,lv,i. â\97\8f[gv,lv]#i = lv i.
+lemma mf_lref: â\88\80gv,lv,i. â\96 [gv,lv]#i = lv i.
// qed.
-lemma mf_gref: â\88\80gv,lv,l. â\97\8f[gv,lv]§l = gv l.
+lemma mf_gref: â\88\80gv,lv,l. â\96 [gv,lv]§l = gv l.
// qed.
lemma mf_bind (p) (I): ∀gv,lv,V,T.
- â\97\8f[gv,lv]â\93\91[p,I]V.T = â\93\91[p,I]â\97\8f[gv,lv]V.â\97\8f[⇡[0]gv,⇡[0←#0]lv]T.
+ â\96 [gv,lv]â\93\91[p,I]V.T = â\93\91[p,I]â\96 [gv,lv]V.â\96 [⇡[0]gv,⇡[0←#0]lv]T.
// qed.
lemma mf_flat (I): ∀gv,lv,V,T.
- â\97\8f[gv,lv]â\93\95[I]V.T = â\93\95[I]â\97\8f[gv,lv]V.â\97\8f[gv,lv]T.
+ â\96 [gv,lv]â\93\95[I]V.T = â\93\95[I]â\96 [gv,lv]V.â\96 [gv,lv]T.
// qed.
lemma mf_delta_drops (h) (G): ∀K,V1,V2. ❨G,K❩ ⊢ V1 ➡[h,0] V2 →
∀T,L,i. ⇩[i] L ≘ K.ⓓV1 →
- â\88\80gv,lv. â\9d¨G,Lâ\9d© â\8a¢ â\97\8f[gv,â\87¡[iâ\86\90#i]lv]T â\9e¡[h,0] â\97\8f[gv,⇡[i←↑[↑i]V2]lv]T.
+ â\88\80gv,lv. â\9d¨G,Lâ\9d© â\8a¢ â\96 [gv,â\87¡[iâ\86\90#i]lv]T â\9e¡[h,0] â\96 [gv,⇡[i←↑[↑i]V2]lv]T.
#h #G #K #V1 #V2 #HV #T elim T -T * //
[ #i #L #j #HKL #gv #lv
>mf_lref >mf_lref
(* Properties with extensional equivalence **********************************)
-lemma mf_comp (T): compatible_3 â\80¦ (λgv,lv.â\97\8f[gv,lv]T) (exteq …) (exteq …) (eq …).
+lemma mf_comp (T): compatible_3 â\80¦ (λgv,lv.â\96 [gv,lv]T) (exteq …) (exteq …) (eq …).
#T elim T -T *
[ //
| #i #gv1 #gv2 #Hgv #lv1 #lv2 #Hlv
(* Advanced properties ******************************************************)
-lemma mf_id (T): â\97\8f[mf_gi,mf_li]T = T.
+lemma mf_id (T): â\96 [mf_gi,mf_li]T = T.
#T elim T -T * //
[ #p #I #V #T #IHV #IHT
<IHV in ⊢ (???%); <IHT in ⊢ (???%); -IHV -IHT
(* Properties with relocation ***********************************************)
-lemma mf_lifts_basic_SO_dx (T) (j): â\88\80gv,lv. â\86\91[j,1]â\97\8f[gv,lv]T = â\97\8f[⇡[j]gv,⇡[j]lv]T.
+lemma mf_lifts_basic_SO_dx (T) (j): â\88\80gv,lv. â\86\91[j,1]â\96 [gv,lv]T = â\96 [⇡[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
definition tm_ap (V) (T) ≝ ⓐV.T.
-definition tm_ti (gv) (lv) (T) â\89\9d â\97\8f[gv,lv]T.
+definition tm_ti (gv) (lv) (T) â\89\9d â\96 [gv,lv]T.
definition TM (h): model ≝ mk_model … .
[ @tm_dd
lemma cpcs_repl (h) (G) (L): replace_2 … (cpcs h G L) (cpcs h G L) (cpcs h G L).
/3 width=5 by cpcs_trans, cpcs_sym/ qed-.
(*
-lemma pippo (h) (gv) (lv) (T): â\97\8f[gv,lv]T = ⟦T⟧{TM h}[gv,lv].
+lemma pippo (h) (gv) (lv) (T): â\96 [gv,lv]T = ⟦T⟧{TM h}[gv,lv].
// qed.
lemma tm_mi (h) (gv1) (gv2) (lv1) (lv2) (p) (W) (T):
<pippo in ⊢ (????%?); >(mf_comp … T) in ⊢ (????%?);
-[2: ;;tm_vpush_vlift_join_O
+[2: @tm_vpush_vlift_join_O
<pippo in ⊢ (????%?);
--- /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 @{ 'BlackSquare $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 gv, break term 46 lv ] break term 46 T )"
- non associative with precedence 46
- for @{ 'BlackCircle $gv $lv $T }.
class "orange"
[ { "functional" * } {
[ { "multiple filling" * } {
- [ "mf" + "( â\97\8f[?,?]? )" "mf_exeq" "mf_lifts" "mf_cpr" *]
+ [ "mf" + "( â\96 [?,?]? )" "mf_exeq" "mf_lifts" "mf_cpr" *]
[ "mf_vpush" + "( ⇡[?←?]? )" "mf_vpush_exteq" "mf_vpush_vlift" * ]
[ "mf_vlift" + "( ⇡[?]? )" "mf_vlift_exteq" * ]
[ "mf_v" * ]
@(acr_abst … H1RP H2RP) /2 width=5 by/
#L3 #V3 #W3 #T3 #cs3 #HL32 #HW03 #HT03 #H1B #H2B
elim (drops_lsubc_trans … H1RP … HL32 … HL02) -L2 #L2 #HL32 #HL20
- lapply (aaa_lifts … L2 W3 … (cs ;; cs3) … HLWB) -HLWB /2 width=4 by drops_trans, lifts_trans/ #HLW2B
- @(IHA (L2. ⓛW3) … (cs + 1 ;; cs3 + 1)) -IHA
+ lapply (aaa_lifts … L2 W3 … (cs ● cs3) … HLWB) -HLWB /2 width=4 by drops_trans, lifts_trans/ #HLW2B
+ @(IHA (L2. ⓛW3) … (cs + 1 ● cs3 + 1)) -IHA
/3 width=5 by lsubc_beta, drops_trans, drops_skip, lifts_trans/
| #G #L #V #T #B #A #_ #_ #IHB #IHA #L0 #cs #HL0 #X #H #L2 #HL20
elim (lifts_inv_flat1 … H) -H #V0 #T0 #HV0 #HT0 #H destruct
'SnAbst L T = (append (LPair LAtom Abst T) L).
definition d_appendable_sn: predicate (lenv→relation term) ≝ λR.
- ∀K,T1,T2. R K T1 T2 → ∀L. R (L ;; K) T1 T2.
+ ∀K,T1,T2. R K T1 T2 → ∀L. R (L ● K) T1 T2.
(* Basic properties *********************************************************)
-lemma append_atom_sn: ∀L. ⋆ ;; L = L.
+lemma append_atom_sn: ∀L. ⋆ ● L = L.
#L elim L -L normalize //
qed.
#L1 #L2 #L3 elim L3 -L3 normalize //
qed.
-lemma append_length: ∀L1,L2. |L1 ;; L2| = |L1| + |L2|.
+lemma append_length: ∀L1,L2. |L1 ● L2| = |L1| + |L2|.
#L1 #L2 elim L2 -L2 normalize //
qed.
(* Basic inversion lemmas ***************************************************)
-lemma append_inj_sn: ∀K1,K2,L1,L2. L1 ;; K1 = L2 ;; K2 → |K1| = |K2| →
+lemma append_inj_sn: ∀K1,K2,L1,L2. L1 ● K1 = L2 ● K2 → |K1| = |K2| →
L1 = L2 ∧ K1 = K2.
#K1 elim K1 -K1
[ * normalize /2 width=1 by conj/
qed-.
(* Note: lemma 750 *)
-lemma append_inj_dx: ∀K1,K2,L1,L2. L1 ;; K1 = L2 ;; K2 → |L1| = |L2| →
+lemma append_inj_dx: ∀K1,K2,L1,L2. L1 ● K1 = L2 ● K2 → |L1| = |L2| →
L1 = L2 ∧ K1 = K2.
#K1 elim K1 -K1
[ * normalize /2 width=1 by conj/
]
qed-.
-lemma append_inv_refl_dx: ∀L,K. L ;; K = L → K = ⋆.
+lemma append_inv_refl_dx: ∀L,K. L ● K = L → K = ⋆.
#L #K #H elim (append_inj_dx … (⋆) … H) //
qed-.
-lemma append_inv_pair_dx: ∀I,L,K,V. L ;; K = L.ⓑ{I}V → K = ⋆.ⓑ{I}V.
+lemma append_inv_pair_dx: ∀I,L,K,V. L ● K = L.ⓑ{I}V → K = ⋆.ⓑ{I}V.
#I #L #K #V #H elim (append_inj_dx … (⋆.ⓑ{I}V) … H) //
qed-.
inductive drops (s:bool): mr2 → relation lenv ≝
| drops_nil : ∀L. drops s (𝐞) L L
| drops_cons: ∀L1,L,L2,cs,l,m.
- drops s cs L1 L → ⬇[s, l, m] L ≡ L2 → drops s (❨l, m❩; cs) L1 L2
+ drops s cs L1 L → ⬇[s, l, m] L ≡ L2 → drops s (❨l, m❩◗ cs) L1 L2
.
interpretation "iterated slicing (local environment) abstract"
/2 width=4 by drops_inv_nil_aux/ qed-.
fact drops_inv_cons_aux: ∀L1,L2,s,cs. ⬇*[s, cs] L1 ≡ L2 →
- ∀l,m,tl. cs = ❨l, m❩; tl →
+ ∀l,m,tl. cs = ❨l, m❩◗ tl →
∃∃L. ⬇*[s, tl] L1 ≡ L & ⬇[s, l, m] L ≡ L2.
#L1 #L2 #s #cs * -L1 -L2 -cs
[ #L #l #m #tl #H destruct
]
qed-.
-lemma drops_inv_cons: ∀L1,L2,s,l,m,cs. ⬇*[s, ❨l, m❩; cs] L1 ≡ L2 →
+lemma drops_inv_cons: ∀L1,L2,s,l,m,cs. ⬇*[s, ❨l, m❩◗ cs] L1 ≡ L2 →
∃∃L. ⬇*[s, cs] L1 ≡ L & ⬇[s, l, m] L ≡ L2.
/2 width=3 by drops_inv_cons_aux/ qed-.
(* Main properties **********************************************************)
theorem drops_trans: ∀L,L2,s,cs2. ⬇*[s, cs2] L ≡ L2 → ∀L1,cs1. ⬇*[s, cs1] L1 ≡ L →
- ⬇*[s, cs2 ;; cs1] L1 ≡ L2.
+ ⬇*[s, cs2 ● cs1] L1 ≡ L2.
#L #L2 #s #cs2 #H elim H -L -L2 -cs2 /3 width=3 by drops_cons/
qed-.
(* Properties on append for local environments ******************************)
lemma frees_append: ∀L2,U,l,i. L2 ⊢ i ϵ 𝐅*[l]⦃U⦄ → i ≤ |L2| →
- ∀L1. L1 ;; L2 ⊢ i ϵ 𝐅*[l]⦃U⦄.
+ ∀L1. L1 ● L2 ⊢ i ϵ 𝐅*[l]⦃U⦄.
#L2 #U #l #i #H elim H -L2 -U -l -i /3 width=2 by frees_eq/
#I #L2 #K2 #U #W #l #i #j #Hlj #Hji #HnU #HLK2 #_ #IHW #Hi #L1
lapply (drop_fwd_length_minus2 … HLK2) normalize #H0
(* Inversion lemmas on append for local environments ************************)
-fact frees_inv_append_aux: ∀L,U,l,i. L ⊢ i ϵ 𝐅*[l]⦃U⦄ → ∀L1,L2. L = L1 ;; L2 →
+fact frees_inv_append_aux: ∀L,U,l,i. L ⊢ i ϵ 𝐅*[l]⦃U⦄ → ∀L1,L2. L = L1 ● L2 →
i ≤ |L2| → L2 ⊢ i ϵ 𝐅*[l]⦃U⦄.
#L #U #l #i #H elim H -L -U -l -i /3 width=2 by frees_eq/
#Z #L #Y #U #X #l #i #j #Hlj #Hji #HnU #HLY #_ #IHW #L1 #L2 #H #Hi destruct
]
qed-.
-lemma frees_inv_append: ∀L1,L2,U,l,i. L1 ;; L2 ⊢ i ϵ 𝐅*[l]⦃U⦄ →
+lemma frees_inv_append: ∀L1,L2,U,l,i. L1 ● L2 ⊢ i ϵ 𝐅*[l]⦃U⦄ →
i ≤ |L2| → L2 ⊢ i ϵ 𝐅*[l]⦃U⦄.
/2 width=4 by frees_inv_append_aux/ qed-.
inductive lifts: mr2 → relation term ≝
| lifts_nil : ∀T. lifts (𝐞) T T
| lifts_cons: ∀T1,T,T2,cs,l,m.
- ⬆[l,m] T1 ≡ T → lifts cs T T2 → lifts (❨l, m❩; cs) T1 T2
+ ⬆[l,m] T1 ≡ T → lifts cs T T2 → lifts (❨l, m❩◗ cs) T1 T2
.
interpretation "generic relocation (term)"
/2 width=3 by lifts_inv_nil_aux/ qed-.
fact lifts_inv_cons_aux: ∀T1,T2,cs. ⬆*[cs] T1 ≡ T2 →
- ∀l,m,tl. cs = ❨l, m❩; tl →
+ ∀l,m,tl. cs = ❨l, m❩◗ tl →
∃∃T. ⬆[l, m] T1 ≡ T & ⬆*[tl] T ≡ T2.
#T1 #T2 #cs * -T1 -T2 -cs
[ #T #l #m #tl #H destruct
/2 width=3 by ex2_intro/
qed-.
-lemma lifts_inv_cons: ∀T1,T2,l,m,cs. ⬆*[❨l, m❩; cs] T1 ≡ T2 →
+lemma lifts_inv_cons: ∀T1,T2,l,m,cs. ⬆*[❨l, m❩◗ cs] T1 ≡ T2 →
∃∃T. ⬆[l, m] T1 ≡ T & ⬆*[cs] T ≡ T2.
/2 width=3 by lifts_inv_cons_aux/ qed-.
(* Main properties **********************************************************)
theorem lifts_trans: ∀T1,T,cs1. ⬆*[cs1] T1 ≡ T → ∀T2:term. ∀cs2. ⬆*[cs2] T ≡ T2 →
- ⬆*[cs1 ;; cs2] T1 ≡ T2.
+ ⬆*[cs1 ● cs2] T1 ≡ T2.
#T1 #T #cs1 #H elim H -T1 -T -cs1 /3 width=3 by lifts_cons/
qed.
fact drop_O1_append_sn_le_aux: ∀L1,L2,s,l,m. ⬇[s, l, m] L1 ≡ L2 →
l = 0 → m ≤ |L1| →
- ∀L. ⬇[s, 0, m] L ;; L1 ≡ L ;; L2.
+ ∀L. ⬇[s, 0, m] L ● L1 ≡ L ● L2.
#L1 #L2 #s #l #m #H elim H -L1 -L2 -l -m normalize
[2,3,4: /4 width=1 by drop_skip_lt, drop_drop, arith_b1, lt_minus_to_plus_r, monotonic_pred/ ]
#l #m #_ #_ #H <(le_n_O_to_eq … H) -H //
qed-.
lemma drop_O1_append_sn_le: ∀L1,L2,s,m. ⬇[s, 0, m] L1 ≡ L2 → m ≤ |L1| →
- ∀L. ⬇[s, 0, m] L ;; L1 ≡ L ;; L2.
+ ∀L. ⬇[s, 0, m] L ● L1 ≡ L ● L2.
/2 width=3 by drop_O1_append_sn_le_aux/ qed.
(* Inversion lemmas on append for local environments ************************)
-lemma drop_O1_inv_append1_ge: ∀K,L1,L2,s,m. ⬇[s, 0, m] L1 ;; L2 ≡ K →
+lemma drop_O1_inv_append1_ge: ∀K,L1,L2,s,m. ⬇[s, 0, m] L1 ● L2 ≡ K →
|L2| ≤ m → ⬇[s, 0, m - |L2|] L1 ≡ K.
#K #L1 #L2 elim L2 -L2 normalize //
#L2 #I #V #IHL2 #s #m #H #H1m
]
qed-.
-lemma drop_O1_inv_append1_le: ∀K,L1,L2,s,m. ⬇[s, 0, m] L1 ;; L2 ≡ K → m ≤ |L2| →
- ∀K2. ⬇[s, 0, m] L2 ≡ K2 → K = L1 ;; K2.
+lemma drop_O1_inv_append1_le: ∀K,L1,L2,s,m. ⬇[s, 0, m] L1 ● L2 ≡ K → m ≤ |L2| →
+ ∀K2. ⬇[s, 0, m] L2 ≡ K2 → K = L1 ● K2.
#K #L1 #L2 elim L2 -L2 normalize
[ #s #m #H1 #H2 #K2 #H3 lapply (le_n_O_to_eq … H2) -H2
#H2 elim (drop_inv_atom1 … H3) -H3 #H3 #_ destruct
| unfold_sort: ∀G,L,k. unfold G L (⋆k) L
| unfold_lref: ∀I,G,L1,L2,K1,K2,V,i. ⬇[i] L1 ≡ K1. ⓑ{I}V →
unfold G K1 V K2 → ⬇[Ⓣ, |L2|, i] L2 ≡ K2 →
- unfold G L1 (#i) (L1;;L2)
+ unfold G L1 (#i) (L1●L2)
| unfold_bind: ∀a,I,G,L1,L2,V,T.
unfold G (L1.ⓑ{I}V) T L2 → unfold G L1 (ⓑ{a,I}V.T) L2
| unfold_flat: ∀I,G,L1,L2,V,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 *)
+(* *)
+(**************************************************************************)
+
+(* GROUND NOTATION **********************************************************)
+
+notation "hvbox( l1 ● break l2 )"
+ right associative with precedence 47
+ for @{ 'BlackCircle $l1 $l2 }.
--- /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 *)
+(* *)
+(**************************************************************************)
+
+(* GROUND NOTATION **********************************************************)
+
+notation "hvbox( ❨ term 46 hd1, break term 46 hd2 ❩◗ break term 46 tl )"
+ non associative with precedence 47
+ for @{ 'BlackHalfCircleRight $hd1 $hd2 $tl }.
non associative with precedence 75
for @{ 'CircledElementE ? }.
-notation > "hvbox( ⓔ{ term 46 C } )"
+notation > "hvbox( ⓔ{ term 46 S } )"
non associative with precedence 75
for @{ 'CircledElementE $S }.
+++ /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 *)
-(* *)
-(**************************************************************************)
-
-(* GROUND NOTATION **********************************************************)
-
-notation "hvbox( l1 ;; break l2 )"
- right associative with precedence 55
- for @{ 'DoubleSemicolon $l1 $l2 }.
(* GROUND NOTATION **********************************************************)
notation < "hvbox( hd ⨁ break tl )"
- right associative with precedence 55
+ right associative with precedence 47
for @{ 'OPlus $S $hd $tl }.
notation > "hvbox( hd ⨁ break tl )"
- right associative with precedence 55
+ right associative with precedence 47
for @{ 'OPlus ? $hd $tl }.
-notation > "hvbox( hd ⨁{ break term 46 S } break term 54 tl )"
- non associative with precedence 55
+notation > "hvbox( hd ⨁{ break term 46 S } break term 46 tl )"
+ non associative with precedence 47
for @{ 'OPlus $S $hd $tl }.
(* GROUND NOTATION **********************************************************)
notation < "hvbox( hd ⨭ break tl )"
- left associative with precedence 50
+ left associative with precedence 47
for @{ 'OPlusLeft $S $hd $tl }.
notation > "hvbox( hd ⨭ break tl )"
- left associative with precedence 50
+ left associative with precedence 47
for @{ 'OPlusLeft ? $hd $tl }.
-notation > "hvbox( hd ⨭{ break term 46 S } break term 50 tl )"
- non associative with precedence 50
+notation > "hvbox( hd ⨭{ break term 46 S } break term 47 tl )"
+ non associative with precedence 47
for @{ 'OPlusLeft $S $hd $tl }.
+++ /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 *)
-(* *)
-(**************************************************************************)
-
-(* GROUND NOTATION **********************************************************)
-
-notation "hvbox( ❨ term 46 hd1, break term 46 hd2 ❩; break term 46 tl )"
- non associative with precedence 75
- for @{ 'Semicolon $hd1 $hd2 $tl }.
(* *)
(**************************************************************************)
-include "ground/notation/functions/double_semicolon_2.ma".
+include "ground/notation/functions/black_circle_2.ma".
include "ground/relocation/fr2_map.ma".
(* CONCATENATION FOR FINITE RELOCATION MAPS WITH PAIRS **********************)
-(* Note: this is compose *)
+(* Note: this is reverse compose *)
(*** fr2_append *)
rec definition fr2_append f1 f2 on f1 ≝ match f1 with
[ fr2_empty ⇒ f2
-| fr2_lcons d h f1 ⇒ ❨d, h❩; fr2_append f1 f2
+| fr2_lcons d h f1 ⇒ ❨d, h❩◗ fr2_append f1 f2
].
interpretation
"append (finite relocation maps with pairs)"
- 'DoubleSemicolon f1 f2 = (fr2_append f1 f2).
+ 'BlackCircle f1 f2 = (fr2_append f1 f2).
(* Basic constructions ******************************************************)
(*** mr2_append_nil *)
lemma fr2_append_empty (f2):
- f2 = 𝐞 ;; f2.
+ f2 = 𝐞 ● f2.
// qed.
(*** mr2_append_cons *)
lemma fr2_append_lcons (d) (h) (f1) (f2):
- ❨d, h❩; (f1 ;; f2) = (❨d, h❩; f1) ;; f2.
+ ❨d, h❩◗ (f1 ● f2) = (❨d, h❩◗ f1) ● f2.
// qed.
(**************************************************************************)
include "ground/notation/functions/element_e_0.ma".
-include "ground/notation/functions/semicolon_3.ma".
+include "ground/notation/functions/black_halfcircleright_3.ma".
include "ground/arith/nat.ma".
(* FINITE RELOCATION MAPS WITH PAIRS ****************************************)
interpretation
"left cons (finite relocation maps with pairs)"
- 'Semicolon d h f = (fr2_lcons d h f).
+ 'BlackHalfCircleRight d h f = (fr2_lcons d h f).
fr2_minus i (𝐞) (𝐞)
(*** minuss_lt *)
| fr2_minus_lt (f1) (f2) (d) (h) (i):
- i < d → fr2_minus i f1 f2 → fr2_minus i (❨d,h❩;f1) (❨d-i,h❩;f2)
+ i < d → fr2_minus i f1 f2 → fr2_minus i (❨d,h❩◗f1) (❨d-i,h❩◗f2)
(*** minuss_ge *)
| fr2_minus_ge (f1) (f2) (d) (h) (i):
- d ≤ i → fr2_minus (h+i) f1 f2 → fr2_minus i (❨d,h❩;f1) f2
+ d ≤ i → fr2_minus (h+i) f1 f2 → fr2_minus i (❨d,h❩◗f1) f2
.
interpretation
(*** minuss_inv_cons1 *)
lemma fr2_minus_inv_lcons_sn (f1) (f2) (d) (h) (i):
- ❨d, h❩;f1 ▭ i ≘ f2 →
+ ❨d, h❩◗f1 ▭ i ≘ f2 →
∨∨ ∧∧ d ≤ i & f1 ▭ h+i ≘ f2
- | ∃∃f. i < d & f1 ▭ i ≘ f & f2 = ❨d-i,h❩;f.
-#g1 #f2 #d #h #i @(insert_eq_1 … (❨d,h❩;g1))
+ | ∃∃f. i < d & f1 ▭ i ≘ f & f2 = ❨d-i,h❩◗f.
+#g1 #f2 #d #h #i @(insert_eq_1 … (❨d,h❩◗g1))
#f1 * -f1 -f2 -i
[ #i #H destruct
| #f1 #f #d1 #h1 #i1 #Hid1 #Hf #H destruct /3 width=3 by ex3_intro, or_intror/
(*** minuss_inv_cons1_ge *)
lemma fr2_minus_inv_lcons_sn_ge (f1) (f2) (d) (h) (i):
- ❨d, h❩;f1 ▭ i ≘ f2 → d ≤ i → f1 ▭ h+i ≘ f2.
+ ❨d, h❩◗f1 ▭ i ≘ f2 → d ≤ i → f1 ▭ h+i ≘ f2.
#f1 #f2 #d #h #i #H
elim (fr2_minus_inv_lcons_sn … H) -H * // #f #Hid #_ #_ #Hdi
elim (nlt_ge_false … Hid Hdi)
(*** minuss_inv_cons1_lt *)
lemma fr2_minus_inv_lcons_sn_lt (f1) (f2) (d) (h) (i):
- ❨d, h❩;f1 ▭ i ≘ f2 → i < d →
- ∃∃f. f1 ▭ i ≘ f & f2 = ❨d-i,h❩;f.
+ ❨d, h❩◗f1 ▭ i ≘ f2 → i < d →
+ ∃∃f. f1 ▭ i ≘ f & f2 = ❨d-i,h❩◗f.
#f1 #f2 #d #h #i #H elim (fr2_minus_inv_lcons_sn … H) -H *
[ #Hdi #_ #Hid elim (nlt_ge_false … Hid Hdi)
| /2 width=3 by ex2_intro/
fr2_nat (𝐞) l l
(*** at_lt *)
| fr2_nat_lt (f) (d) (h) (l1) (l2):
- l1 < d → fr2_nat f l1 l2 → fr2_nat (❨d,h❩;f) l1 l2
+ l1 < d → fr2_nat f l1 l2 → fr2_nat (❨d,h❩◗f) l1 l2
(*** at_ge *)
| fr2_nat_ge (f) (d) (h) (l1) (l2):
- d ≤ l1 → fr2_nat f (l1 + h) l2 → fr2_nat (❨d,h❩;f) l1 l2
+ d ≤ l1 → fr2_nat f (l1 + h) l2 → fr2_nat (❨d,h❩◗f) l1 l2
.
interpretation
(*** at_inv_cons *)
lemma fr2_nat_inv_lcons (f) (d) (h) (l1) (l2):
- @❨l1, ❨d,h❩;f❩ ≘ l2 →
+ @❨l1, ❨d,h❩◗f❩ ≘ l2 →
∨∨ ∧∧ l1 < d & @❨l1, f❩ ≘ l2
| ∧∧ d ≤ l1 & @❨l1+h, f❩ ≘ l2.
-#g #d #h #l1 #l2 @(insert_eq_1 … (❨d, h❩;g))
+#g #d #h #l1 #l2 @(insert_eq_1 … (❨d, h❩◗g))
#f * -f -l1 -l2
[ #l #H destruct
| #f1 #d1 #h1 #l1 #l2 #Hld1 #Hl12 #H destruct /3 width=1 by or_introl, conj/
(*** at_inv_cons *)
lemma fr2_nat_inv_lcons_lt (f) (d) (h) (l1) (l2):
- @❨l1, ❨d,h❩;f❩ ≘ l2 → l1 < d → @❨l1, f❩ ≘ l2.
+ @❨l1, ❨d,h❩◗f❩ ≘ l2 → l1 < d → @❨l1, f❩ ≘ l2.
#f #d #h #l1 #h2 #H
elim (fr2_nat_inv_lcons … H) -H * // #Hdl1 #_ #Hl1d
elim (nlt_ge_false … Hl1d Hdl1)
(*** at_inv_cons *)
lemma fr2_nat_inv_lcons_ge (f) (d) (h) (l1) (l2):
- @❨l1, ❨d,h❩;f❩ ≘ l2 → d ≤ l1 → @❨l1+h, f❩ ≘ l2.
+ @❨l1, ❨d,h❩◗f❩ ≘ l2 → d ≤ l1 → @❨l1+h, f❩ ≘ l2.
#f #d #h #l1 #h2 #H
elim (fr2_nat_inv_lcons … H) -H * // #Hl1d #_ #Hdl1
elim (nlt_ge_false … Hl1d Hdl1)
(*** pluss *)
rec definition fr2_plus (f:fr2_map) (n:nat) on f ≝ match f with
[ fr2_empty ⇒ 𝐞
-| fr2_lcons d h f ⇒ ❨d+n,h❩;fr2_plus f n
+| fr2_lcons d h f ⇒ ❨d+n,h❩◗fr2_plus f n
].
interpretation
(*** pluss_SO2 *)
lemma fr2_plus_lcons_unit (d) (h) (f):
- ((❨d,h❩;f)+𝟏) = ❨↑d,h❩;f+𝟏.
+ ((❨d,h❩◗f)+𝟏) = ❨↑d,h❩◗f+𝟏.
normalize // qed.
(* Basic inversions *********************************************************)
(*** pluss_inv_cons2 *)
lemma fr2_plus_inv_lcons_dx (n) (d) (h) (f2) (f):
- f + n = ❨d,h❩;f2 →
- ∃∃f1. f1+n = f2 & f = ❨d-n,h❩;f1.
+ f + n = ❨d,h❩◗f2 →
+ ∃∃f1. f1+n = f2 & f = ❨d-n,h❩◗f1.
#n #d #h #f2 *
[ normalize #H destruct
| #d1 #h1 #f1 whd in ⊢ (??%?→?); #H destruct
[ { "finite relocation with pairs" * } {
[ "fr2_nat ( @❨?,?❩ ≘ ? )" "fr2_nat_nat" * ]
[ "fr2_minus ( ? ▭ ? ≘ ? )" * ]
- [ "fr2_append ( ?;;? )" * ]
+ [ "fr2_append ( ?●? )" * ]
[ "fr2_plus ( ?+? )" * ]
- [ "fr2_map ( 𝐞 ) ( ❨?,?❩;? )" * ]
+ [ "fr2_map ( 𝐞 ) ( ❨?,?❩◗? )" * ]
}
]
[ { "total relocation" * } {
projects / helm.git / commitdiff