From: Ferruccio Guidi Date: Tue, 23 Aug 2022 16:17:59 +0000 (+0200) Subject: update in ground X-Git-Tag: make_still_working~41 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=15a2da1b45b2fd34ac67dcb58fc4b94330d18a93 update in ground + notation update and renaming --- diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/apply_2.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/apply_2.ma deleted file mode 100644 index 2baa23e2f..000000000 --- a/matita/matita/contribs/lambdadelta/ground/notation/functions/apply_2.ma +++ /dev/null @@ -1,19 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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( f ＠❨ break term 46 a ❩ )" - non associative with precedence 60 - for @{ 'Apply $f $a }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/applysucc_2.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/applysucc_2.ma deleted file mode 100644 index 177d04382..000000000 --- a/matita/matita/contribs/lambdadelta/ground/notation/functions/applysucc_2.ma +++ /dev/null @@ -1,19 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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( f @↑❨ break term 46 a ❩ )" - non associative with precedence 60 - for @{ 'ApplySucc $f $a }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/at_2.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/at_2.ma new file mode 100644 index 000000000..af60609e0 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground/notation/functions/at_2.ma @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||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( f ＠❨ break term 46 a ❩ )" + non associative with precedence 60 + for @{ 'At $f $a }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/atsection_2.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/atsection_2.ma new file mode 100644 index 000000000..7867ea59d --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground/notation/functions/atsection_2.ma @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||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( f ＠§❨ break term 46 a ❩ )" + non associative with precedence 60 + for @{ 'AtSection $f $a }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/relations/ratsection_3.ma b/matita/matita/contribs/lambdadelta/ground/notation/relations/ratsection_3.ma new file mode 100644 index 000000000..688b6381b --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground/notation/relations/ratsection_3.ma @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||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 T1 , break term 46 f ❩ ≘ break term 46 T2 )" + non associative with precedence 45 + for @{ 'RAtSection $T1 $f $T2 }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/relations/ratsucc_3.ma b/matita/matita/contribs/lambdadelta/ground/notation/relations/ratsucc_3.ma deleted file mode 100644 index b5a43f6da..000000000 --- a/matita/matita/contribs/lambdadelta/ground/notation/relations/ratsucc_3.ma +++ /dev/null @@ -1,19 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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 T1 , break term 46 f ❩ ≘ break term 46 T2 )" - non associative with precedence 45 - for @{ 'RAtSucc $T1 $f $T2 }. diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/fr2_nat.ma b/matita/matita/contribs/lambdadelta/ground/relocation/fr2_nat.ma index 0a70d2f45..59e8c9fe6 100644 --- a/matita/matita/contribs/lambdadelta/ground/relocation/fr2_nat.ma +++ b/matita/matita/contribs/lambdadelta/ground/relocation/fr2_nat.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "ground/notation/relations/ratsucc_3.ma". +include "ground/notation/relations/ratsection_3.ma". include "ground/arith/nat_plus.ma". include "ground/arith/nat_lt.ma". include "ground/relocation/fr2_map.ma". @@ -34,13 +34,13 @@ inductive fr2_nat: fr2_map → relation nat ≝ interpretation "non-negative relational application (finite relocation maps with pairs)" - 'RAtSucc l1 f l2 = (fr2_nat f l1 l2). + 'RAtSection l1 f l2 = (fr2_nat f l1 l2). (* Basic inversions *********************************************************) (*** at_inv_nil *) lemma fr2_nat_inv_empty (l1) (l2): - @↑❨l1, 𝐞❩ ≘ l2 → l1 = l2. + ＠§❨l1, 𝐞❩ ≘ l2 → l1 = l2. #l1 #l2 @(insert_eq_1 … (𝐞)) #f * -f -l1 -l2 [ // @@ -51,9 +51,9 @@ qed-. (*** at_inv_cons *) lemma fr2_nat_inv_lcons (f) (d) (h) (l1) (l2): - @↑❨l1, ❨d,h❩◗f❩ ≘ l2 → - ∨∨ ∧∧ l1 < d & @↑❨l1, f❩ ≘ l2 - | ∧∧ d ≤ l1 & @↑❨l1+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)) #f * -f -l1 -l2 [ #l #H destruct @@ -64,7 +64,7 @@ qed-. (*** 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) @@ -72,7 +72,7 @@ qed-. (*** 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) diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/fr2_nat_nat.ma b/matita/matita/contribs/lambdadelta/ground/relocation/fr2_nat_nat.ma index c84990142..287e6cd58 100644 --- a/matita/matita/contribs/lambdadelta/ground/relocation/fr2_nat_nat.ma +++ b/matita/matita/contribs/lambdadelta/ground/relocation/fr2_nat_nat.ma @@ -20,7 +20,7 @@ include "ground/relocation/fr2_nat.ma". (*** at_mono *) theorem fr2_nat_mono (f) (l): - ∀l1. @↑❨l, f❩ ≘ l1 → ∀l2. @↑❨l, f❩ ≘ l2 → l1 = l2. + ∀l1. ＠§❨l, f❩ ≘ l1 → ∀l2. ＠§❨l, f❩ ≘ l2 → l1 = l2. #f #l #l1 #H elim H -f -l -l1 [ #l #x #H <(fr2_nat_inv_empty … H) -x // | #f #d #h #l #l1 #Hld #_ #IH #x #H diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/nap.ma b/matita/matita/contribs/lambdadelta/ground/relocation/nap.ma index a5ab2dcb7..921863e50 100644 --- a/matita/matita/contribs/lambdadelta/ground/relocation/nap.ma +++ b/matita/matita/contribs/lambdadelta/ground/relocation/nap.ma @@ -1,7 +1,7 @@ include "ground/relocation/tr_uni_pap.ma". include "ground/relocation/tr_compose_pap.ma". include "ground/relocation/tr_pap_eq.ma". -include "ground/notation/functions/applysucc_2.ma". +include "ground/notation/functions/atsection_2.ma". include "ground/arith/nat_lt.ma". include "ground/arith/nat_plus_rplus.ma". include "ground/arith/nat_pred_succ.ma". @@ -17,46 +17,46 @@ definition tr_nap (f) (l:nat): nat ≝ interpretation "functional non-negative application (total relocation maps)" - 'ApplySucc f l = (tr_nap f l). + 'AtSection f l = (tr_nap f l). lemma tr_nap_unfold (f) (l): - ↓(f＠⧣❨↑l❩) = f@↑❨l❩. + ↓(f＠⧣❨↑l❩) = f＠§❨l❩. // qed. lemma tr_pap_succ_nap (f) (l): - ↑(f@↑❨l❩) = f＠⧣❨↑l❩. + ↑(f＠§❨l❩) = f＠⧣❨↑l❩. // qed. lemma tr_compose_nap (f2) (f1) (l): - f2@↑❨f1@↑❨l❩❩ = (f2∘f1)@↑❨l❩. + f2＠§❨f1＠§❨l❩❩ = (f2∘f1)＠§❨l❩. #f2 #f1 #l (npsucc_pred i1) in ⊢ (%→?); >(npsucc_pred i2) in ⊢ (%→?); // @@ -56,7 +56,7 @@ qed. (*** pr_nat_inv_ppx *) lemma pr_nat_inv_zero_push (f) (l1) (l2): - @↑❨l1,f❩ ≘ l2 → ∀g. 𝟎 = l1 → ⫯g = f → 𝟎 = l2. + ＠§❨l1,f❩ ≘ l2 → ∀g. 𝟎 = l1 → ⫯g = f → 𝟎 = l2. #f #l1 #l2 #H #g #H1 #H2 destruct lapply (pr_pat_inv_unit_push … H ???) -H /2 width=2 by eq_inv_npsucc_bi/ @@ -64,8 +64,8 @@ qed-. (*** pr_nat_inv_npx *) lemma pr_nat_inv_succ_push (f) (l1) (l2): - @↑❨l1,f❩ ≘ l2 → ∀g,k1. ↑k1 = l1 → ⫯g = f → - ∃∃k2. @↑❨k1,g❩ ≘ k2 & ↑k2 = l2. + ＠§❨l1,f❩ ≘ l2 → ∀g,k1. ↑k1 = l1 → ⫯g = f → + ∃∃k2. ＠§❨k1,g❩ ≘ k2 & ↑k2 = l2. #f #l1 #l2 #H #g #k1 #H1 #H2 destruct elim (pr_pat_inv_succ_push … H) -H [|*: // ] #k2 #Hg >(npsucc_pred (↑l2)) #H @@ -74,8 +74,8 @@ qed-. (*** pr_nat_inv_xnx *) lemma pr_nat_inv_next (f) (l1) (l2): - @↑❨l1,f❩ ≘ l2 → ∀g. ↑g = f → - ∃∃k2. @↑❨l1,g❩ ≘ k2 & ↑k2 = l2. + ＠§❨l1,f❩ ≘ l2 → ∀g. ↑g = f → + ∃∃k2. ＠§❨l1,g❩ ≘ k2 & ↑k2 = l2. #f #l1 #l2 #H #g #H1 destruct elim (pr_pat_inv_next … H) -H [|*: // ] #k2 >(npsucc_pred (k2)) in ⊢ (%→?→?); #Hg #H @@ -86,50 +86,50 @@ qed-. (*** pr_nat_inv_ppn *) lemma pr_nat_inv_zero_push_succ (f) (l1) (l2): - @↑❨l1,f❩ ≘ l2 → ∀g,k2. 𝟎 = l1 → ⫯g = f → ↑k2 = l2 → ⊥. + ＠§❨l1,f❩ ≘ l2 → ∀g,k2. 𝟎 = l1 → ⫯g = f → ↑k2 = l2 → ⊥. #f #l1 #l2 #Hf #g #k2 #H1 #H <(pr_nat_inv_zero_push … Hf … H1 H) -f -g -l1 -l2 /2 width=3 by eq_inv_nsucc_zero/ qed-. (*** pr_nat_inv_npp *) lemma pr_nat_inv_succ_push_zero (f) (l1) (l2): - @↑❨l1,f❩ ≘ l2 → ∀g,k1. ↑k1 = l1 → ⫯g = f → 𝟎 = l2 → ⊥. + ＠§❨l1,f❩ ≘ l2 → ∀g,k1. ↑k1 = l1 → ⫯g = f → 𝟎 = l2 → ⊥. #f #l1 #l2 #Hf #g #k1 #H1 #H elim (pr_nat_inv_succ_push … Hf … H1 H) -f -l1 #x2 #Hg * -l2 /2 width=3 by eq_inv_zero_nsucc/ qed-. (*** pr_nat_inv_npn *) lemma pr_nat_inv_succ_push_succ (f) (l1) (l2): - @↑❨l1,f❩ ≘ l2 → ∀g,k1,k2. ↑k1 = l1 → ⫯g = f → ↑k2 = l2 → @↑❨k1,g❩ ≘ k2. + ＠§❨l1,f❩ ≘ l2 → ∀g,k1,k2. ↑k1 = l1 → ⫯g = f → ↑k2 = l2 → ＠§❨k1,g❩ ≘ k2. #f #l1 #l2 #Hf #g #k1 #k2 #H1 #H elim (pr_nat_inv_succ_push … Hf … H1 H) -f -l1 #x2 #Hg * -l2 #H >(eq_inv_nsucc_bi … H) -k2 // qed-. (*** pr_nat_inv_xnp *) lemma pr_nat_inv_next_zero (f) (l1) (l2): - @↑❨l1,f❩ ≘ l2 → ∀g. ↑g = f → 𝟎 = l2 → ⊥. + ＠§❨l1,f❩ ≘ l2 → ∀g. ↑g = f → 𝟎 = l2 → ⊥. #f #l1 #l2 #Hf #g #H elim (pr_nat_inv_next … Hf … H) -f #x2 #Hg * -l2 /2 width=3 by eq_inv_zero_nsucc/ qed-. (*** pr_nat_inv_xnn *) lemma pr_nat_inv_next_succ (f) (l1) (l2): - @↑❨l1,f❩ ≘ l2 → ∀g,k2. ↑g = f → ↑k2 = l2 → @↑❨l1,g❩ ≘ k2. + ＠§❨l1,f❩ ≘ l2 → ∀g,k2. ↑g = f → ↑k2 = l2 → ＠§❨l1,g❩ ≘ k2. #f #l1 #l2 #Hf #g #k2 #H elim (pr_nat_inv_next … Hf … H) -f #x2 #Hg * -l2 #H >(eq_inv_nsucc_bi … H) -k2 // qed-. (*** pr_nat_inv_pxp *) lemma pr_nat_inv_zero_bi (f) (l1) (l2): - @↑❨l1,f❩ ≘ l2 → 𝟎 = l1 → 𝟎 = l2 → ∃g. ⫯g = f. + ＠§❨l1,f❩ ≘ l2 → 𝟎 = l1 → 𝟎 = l2 → ∃g. ⫯g = f. #f elim (pr_map_split_tl … f) /2 width=2 by ex_intro/ #H #l1 #l2 #Hf #H1 #H2 cases (pr_nat_inv_next_zero … Hf … H H2) qed-. (*** pr_nat_inv_pxn *) lemma pr_nat_inv_zero_succ (f) (l1) (l2): - @↑❨l1,f❩ ≘ l2 → ∀k2. 𝟎 = l1 → ↑k2 = l2 → - ∃∃g. @↑❨l1,g❩ ≘ k2 & ↑g = f. + ＠§❨l1,f❩ ≘ l2 → ∀k2. 𝟎 = l1 → ↑k2 = l2 → + ∃∃g. ＠§❨l1,g❩ ≘ k2 & ↑g = f. #f elim (pr_map_split_tl … f) #H #l1 #l2 #Hf #k2 #H1 #H2 [ elim (pr_nat_inv_zero_push_succ … Hf … H1 H H2) @@ -139,7 +139,7 @@ qed-. (*** pr_nat_inv_nxp *) lemma pr_nat_inv_succ_zero (f) (l1) (l2): - @↑❨l1,f❩ ≘ l2 → ∀k1. ↑k1 = l1 → 𝟎 = l2 → ⊥. + ＠§❨l1,f❩ ≘ l2 → ∀k1. ↑k1 = l1 → 𝟎 = l2 → ⊥. #f elim (pr_map_split_tl f) #H #l1 #l2 #Hf #k1 #H1 #H2 [ elim (pr_nat_inv_succ_push_zero … Hf … H1 H H2) @@ -149,9 +149,9 @@ qed-. (*** pr_nat_inv_nxn *) lemma pr_nat_inv_succ_bi (f) (l1) (l2): - @↑❨l1,f❩ ≘ l2 → ∀k1,k2. ↑k1 = l1 → ↑k2 = l2 → - ∨∨ ∃∃g. @↑❨k1,g❩ ≘ k2 & ⫯g = f - | ∃∃g. @↑❨l1,g❩ ≘ k2 & ↑g = f. + ＠§❨l1,f❩ ≘ l2 → ∀k1,k2. ↑k1 = l1 → ↑k2 = l2 → + ∨∨ ∃∃g. ＠§❨k1,g❩ ≘ k2 & ⫯g = f + | ∃∃g. ＠§❨l1,g❩ ≘ k2 & ↑g = f. #f elim (pr_map_split_tl f) * /4 width=7 by pr_nat_inv_next_succ, pr_nat_inv_succ_push_succ, ex2_intro, or_intror, or_introl/ qed-. @@ -159,9 +159,9 @@ qed-. (* Note: the following inversion lemmas must be checked *) (*** pr_nat_inv_xpx *) lemma pr_nat_inv_push (f) (l1) (l2): - @↑❨l1,f❩ ≘ l2 → ∀g. ⫯g = f → + ＠§❨l1,f❩ ≘ l2 → ∀g. ⫯g = f → ∨∨ ∧∧ 𝟎 = l1 & 𝟎 = l2 - | ∃∃k1,k2. @↑❨k1,g❩ ≘ k2 & ↑k1 = l1 & ↑k2 = l2. + | ∃∃k1,k2. ＠§❨k1,g❩ ≘ k2 & ↑k1 = l1 & ↑k2 = l2. #f * [2: #l1 ] #l2 #Hf #g #H [ elim (pr_nat_inv_succ_push … Hf … H) -f /3 width=5 by or_intror, ex3_2_intro/ | >(pr_nat_inv_zero_push … Hf … H) -f /3 width=1 by conj, or_introl/ @@ -170,15 +170,15 @@ qed-. (*** pr_nat_inv_xpp *) lemma pr_nat_inv_push_zero (f) (l1) (l2): - @↑❨l1,f❩ ≘ l2 → ∀g. ⫯g = f → 𝟎 = l2 → 𝟎 = l1. + ＠§❨l1,f❩ ≘ l2 → ∀g. ⫯g = f → 𝟎 = l2 → 𝟎 = l1. #f #l1 #l2 #Hf #g #H elim (pr_nat_inv_push … Hf … H) -f * // #k1 #k2 #_ #_ * -l2 #H elim (eq_inv_zero_nsucc … H) qed-. (*** pr_nat_inv_xpn *) lemma pr_nat_inv_push_succ (f) (l1) (l2): - @↑❨l1,f❩ ≘ l2 → ∀g,k2. ⫯g = f → ↑k2 = l2 → - ∃∃k1. @↑❨k1,g❩ ≘ k2 & ↑k1 = l1. + ＠§❨l1,f❩ ≘ l2 → ∀g,k2. ⫯g = f → ↑k2 = l2 → + ∃∃k1. ＠§❨k1,g❩ ≘ k2 & ↑k1 = l1. #f #l1 #l2 #Hf #g #k2 #H elim (pr_nat_inv_push … Hf … H) -f * [ #_ * -l2 #H elim (eq_inv_nsucc_zero … H) | #x1 #x2 #Hg #H1 * -l2 #H @@ -189,7 +189,7 @@ qed-. (*** pr_nat_inv_xxp *) lemma pr_nat_inv_zero_dx (f) (l1) (l2): - @↑❨l1,f❩ ≘ l2 → 𝟎 = l2 → ∃∃g. 𝟎 = l1 & ⫯g = f. + ＠§❨l1,f❩ ≘ l2 → 𝟎 = l2 → ∃∃g. 𝟎 = l1 & ⫯g = f. #f elim (pr_map_split_tl f) #H #l1 #l2 #Hf #H2 [ /3 width=6 by pr_nat_inv_push_zero, ex2_intro/ @@ -198,9 +198,9 @@ lemma pr_nat_inv_zero_dx (f) (l1) (l2): qed-. (*** pr_nat_inv_xxn *) -lemma pr_nat_inv_succ_dx (f) (l1) (l2): @↑❨l1,f❩ ≘ l2 → ∀k2. ↑k2 = l2 → - ∨∨ ∃∃g,k1. @↑❨k1,g❩ ≘ k2 & ↑k1 = l1 & ⫯g = f - | ∃∃g. @↑❨l1,g❩ ≘ k2 & ↑g = f. +lemma pr_nat_inv_succ_dx (f) (l1) (l2): ＠§❨l1,f❩ ≘ l2 → ∀k2. ↑k2 = l2 → + ∨∨ ∃∃g,k1. ＠§❨k1,g❩ ≘ k2 & ↑k1 = l1 & ⫯g = f + | ∃∃g. ＠§❨l1,g❩ ≘ k2 & ↑g = f. #f elim (pr_map_split_tl f) #H #l1 #l2 #Hf #k2 #H2 [ elim (pr_nat_inv_push_succ … Hf … H H2) -l2 /3 width=5 by or_introl, ex3_2_intro/ diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_nat_basic.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_nat_basic.ma index edb5117aa..9c93c6e23 100644 --- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_nat_basic.ma +++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_nat_basic.ma @@ -20,7 +20,7 @@ include "ground/relocation/pr_nat_uni.ma". (* Constructions with pr_basic **********************************************) lemma pr_nat_basic_lt (m) (n) (l): - l < m → @↑❨l, 𝐛❨m,n❩❩ ≘ l. + l < m → ＠§❨l, 𝐛❨m,n❩❩ ≘ l. #m @(nat_ind_succ … m) -m [ #n #i #H elim (nlt_inv_zero_dx … H) | #m #IH #n #l @(nat_ind_succ … l) -l @@ -33,7 +33,7 @@ lemma pr_nat_basic_lt (m) (n) (l): qed. lemma pr_nat_basic_ge (m) (n) (l): - m ≤ l → @↑❨l, 𝐛❨m,n❩❩ ≘ l+n. + m ≤ l → ＠§❨l, 𝐛❨m,n❩❩ ≘ l+n. #m @(nat_ind_succ … m) -m // #m #IH #n #l #H elim (nle_inv_succ_sn … H) -H #Hml #H >H -H @@ -43,9 +43,9 @@ qed. (* Inversions with pr_basic *************************************************) lemma pr_nat_basic_inv_lt (m) (n) (l) (k): - l < m → @↑❨l, 𝐛❨m,n❩❩ ≘ k → l = k. + l < m → ＠§❨l, 𝐛❨m,n❩❩ ≘ k → l = k. /3 width=4 by pr_nat_basic_lt, pr_nat_mono/ qed-. lemma pr_nat_basic_inv_ge (m) (n) (l) (k): - m ≤ l → @↑❨l, 𝐛❨m,n❩❩ ≘ k → l+n = k. + m ≤ l → ＠§❨l, 𝐛❨m,n❩❩ ≘ k → l+n = k. /3 width=4 by pr_nat_basic_ge, pr_nat_mono/ qed-. diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_nat_nat.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_nat_nat.ma index 481ff1517..cfba24b07 100644 --- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_nat_nat.ma +++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_nat_nat.ma @@ -20,7 +20,7 @@ include "ground/relocation/pr_nat.ma". (* Main destructions ********************************************************) theorem pr_nat_monotonic (k2) (l2) (f): - @↑❨l2,f❩ ≘ k2 → ∀k1,l1. @↑❨l1,f❩ ≘ k1 → l1 < l2 → k1 < k2. + ＠§❨l2,f❩ ≘ k2 → ∀k1,l1. ＠§❨l1,f❩ ≘ k1 → l1 < l2 → k1 < k2. #k2 @(nat_ind_succ … k2) -k2 [ #l2 #f #H2f elim (pr_nat_inv_zero_dx … H2f) -H2f // #g #H21 #_ #k1 #l1 #_ #Hi destruct @@ -37,7 +37,7 @@ theorem pr_nat_monotonic (k2) (l2) (f): qed-. theorem pr_nat_inv_monotonic (k1) (l1) (f): - @↑❨l1,f❩ ≘ k1 → ∀k2,l2. @↑❨l2,f❩ ≘ k2 → k1 < k2 → l1 < l2. + ＠§❨l1,f❩ ≘ k1 → ∀k2,l2. ＠§❨l2,f❩ ≘ k2 → k1 < k2 → l1 < l2. #k1 @(nat_ind_succ … k1) -k1 [ #l1 #f #H1f elim (pr_nat_inv_zero_dx … H1f) -H1f // #g * -l1 #H #k2 #l2 #H2f #Hk @@ -59,14 +59,14 @@ theorem pr_nat_inv_monotonic (k1) (l1) (f): qed-. theorem pr_nat_mono (f) (l) (l1) (l2): - @↑❨l,f❩ ≘ l1 → @↑❨l,f❩ ≘ l2 → l2 = l1. + ＠§❨l,f❩ ≘ l1 → ＠§❨l,f❩ ≘ l2 → l2 = l1. #f #l #l1 #l2 #H1 #H2 elim (nat_split_lt_eq_gt l2 l1) // #Hi elim (nlt_ge_false l l) /2 width=6 by pr_nat_inv_monotonic/ qed-. theorem pr_nat_inj (f) (l1) (l2) (l): - @↑❨l1,f❩ ≘ l → @↑❨l2,f❩ ≘ l → l1 = l2. + ＠§❨l1,f❩ ≘ l → ＠§❨l2,f❩ ≘ l → l1 = l2. #f #l1 #l2 #l #H1 #H2 elim (nat_split_lt_eq_gt l2 l1) // #Hi elim (nlt_ge_false l l) /2 width=6 by pr_nat_monotonic/ diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_nat_uni.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_nat_uni.ma index 114284805..8b0f30841 100644 --- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_nat_uni.ma +++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_nat_uni.ma @@ -21,12 +21,12 @@ include "ground/relocation/pr_nat_nat.ma". (* Constructions with pr_uni ************************************************) lemma pr_nat_uni (n) (l): - @↑❨l,𝐮❨n❩❩ ≘ l+n. + ＠§❨l,𝐮❨n❩❩ ≘ l+n. /2 width=1 by pr_nat_pred_bi/ qed. (* Inversions with pr_uni ***************************************************) lemma pr_nat_inv_uni (n) (l) (k): - @↑❨l,𝐮❨n❩❩ ≘ k → k = l+n. + ＠§❨l,𝐮❨n❩❩ ≘ k → k = l+n. /2 width=4 by pr_nat_mono/ qed-. diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/xap.ma b/matita/matita/contribs/lambdadelta/ground/relocation/xap.ma index 073ffed7f..aef0c26e1 100644 --- a/matita/matita/contribs/lambdadelta/ground/relocation/xap.ma +++ b/matita/matita/contribs/lambdadelta/ground/relocation/xap.ma @@ -1,20 +1,19 @@ - (**) (* reverse include *) include "ground/arith/nat_rplus_pplus.ma". include "ground/relocation/tr_pn_eq.ma". include "ground/relocation/tr_compose_pn.ma". include "ground/relocation/nap.ma". -include "ground/notation/functions/apply_2.ma". +include "ground/notation/functions/at_2.ma". definition tr_xap (f) (l:nat): nat ≝ - (⫯f)@↑❨l❩. + (⫯f)＠§❨l❩. interpretation "functional extended application (total relocation maps)" - 'Apply f l = (tr_xap f l). + 'At f l = (tr_xap f l). lemma tr_xap_unfold (f) (l): - (⫯f)@↑❨l❩ = f＠❨l❩. + (⫯f)＠§❨l❩ = f＠❨l❩. // qed. lemma tr_xap_zero (f): @@ -26,7 +25,7 @@ lemma tr_xap_ninj (f) (p): // qed. lemma tr_xap_succ_nap (f) (n): - ↑(f@↑❨n❩) = f＠❨↑n❩. + ↑(f＠§❨n❩) = f＠❨↑n❩. #f #n