From 3c78efa39d4783f83638b1aabe8d776d83aabf35 Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Tue, 3 May 2022 19:46:49 +0200
Subject: [PATCH] update in delayed_updating

+ some notation updated
+ some unused files removed
---
 .../delayed_updating/etc/lift/dfr.etc         |  37 ------
 .../delayed_updating/etc/lift/dfr_ifr.etc     | 106 ------------------
 .../delayed_updating/etc/lift/fsubst.etc      |  28 -----
 .../delayed_updating/etc/lift/fsubst_eq.etc   |  33 ------
 .../delayed_updating/etc/lift/ifr.etc         |  36 ------
 .../delayed_updating/reduction/dfr.ma         |   4 +-
 .../delayed_updating/reduction/dfr_ifr.ma     |  23 +++-
 .../delayed_updating/reduction/ifr.ma         |   4 +-
 .../delayed_updating/syntax/path_depth.ma     |  28 ++---
 .../syntax/path_structure_depth.ma            |   2 +-
 .../delayed_updating/unwind1/unwind.ma        |   8 +-
 .../delayed_updating/unwind1/unwind_eq.ma     |  10 +-
 .../unwind1/unwind_structure.ma               |  22 ++--
 .../unwind1/unwind_structure_depth.ma         |   2 +-
 matita/matita/predefined_virtuals.ml          |   2 +-
 15 files changed, 60 insertions(+), 285 deletions(-)
 delete mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/etc/lift/dfr.etc
 delete mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/etc/lift/dfr_ifr.etc
 delete mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/etc/lift/fsubst.etc
 delete mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/etc/lift/fsubst_eq.etc
 delete mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/etc/lift/ifr.etc

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/etc/lift/dfr.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/lift/dfr.etc
deleted file mode 100644
index b568c322a..000000000
--- a/matita/matita/contribs/lambdadelta/delayed_updating/etc/lift/dfr.etc
+++ /dev/null
@@ -1,37 +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                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-include "delayed_updating/syntax/prototerm_constructors.ma".
-include "delayed_updating/syntax/prototerm_equivalence.ma".
-include "delayed_updating/substitution/fsubst.ma".
-include "delayed_updating/substitution/unwind.ma".
-include "delayed_updating/syntax/path_structure.ma".
-include "delayed_updating/syntax/path_balanced.ma".
-include "delayed_updating/syntax/path_depth.ma".
-include "delayed_updating/notation/relations/black_rightarrow_df_4.ma".
-include "ground/xoa/ex_1_2.ma".
-include "ground/xoa/and_4.ma".
-
-(* DELAYED FOCUSED REDUCTION ************************************************)
-
-definition dfr (p) (q): relation2 prototerm prototerm ≝
-           λt1,t2. ∃∃b,n.
-           let r ≝ p●𝗔◗b●𝗟◗q in
-           ∧∧ ⊗b ϵ 𝐁 & ∀f. ↑❘q❘ = (↑[q]⫯f)@❨n❩ & r◖𝗱n ϵ t1 &
-              t1[⋔r←𝛗(n+❘b❘).(t1⋔(p◖𝗦))] ⇔ t2
-.
-
-interpretation
-  "focused balanced reduction with delayed updating (prototerm)"
-  'BlackRightArrowDF t1 p q t2 = (dfr p q t1 t2).
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/etc/lift/dfr_ifr.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/lift/dfr_ifr.etc
deleted file mode 100644
index 069415421..000000000
--- a/matita/matita/contribs/lambdadelta/delayed_updating/etc/lift/dfr_ifr.etc
+++ /dev/null
@@ -1,106 +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                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-include "delayed_updating/reduction/dfr.ma".
-include "delayed_updating/reduction/ifr.ma".
-include "delayed_updating/substitution/fsubst_unwind.ma".
-include "delayed_updating/substitution/fsubst_eq.ma".
-include "delayed_updating/substitution/unwind_constructors.ma".
-include "delayed_updating/substitution/unwind_preterm_eq.ma".
-include "delayed_updating/substitution/unwind_structure_depth.ma".
-include "delayed_updating/substitution/unwind_depth.ma".
-include "delayed_updating/syntax/prototerm_proper_constructors.ma".
-include "delayed_updating/syntax/path_structure_depth.ma".
-include "ground/relocation/tr_uni_compose.ma".
-include "ground/relocation/tr_pap_pushs.ma".
-
-(* DELAYED FOCUSED REDUCTION ************************************************)
-
-lemma tr_uni_eq_repl (n1) (n2):
-      n1 = n2 → 𝐮❨n1❩ ≗ 𝐮❨n2❩.
-// qed.
-
-axiom pippo (b) (q) (n):
-      ↑❘q❘ = (↑[q]𝐢)@❨n❩ →
-      ↑❘q❘+❘b❘= (↑[b●𝗟◗q]𝐢)@❨n+❘b❘❩.
-
-lemma unwind_rmap_tls_eq_id (p) (n):
-      ❘p❘ = ↑[p]𝐢@❨n❩ →
-      (𝐢) ≗ ⇂*[n]↑[p]𝐢.
-#p @(list_ind_rcons … p) -p
-[ #n <depth_empty #H destruct
-| #p * [ #m ] #IH #n
-  [ <depth_d_dx <unwind_rmap_pap_d_dx #H0
-    @(stream_eq_trans … (unwind_rmap_tls_d_dx …))
-    @(stream_eq_trans … (IH …)) -IH //
-  | /2 width=1 by/
-  | <depth_L_dx <unwind_rmap_L_dx
-    cases n -n [| #n ] #H0
-    [
-    | 
-    ]
-  | /2 width=1 by/
-  | /2 width=1 by/
-  ]
-]
-
-
-(*  (↑❘q❘+❘b❘=↑[b●𝗟◗q]𝐢@❨n+❘b❘❩ *)
-(* [↑[p]𝐢@❨n❩]⫯*[❘p❘]f∘⇂*[n]↑[p]𝐢) *)
-lemma unwind_rmap_tls_eq (f) (p) (n):
-      ❘p❘ = ↑[p]𝐢@❨n❩ →
-      f ≗ ⇂*[n]↑[p]f.
-#f #p #n #Hp
-@(stream_eq_canc_dx … (stream_tls_eq_repl …))
-[| @unwind_rmap_decompose | skip ]
-<tr_compose_tls <Hp
-
-@(stream_eq_canc_dx) … (unwind_rmap_decompose …)) 
-
-lemma dfr_unwind_bi (f) (p) (q) (t1) (t2): t1 ϵ 𝐓 →
-      t1 ➡𝐝𝐟[p,q] t2 → ↑[f]t1 ➡𝐟[⊗p,⊗q] ↑[f]t2.
-#f #p #q #t1 #t2 #H0t1
-* #b #n * #Hb #Hn  #Ht1 #Ht2
-@(ex1_2_intro … (⊗b) (↑❘⊗q❘)) @and4_intro
-[ //
-| #g <unwind_rmap_structure <depth_structure
-  >tr_pushs_swap <tr_pap_pushs_le //
-| lapply (in_comp_unwind_bi f … Ht1) -Ht1 -H0t1 -Hb -Ht2
-  <unwind_path_d_empty_dx //
-| lapply (unwind_term_eq_repl_dx f … Ht2) -Ht2 #Ht2
-  @(subset_eq_trans … Ht2) -t2
-  @(subset_eq_trans … (unwind_fsubst …))
-  [ <unwind_rmap_append <unwind_rmap_A_sn (* <unwind_rmap_append <unwind_rmap_L_sn *)
-    <structure_append <structure_A_sn <structure_append <structure_L_sn
-    <depth_append <depth_L_sn <depth_structure <depth_structure
-    @fsubst_eq_repl [ // ]
-    @(subset_eq_trans … (unwind_iref …))
-    @(subset_eq_canc_sn … (unwind_term_eq_repl_dx …))
-    [ @unwind_grafted_S /2 width=2 by ex_intro/ | skip ]
-    @(subset_eq_trans … (unwind_term_after …))
-    @(subset_eq_canc_dx … (unwind_term_after …))
-    @unwind_term_eq_repl_sn -t1
-    @(stream_eq_trans … (tr_compose_uni_dx …))
-    lapply (Hn (𝐢)) -Hn >tr_id_unfold #Hn
-    lapply (pippo … b … Hn) -Hn #Hn
-    @tr_compose_eq_repl
-    [ <unwind_rmap_pap_le //
-      <Hn <nrplus_inj_sn //
-    |
-    ]
-  | //
-  | /2 width=2 by ex_intro/
-  | //
-  ]
-]
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/etc/lift/fsubst.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/lift/fsubst.etc
deleted file mode 100644
index adbc16c04..000000000
--- a/matita/matita/contribs/lambdadelta/delayed_updating/etc/lift/fsubst.etc
+++ /dev/null
@@ -1,28 +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                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-include "delayed_updating/syntax/prototerm.ma".
-include "delayed_updating/notation/functions/pitchforkleftarrow_3.ma".
-
-(* FOCALIZED SUBSTITUTION ***************************************************)
-
-definition fsubst (p) (u): prototerm → prototerm ≝
-           λt,q.
-           ∨∨ ∃∃r. r ϵ u & p●r = q
-            | ∧∧ q ϵ t & (∀r. p●r = q → ⊥)
-.
-
-interpretation
-  "focalized substitution (prototerm)"
-  'PitchforkLeftArrow t p u = (fsubst p u t).
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/etc/lift/fsubst_eq.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/lift/fsubst_eq.etc
deleted file mode 100644
index a6681b592..000000000
--- a/matita/matita/contribs/lambdadelta/delayed_updating/etc/lift/fsubst_eq.etc
+++ /dev/null
@@ -1,33 +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                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-include "delayed_updating/substitution/fsubst.ma".
-include "delayed_updating/syntax/prototerm_equivalence.ma".
-
-(* Constructions with subset_equivalence ************************************)
-
-lemma subset_inclusion_fsubst_bi (t1) (t2) (u1) (u2) (p):
-      t1 ⊆ t2 → u1 ⊆ u2 → t1[⋔p←u1] ⊆ t2[⋔p←u2].
-#t1 #t2 #u1 #u2 #p #Ht #Hu #q * *
-[ #r #Hr #H0 destruct
-  /4 width=3 by ex2_intro, or_introl/
-| /4 width=2 by or_intror, conj/
-]
-qed.
-
-lemma fsubst_eq_repl (t1) (t2) (u1) (u2) (p):
-      t1 ⇔ t2 → u1 ⇔ u2 → t1[⋔p←u1] ⇔ t2[⋔p←u2].
-#t1 #t2 #u1 #u2 #p * #H1t #H2t * #H1u #H2u
-/3 width=5 by conj, subset_inclusion_fsubst_bi/
-qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/etc/lift/ifr.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/lift/ifr.etc
deleted file mode 100644
index 054aef5bf..000000000
--- a/matita/matita/contribs/lambdadelta/delayed_updating/etc/lift/ifr.etc
+++ /dev/null
@@ -1,36 +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                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-include "delayed_updating/substitution/fsubst.ma".
-include "delayed_updating/substitution/unwind_prototerm.ma".
-include "delayed_updating/syntax/prototerm_equivalence.ma".
-include "delayed_updating/syntax/path_depth.ma".
-include "delayed_updating/syntax/path_structure.ma".
-include "delayed_updating/syntax/path_balanced.ma".
-include "delayed_updating/notation/relations/black_rightarrow_f_4.ma".
-include "ground/xoa/ex_1_2.ma".
-include "ground/xoa/and_4.ma".
-
-(* IMMEDIATE FOCUSED REDUCTION ************************************************)
-
-definition ifr (p) (q): relation2 prototerm prototerm ≝
-           λt1,t2. ∃∃b,n.
-           let r ≝ p●𝗔◗b●𝗟◗q in
-           ∧∧ ⊗b ϵ 𝐁 & ∀f. ↑❘q❘ = (↑[q]⫯f)@❨n❩ & r◖𝗱n ϵ t1 &
-              t1[⋔r←↑[𝐮❨❘b●𝗟◗q❘❩](t1⋔(p◖𝗦))] ⇔ t2
-.
-
-interpretation
-  "focused balanced reduction with immediate updating (prototerm)"
-  'BlackRightArrowF t1 p q t2 = (ifr p q t1 t2).
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr.ma
index 576df6ec6..849c5f32d 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr.ma
@@ -28,8 +28,8 @@ include "ground/xoa/and_4.ma".
 definition dfr (p) (q): relation2 prototerm prototerm ≝
            λt1,t2. ∃∃b,n.
            let r ≝ p●𝗔◗b●𝗟◗q in
-           ∧∧ (⊗b ϵ 𝐁 ∧ 𝟎 = ❘b❘) & ↑❘q❘ = (▼[r]𝐢)@❨n❩ & r◖𝗱n ϵ t1 &
-              t1[⋔r←𝛗(n+❘b❘).(t1⋔(p◖𝗦))] ⇔ t2
+           ∧∧ (⊗b ϵ 𝐁 ∧ 𝟎 = ♭b) & ↑♭q = (▼[r]𝐢)@❨n❩ & r◖𝗱n ϵ t1 &
+              t1[⋔r←𝛗(n+♭b).(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 dd24f8568..2d3fdbdf5 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_ifr.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_ifr.ma
@@ -14,11 +14,13 @@
 
 include "delayed_updating/reduction/dfr.ma".
 include "delayed_updating/reduction/ifr.ma".
+
 include "delayed_updating/unwind1/unwind_fsubst.ma".
 include "delayed_updating/unwind1/unwind_constructors.ma".
 include "delayed_updating/unwind1/unwind_preterm_eq.ma".
 include "delayed_updating/unwind1/unwind_structure_depth.ma".
 include "delayed_updating/unwind1/unwind_depth.ma".
+
 include "delayed_updating/substitution/fsubst_eq.ma".
 include "delayed_updating/substitution/lift_prototerm_eq.ma".
 include "delayed_updating/syntax/prototerm_proper_constructors.ma".
@@ -71,9 +73,9 @@ lemma dfr_unwind_id_bi (p) (q) (t1) (t2): t1 ϵ 𝐓 →
       t1 ➡𝐝𝐟[p,q] t2 → ▼[𝐢]t1 ➡𝐟[⊗p,⊗q] ▼[𝐢]t2.
 #p #q #t1 #t2 #H0t1
 * #b #n * #Hb #Hn #Ht1 #Ht2
-@(ex1_2_intro … (⊗b) (↑❘⊗q❘)) @and4_intro
+@(ex1_2_intro … (⊗b) (↑♭⊗q)) @and4_intro
 [ //
-| //
+| (*//*)
 | lapply (in_comp_unwind_bi (𝐢) … Ht1) -Ht1 -H0t1 -Hb -Ht2
   <unwind_path_d_empty_dx <depth_structure //
 | lapply (unwind_term_eq_repl_dx (𝐢) … Ht2) -Ht2 #Ht2
@@ -85,11 +87,21 @@ lemma dfr_unwind_id_bi (p) (q) (t1) (t2): t1 ϵ 𝐓 →
     @fsubst_eq_repl [ // ]
     @(subset_eq_trans … (unwind_iref …))
 
-    elim Hb -Hb #Hb #H0 <H0 -H0 <nrplus_zero_dx <nplus_zero_dx <Hn
+    elim Hb -Hb #Hb #H0 <H0 -H0 <nrplus_zero_dx <nplus_zero_dx <nsucc_unfold
+    >Hn
     @(subset_eq_canc_sn … (lift_term_eq_repl_dx …))
     [ @unwind_grafted_S /2 width=2 by ex_intro/ | skip ]
-
+    <Hn <Hn
+(*    
+    @(subset_eq_trans … (lift_term_eq_repl_dx …))
+    [ @(unwind_term_eq_repl_sn … (tls_succ_unwind q …)) | skip ]
+*)
 (*
+    
+    @subset_eq_trans
+    [2: @unwind_term_eq_repl_dx
+    @(subset_eq_canc_sn … (unwind_term_eq_repl_dx …))
+
     @(subset_eq_canc_sn … (unwind_term_eq_repl_dx …))
     [ @unwind_grafted_S /2 width=2 by ex_intro/ | skip ]
 
@@ -116,3 +128,6 @@ Hn : ↑❘q❘ = ↑[p●𝗔◗b●𝗟◗q]𝐢@❨n❩
 ---------------------------
 ↑[𝐮❨↑❘q❘+❘b❘❩] ↑[↑[p]𝐢] t ⇔ ↑[𝐮❨↑[p●𝗔◗b●𝗟◗q]𝐢@❨n+❘b❘❩❩] t
 *)
+(*
+(↑[𝐮❨↑❘q❘❩]▼[⇂*[↑❘q❘]▼[p●𝗟◗q]𝐢](t1⋔(p◖𝗦))⇔▼[𝐮❨↑❘q❘❩∘▼[p●𝗔◗b●𝗟◗q]𝐢](t1⋔(p◖𝗦))
+*)
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr.ma
index 8d0cfc52d..d2a33afc2 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr.ma
@@ -28,8 +28,8 @@ include "ground/xoa/and_4.ma".
 definition ifr (p) (q): relation2 prototerm prototerm ≝
            λt1,t2. ∃∃b,n.
            let r ≝ p●𝗔◗b●𝗟◗q in
-           ∧∧ (⊗b ϵ 𝐁 ∧ 𝟎 = ❘b❘) & ↑❘q❘ = (▼[r]𝐢)@❨n❩ & r◖𝗱n ϵ t1 &
-              t1[⋔r←↑[𝐮❨❘b●𝗟◗q❘❩](t1⋔(p◖𝗦))] ⇔ t2
+           ∧∧ (⊗b ϵ 𝐁 ∧ 𝟎 = ♭b) & ↑♭q = (▼[r]𝐢)@❨n❩ & r◖𝗱n ϵ t1 &
+              t1[⋔r←↑[𝐮❨♭(b●𝗟◗q)❩](t1⋔(p◖𝗦))] ⇔ t2
 .
 
 interpretation
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 cdf24943a..474bbcbda 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_depth.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_depth.ma
@@ -13,8 +13,8 @@
 (**************************************************************************)
 
 include "delayed_updating/syntax/path.ma".
+include "delayed_updating/notation/functions/flat_1.ma".
 include "ground/arith/nat_plus.ma".
-include "ground/notation/functions/verticalbars_1.ma".
 
 (* DEPTH FOR PATH ***********************************************************)
 
@@ -33,32 +33,32 @@ match p with
 
 interpretation
   "depth (path)"
-  'VerticalBars p = (depth p).
+  'Flat p = (depth p).
 
 (* Basic constructions ******************************************************)
 
-lemma depth_empty: 𝟎 = ❘𝐞❘.
+lemma depth_empty: 𝟎 = ♭𝐞.
 // qed.
 
-lemma depth_d_sn (q) (n): ❘q❘ = ❘𝗱n◗q❘.
+lemma depth_d_sn (q) (n): ♭q = ♭(𝗱n◗q).
 // qed.
 
-lemma depth_m_sn (q): ❘q❘ = ❘𝗺◗q❘.
+lemma depth_m_sn (q): ♭q = ♭(𝗺◗q).
 // qed.
 
-lemma depth_L_sn (q): ↑❘q❘ = ❘𝗟◗q❘.
+lemma depth_L_sn (q): ↑♭q = ♭(𝗟◗q).
 // qed.
 
-lemma depth_A_sn (q): ❘q❘ = ❘𝗔◗q❘.
+lemma depth_A_sn (q): ♭q = ♭(𝗔◗q).
 // qed.
 
-lemma depth_S_sn (q): ❘q❘ = ❘𝗦◗q❘.
+lemma depth_S_sn (q): ♭q = ♭(𝗦◗q).
 // qed.
 
 (* Main constructions *******************************************************)
 
 theorem depth_append (p1) (p2):
-        ❘p2❘+❘p1❘ = ❘p1●p2❘.
+        (♭p2)+(♭p1) = ♭(p1●p2).
 #p1 elim p1 -p1 //
 * [ #n ] #p1 #IH #p2 <list_append_lcons_sn
 [ <depth_d_sn <depth_d_sn //
@@ -72,21 +72,21 @@ qed.
 (* Constructions with list_rcons ********************************************)
 
 lemma depth_d_dx (p) (n):
-      ❘p❘ = ❘p◖𝗱n❘.
+      ♭p = ♭(p◖𝗱n).
 // qed.
 
 lemma depth_m_dx (p):
-      ❘p❘ = ❘p◖𝗺❘.
+      ♭p = ♭(p◖𝗺).
 // qed.
 
 lemma depth_L_dx (p):
-      ↑❘p❘ = ❘p◖𝗟❘.
+      ↑♭p = ♭(p◖𝗟).
 // qed.
 
 lemma depth_A_dx (p):
-      ❘p❘ = ❘p◖𝗔❘.
+      ♭p = ♭(p◖𝗔).
 // qed.
 
 lemma depth_S_dx (p):
-      ❘p❘ = ❘p◖𝗦❘.
+      ♭p = ♭(p◖𝗦).
 // qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_structure_depth.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_structure_depth.ma
index 700da6a46..464821793 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_structure_depth.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_structure_depth.ma
@@ -20,7 +20,7 @@ include "delayed_updating/syntax/path_depth.ma".
 (* Constructions with depth *************************************************)
 
 lemma depth_structure (p):
-      ❘p❘ = ❘⊗p❘.
+      ♭p = ♭⊗p.
 #p elim p -p //
 * [ #n ] #p #IH //
 [ <structure_L_sn <depth_L_sn <depth_L_sn //
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind.ma
index 43e634114..e5a6ea13f 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind.ma
@@ -63,11 +63,11 @@ lemma unwind_empty (A) (k) (f):
       k f (𝐞) = ▼{A}❨k, f, 𝐞❩.
 // qed.
 
-lemma unwind_d_empty_sn (A) (k) (n) (f):
+lemma unwind_d_empty (A) (k) (n) (f):
       ▼❨(λg,p. k g (𝗱(f@❨n❩)◗p)), 𝐮❨f@❨n❩❩, 𝐞❩ = ▼{A}❨k, f, 𝗱n◗𝐞❩.
 // qed.
 
-lemma unwind_d_lcons_sn (A) (k) (p) (l) (n) (f):
+lemma unwind_d_lcons (A) (k) (p) (l) (n) (f):
       ▼❨k, 𝐮❨f@❨n❩❩, l◗p❩ = ▼{A}❨k, f, 𝗱n◗l◗p❩.
 // qed.
 
@@ -93,11 +93,11 @@ lemma unwind_path_empty (f):
       (𝐞) = ▼[f]𝐞.
 // qed.
 
-lemma unwind_path_d_empty_sn (f) (n):
+lemma unwind_path_d_empty (f) (n):
       𝗱(f@❨n❩)◗𝐞 = ▼[f](𝗱n◗𝐞).
 // qed.
 
-lemma unwind_path_d_lcons_sn (f) (p) (l) (n):
+lemma unwind_path_d_lcons (f) (p) (l) (n):
       ▼[𝐮❨f@❨n❩❩](l◗p) = ▼[f](𝗱n◗l◗p).
 // qed.
 
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind_eq.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind_eq.ma
index 2a03b6831..8943b7335 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind_eq.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind_eq.ma
@@ -33,9 +33,9 @@ lemma unwind_eq_repl (A) (p) (k1) (k2):
 #A #p @(path_ind_unwind … p) -p [| #n #IH | #n #l0 #q #IH |*: #q #IH ]
 #k1 #k2 #Hk #f1 #f2 #Hf
 [ <unwind_empty <unwind_empty /2 width=1 by/
-| <unwind_d_empty_sn <unwind_d_empty_sn <(tr_pap_eq_repl … Hf)
+| <unwind_d_empty <unwind_d_empty <(tr_pap_eq_repl … Hf)
   /2 width=1 by stream_eq_refl/
-| <unwind_d_lcons_sn <unwind_d_lcons_sn
+| <unwind_d_lcons <unwind_d_lcons
   /5 width=1 by tr_uni_eq_repl, tr_pap_eq_repl, eq_f/ 
 | /2 width=1 by/
 | /3 width=1 by tr_push_eq_repl/
@@ -72,7 +72,7 @@ lemma unwind_path_eq_repl (p):
 lemma unwind_path_append_sn (p) (f) (q):
       q●▼[f]p = ▼❨(λg,p. proj_path g (q●p)), f, p❩.
 #p @(path_ind_unwind … p) -p // [ #n #l #p |*: #p ] #IH #f #q
-[ <unwind_d_lcons_sn <unwind_d_lcons_sn <IH -IH //
+[ <unwind_d_lcons <unwind_d_lcons <IH -IH //
 | <unwind_m_sn <unwind_m_sn //
 | <unwind_L_sn <unwind_L_sn >unwind_lcons_alt // >unwind_append_rcons_sn //
   <IH <IH -IH <list_append_rcons_sn //
@@ -104,8 +104,8 @@ lemma unwind_path_S_sn (f) (p):
 lemma unwind_path_after_id_sn (p) (f):
       ▼[𝐢]▼[f]p = ▼[f]p.
 #p @(path_ind_unwind … p) -p // [ #n | #n #l #p | #p ] #IH #f
-[ <unwind_path_d_empty_sn //
-| <unwind_path_d_lcons_sn //
+[ <unwind_path_d_empty //
+| <unwind_path_d_lcons //
 | <unwind_path_L_sn <unwind_path_L_sn //
 ]
 qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind_structure.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind_structure.ma
index 27d369219..ed025110a 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind_structure.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind_structure.ma
@@ -46,7 +46,7 @@ lemma unwind_append_proper_dx (p2) (p1) (f): p2 ϵ 𝐏 →
 #p2 #p1 @(path_ind_unwind … p1) -p1 //
 [ #n | #n #l #p1 |*: #p1 ] #IH #f #Hp2
 [ elim (ppc_inv_lcons … Hp2) -Hp2 #l #q #H destruct //
-| <unwind_path_d_lcons_sn <IH //
+| <unwind_path_d_lcons <IH //
 | <unwind_path_m_sn <IH //
 | <unwind_path_L_sn <IH //
 | <unwind_path_A_sn <IH //
@@ -114,9 +114,9 @@ lemma unwind_path_inv_d_sn (k) (q) (p) (f):
 #k #q #p @(path_ind_unwind … p) -p
 [| #n | #n #l #p |*: #p ] [|*: #IH ] #f
 [ <unwind_path_empty #H destruct
-| <unwind_path_d_empty_sn #H destruct -IH
+| <unwind_path_d_empty #H destruct -IH
   /2 width=5 by ex4_2_intro/
-| <unwind_path_d_lcons_sn #H
+| <unwind_path_d_lcons #H
   elim (IH … H) -IH -H #r #h #Hr #Hh #Hq #Hp destruct
   /2 width=5 by ex4_2_intro/
 | <unwind_path_m_sn #H
@@ -133,8 +133,8 @@ lemma unwind_path_inv_m_sn (q) (p) (f):
 #q #p @(path_ind_unwind … p) -p
 [| #n | #n #l #p |*: #p ] [|*: #IH ] #f
 [ <unwind_path_empty #H destruct
-| <unwind_path_d_empty_sn #H destruct
-| <unwind_path_d_lcons_sn #H /2 width=2 by/
+| <unwind_path_d_empty #H destruct
+| <unwind_path_d_lcons #H /2 width=2 by/
 | <unwind_path_m_sn #H /2 width=2 by/
 | <unwind_path_L_sn #H destruct
 | <unwind_path_A_sn #H destruct
@@ -148,8 +148,8 @@ lemma unwind_path_inv_L_sn (q) (p) (f):
 #q #p @(path_ind_unwind … p) -p
 [| #n | #n #l #p |*: #p ] [|*: #IH ] #f
 [ <unwind_path_empty #H destruct
-| <unwind_path_d_empty_sn #H destruct
-| <unwind_path_d_lcons_sn #H
+| <unwind_path_d_empty #H destruct
+| <unwind_path_d_lcons #H
   elim (IH … H) -IH -H #r1 #r2 #Hr1 #Hq #Hp destruct
   /2 width=5 by ex3_2_intro/
 | <unwind_path_m_sn #H
@@ -168,8 +168,8 @@ lemma unwind_path_inv_A_sn (q) (p) (f):
 #q #p @(path_ind_unwind … p) -p
 [| #n | #n #l #p |*: #p ] [|*: #IH ] #f
 [ <unwind_path_empty #H destruct
-| <unwind_path_d_empty_sn #H destruct
-| <unwind_path_d_lcons_sn #H
+| <unwind_path_d_empty #H destruct
+| <unwind_path_d_lcons #H
   elim (IH … H) -IH -H #r1 #r2 #Hr1 #Hq #Hp destruct
   /2 width=5 by ex3_2_intro/
 | <unwind_path_m_sn #H
@@ -188,8 +188,8 @@ lemma unwind_path_inv_S_sn (q) (p) (f):
 #q #p @(path_ind_unwind … p) -p
 [| #n | #n #l #p |*: #p ] [|*: #IH ] #f
 [ <unwind_path_empty #H destruct
-| <unwind_path_d_empty_sn #H destruct
-| <unwind_path_d_lcons_sn #H
+| <unwind_path_d_empty #H destruct
+| <unwind_path_d_lcons #H
   elim (IH … H) -IH -H #r1 #r2 #Hr1 #Hq #Hp destruct
   /2 width=5 by ex3_2_intro/
 | <unwind_path_m_sn #H
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind_structure_depth.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind_structure_depth.ma
index c13471e81..df3423e16 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind_structure_depth.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind_structure_depth.ma
@@ -22,7 +22,7 @@ include "ground/arith/nat_pred_succ.ma".
 (* Basic constructions with structure and depth ****************************)
 
 lemma unwind_rmap_structure (p) (f):
-      (⫯*[❘p❘]f) = ▼[⊗p]f.
+      (⫯*[♭p]f) = ▼[⊗p]f.
 #p elim p -p //
 * [ #n ] #p #IH #f //
 [ <unwind_rmap_A_sn //
diff --git a/matita/matita/predefined_virtuals.ml b/matita/matita/predefined_virtuals.ml
index 2ec69e63f..92cb18cfa 100644
--- a/matita/matita/predefined_virtuals.ml
+++ b/matita/matita/predefined_virtuals.ml
@@ -1537,7 +1537,7 @@ let predefined_classes = [
  ["∨"; "⩖"; "∪"; "∩"; "⋓"; "⋒" ] ;
  ["a"; "α"; "𝕒"; "𝐚"; "𝛂"; "ⓐ"; ] ;
  ["A"; "ℵ"; "𝔸"; "𝐀"; "Ⓐ"; "𝗔"; ] ;
- ["b"; "β"; "ß"; "𝕓"; "𝐛"; "𝛃"; "ⓑ"; ] ;
+ ["b"; "β"; "ß"; "𝕓"; "𝐛"; "𝛃"; "ⓑ"; "♭"; ] ;
  ["B"; "ℶ"; "ℬ"; "𝔹"; "𝐁"; "Ⓑ"; ] ;
  ["c"; "𝕔"; "𝐜"; "ⓒ"; ] ;
  ["C"; "ℭ"; "∁"; "𝐂"; "ℂ"; "Ⓒ"; ] ;
-- 
2.39.2