From cc178d85bc4fec05b6a9dd176f338b3275beb3d9 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sat, 8 Jan 2022 21:09:45 +0100 Subject: [PATCH] update in ground and delayed updating + notation at level 75 moved at level 70 + dfr, ifr: path depth was not considered --- .../notation/functions/at_2.ma | 4 +- .../notation/functions/class_d_phi_0.ma | 2 +- .../notation/functions/edgelabel_a_0.ma | 2 +- .../notation/functions/edgelabel_l_0.ma | 2 +- .../notation/functions/edgelabel_s_0.ma | 2 +- .../notation/functions/hash_1.ma | 2 +- .../notation/functions/lamda_1.ma | 4 +- .../notation/functions/nodelabel_d_1.ma | 2 +- .../notation/functions/phi_2.ma | 4 +- .../notation/functions/uparrow_2.ma | 4 +- .../notation/functions/uparrow_4.ma | 6 +-- .../notation/functions/uptriangle_1.ma | 4 +- .../delayed_updating/reduction/dfr.ma | 5 +- .../delayed_updating/reduction/dfr_ifr.ma | 2 +- .../delayed_updating/reduction/ifr.ma | 5 +- .../delayed_updating/substitution/lift.ma | 8 +-- .../delayed_updating/syntax/bdd_term.ma | 8 +-- .../delayed_updating/syntax/path_balanced.ma | 2 +- .../delayed_updating/syntax/path_depth.ma | 52 +++++++++++++++++++ .../lambdadelta/ground/lib/list_length.ma | 21 ++++---- .../ground/lib/subset_equivalence.ma | 2 +- .../ground/lib/subset_inclusion.ma | 2 +- .../notation/functions/circled_element_e_1.ma | 6 +-- .../ground/notation/functions/downarrow_1.ma | 4 +- .../notation/functions/downharpoonleft_2.ma | 12 ++--- .../notation/functions/downharpoonright_2.ma | 12 ++--- .../functions/downharpoonrightstar_3.ma | 12 ++--- .../ground/notation/functions/downspoon_1.ma | 4 +- .../notation/functions/downspoonstar_2.ma | 4 +- .../ground/notation/functions/element_b_2.ma | 2 +- .../ground/notation/functions/element_e_0.ma | 2 +- .../ground/notation/functions/element_i_0.ma | 2 +- .../ground/notation/functions/element_t_1.ma | 2 +- .../ground/notation/functions/element_u_1.ma | 2 +- .../ground/notation/functions/infinity_0.ma | 2 +- .../ground/notation/functions/no_0.ma | 2 +- .../ground/notation/functions/one_0.ma | 2 +- .../ground/notation/functions/onezero_0.ma | 2 +- .../ground/notation/functions/powerclass_1.ma | 2 +- .../ground/notation/functions/tuple_4.ma | 2 +- .../ground/notation/functions/two_0.ma | 2 +- .../ground/notation/functions/uparrow_1.ma | 4 +- .../notation/functions/uparrowstar_2.ma | 4 +- .../notation/functions/updownarrowstar_1.ma | 4 +- .../ground/notation/functions/upspoon_1.ma | 4 +- .../notation/functions/upspoonstar_2.ma | 4 +- .../notation/functions/verticalbars_1.ma | 19 +++++++ .../ground/notation/functions/yes_0.ma | 2 +- .../ground/notation/functions/zero_0.ma | 2 +- .../ground/notation/functions/zeroone_0.ma | 2 +- .../ground/notation/functions/zerozero_0.ma | 2 +- .../ground/relocation/pr_pat_pat_id.ma | 4 +- matita/matita/predefined_virtuals.ml | 2 +- 53 files changed, 176 insertions(+), 100 deletions(-) create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_depth.ma create mode 100644 matita/matita/contribs/lambdadelta/ground/notation/functions/verticalbars_1.ma diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/at_2.ma b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/at_2.ma index cf5c8f623..f17d53ff8 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/at_2.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/at_2.ma @@ -14,6 +14,6 @@ (* NOTATION FOR DELAYED UPDATING ********************************************) -notation "hvbox( @ break term 76 u . break term 75 t )" - non associative with precedence 75 +notation "hvbox( @ break term 71 u . break term 70 t )" + non associative with precedence 70 for @{ 'At $u $t }. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/class_d_phi_0.ma b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/class_d_phi_0.ma index 2e2651dbf..d45317626 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/class_d_phi_0.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/class_d_phi_0.ma @@ -15,5 +15,5 @@ (* NOTATION FOR DELAYED UPDATING ********************************************) notation "hvbox( 𝐃𝛗 )" - non associative with precedence 75 + non associative with precedence 70 for @{ 'ClassDPhi }. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/edgelabel_a_0.ma b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/edgelabel_a_0.ma index 0889615b1..c3051e720 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/edgelabel_a_0.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/edgelabel_a_0.ma @@ -15,5 +15,5 @@ (* NOTATION FOR DELAYED UPDATING ********************************************) notation "hvbox( 𝗔 )" - non associative with precedence 75 + non associative with precedence 70 for @{ 'EdgeLabelA }. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/edgelabel_l_0.ma b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/edgelabel_l_0.ma index 980f4312e..e03e62aea 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/edgelabel_l_0.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/edgelabel_l_0.ma @@ -15,5 +15,5 @@ (* NOTATION FOR DELAYED UPDATING ********************************************) notation "hvbox( 𝗟 )" - non associative with precedence 75 + non associative with precedence 70 for @{ 'EdgeLabelL }. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/edgelabel_s_0.ma b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/edgelabel_s_0.ma index d9d91826a..1f111d4a9 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/edgelabel_s_0.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/edgelabel_s_0.ma @@ -15,5 +15,5 @@ (* NOTATION FOR DELAYED UPDATING ********************************************) notation "hvbox( 𝗦 )" - non associative with precedence 75 + non associative with precedence 70 for @{ 'EdgeLabelS }. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/hash_1.ma b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/hash_1.ma index 8d85b354a..9369e0840 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/hash_1.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/hash_1.ma @@ -15,5 +15,5 @@ (* NOTATION FOR DELAYED UPDATING ********************************************) notation "hvbox( # break term 90 n )" - non associative with precedence 75 + non associative with precedence 70 for @{ 'Hash $n }. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/lamda_1.ma b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/lamda_1.ma index 6f8d020a9..12453dc42 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/lamda_1.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/lamda_1.ma @@ -14,6 +14,6 @@ (* NOTATION FOR DELAYED UPDATING ********************************************) -notation "hvbox( 𝛌. break term 75 t )" - non associative with precedence 75 +notation "hvbox( 𝛌. break term 70 t )" + non associative with precedence 70 for @{ 'Lamda $t }. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/nodelabel_d_1.ma b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/nodelabel_d_1.ma index 919edaa64..f95126621 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/nodelabel_d_1.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/nodelabel_d_1.ma @@ -15,5 +15,5 @@ (* NOTATION FOR DELAYED UPDATING ********************************************) notation "hvbox( 𝗱❨ break term 46 a ❩ )" - non associative with precedence 75 + non associative with precedence 70 for @{ 'NodeLabelD $a }. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/phi_2.ma b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/phi_2.ma index 7d04cc37a..127815423 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/phi_2.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/phi_2.ma @@ -14,6 +14,6 @@ (* NOTATION FOR DELAYED UPDATING ********************************************) -notation "hvbox( 𝛗 break term 76 n. break term 75 t )" - non associative with precedence 75 +notation "hvbox( 𝛗 break term 76 n. break term 70 t )" + non associative with precedence 70 for @{ 'Phi $n $t }. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/uparrow_2.ma b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/uparrow_2.ma index c80ffe09f..2cbac4b24 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/uparrow_2.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/uparrow_2.ma @@ -14,6 +14,6 @@ (* NOTATION FOR DELAYED UPDATING ********************************************) -notation "hvbox( ↑[ term 46 t1 ] break term 75 t2 )" - non associative with precedence 75 +notation "hvbox( ↑[ term 46 t1 ] break term 70 t2 )" + non associative with precedence 70 for @{ 'UpArrow $t1 $t2 }. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/uparrow_4.ma b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/uparrow_4.ma index 1f35274c9..6d638c86a 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/uparrow_4.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/uparrow_4.ma @@ -15,13 +15,13 @@ (* NOTATION FOR DELAYED UPDATING ********************************************) notation < "hvbox( ↑❨ term 46 k, break term 46 p, break term 46 f ❩ )" - non associative with precedence 75 + non associative with precedence 70 for @{ 'UpArrow $S $k $p $f }. notation > "hvbox( ↑❨ term 46 k, break term 46 p, break term 46 f ❩ )" - non associative with precedence 75 + non associative with precedence 70 for @{ 'UpArrow ? $k $p $f }. notation > "hvbox( ↑{ term 46 S }❨ break term 46 k, break term 46 p, break term 46 f ❩ )" - non associative with precedence 75 + non associative with precedence 70 for @{ 'UpArrow $S $k $p $f }. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/uptriangle_1.ma b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/uptriangle_1.ma index 09ceac1e5..df2bee52c 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/uptriangle_1.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/uptriangle_1.ma @@ -14,6 +14,6 @@ (* NOTATION FOR DELAYED UPDATING ********************************************) -notation "hvbox( ▵ term 75 t )" - non associative with precedence 75 +notation "hvbox( ▵ term 70 t )" + non associative with precedence 70 for @{ 'UpTriangle $t }. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr.ma index 8c84de0f2..689003106 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr.ma @@ -12,6 +12,7 @@ (* *) (**************************************************************************) +include "delayed_updating/syntax/path_depth.ma". include "delayed_updating/syntax/path_structure.ma". include "delayed_updating/syntax/path_balanced.ma". include "delayed_updating/substitution/fsubst.ma". @@ -20,8 +21,8 @@ include "delayed_updating/notation/relations/black_rightarrow_df_4.ma". (* DELAYED FOCUSED REDUCTION ************************************************) inductive dfr (p) (q) (t): predicate preterm ≝ -| dfr_beta (b) (n): - let r ≝ p●𝗔◗b●𝗟◗q◖𝗱❨n❩ in +| dfr_beta (b): + let r ≝ p●𝗔◗b●𝗟◗q◖𝗱❨↑❘q❘❩ in r ϵ t → ⊓⊗b → dfr p q t (t[⋔r←t⋔(p◖𝗦)]) . diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_ifr.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_ifr.ma index bd62d8e6b..015958b54 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_ifr.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_ifr.ma @@ -20,4 +20,4 @@ include "delayed_updating/reduction/dfr.ma". lemma dfr_lift_bi (f) (p) (q) (t1) (t2): t1 ➡𝐝𝐟[p,q] t2 → ↑[f]t1 ➡𝐟[⊗p,⊗q] ↑[f]t2. #f #p #q #t1 #t2 -* #b #n #Hr #Hb +* #b #Hr #Hb diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr.ma index 53853273b..4f8c282b1 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr.ma @@ -12,6 +12,7 @@ (* *) (**************************************************************************) +include "delayed_updating/syntax/path_depth.ma". include "delayed_updating/syntax/path_structure.ma". include "delayed_updating/syntax/path_balanced.ma". include "delayed_updating/substitution/fsubst.ma". @@ -21,9 +22,9 @@ include "delayed_updating/notation/relations/black_rightarrow_f_4.ma". (* IMMEDIATE FOCUSED REDUCTION ************************************************) inductive ifr (p) (q) (t): predicate preterm ≝ -| ifr_beta (b) (n): +| ifr_beta (b): let r ≝ p●𝗔◗b●𝗟◗q in - r◖𝗱❨n❩ ϵ t → ⊓⊗b → ifr p q t (t[⋔r←↑[𝐮❨n❩]t⋔(p◖𝗦)]) + r◖𝗱❨↑❘q❘❩ ϵ t → ⊓⊗b → ifr p q t (t[⋔r←↑[𝐮❨↑❘q❘❩]t⋔(p◖𝗦)]) . interpretation diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift.ma index f0d5ebd58..0293e8666 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift.ma @@ -26,7 +26,7 @@ definition lift_continuation (A:Type[0]) ≝ (* Note: inner numeric labels are not liftable, so they are removed *) rec definition lift_gen (A:Type[0]) (k:lift_continuation A) (p) (f) on p ≝ match p with -[ list_empty ⇒ k 𝐞 f +[ list_empty ⇒ k (𝐞) f | list_lcons l q ⇒ match l with [ label_node_d n ⇒ @@ -59,7 +59,7 @@ interpretation (* Basic constructions ******************************************************) lemma lift_empty (A) (k) (f): - k 𝐞 f = ↑{A}❨k, 𝐞, f❩. + k (𝐞) f = ↑{A}❨k, 𝐞, f❩. // qed. lemma lift_d_empty_sn (A) (k) (n) (f): @@ -123,8 +123,8 @@ qed. (* Advanced eliminations with path ******************************************) lemma path_ind_lift (Q:predicate …): - Q 𝐞 → - (∀n. Q 𝐞 → Q (𝗱❨n❩◗𝐞)) → + Q (𝐞) → + (∀n. Q (𝐞) → Q (𝗱❨n❩◗𝐞)) → (∀n,l,p. Q (l◗p) → Q (𝗱❨n❩◗l◗p)) → (∀p. Q p → Q (𝗟◗p)) → (∀p. Q p → Q (𝗔◗p)) → diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/bdd_term.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/bdd_term.ma index 1f8dfd1b5..d9f371823 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/bdd_term.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/bdd_term.ma @@ -24,10 +24,10 @@ include "delayed_updating/notation/functions/class_d_phi_0.ma". (* BY-DEPTH DELAYED (BDD) TERM **********************************************) inductive bdd: 𝒫❨preterm❩ ≝ -| bdd_oref: ∀n. bdd #n -| bdd_iref: ∀t,n. bdd t → bdd 𝛗n.t -| bdd_abst: ∀t. bdd t → bdd 𝛌.t -| bdd_appl: ∀u,t. bdd u → bdd t → bdd @u.t +| bdd_oref: ∀n. bdd (#n) +| bdd_iref: ∀t,n. bdd t → bdd (𝛗n.t) +| bdd_abst: ∀t. bdd t → bdd (𝛌.t) +| bdd_appl: ∀u,t. bdd u → bdd t → bdd (@u.t) | bdd_conv: ∀t1,t2. t1 ⇔ t2 → bdd t1 → bdd t2 . diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_balanced.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_balanced.ma index e28a95101..ffdbf93e4 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_balanced.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_balanced.ma @@ -19,7 +19,7 @@ include "delayed_updating/notation/relations/predicate_squarecap_1.ma". (* This condition applies to a structural path *) inductive pbc: predicate path ≝ -| pbc_empty: pbc 𝐞 +| pbc_empty: pbc (𝐞) | pbc_redex: ∀b. pbc b → pbc (𝗔◗b◖𝗟) | pbc_after: ∀b1,b2. pbc b1 → pbc b2 → pbc (b1●b2) . diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_depth.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_depth.ma new file mode 100644 index 000000000..e76c4943b --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_depth.ma @@ -0,0 +1,52 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "delayed_updating/syntax/path.ma". +include "ground/arith/nat_succ.ma". +include "ground/notation/functions/verticalbars_1.ma". + +(* DEPTH FOR PATH ***********************************************************) + +rec definition depth (p) on p: nat ≝ +match p with +[ list_empty ⇒ 𝟎 +| list_lcons l q ⇒ + match l with + [ label_node_d _ ⇒ depth q + | label_edge_L ⇒ ↑(depth q) + | label_edge_A ⇒ depth q + | label_edge_S ⇒ depth q + ] +]. + +interpretation + "depth (path)" + 'VerticalBars p = (depth p). + +(* Basic constructions ******************************************************) + +lemma depth_empty: 𝟎 = ❘𝐞❘. +// qed. + +lemma depth_d (q) (n): ❘q❘ = ❘𝗱❨n❩◗q❘. +// qed. + +lemma depth_L (q): ↑❘q❘ = ❘𝗟◗q❘. +// qed. + +lemma depth_A (q): ❘q❘ = ❘𝗔◗q❘. +// qed. + +lemma depth_S (q): ❘q❘ = ❘𝗦◗q❘. +// qed. diff --git a/matita/matita/contribs/lambdadelta/ground/lib/list_length.ma b/matita/matita/contribs/lambdadelta/ground/lib/list_length.ma index a0ba8d77b..e4df2ae4d 100644 --- a/matita/matita/contribs/lambdadelta/ground/lib/list_length.ma +++ b/matita/matita/contribs/lambdadelta/ground/lib/list_length.ma @@ -12,6 +12,7 @@ (* *) (**************************************************************************) +include "ground/notation/functions/verticalbars_1.ma". include "ground/lib/list.ma". include "ground/arith/nat_succ.ma". @@ -24,31 +25,33 @@ rec definition list_length A (l:list A) on l ≝ match l with interpretation "length (lists)" - 'card l = (list_length ? l). + 'VerticalBars l = (list_length ? l). (* Basic constructions ******************************************************) -lemma list_length_empty (A:Type[0]): |list_empty A| = 𝟎. +lemma list_length_empty (A:Type[0]): + ❘list_empty A❘ = 𝟎. // qed. -lemma list_length_lcons (A:Type[0]) (l:list A) (a:A): |a⨮l| = ↑|l|. +lemma list_length_lcons (A:Type[0]) (l:list A) (a:A): + ❘a⨮l❘ = ↑❘l❘. // qed. (* Basic inversions *********************************************************) lemma list_length_inv_zero_dx (A:Type[0]) (l:list A): - |l| = 𝟎 → l = ⓔ. + ❘l❘ = 𝟎 → l = ⓔ. #A * // #a #l >list_length_lcons #H elim (eq_inv_nsucc_zero … H) qed-. lemma list_length_inv_zero_sn (A:Type[0]) (l:list A): - (𝟎) = |l| → l = ⓔ. + (𝟎) = ❘l❘ → l = ⓔ. /2 width=1 by list_length_inv_zero_dx/ qed-. lemma list_length_inv_succ_dx (A:Type[0]) (l:list A) (x): - |l| = ↑x → - ∃∃tl,a. x = |tl| & l = a ⨮ tl. + ❘l❘ = ↑x → + ∃∃tl,a. x = ❘tl❘ & l = a ⨮ tl. #A * [ #x >list_length_empty #H elim (eq_inv_zero_nsucc … H) @@ -58,6 +61,6 @@ lemma list_length_inv_succ_dx (A:Type[0]) (l:list A) (x): qed-. lemma list_length_inv_succ_sn (A:Type[0]) (l:list A) (x): - ↑x = |l| → - ∃∃tl,a. x = |tl| & l = a ⨮ tl. + ↑x = ❘l❘ → + ∃∃tl,a. x = ❘tl❘ & l = a ⨮ tl. /2 width=1 by list_length_inv_succ_dx/ qed-. diff --git a/matita/matita/contribs/lambdadelta/ground/lib/subset_equivalence.ma b/matita/matita/contribs/lambdadelta/ground/lib/subset_equivalence.ma index b3957eaf3..cddb51e89 100644 --- a/matita/matita/contribs/lambdadelta/ground/lib/subset_equivalence.ma +++ b/matita/matita/contribs/lambdadelta/ground/lib/subset_equivalence.ma @@ -17,7 +17,7 @@ include "ground/lib/subset_inclusion.ma". (* EQUIVALENCE FOR SUBSETS **************************************************) -definition subset_eq (A): relation2 𝒫❨A❩ 𝒫❨A❩ ≝ +definition subset_eq (A): relation2 (𝒫❨A❩) (𝒫❨A❩) ≝ λu1,u2. ∧∧ u1 ⊆ u2 & u2 ⊆ u1. interpretation diff --git a/matita/matita/contribs/lambdadelta/ground/lib/subset_inclusion.ma b/matita/matita/contribs/lambdadelta/ground/lib/subset_inclusion.ma index 6f2e5c9b7..68eba7c1b 100644 --- a/matita/matita/contribs/lambdadelta/ground/lib/subset_inclusion.ma +++ b/matita/matita/contribs/lambdadelta/ground/lib/subset_inclusion.ma @@ -16,7 +16,7 @@ include "ground/lib/subset.ma". (* INCLUSION FOR SUBSETS ****************************************************) -definition subset_le (A): relation2 𝒫❨A❩ 𝒫❨A❩ ≝ +definition subset_le (A): relation2 (𝒫❨A❩) (𝒫❨A❩) ≝ λu1,u2. ∀p. p ϵ u1 → p ϵ u2. interpretation diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/circled_element_e_1.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/circled_element_e_1.ma index 9b0b84f56..1ce2e5d06 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/functions/circled_element_e_1.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/functions/circled_element_e_1.ma @@ -15,13 +15,13 @@ (* GROUND NOTATION **********************************************************) notation < "hvbox( ⓔ )" - non associative with precedence 75 + non associative with precedence 70 for @{ 'CircledElementE $S }. notation > "hvbox( ⓔ )" - non associative with precedence 75 + non associative with precedence 70 for @{ 'CircledElementE ? }. notation > "hvbox( ⓔ{ term 46 S } )" - non associative with precedence 75 + non associative with precedence 70 for @{ 'CircledElementE $S }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/downarrow_1.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/downarrow_1.ma index 6bc204a00..46000a861 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/functions/downarrow_1.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/functions/downarrow_1.ma @@ -14,6 +14,6 @@ (* GROUND NOTATION **********************************************************) -notation "hvbox( ↓ term 75 T )" - non associative with precedence 75 +notation "hvbox( ↓ term 70 T )" + non associative with precedence 70 for @{ 'DownArrow $T }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/downharpoonleft_2.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/downharpoonleft_2.ma index ca6946fb3..864a4ed5c 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/functions/downharpoonleft_2.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/functions/downharpoonleft_2.ma @@ -14,14 +14,14 @@ (* GROUND NOTATION **********************************************************) -notation < "hvbox( ⇃ term 75 a )" - non associative with precedence 75 +notation < "hvbox( ⇃ term 70 a )" + non associative with precedence 70 for @{ 'DownHarpoonLeft $S $a }. -notation > "hvbox( ⇃ term 75 a )" - non associative with precedence 75 +notation > "hvbox( ⇃ term 70 a )" + non associative with precedence 70 for @{ 'DownHarpoonLeft ? $a }. -notation > "hvbox( ⇃{ term 46 S } break term 75 a )" - non associative with precedence 75 +notation > "hvbox( ⇃{ term 46 S } break term 70 a )" + non associative with precedence 70 for @{ 'DownHarpoonLeft $S $a }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/downharpoonright_2.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/downharpoonright_2.ma index 3fdc1a8dc..4d332322e 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/functions/downharpoonright_2.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/functions/downharpoonright_2.ma @@ -14,14 +14,14 @@ (* GROUND NOTATION **********************************************************) -notation < "hvbox( ⇂ term 75 a )" - non associative with precedence 75 +notation < "hvbox( ⇂ term 70 a )" + non associative with precedence 70 for @{ 'DownHarpoonRight $S $a }. -notation > "hvbox( ⇂ term 75 a )" - non associative with precedence 75 +notation > "hvbox( ⇂ term 70 a )" + non associative with precedence 70 for @{ 'DownHarpoonRight ? $a }. -notation > "hvbox( ⇂{ term 46 S } break term 75 a )" - non associative with precedence 75 +notation > "hvbox( ⇂{ term 46 S } break term 70 a )" + non associative with precedence 70 for @{ 'DownHarpoonRight $S $a }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/downharpoonrightstar_3.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/downharpoonrightstar_3.ma index 017bd72d6..0a3a0ff2f 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/functions/downharpoonrightstar_3.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/functions/downharpoonrightstar_3.ma @@ -14,14 +14,14 @@ (* GROUND NOTATION **********************************************************) -notation < "hvbox( ⇂*[ break term 46 n ] break term 75 a )" - non associative with precedence 75 +notation < "hvbox( ⇂*[ break term 46 n ] break term 70 a )" + non associative with precedence 70 for @{ 'DownHarpoonRightStar $S $n $a }. -notation > "hvbox( ⇂*[ break term 46 n ] break term 75 a )" - non associative with precedence 75 +notation > "hvbox( ⇂*[ break term 46 n ] break term 70 a )" + non associative with precedence 70 for @{ 'DownHarpoonRightStar ? $n $a }. -notation > "hvbox( ⇂*{ term 46 S }[ break term 46 n ] break term 75 a )" - non associative with precedence 75 +notation > "hvbox( ⇂*{ term 46 S }[ break term 46 n ] break term 70 a )" + non associative with precedence 70 for @{ 'DownHarpoonRightStar $S $n $a }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/downspoon_1.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/downspoon_1.ma index e4bc3eb13..af69da11b 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/functions/downspoon_1.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/functions/downspoon_1.ma @@ -14,6 +14,6 @@ (* GROUND NOTATION **********************************************************) -notation "hvbox( ⫰ term 75 T )" - non associative with precedence 75 +notation "hvbox( ⫰ term 70 T )" + non associative with precedence 70 for @{ 'DownSpoon $T }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/downspoonstar_2.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/downspoonstar_2.ma index 03f188bd7..a3688f3a0 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/functions/downspoonstar_2.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/functions/downspoonstar_2.ma @@ -14,6 +14,6 @@ (* GROUND NOTATION **********************************************************) -notation "hvbox( ⫰ *[ term 46 n ] break term 75 T )" - non associative with precedence 75 +notation "hvbox( ⫰ *[ term 46 n ] break term 70 T )" + non associative with precedence 70 for @{ 'DownSpoonStar $n $T }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/element_b_2.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/element_b_2.ma index 679cab596..23dbe7a26 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/functions/element_b_2.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/functions/element_b_2.ma @@ -15,5 +15,5 @@ (* GROUND NOTATION **********************************************************) notation "hvbox( 𝐛❨ term 46 d, break term 46 h ❩ )" - non associative with precedence 75 + non associative with precedence 70 for @{ 'ElementB $d $h }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/element_e_0.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/element_e_0.ma index d890760a2..41d0fef1a 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/functions/element_e_0.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/functions/element_e_0.ma @@ -15,5 +15,5 @@ (* GROUND NOTATION **********************************************************) notation "𝐞" - non associative with precedence 75 + non associative with precedence 70 for @{ 'ElementE }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/element_i_0.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/element_i_0.ma index d3d8cdbf0..80db802a6 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/functions/element_i_0.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/functions/element_i_0.ma @@ -15,5 +15,5 @@ (* GROUND NOTATION **********************************************************) notation "hvbox( 𝐢 )" - non associative with precedence 75 + non associative with precedence 70 for @{ 'ElementI }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/element_t_1.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/element_t_1.ma index 7e136deb6..816d28fb4 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/functions/element_t_1.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/functions/element_t_1.ma @@ -15,5 +15,5 @@ (* GROUND NOTATION **********************************************************) notation "hvbox( 𝐭❨ break term 46 a ❩ )" - non associative with precedence 75 + non associative with precedence 70 for @{ 'ElementT $a }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/element_u_1.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/element_u_1.ma index 48922bebb..28f857386 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/functions/element_u_1.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/functions/element_u_1.ma @@ -15,5 +15,5 @@ (* GROUND NOTATION **********************************************************) notation "hvbox( 𝐮 ❨ break term 46 a ❩ )" - non associative with precedence 75 + non associative with precedence 70 for @{ 'ElementU $a }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/infinity_0.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/infinity_0.ma index 733384f17..4415410b1 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/functions/infinity_0.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/functions/infinity_0.ma @@ -15,5 +15,5 @@ (* GROUND NOTATION **********************************************************) notation "∞" - non associative with precedence 75 + non associative with precedence 70 for @{ 'Infinity }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/no_0.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/no_0.ma index ff366672e..9b677d05d 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/functions/no_0.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/functions/no_0.ma @@ -15,5 +15,5 @@ (* GROUND NOTATION **********************************************************) notation "Ⓕ" - non associative with precedence 75 + non associative with precedence 70 for @{'no}. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/one_0.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/one_0.ma index 54fd7e8e7..c60fb157e 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/functions/one_0.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/functions/one_0.ma @@ -15,5 +15,5 @@ (* GROUND NOTATION **********************************************************) notation "𝟏" - non associative with precedence 75 + non associative with precedence 70 for @{ 'One }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/onezero_0.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/onezero_0.ma index dcb2622ed..4bf78abc3 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/functions/onezero_0.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/functions/onezero_0.ma @@ -15,5 +15,5 @@ (* GROUND NOTATION **********************************************************) notation "𝟙𝟘" - non associative with precedence 75 + non associative with precedence 70 for @{ 'OneZero }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/powerclass_1.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/powerclass_1.ma index 8eab6e62f..553fd7d34 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/functions/powerclass_1.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/functions/powerclass_1.ma @@ -15,5 +15,5 @@ (* GROUND NOTATION **********************************************************) notation "hvbox( 𝒫 ❨ break term 46 S ❩ )" - non associative with precedence 75 + non associative with precedence 70 for @{ 'PowerClass $S }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/tuple_4.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/tuple_4.ma index bf633f668..af218aff6 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/functions/tuple_4.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/functions/tuple_4.ma @@ -15,5 +15,5 @@ (* GROUND NOTATION **********************************************************) notation "hvbox ( 〈 term 46 x1, break term 46 x2 , break term 46 x3, break term 46 x4 〉 )" - non associative with precedence 75 + non associative with precedence 70 for @{ 'Tuple $x1 $x2 $x3 $x4 }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/two_0.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/two_0.ma index e2c957b8b..acbe4e48a 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/functions/two_0.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/functions/two_0.ma @@ -15,5 +15,5 @@ (* GROUND NOTATION **********************************************************) notation "𝟐" - non associative with precedence 75 + non associative with precedence 70 for @{ 'Two }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/uparrow_1.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/uparrow_1.ma index 759802da5..cc3bb324b 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/functions/uparrow_1.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/functions/uparrow_1.ma @@ -14,6 +14,6 @@ (* GROUND NOTATION **********************************************************) -notation "hvbox( ↑ term 75 T )" - non associative with precedence 75 +notation "hvbox( ↑ term 70 T )" + non associative with precedence 70 for @{ 'UpArrow $T }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/uparrowstar_2.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/uparrowstar_2.ma index c25f90ffa..899beb264 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/functions/uparrowstar_2.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/functions/uparrowstar_2.ma @@ -14,6 +14,6 @@ (* GROUND NOTATION **********************************************************) -notation "hvbox( ↑*[ term 46 n ] break term 75 T )" - non associative with precedence 75 +notation "hvbox( ↑*[ term 46 n ] break term 70 T )" + non associative with precedence 70 for @{ 'UpArrowStar $n $T }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/updownarrowstar_1.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/updownarrowstar_1.ma index 9c2d6625b..b2a9bd413 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/functions/updownarrowstar_1.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/functions/updownarrowstar_1.ma @@ -14,6 +14,6 @@ (* GROUND NOTATION **********************************************************) -notation "hvbox( ↕* term 75 T )" - non associative with precedence 75 +notation "hvbox( ↕* term 70 T )" + non associative with precedence 70 for @{ 'UpDownArrowStar $T }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/upspoon_1.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/upspoon_1.ma index 8299766a9..503473ab6 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/functions/upspoon_1.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/functions/upspoon_1.ma @@ -14,6 +14,6 @@ (* GROUND NOTATION **********************************************************) -notation "hvbox( ⫯ term 75 T )" - non associative with precedence 75 +notation "hvbox( ⫯ term 70 T )" + non associative with precedence 70 for @{ 'UpSpoon $T }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/upspoonstar_2.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/upspoonstar_2.ma index 31015e1bd..042239a60 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/functions/upspoonstar_2.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/functions/upspoonstar_2.ma @@ -14,6 +14,6 @@ (* GROUND NOTATION **********************************************************) -notation "hvbox( ⫯*[ term 46 n ] break term 75 T )" - non associative with precedence 75 +notation "hvbox( ⫯*[ term 46 n ] break term 70 T )" + non associative with precedence 70 for @{ 'UpSpoonStar $n $T }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/verticalbars_1.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/verticalbars_1.ma new file mode 100644 index 000000000..85e0be00c --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground/notation/functions/verticalbars_1.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 C ❘ )" + non associative with precedence 70 + for @{ 'VerticalBars $C }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/yes_0.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/yes_0.ma index 5b9480042..ff2941343 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/functions/yes_0.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/functions/yes_0.ma @@ -15,5 +15,5 @@ (* GROUND NOTATION **********************************************************) notation "Ⓣ" - non associative with precedence 75 + non associative with precedence 70 for @{'yes}. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/zero_0.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/zero_0.ma index a4dc1a442..895c8e772 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/functions/zero_0.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/functions/zero_0.ma @@ -15,5 +15,5 @@ (* GROUND NOTATION **********************************************************) notation "𝟎" - non associative with precedence 75 + non associative with precedence 70 for @{ 'Zero }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/zeroone_0.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/zeroone_0.ma index 1814c9bfa..3b6d7b5b8 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/functions/zeroone_0.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/functions/zeroone_0.ma @@ -15,5 +15,5 @@ (* GROUND NOTATION **********************************************************) notation "𝟘𝟙" - non associative with precedence 75 + non associative with precedence 70 for @{ 'ZeroOne }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/zerozero_0.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/zerozero_0.ma index 957111fd2..bf61a2153 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/functions/zerozero_0.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/functions/zerozero_0.ma @@ -15,5 +15,5 @@ (* GROUND NOTATION **********************************************************) notation "𝟘𝟘" - non associative with precedence 75 + non associative with precedence 70 for @{ 'ZeroZero }. diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_pat_pat_id.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_pat_pat_id.ma index 3fb5d1789..90bee366b 100644 --- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_pat_pat_id.ma +++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_pat_pat_id.ma @@ -28,7 +28,7 @@ lemma pr_pat_id_des (i1) (i2): (*** at_div_id_dx *) theorem pr_pat_div_id_dx (f): - H_pr_pat_div f 𝐢 𝐢 f. + H_pr_pat_div f (𝐢 ) (𝐢) f. #f #jf #j0 #j #Hf #H0 lapply (pr_pat_id_des … H0) -H0 #H destruct /2 width=3 by ex2_intro/ @@ -36,5 +36,5 @@ qed-. (*** at_div_id_sn *) theorem pr_pat_div_id_sn (f): - H_pr_pat_div 𝐢 f f 𝐢. + H_pr_pat_div (𝐢) f f (𝐢). /3 width=6 by pr_pat_div_id_dx, pr_pat_div_comm/ qed-. diff --git a/matita/matita/predefined_virtuals.ml b/matita/matita/predefined_virtuals.ml index 94f34fb10..d8528aae2 100644 --- a/matita/matita/predefined_virtuals.ml +++ b/matita/matita/predefined_virtuals.ml @@ -1504,7 +1504,7 @@ let load_predefined_virtuals () = let predefined_classes = [ ["&"; "⅋"; ]; - ["|"; "∥"; ]; + ["|"; "❘"; "∥"; ]; ["!"; "¡"; "⫯"; "⫰"; "⟟"; "⫱"; ]; ["?"; "¿"; "⸮"; ]; [":"; "⁝"; ]; -- 2.39.2