From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Sat, 22 Jan 2022 00:35:11 +0000 (+0100)
Subject: update in delayed_updating
X-Git-Tag: make_still_working~105
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=13584a37bbcde10e03c8a488f5b93e1e042da0a6

update in delayed_updating

+ mark label added
+ bugs fixed in depth and reduction
+ two notations changed
---

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/class_b_0.ma b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/class_b_0.ma
new file mode 100644
index 000000000..46c63d436
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/class_b_0.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                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* NOTATION FOR DELAYED UPDATING ********************************************)
+
+notation "hvbox( 𝐁 )"
+  non associative with precedence 70
+  for @{ 'ClassB }.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/class_p_0.ma b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/class_p_0.ma
new file mode 100644
index 000000000..9f9bbd754
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/class_p_0.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                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* NOTATION FOR DELAYED UPDATING ********************************************)
+
+notation "hvbox( 𝐏 )"
+  non associative with precedence 70
+  for @{ 'ClassP }.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/m_hook_1.ma b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/m_hook_1.ma
new file mode 100644
index 000000000..0860eaffa
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/m_hook_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                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* NOTATION FOR DELAYED UPDATING ********************************************)
+
+notation "hvbox( ɱ. break term 70 t )"
+  non associative with precedence 70
+  for @{ 'MHook $t }.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/nodelabel_m_0.ma b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/nodelabel_m_0.ma
new file mode 100644
index 000000000..f34f1a7ee
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/nodelabel_m_0.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                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* NOTATION FOR DELAYED UPDATING ********************************************)
+
+notation "hvbox( 𝗺 )"
+  non associative with precedence 70
+  for @{ 'NodeLabelM }.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/relations/predicate_p_tail_1.ma b/matita/matita/contribs/lambdadelta/delayed_updating/notation/relations/predicate_p_tail_1.ma
deleted file mode 100644
index 73397b8d9..000000000
--- a/matita/matita/contribs/lambdadelta/delayed_updating/notation/relations/predicate_p_tail_1.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                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-(* NOTATION FOR DELAYED UPDATING ********************************************)
-
-notation "hvbox( Ꝕ term 70 x )"
-  non associative with precedence 45
-  for @{ 'PredicatePTail $x }.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/relations/predicate_squarecap_1.ma b/matita/matita/contribs/lambdadelta/delayed_updating/notation/relations/predicate_squarecap_1.ma
deleted file mode 100644
index 64e50fc91..000000000
--- a/matita/matita/contribs/lambdadelta/delayed_updating/notation/relations/predicate_squarecap_1.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                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-(* NOTATION FOR DELAYED UPDATING ********************************************)
-
-notation "hvbox( ⊓ term 70 p )"
-  non associative with precedence 45
-  for @{ 'PredicateSquareCap $p }.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr.ma
index 5b5036593..2ff6159cf 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr.ma
@@ -25,8 +25,8 @@ include "delayed_updating/notation/relations/black_rightarrow_df_4.ma".
 definition dfr (p) (q): relation2 prototerm prototerm ≝
            λt1,t2. ∃b.
            let r ≝ p●𝗔◗b●𝗟◗q in
-           ∧∧ ⊓(⊗b) & r◖𝗱(↑❘q❘) ϵ t1 &
-              t2 ⇔ t1[⋔r←𝛗(↑❘q❘).t1⋔(p◖𝗦)]
+           ∧∧ ⊗b ϵ 𝐁 & r◖𝗱❘q❘ ϵ t1 &
+              t1[⋔r←𝛗❘q❘.(t1⋔(p◖𝗦))] ⇔ t2
 .
 
 interpretation
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 5d6c3cfef..73d4cbf46 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_ifr.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_ifr.ma
@@ -15,6 +15,7 @@
 include "delayed_updating/reduction/dfr.ma".
 include "delayed_updating/reduction/ifr.ma".
 include "delayed_updating/substitution/fsubst_lift.ma".
+include "delayed_updating/syntax/prototerm_proper_constructors.ma".
 
 (* DELAYED FOCUSED REDUCTION ************************************************)
 
@@ -24,9 +25,15 @@ lemma dfr_lift_bi (f) (p) (q) (t1) (t2): t1 ϵ 𝐓 →
 * #b * #Hb #Ht1 #Ht2
 @(ex_intro … (⊗b)) @and3_intro
 [ //
-| lapply (in_comp_lift_bi f … Ht1) -Ht1 #Ht1 
-
-
-
-
+| lapply (in_comp_lift_bi f … Ht1) -Ht1 #Ht1
+| lapply (eq_lift_bi f … Ht2) -Ht2 #Ht2
+  @(subset_eq_trans … Ht2) -t2
+  @(subset_eq_trans … (lift_fsubst …))
+  [ <structure_append <structure_A_sn <structure_append <structure_L_sn
+  | //
+  | /2 width=2 by ex_intro/
+  | //
+  ]
+]
+  
 
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr.ma
index 582f6ed57..b58f9ee18 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr.ma
@@ -24,8 +24,8 @@ include "delayed_updating/notation/relations/black_rightarrow_f_4.ma".
 definition ifr (p) (q): relation2 prototerm prototerm ≝
            λt1,t2. ∃b.
            let r ≝ p●𝗔◗b●𝗟◗q in
-           ∧∧ ⊓(⊗b) & r◖𝗱(↑❘q❘) ϵ t1 &
-              t2 ⇔ t1[⋔r←↑[𝐮❨↑❘q❘❩]t1⋔(p◖𝗦)]
+           ∧∧ ⊗b ϵ 𝐁 & r◖𝗱❘q❘ ϵ t1 &
+              t1[⋔r←↑[𝐮❨❘q❘❩](t1⋔(p◖𝗦))] ⇔ t2
 .
 
 interpretation
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/fsubst_lift.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/fsubst_lift.ma
index 08ff3ebb3..21186fdd6 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/fsubst_lift.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/fsubst_lift.ma
@@ -20,12 +20,12 @@ include "delayed_updating/syntax/prototerm_proper.ma".
 
 (* FOCALIZED SUBSTITUTION ***************************************************)
 
-lemma lift_fsubst_sn (f) (t) (u) (p): Ꝕu →
+lemma lift_fsubst_sn (f) (t) (u) (p): u ϵ 𝐏 →
       (↑[f]t)[⋔(⊗p)←↑[↑[p]f]u] ⊆ ↑[f](t[⋔p←u]).
 #f #t #u #p #Hu #ql * *
 [ #rl * #r #Hr #H1 #H2 destruct
   >lift_append_proper_dx
-  /4 width=1 by subset_in_ext_f1_dx, or_introl/
+  /4 width=5 by in_comp_lift_bi, in_ppc_comp_trans, or_introl, ex2_intro/
 | * #q #Hq #H1 #H0
   @(ex2_intro … H1) @or_intror @conj // *
   [ <list_append_empty_dx #H2 destruct
@@ -36,15 +36,15 @@ lemma lift_fsubst_sn (f) (t) (u) (p): Ꝕu →
 ]
 qed-.
 
-lemma lift_fsubst_dx (f) (t) (u) (p): Ꝕu → p ϵ ▵t → t ϵ 𝐓 →
+lemma lift_fsubst_dx (f) (t) (u) (p): u ϵ 𝐏 → p ϵ ▵t → t ϵ 𝐓 →
       ↑[f](t[⋔p←u]) ⊆ (↑[f]t)[⋔(⊗p)←↑[↑[p]f]u].
 #f #t #u #p #Hu #H1p #H2p #ql * #q * *
 [ #r #Hu #H1 #H2 destruct
   @or_introl @ex2_intro
-  [|| <lift_append_proper_dx /2 width=1 by/ ]
+  [|| <lift_append_proper_dx /2 width=5 by in_ppc_comp_trans/ ]
   /2 width=3 by ex2_intro/
 | #Hq #H0 #H1 destruct
-  @or_intror @conj [ /2 width=1 by subset_in_ext_f1_dx/ ] *
+  @or_intror @conj [ /2 width=1 by in_comp_lift_bi/ ] *
   [ <list_append_empty_dx #Hr @(H0 … (𝐞)) -H0
     <list_append_empty_dx @H2p -H2p /2 width=1 by prototerm_in_comp_root/
   | #l #r #Hr
@@ -54,6 +54,6 @@ lemma lift_fsubst_dx (f) (t) (u) (p): Ꝕu → p ϵ ▵t → t ϵ 𝐓 →
 ]
 qed-.
 
-lemma lift_fsubst (f) (t) (u) (p): Ꝕu → p ϵ ▵t → t ϵ 𝐓 →
+lemma lift_fsubst (f) (t) (u) (p): u ϵ 𝐏 → p ϵ ▵t → t ϵ 𝐓 →
       (↑[f]t)[⋔(⊗p)←↑[↑[p]f]u] ⇔ ↑[f](t[⋔p←u]).
 /4 width=3 by lift_fsubst_sn, conj, lift_fsubst_dx/ qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift.ma
index 0dbb6043a..fa6328684 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift.ma
@@ -29,14 +29,15 @@ match p with
 [ list_empty     ⇒ k f (𝐞)
 | list_lcons l q ⇒
   match l with
-  [ label_node_d n ⇒
+  [ label_d n ⇒
     match q with
     [ list_empty     ⇒ lift_gen (A) (λg,p. k g (𝗱(f@❨n❩)◗p)) (f∘𝐮❨n❩) q
     | list_lcons _ _ ⇒ lift_gen (A) k (f∘𝐮❨n❩) q
     ]
-  | label_edge_L   ⇒ lift_gen (A) (λg,p. k g (𝗟◗p)) (⫯f) q
-  | label_edge_A   ⇒ lift_gen (A) (λg,p. k g (𝗔◗p)) f q
-  | label_edge_S   ⇒ lift_gen (A) (λg,p. k g (𝗦◗p)) f q
+  | label_m   ⇒ lift_gen (A) k f q
+  | label_L   ⇒ lift_gen (A) (λg,p. k g (𝗟◗p)) (⫯f) q
+  | label_A   ⇒ lift_gen (A) (λg,p. k g (𝗔◗p)) f q
+  | label_S   ⇒ lift_gen (A) (λg,p. k g (𝗦◗p)) f q
   ]
 ].
 
@@ -72,6 +73,10 @@ lemma lift_d_lcons_sn (A) (k) (p) (l) (n) (f):
       ↑❨k, f∘𝐮❨ninj n❩, l◗p❩ = ↑{A}❨k, f, 𝗱n◗l◗p❩.
 // qed.
 
+lemma lift_m_sn (A) (k) (p) (f):
+      ↑❨k, f, p❩ = ↑{A}❨k, f, 𝗺◗p❩.
+// qed.
+
 lemma lift_L_sn (A) (k) (p) (f):
       ↑❨(λg,p. k g (𝗟◗p)), ⫯f, p❩ = ↑{A}❨k, f, 𝗟◗p❩.
 // qed.
@@ -98,12 +103,20 @@ lemma lift_path_d_lcons_sn (f) (p) (l) (n):
       ↑[f∘𝐮❨ninj n❩](l◗p) = ↑[f](𝗱n◗l◗p).
 // qed.
 
+lemma lift_path_m_sn (f) (p):
+      ↑[f]p = ↑[f](𝗺◗p).
+// qed.
+
 (* Basic constructions with proj_rmap ***************************************)
 
 lemma lift_rmap_d_sn (f) (p) (n):
       ↑[p](f∘𝐮❨ninj n❩) = ↑[𝗱n◗p]f.
 #f * // qed.
 
+lemma lift_rmap_m_sn (f) (p):
+      ↑[p]f = ↑[𝗺◗p]f.
+// qed.
+
 lemma lift_rmap_L_sn (f) (p):
       ↑[p](⫯f) = ↑[𝗟◗p]f.
 // qed.
@@ -121,7 +134,8 @@ lemma lift_rmap_S_sn (f) (p):
 lemma lift_rmap_append (p2) (p1) (f):
       ↑[p2]↑[p1]f = ↑[p1●p2]f.
 #p2 #p1 elim p1 -p1 // * [ #n ] #p1 #IH #f //
-[ <lift_rmap_A_sn <lift_rmap_A_sn //
+[ <lift_rmap_m_sn <lift_rmap_m_sn //
+| <lift_rmap_A_sn <lift_rmap_A_sn //
 | <lift_rmap_S_sn <lift_rmap_S_sn //
 ]
 qed.
@@ -132,11 +146,12 @@ lemma path_ind_lift (Q:predicate …):
       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)) →
       (∀p. Q p → Q (𝗔◗p)) →
       (∀p. Q p → Q (𝗦◗p)) →
       ∀p. Q p.
-#Q #IH1 #IH2 #IH3 #IH4 #IH5 #IH6 #p
+#Q #IH1 #IH2 #IH3 #IH4 #IH5 #IH6 #IH7 #p
 elim p -p [| * [ #n * ] ]
 /2 width=1 by/
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_eq.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_eq.ma
index 3413b07db..0273a3eb8 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_eq.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_eq.ma
@@ -55,6 +55,7 @@ lemma lift_path_append_sn (p) (f) (q):
       q●↑[f]p = ↑❨(λg,p. proj_path g (q●p)), f, p❩.
 #p @(path_ind_lift … p) -p // [ #n #l #p |*: #p ] #IH #f #q
 [ <lift_d_lcons_sn <lift_d_lcons_sn <IH -IH //
+| <lift_m_sn <lift_m_sn //
 | <lift_L_sn <lift_L_sn >lift_lcons_alt >lift_append_rcons_sn
   <IH <IH -IH <list_append_rcons_sn //
 | <lift_A_sn <lift_A_sn >lift_lcons_alt >lift_append_rcons_sn
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_prototerm.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_prototerm.ma
index 919326045..4a0615a3c 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_prototerm.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_prototerm.ma
@@ -26,4 +26,10 @@ interpretation
 
 lemma in_comp_lift_bi (f) (p) (t):
       p ϵ t → ↑[f]p ϵ ↑[f]t.
-/2 width=1 by subset_in_ext_f1_dx/ qed.
+/2 width=1 by subset_in_ext_f1_dx/
+qed.
+
+lemma eq_lift_bi (f) (t1) (t2):
+      t1 ⇔ t2 → ↑[f]t1 ⇔ ↑[f]t2.
+/2 width=1 by subset_equivalence_ext_f1_bi/
+qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_structure.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_structure.ma
index 4db66c064..b9bc27c54 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_structure.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_structure.ma
@@ -41,12 +41,13 @@ lemma lift_des_structure (q) (p) (f):
 
 (* Constructions with proper condition for path *****************************)
 
-lemma lift_append_proper_dx (p2) (p1) (f): Ꝕp2 →
+lemma lift_append_proper_dx (p2) (p1) (f): p2 ϵ 𝐏 →
       (⊗p1)●(↑[↑[p1]f]p2) = ↑[f](p1●p2).
 #p2 #p1 @(path_ind_lift … p1) -p1 //
 [ #n | #n #l #p1 |*: #p1 ] #IH #f #Hp2
 [ elim (ppc_inv_lcons … Hp2) -Hp2 #l #q #H destruct //
 | <lift_path_d_lcons_sn <IH //
+| <lift_path_m_sn <IH //
 | <lift_path_L_sn <IH //
 | <lift_path_A_sn <IH //
 | <lift_path_S_sn <IH //
@@ -60,6 +61,11 @@ lemma lift_d_empty_dx (n) (p) (f):
 #n #p #f <lift_append_proper_dx // 
 qed.
 
+lemma lift_m_dx (p) (f):
+      ⊗p = ↑[f](p◖𝗺).
+#p #f <lift_append_proper_dx //
+qed.
+
 lemma lift_L_dx (p) (f):
       (⊗p)◖𝗟 = ↑[f](p◖𝗟).
 #p #f <lift_append_proper_dx //
@@ -96,6 +102,23 @@ lemma lift_path_inv_d_sn (k) (q) (p) (f):
 | <lift_path_d_lcons_sn #H
   elim (IH … H) -IH -H #r #h #Hr #Hh #Hq #Hp destruct
   /2 width=5 by ex4_2_intro/
+| <lift_path_m_sn #H
+  elim (IH … H) -IH -H #r #h #Hr #Hh #Hq #Hp destruct
+  /2 width=5 by ex4_2_intro/
+| <lift_path_L_sn #H destruct
+| <lift_path_A_sn #H destruct
+| <lift_path_S_sn #H destruct
+]
+qed-.
+
+lemma lift_path_inv_m_sn (q) (p) (f):
+      (𝗺◗q) = ↑[f]p → ⊥.
+#q #p @(path_ind_lift … p) -p
+[| #n | #n #l #p |*: #p ] [|*: #IH ] #f
+[ <lift_path_empty #H destruct
+| <lift_path_d_empty_sn #H destruct
+| <lift_path_d_lcons_sn #H /2 width=2 by/
+| <lift_path_m_sn #H /2 width=2 by/
 | <lift_path_L_sn #H destruct
 | <lift_path_A_sn #H destruct
 | <lift_path_S_sn #H destruct
@@ -112,6 +135,9 @@ lemma lift_path_inv_L_sn (q) (p) (f):
 | <lift_path_d_lcons_sn #H
   elim (IH … H) -IH -H #r1 #r2 #Hr1 #Hq #Hp destruct
   /2 width=5 by ex3_2_intro/
+| <lift_path_m_sn #H
+  elim (IH … H) -IH -H #r1 #r2 #Hr1 #Hq #Hp destruct
+  /2 width=5 by ex3_2_intro/
 | <lift_path_L_sn #H destruct -IH
   /2 width=5 by ex3_2_intro/
 | <lift_path_A_sn #H destruct
@@ -129,6 +155,9 @@ lemma lift_path_inv_A_sn (q) (p) (f):
 | <lift_path_d_lcons_sn #H
   elim (IH … H) -IH -H #r1 #r2 #Hr1 #Hq #Hp destruct
   /2 width=5 by ex3_2_intro/
+| <lift_path_m_sn #H
+  elim (IH … H) -IH -H #r1 #r2 #Hr1 #Hq #Hp destruct
+  /2 width=5 by ex3_2_intro/
 | <lift_path_L_sn #H destruct
 | <lift_path_A_sn #H destruct -IH
   /2 width=5 by ex3_2_intro/
@@ -146,7 +175,9 @@ lemma lift_path_inv_S_sn (q) (p) (f):
 | <lift_path_d_lcons_sn #H
   elim (IH … H) -IH -H #r1 #r2 #Hr1 #Hq #Hp destruct
   /2 width=5 by ex3_2_intro/
-| <lift_path_L_sn #H destruct
+| <lift_path_m_sn #H
+  elim (IH … H) -IH -H #r1 #r2 #Hr1 #Hq #Hp destruct
+  /2 width=5 by ex3_2_intro/| <lift_path_L_sn #H destruct
 | <lift_path_A_sn #H destruct
 | <lift_path_S_sn #H destruct -IH
   /2 width=5 by ex3_2_intro/
@@ -155,8 +186,8 @@ qed-.
 
 (* Inversions with proper condition for path ********************************)
 
-lemma lift_inv_append_proper_dx (q2) (q1) (p) (f): Ꝕq2 →
-      q1●q2 = ↑[f]p →
+lemma lift_inv_append_proper_dx (q2) (q1) (p) (f):
+      q2 ϵ 𝐏 → q1●q2 = ↑[f]p →
       ∃∃p1,p2. ⊗p1 = q1 & ↑[↑[p1]f]p2 = q2 & p1●p2 = p.
 #q2 #q1 elim q1 -q1
 [ #p #f #Hq2 <list_append_empty_sn #H destruct
@@ -165,6 +196,7 @@ lemma lift_inv_append_proper_dx (q2) (q1) (p) (f): Ꝕq2 →
   [ elim (lift_path_inv_d_sn … H) -H #r1 #m1 #_ #_ #H0 #_ -IH
     elim (eq_inv_list_empty_append … H0) -H0 #_ #H0 destruct
     elim Hq2 -Hq2 //
+  | elim (lift_path_inv_m_sn … H)
   | elim (lift_path_inv_L_sn … H) -H #r1 #s1 #Hr1 #Hs1 #H0 destruct
     elim (IH … Hs1) -IH -Hs1 // -Hq2 #p1 #p2 #H1 #H2 #H3 destruct
     @(ex3_2_intro … (r1●𝗟◗p1)) //
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 ee69726db..897773a42 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/bdd_term.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/bdd_term.ma
@@ -35,12 +35,14 @@ interpretation
   "by-depth delayed (prototerm)"
   'ClassDPhi = (bdd).
 
+(*
+
 (* Basic inversions *********************************************************)
 
 lemma bdd_inv_in_comp_gen:
       ∀t,p. t ϵ 𝐃𝛗 → p ϵ t →
       ∨∨ ∃∃n. #n ⇔ t & 𝗱n◗𝐞 = p
-       | ∃∃u,q,n. u ϵ 𝐃𝛗 & q ϵ u & 𝛗n.u ⇔ t & 𝗱n◗q = p
+       | ∃∃u,q,n. u ϵ 𝐃𝛗 & q ϵ u & 𝛗n.u ⇔ t & 𝗱n◗𝗺◗q = p
        | ∃∃u,q. u ϵ 𝐃𝛗 & q ϵ u & 𝛌.u ⇔ t & 𝗟◗q = p
        | ∃∃v,u,q. v ϵ 𝐃𝛗 & u ϵ 𝐃𝛗 & q ϵ u & @v.u ⇔ t & 𝗔◗q = p
        | ∃∃v,u,q. v ϵ 𝐃𝛗 & u ϵ 𝐃𝛗 & q ϵ v & @v.u ⇔ t & 𝗦◗q = p
@@ -64,12 +66,13 @@ qed-.
 lemma bdd_inv_in_comp_d:
       ∀t,q,n. t ϵ 𝐃𝛗 → 𝗱n◗q ϵ t →
       ∨∨ ∧∧ #n ⇔ t & 𝐞 = q
-       | ∃∃u. u ϵ 𝐃𝛗 & q ϵ u & 𝛗n.u ⇔ t
+       | ∃∃u. u ϵ 𝐃𝛗 & q ϵ ɱ.u & 𝛗n.u ⇔ t
 .
 #t #q #n #Ht #Hq
 elim (bdd_inv_in_comp_gen … Ht Hq) -Ht -Hq *
 [ #n0 #H1 #H2 destruct /3 width=1 by or_introl, conj/
-| #u0 #q0 #n0 #Hu0 #Hq0 #H1 #H2 destruct /3 width=4 by ex3_intro, or_intror/
+| #u0 #q0 #n0 #Hu0 #Hq0 #H1 #H2 destruct
+ /4 width=4 by ex3_intro, ex2_intro, or_intror/
 | #u0 #q0 #_ #_ #_ #H0 destruct
 | #v0 #u0 #q0 #_ #_ #_ #_ #H0 destruct
 | #v0 #u0 #q0 #_ #_ #_ #_ #H0 destruct
@@ -79,7 +82,7 @@ qed-.
 lemma bdd_inv_in_root_d:
       ∀t,q,n. t ϵ 𝐃𝛗 → 𝗱n◗q ϵ ▵t →
       ∨∨ ∧∧ #n ⇔ t & 𝐞 = q
-       | ∃∃u. u ϵ 𝐃𝛗 & q ϵ ▵u & 𝛗n.u ⇔ t
+       | ∃∃u. u ϵ 𝐃𝛗 & q ϵ ▵ɱ.u & 𝛗n.u ⇔ t
 .
 #t #q #n #Ht * #r #Hq
 elim (bdd_inv_in_comp_d … Ht Hq) -Ht -Hq *
@@ -210,3 +213,4 @@ lemma bbd_mono_in_root_d:
   ]
 ]
 qed-.
+*)
\ No newline at end of file
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/label.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/label.ma
index d2a5c0783..74318f333 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/label.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/label.ma
@@ -14,6 +14,7 @@
 
 include "ground/arith/pnat.ma".
 include "delayed_updating/notation/functions/nodelabel_d_1.ma".
+include "delayed_updating/notation/functions/nodelabel_m_0.ma".
 include "delayed_updating/notation/functions/edgelabel_l_0.ma".
 include "delayed_updating/notation/functions/edgelabel_a_0.ma".
 include "delayed_updating/notation/functions/edgelabel_s_0.ma".
@@ -21,24 +22,29 @@ include "delayed_updating/notation/functions/edgelabel_s_0.ma".
 (* LABEL ********************************************************************)
 
 inductive label: Type[0] ≝
-| label_node_d: pnat → label
-| label_edge_L: label
-| label_edge_A: label
-| label_edge_S: label
+| label_d: pnat → label
+| label_m: label
+| label_L: label
+| label_A: label
+| label_S: label
 .
 
 interpretation
   "variable reference by depth (label)"
-  'NodeLabelD p = (label_node_d p).
+  'NodeLabelD p = (label_d p).
+
+interpretation
+  "mark (label)"
+  'NodeLabelM = (label_m).
 
 interpretation
   "name-free functional abstruction (label)"
-  'EdgeLabelL = (label_edge_L).
+  'EdgeLabelL = (label_L).
 
 interpretation
   "application (label)"
-  'EdgeLabelA = (label_edge_A).
+  'EdgeLabelA = (label_A).
 
 interpretation
   "side branch (label)"
-  'EdgeLabelS = (label_edge_S).
+  'EdgeLabelS = (label_S).
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 ffdbf93e4..017cfc5ba 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_balanced.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_balanced.ma
@@ -13,17 +13,17 @@
 (**************************************************************************)
 
 include "delayed_updating/syntax/path.ma".
-include "delayed_updating/notation/relations/predicate_squarecap_1.ma".
+include "delayed_updating/notation/functions/class_b_0.ma".
 
 (* BALANCE CONDITION FOR PATH ***********************************************)
 
 (* 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)
 .
 
 interpretation
   "balance condition (path)"
-  'PredicateSquareCap p = (pbc p).
+  'ClassB = (pbc).
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_depth.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_depth.ma
index efeaf86b4..88952c2bc 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_depth.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_depth.ma
@@ -13,20 +13,20 @@
 (**************************************************************************)
 
 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 ≝
+rec definition depth (p) on p: pnat ≝
 match p with
-[ list_empty     ⇒ 𝟎
+[ 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
+  [ label_d _ ⇒ depth q
+  | label_m   ⇒ depth q
+  | label_L   ⇒ ↑(depth q)
+  | label_A   ⇒ depth q
+  | label_S   ⇒ depth q
   ]
 ].
 
@@ -36,12 +36,15 @@ interpretation
 
 (* Basic constructions ******************************************************)
 
-lemma depth_empty: 𝟎 = ❘𝐞❘.
+lemma depth_empty: 𝟏 = ❘𝐞❘.
 // qed.
 
 lemma depth_d (q) (n): ❘q❘ = ❘𝗱n◗q❘.
 // qed.
 
+lemma depth_m (q): ❘q❘ = ❘𝗺◗q❘.
+// qed.
+
 lemma depth_L (q): ↑❘q❘ = ❘𝗟◗q❘.
 // qed.
 
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_proper.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_proper.ma
index e519394f4..fca2eb91a 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_proper.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_proper.ma
@@ -13,7 +13,8 @@
 (**************************************************************************)
 
 include "delayed_updating/syntax/path.ma".
-include "delayed_updating/notation/relations/predicate_p_tail_1.ma".
+include "delayed_updating/notation/functions/class_p_0.ma".
+include "ground/lib/subset.ma".
 include "ground/xoa/ex_1_2.ma".
 
 (* PROPER CONDITION FOR PATH ************************************************)
@@ -24,18 +25,18 @@ definition ppc: predicate path ≝
 
 interpretation
   "proper condition (path)"
-  'PredicatePTail p = (ppc p).
+  'ClassP = (ppc).
 
 (* Basic constructions ******************************************************)
 
-lemma ppc_lcons (l) (q): Ꝕ(l◗q).
+lemma ppc_lcons (l) (q): l◗q ϵ 𝐏.
 #l #p #H destruct
 qed.
 
 (* Basic inversions ********************************************************)
 
 lemma ppc_inv_lcons (p):
-      Ꝕp → ∃∃l,q. l◗q = p.
+      p ϵ 𝐏 → ∃∃l,q. l◗q = p.
 *
 [ #H elim H -H //
 | #l #q #_ /2 width=3 by ex1_2_intro/
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_structure.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_structure.ma
index 8c60eea75..0330665ad 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_structure.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_structure.ma
@@ -22,10 +22,11 @@ match p with
 [ list_empty     ⇒ 𝐞
 | list_lcons l q ⇒
    match l with
-   [ label_node_d n ⇒ structure q
-   | label_edge_L   ⇒ 𝗟◗structure q
-   | label_edge_A   ⇒ 𝗔◗structure q
-   | label_edge_S   ⇒ 𝗦◗structure q
+   [ label_d n ⇒ structure q
+   | label_m   ⇒ structure q
+   | label_L   ⇒ 𝗟◗structure q
+   | label_A   ⇒ 𝗔◗structure q
+   | label_S   ⇒ 𝗦◗structure q
    ]
 ].
 
@@ -43,16 +44,20 @@ lemma structure_d_sn (p) (n):
       ⊗p = ⊗(𝗱n◗p).
 // qed.
 
+lemma structure_m_sn (p):
+      ⊗p = ⊗(𝗺◗p).
+// qed.
+
 lemma structure_L_sn (p):
-      𝗟◗⊗p = ⊗(𝗟◗p).
+      (𝗟◗⊗p) = ⊗(𝗟◗p).
 // qed.
 
 lemma structure_A_sn (p):
-      𝗔◗⊗p = ⊗(𝗔◗p).
+      (𝗔◗⊗p) = ⊗(𝗔◗p).
 // qed.
 
 lemma structure_S_sn (p):
-      𝗦◗⊗p = ⊗(𝗦◗p).
+      (𝗦◗⊗p) = ⊗(𝗦◗p).
 // qed.
 
 (* Main constructions *******************************************************)
@@ -75,6 +80,11 @@ lemma structure_d_dx (p) (n):
 #p #n <structure_append //
 qed.
 
+lemma structure_m_dx (p):
+      ⊗p = ⊗(p◖𝗺).
+#p <structure_append //
+qed.
+
 lemma structure_L_dx (p):
       (⊗p)◖𝗟 = ⊗(p◖𝗟).
 #p <structure_append //
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm_constructors.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm_constructors.ma
index 1d3aeedf5..fd86ef975 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm_constructors.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm_constructors.ma
@@ -13,6 +13,7 @@
 (**************************************************************************)
 
 include "delayed_updating/syntax/prototerm.ma".
+include "delayed_updating/notation/functions/m_hook_1.ma".
 include "delayed_updating/notation/functions/hash_1.ma".
 include "delayed_updating/notation/functions/phi_2.ma".
 include "delayed_updating/notation/functions/lamda_1.ma".
@@ -26,26 +27,33 @@ definition prototerm_node_0 (l): prototerm ≝
 definition prototerm_node_1 (l): prototerm → prototerm ≝
            λt,p. ∃∃q. q ϵ t & l◗q = p.
 
+definition prototerm_node_1_2 (l1) (l2): prototerm → prototerm ≝
+           λt,p. ∃∃q. q ϵ t & l1◗l2◗q = p.
+
 definition prototerm_node_2 (l1) (l2): prototerm → prototerm → prototerm ≝
            λt1,t2,p.
            ∨∨ ∃∃q. q ϵ t1 & l1◗q = p
             | ∃∃q. q ϵ t2 & l2◗q = p.
 
+interpretation
+  "mark (prototerm)"
+  'MHook t = (prototerm_node_1 label_m t).
+
 interpretation
   "outer variable reference by depth (prototerm)"
-  'Hash n = (prototerm_node_0 (label_node_d n)).
+  'Hash n = (prototerm_node_0 (label_d n)).
 
 interpretation
   "inner variable reference by depth (prototerm)"
-  'Phi n t = (prototerm_node_1 (label_node_d n) t).
+  'Phi n t = (prototerm_node_1_2 (label_d n) label_m t).
 
 interpretation
   "name-free functional abstraction (prototerm)"
-  'Lamda t = (prototerm_node_1 label_edge_L t).
+  'Lamda t = (prototerm_node_1 label_L t).
 
 interpretation
   "application (prototerm)"
-  'At u t = (prototerm_node_2 label_edge_S label_edge_A u t).
+  'At u t = (prototerm_node_2 label_S label_A u t).
 
 (* Basic Inversions *********************************************************)
 
@@ -60,17 +68,25 @@ qed-.
 
 lemma prototerm_in_root_inv_lcons_iref:
       ∀t,p,l,n. l◗p ϵ ▵𝛗n.t →
-      ∧∧ 𝗱n = l & p ϵ ▵t.
-#t #p #l #n * #q
-<list_append_lcons_sn * #r #Hr #H0 destruct
+      ∧∧ 𝗱n = l & p ϵ ▵ɱ.t.
+#t #p #l #n * #q * #r #Hr
+<list_append_lcons_sn #H0 destruct -H0
+/4 width=4 by ex2_intro, ex_intro, conj/
+qed-.
+
+lemma prototerm_in_root_inv_lcons_mark:
+      ∀t,p,l. l◗p ϵ ▵ɱ.t →
+      ∧∧ 𝗺 = l & p ϵ ▵t.
+#t #p #l * #q * #r #Hr
+<list_append_lcons_sn #H0 destruct
 /3 width=2 by ex_intro, conj/
 qed-.
 
 lemma prototerm_in_root_inv_lcons_abst:
       ∀t,p,l. l◗p ϵ ▵𝛌.t →
       ∧∧ 𝗟 = l & p ϵ ▵t.
-#t #p #l * #q
-<list_append_lcons_sn * #r #Hr #H0 destruct
+#t #p #l * #q * #r #Hr
+<list_append_lcons_sn #H0 destruct
 /3 width=2 by ex_intro, conj/
 qed-.
 
@@ -78,7 +94,7 @@ lemma prototerm_in_root_inv_lcons_appl:
       ∀u,t,p,l. l◗p ϵ ▵@u.t →
       ∨∨ ∧∧ 𝗦 = l & p ϵ ▵u
        | ∧∧ 𝗔 = l & p ϵ ▵t.
-#u #t #p #l * #q
-<list_append_lcons_sn * * #r #Hr #H0 destruct
+#u #t #p #l * #q * * #r #Hr
+<list_append_lcons_sn #H0 destruct
 /4 width=2 by ex_intro, or_introl, or_intror, conj/
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm_proper.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm_proper.ma
index 9a5569726..b2bb92cf8 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm_proper.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm_proper.ma
@@ -12,6 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "delayed_updating/syntax/prototerm.ma".
 include "delayed_updating/syntax/path_proper.ma".
 include "ground/lib/subset_ext_equivalence.ma".
 
@@ -19,17 +20,23 @@ include "ground/lib/subset_ext_equivalence.ma".
 
 interpretation
   "proper condition (prototerm)"
-  'PredicatePTail t = (subset_ext_p1 path ppc t).
+  'ClassP = (subset_ext_p1 path ppc).
 
 (* Basic constructions ******************************************************)
 
 lemma tpc_i (t):
-      (𝐞 ⧸ϵ t) → Ꝕt.
+      (𝐞 ⧸ϵ t) → t ϵ 𝐏.
 #t #Ht * //
 #H elim (Ht H)
 qed.
 
 (* Basic inversions *********************************************************)
 
-lemma tpc_e (t): Ꝕt → 𝐞 ϵ t → ⊥.
-/2 width=5 by subset_in_inv_ext_p1_dx/ qed-.
+lemma in_ppc_comp_trans (t) (p):
+      p ϵ t → t ϵ 𝐏 → p ϵ 𝐏.
+#t #p #Hp #Ht
+@(Ht … Hp)
+qed-.
+
+lemma tpc_e (t): 𝐞 ϵ t → t ϵ 𝐏 → ⊥.
+/2 width=5 by in_ppc_comp_trans/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm_proper_constructors.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm_proper_constructors.ma
new file mode 100644
index 000000000..c7bb79244
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm_proper_constructors.ma
@@ -0,0 +1,25 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/prototerm_proper.ma".
+include "delayed_updating/syntax/prototerm_constructors.ma".
+
+(* PROPER CONDITION FOR PROTOTERM *******************************************)
+
+(* Constructions with prototerm constructors ********************************)
+
+lemma ppc_iref (t) (n):
+      (𝛗n.t) ϵ 𝐏.
+#t #n #p * #q #Hq #H0 destruct //
+qed.
diff --git a/matita/matita/predefined_virtuals.ml b/matita/matita/predefined_virtuals.ml
index 548bb9a93..2ec69e63f 100644
--- a/matita/matita/predefined_virtuals.ml
+++ b/matita/matita/predefined_virtuals.ml
@@ -1559,7 +1559,7 @@ let predefined_classes = [
  ["K"; "𝕂"; "𝐊"; "Ⓚ"; ] ;
  ["l"; "λ"; "𝕝"; "𝐥"; "𝛌"; "ⓛ"; ] ;
  ["L"; "Λ"; "𝕃"; "𝐋"; "𝚲"; "Ⓛ"; "𝗟"; ] ;
- ["m"; "μ"; "𝕞"; "𝐦"; "𝛍"; "ⓜ"; ] ;
+ ["m"; "μ"; "𝕞"; "𝐦"; "𝛍"; "ⓜ"; "𝗺"; "ɱ"; ] ;
  ["M"; "ℳ"; "𝕄"; "𝐌"; "Ⓜ"; ] ;
  ["n"; "𝕟"; "𝐧"; "𝛈"; "ⓝ"; ] ;
  ["N"; "ℕ"; "№"; "𝐍"; "Ⓝ"; ] ;