From 3bf7a0b4185dbffe5b822c907956acdbe2d1c559 Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Tue, 21 Jun 2022 01:33:06 +0200
Subject: [PATCH] update in delayed_updating

+ WIP on lift
+ notation changed for delayed updating (term constructor)
+ minor corrections
---
 .../functions/phi_2.ma => etc/phi_2.etc}      |   0
 .../{class_d_phi_0.ma => class_d_tau_0.ma}    |   4 +-
 .../notation/functions/tau_2.ma               |  19 +++
 .../delayed_updating/reduction/dfr.ma         |   2 +-
 .../substitution/fsubst_eq.ma                 |   2 +
 .../substitution/fsubst_lift.ma               |  54 +++++++
 .../substitution/lift_constructors.ma         |   8 +-
 .../delayed_updating/substitution/lift_eq.ma  | 134 ++++++++++++++++++
 .../delayed_updating/syntax/bdd_term.ma       |  50 +++----
 .../syntax/prototerm_constructors.ma          |  10 +-
 .../syntax/prototerm_constructors_eq.ma       |   2 +-
 .../syntax/prototerm_proper_constructors.ma   |   2 +-
 .../unwind/unwind2_constructors.ma            |   6 +-
 .../unwind/unwind2_preterm_fsubst.ma          |   2 +-
 .../unwind/unwind_gen_structure.ma            |   4 +-
 15 files changed, 254 insertions(+), 45 deletions(-)
 rename matita/matita/contribs/lambdadelta/delayed_updating/{notation/functions/phi_2.ma => etc/phi_2.etc} (100%)
 rename matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/{class_d_phi_0.ma => class_d_tau_0.ma} (95%)
 create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/tau_2.ma
 create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/substitution/fsubst_lift.ma

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/phi_2.ma b/matita/matita/contribs/lambdadelta/delayed_updating/etc/phi_2.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/phi_2.ma
rename to matita/matita/contribs/lambdadelta/delayed_updating/etc/phi_2.etc
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_tau_0.ma
similarity index 95%
rename from matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/class_d_phi_0.ma
rename to matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/class_d_tau_0.ma
index d45317626..8b21ae579 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_tau_0.ma
@@ -14,6 +14,6 @@
 
 (* NOTATION FOR DELAYED UPDATING ********************************************)
 
-notation "hvbox( 𝐃𝛗 )"
+notation "hvbox( 𝐃𝛕 )"
   non associative with precedence 70
-  for @{ 'ClassDPhi }.
+  for @{ 'ClassDTau }.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/tau_2.ma b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/tau_2.ma
new file mode 100644
index 000000000..099360cce
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/tau_2.ma
@@ -0,0 +1,19 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* NOTATION FOR DELAYED UPDATING ********************************************)
+
+notation "hvbox( 𝛕 break term 76 n. break term 70 t )"
+  non associative with precedence 70
+  for @{ 'Tau $n $t }.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr.ma
index 738553c7d..193136433 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr.ma
@@ -26,7 +26,7 @@ definition dfr (p) (q): relation2 prototerm prototerm ≝
            λt1,t2. ∃n:pnat.
            let r ≝ p●𝗔◗𝗟◗q in
            ∧∧ (𝗟◗q)ᴿ = ↳[n](rᴿ) & r◖𝗱n ϵ t1 &
-              t1[⋔r←𝛗n.(t1⋔(p◖𝗦))] ⇔ t2
+              t1[⋔r←𝛕n.(t1⋔(p◖𝗦))] ⇔ t2
 .
 
 interpretation
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/fsubst_eq.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/fsubst_eq.ma
index a3a349419..c3f6cfa11 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/fsubst_eq.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/fsubst_eq.ma
@@ -15,6 +15,8 @@
 include "delayed_updating/substitution/fsubst.ma".
 include "delayed_updating/syntax/prototerm_eq.ma".
 
+(* FOCALIZED SUBSTITUTION ***************************************************)
+
 (* Constructions with subset_equivalence ************************************)
 
 lemma subset_inclusion_fsubst_bi (t1) (t2) (u1) (u2) (p):
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/fsubst_lift.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/fsubst_lift.ma
new file mode 100644
index 000000000..e1be5ded0
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/fsubst_lift.ma
@@ -0,0 +1,54 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/lift_prototerm_eq.ma".
+(*
+include "delayed_updating/syntax/preterm.ma".
+include "delayed_updating/syntax/prototerm_proper.ma".
+*)
+(* FOCALIZED SUBSTITUTION ***************************************************)
+
+(* Constructions with lift for preterm **************************************)
+
+lemma lift_term_fsubst_sn (f) (t) (u) (p):
+      (↑[f]t)[⋔(↑[f]p)←↑[↑[p]f]u] ⊆ ↑[f](t[⋔p←u]).
+#f #t #u #p #ql * *
+[ #rl * #r #Hr #H1 #H2 destruct
+  >lift_path_append
+  /4 width=3 by in_comp_lift_path_term, or_introl, ex2_intro/
+| * #q #Hq #H1 #H0
+  @(ex2_intro … H1) @or_intror @conj // -Hq #r #H2 destruct
+  /2 width=2 by/
+]
+qed-.
+
+lemma lift_term_fsubst_dx (f) (t) (u) (p):
+      ↑[f](t[⋔p←u]) ⊆ (↑[f]t)[⋔(↑[f]p)←↑[↑[p]f]u].
+#f #t #u #p #ql * #q * *
+[ #r #Hu #H1 #H2 destruct
+  @or_introl @ex2_intro
+  [|| <lift_path_append // ]
+  /2 width=3 by ex2_intro/
+| #Hq #H0 #H1 destruct
+  @or_intror @conj [ /2 width=1 by in_comp_lift_path_term/ ] -Hq #r #Hr
+  elim (lift_path_inv_append_dx … Hr) -Hr #s1 #s2 #Hs1 #_ #H1 destruct
+  lapply (lift_path_inj … Hs1) -Hs1 #H1 destruct 
+  /2 width=2 by/
+]
+qed-.
+
+lemma lift_term_fsubst (f) (t) (u) (p):
+      (↑[f]t)[⋔(↑[f]p)←↑[↑[p]f]u] ⇔ ↑[f](t[⋔p←u]).
+/3 width=1 by lift_term_fsubst_sn, conj, lift_term_fsubst_dx/ qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_constructors.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_constructors.ma
index 2fae75c26..d7dde19bc 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_constructors.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_constructors.ma
@@ -19,26 +19,26 @@ include "delayed_updating/syntax/prototerm_constructors_eq.ma".
 (* LIFT FOR PROTOTERM *******************************************************)
 
 lemma lift_iref_sn (f) (t:prototerm) (n:pnat):
-      (𝛗f＠⧣❨n❩.↑[⇂*[n]f]t) ⊆ ↑[f](𝛗n.t).
+      (𝛕f＠⧣❨n❩.↑[⇂*[n]f]t) ⊆ ↑[f](𝛕n.t).
 #f #t #n #p * #q * #r #Hr #H1 #H2 destruct
 @(ex2_intro … (𝗱n◗𝗺◗r))
 /2 width=1 by in_comp_iref/
 qed-.
 
 lemma lift_iref_dx (f) (t) (n:pnat):
-      ↑[f](𝛗n.t) ⊆ 𝛗f＠⧣❨n❩.↑[⇂*[n]f]t.
+      ↑[f](𝛕n.t) ⊆ 𝛕f＠⧣❨n❩.↑[⇂*[n]f]t.
 #f #t #n #p * #q #Hq #H0 destruct
 elim (in_comp_inv_iref … Hq) -Hq #p #H0 #Hp destruct
 /3 width=1 by in_comp_iref, in_comp_lift_path_term/
 qed-.
 
 lemma lift_iref (f) (t) (n:pnat):
-      (𝛗f＠⧣❨n❩.↑[⇂*[n]f]t) ⇔ ↑[f](𝛗n.t).
+      (𝛕f＠⧣❨n❩.↑[⇂*[n]f]t) ⇔ ↑[f](𝛕n.t).
 /3 width=1 by conj, lift_iref_sn, lift_iref_dx/
 qed.
 
 lemma lift_iref_uni (t) (m) (n):
-      (𝛗(n+m).t) ⇔ ↑[𝐮❨m❩](𝛗n.t).
+      (𝛕(n+m).t) ⇔ ↑[𝐮❨m❩](𝛕n.t).
 #t #m #n
 @(subset_eq_trans … (lift_iref …))
 <tr_uni_pap >nsucc_pnpred <tr_tls_succ_uni
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 9c4b0f3b5..5ab8d7f05 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_eq.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_eq.ma
@@ -13,6 +13,7 @@
 (**************************************************************************)
 
 include "delayed_updating/substitution/lift.ma".
+include "ground/relocation/tr_pap_pap.ma".
 include "ground/relocation/tr_pap_eq.ma".
 include "ground/relocation/tr_pn_eq.ma".
 include "ground/lib/stream_tls_eq.ma".
@@ -143,6 +144,139 @@ lemma lift_path_S_dx (f) (p):
 #f #p <lift_path_append //
 qed.
 
+(* Advanced inversions ******************************************************)
+
+lemma lift_path_inv_empty (f) (p):
+      (𝐞) = ↑[f]p → 𝐞 = p.
+#f * // * [ #n ] #p
+[ <lift_path_d_sn
+| <lift_path_m_sn
+| <lift_path_L_sn
+| <lift_path_A_sn
+| <lift_path_S_sn
+] #H destruct
+qed-.
+
+lemma lift_path_inv_d_sn (f) (p) (q) (k):
+      (𝗱k◗q) = ↑[f]p →
+      ∃∃r,h. k = f＠⧣❨h❩ & q = ↑[⇂*[h]f]r & 𝗱h◗r = p.
+#f * [| * [ #n ] #p ] #q #k
+[ <lift_path_empty
+| <lift_path_d_sn
+| <lift_path_m_sn
+| <lift_path_L_sn
+| <lift_path_A_sn
+| <lift_path_S_sn
+] #H destruct
+/2 width=5 by ex3_2_intro/
+qed-.
+
+lemma lift_path_inv_m_sn (f) (p) (q):
+      (𝗺◗q) = ↑[f]p →
+      ∃∃r. q = ↑[f]r & 𝗺◗r = p.
+#f * [| * [ #n ] #p ] #q
+[ <lift_path_empty
+| <lift_path_d_sn
+| <lift_path_m_sn
+| <lift_path_L_sn
+| <lift_path_A_sn
+| <lift_path_S_sn
+] #H destruct
+/2 width=3 by ex2_intro/
+qed-.
+
+lemma lift_path_inv_L_sn (f) (p) (q):
+      (𝗟◗q) = ↑[f]p →
+      ∃∃r. q = ↑[⫯f]r & 𝗟◗r = p.
+#f * [| * [ #n ] #p ] #q
+[ <lift_path_empty
+| <lift_path_d_sn
+| <lift_path_m_sn
+| <lift_path_L_sn
+| <lift_path_A_sn
+| <lift_path_S_sn
+] #H destruct
+/2 width=3 by ex2_intro/
+qed-.
+
+lemma lift_path_inv_A_sn (f) (p) (q):
+      (𝗔◗q) = ↑[f]p →
+      ∃∃r. q = ↑[f]r & 𝗔◗r = p.
+#f * [| * [ #n ] #p ] #q
+[ <lift_path_empty
+| <lift_path_d_sn
+| <lift_path_m_sn
+| <lift_path_L_sn
+| <lift_path_A_sn
+| <lift_path_S_sn
+] #H destruct
+/2 width=3 by ex2_intro/
+qed-.
+
+lemma lift_path_inv_S_sn (f) (p) (q):
+      (𝗦◗q) = ↑[f]p →
+      ∃∃r. q = ↑[f]r & 𝗦◗r = p.
+#f * [| * [ #n ] #p ] #q
+[ <lift_path_empty
+| <lift_path_d_sn
+| <lift_path_m_sn
+| <lift_path_L_sn
+| <lift_path_A_sn
+| <lift_path_S_sn
+] #H destruct
+/2 width=3 by ex2_intro/
+qed-.
+
+lemma lift_path_inv_append_dx (q2) (q1) (p) (f):
+      q1●q2 = ↑[f]p →
+      ∃∃p1,p2. q1 = ↑[f]p1 & q2 = ↑[↑[p1]f]p2 & p1●p2 = p.
+#q2 #q1 elim q1 -q1
+[| * [ #n1 ] #q1 #IH ] #p #f
+[ <list_append_empty_sn #H0 destruct
+  /2 width=5 by ex3_2_intro/
+| <list_append_lcons_sn #H0
+  elim (lift_path_inv_d_sn … H0) -H0 #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)) //
+    <structure_append <Hr1 -Hr1 //
+  | elim (lift_path_inv_A_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)) //
+    <structure_append <Hr1 -Hr1 //
+  | elim (lift_path_inv_S_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)) //
+    <structure_append <Hr1 -Hr1 //
+  ]
+]
+qed-.
+
+(* Main inversions **********************************************************)
+
+theorem lift_path_inj (q:path) (p) (f):
+        ↑[f]q = ↑[f]p → q = p.
+#q elim q -q [| * [ #k ] #q #IH ] #p #f
+[ <lift_path_empty #H0
+  <(lift_path_inv_empty … H0) -H0 //
+| <lift_path_d_sn #H0
+  elim (lift_path_inv_d_sn … H0) -H0 #r #h #H0
+  <(tr_pap_inj ????? H0) -h [1,3: // ] #Hr #H0 destruct
+| <lift_path_m_sn #H0
+  elim (lift_path_inv_m_sn … H0) -H0 #r #Hr #H0 destruct
+| <lift_path_L_sn #H0
+  elim (lift_path_inv_L_sn … H0) -H0 #r #Hr #H0 destruct
+| <lift_path_A_sn #H0
+  elim (lift_path_inv_A_sn … H0) -H0 #r #Hr #H0 destruct
+| <lift_path_S_sn #H0
+  elim (lift_path_inv_S_sn … H0) -H0 #r #Hr #H0 destruct
+]
+<(IH … Hr) -r -IH //
+qed-.
+
 (* COMMENT 
 
 (* Advanced constructions with proj_rmap and stream_tls *********************)
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 6a70f61cb..9f8238432 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/bdd_term.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/bdd_term.ma
@@ -14,7 +14,7 @@
 
 include "delayed_updating/syntax/prototerm_constructors.ma".
 include "delayed_updating/syntax/prototerm_eq.ma".
-include "delayed_updating/notation/functions/class_d_phi_0.ma".
+include "delayed_updating/notation/functions/class_d_tau_0.ma".
 include "ground/xoa/or_5.ma".
 include "ground/xoa/ex_3_1.ma".
 include "ground/xoa/ex_4_2.ma".
@@ -25,7 +25,7 @@ include "ground/xoa/ex_5_3.ma".
 
 inductive bdd: 𝒫❨prototerm❩ ≝
 | bdd_oref: ∀n. bdd (⧣n)
-| bdd_iref: ∀t,n. bdd t → bdd (𝛗n.t)
+| 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
@@ -33,19 +33,19 @@ inductive bdd: 𝒫❨prototerm❩ ≝
 
 interpretation
   "by-depth delayed (prototerm)"
-  'ClassDPhi = (bdd).
+  'ClassDTau = (bdd).
 
 (* COMMENT
 
 (* Basic inversions *********************************************************)
 
 lemma bdd_inv_in_comp_gen:
-      ∀t,p. t ϵ 𝐃𝛗 → p ϵ t →
+      ∀t,p. t ϵ 𝐃𝛕 → p ϵ t →
       ∨∨ ∃∃n. #n ⇔ t & 𝗱n◗𝐞 = 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
+       | ∃∃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
 .
 #t #p #H elim H -H
 [ #n * /3 width=3 by or5_intro0, ex2_intro/
@@ -64,9 +64,9 @@ lemma bdd_inv_in_comp_gen:
 qed-.
 
 lemma bdd_inv_in_comp_d:
-      ∀t,q,n. t ϵ 𝐃𝛗 → 𝗱n◗q ϵ t →
+      ∀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 *
@@ -80,9 +80,9 @@ elim (bdd_inv_in_comp_gen … Ht Hq) -Ht -Hq *
 qed-.
 
 lemma bdd_inv_in_root_d:
-      ∀t,q,n. t ϵ 𝐃𝛗 → 𝗱n◗q ϵ ▵t →
+      ∀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 *
@@ -95,8 +95,8 @@ elim (bdd_inv_in_comp_d … Ht Hq) -Ht -Hq *
 qed-.
 
 lemma bdd_inv_in_comp_L:
-      ∀t,q. t ϵ 𝐃𝛗 → 𝗟◗q ϵ t →
-      ∃∃u. u ϵ 𝐃𝛗 & q ϵ u & 𝛌.u ⇔ t
+      ∀t,q. t ϵ 𝐃𝛕 → 𝗟◗q ϵ t →
+      ∃∃u. u ϵ 𝐃𝛕 & q ϵ u & 𝛌.u ⇔ t
 .
 #t #q #Ht #Hq
 elim (bdd_inv_in_comp_gen … Ht Hq) -Ht -Hq *
@@ -109,8 +109,8 @@ elim (bdd_inv_in_comp_gen … Ht Hq) -Ht -Hq *
 qed-.
 
 lemma bdd_inv_in_root_L:
-      ∀t,q. t ϵ 𝐃𝛗 → 𝗟◗q ϵ ▵t →
-      ∃∃u. u ϵ 𝐃𝛗 & q ϵ ▵u & 𝛌.u ⇔ t.
+      ∀t,q. t ϵ 𝐃𝛕 → 𝗟◗q ϵ ▵t →
+      ∃∃u. u ϵ 𝐃𝛕 & q ϵ ▵u & 𝛌.u ⇔ t.
 #t #q #Ht * #r #Hq
 elim (bdd_inv_in_comp_L … Ht Hq) -Ht -Hq
 #u #Hu #Hq #H0 destruct
@@ -118,8 +118,8 @@ elim (bdd_inv_in_comp_L … Ht Hq) -Ht -Hq
 qed-.
 
 lemma bdd_inv_in_comp_A:
-      ∀t,q. t ϵ 𝐃𝛗 → 𝗔◗q ϵ t →
-      ∃∃v,u. v ϵ 𝐃𝛗 & u ϵ 𝐃𝛗 & q ϵ u & @v.u ⇔ t
+      ∀t,q. t ϵ 𝐃𝛕 → 𝗔◗q ϵ t →
+      ∃∃v,u. v ϵ 𝐃𝛕 & u ϵ 𝐃𝛕 & q ϵ u & @v.u ⇔ t
 .
 #t #q #Ht #Hq
 elim (bdd_inv_in_comp_gen … Ht Hq) -Ht -Hq *
@@ -132,8 +132,8 @@ elim (bdd_inv_in_comp_gen … Ht Hq) -Ht -Hq *
 qed-.
 
 lemma bdd_inv_in_root_A:
-      ∀t,q. t ϵ 𝐃𝛗 → 𝗔◗q ϵ ▵t →
-      ∃∃v,u. v ϵ 𝐃𝛗 & u ϵ 𝐃𝛗 & q ϵ ▵u & @v.u ⇔ t
+      ∀t,q. t ϵ 𝐃𝛕 → 𝗔◗q ϵ ▵t →
+      ∃∃v,u. v ϵ 𝐃𝛕 & u ϵ 𝐃𝛕 & q ϵ ▵u & @v.u ⇔ t
 .
 #t #q #Ht * #r #Hq
 elim (bdd_inv_in_comp_A … Ht Hq) -Ht -Hq
@@ -142,8 +142,8 @@ elim (bdd_inv_in_comp_A … Ht Hq) -Ht -Hq
 qed-.
 
 lemma bdd_inv_in_comp_S:
-      ∀t,q. t ϵ 𝐃𝛗 → 𝗦◗q ϵ t →
-      ∃∃v,u. v ϵ 𝐃𝛗 & u ϵ 𝐃𝛗 & q ϵ v & @v.u ⇔ t
+      ∀t,q. t ϵ 𝐃𝛕 → 𝗦◗q ϵ t →
+      ∃∃v,u. v ϵ 𝐃𝛕 & u ϵ 𝐃𝛕 & q ϵ v & @v.u ⇔ t
 .
 #t #q #Ht #Hq
 elim (bdd_inv_in_comp_gen … Ht Hq) -Ht -Hq *
@@ -156,8 +156,8 @@ elim (bdd_inv_in_comp_gen … Ht Hq) -Ht -Hq *
 qed-.
 
 lemma bdd_inv_in_root_S:
-      ∀t,q. t ϵ 𝐃𝛗 → 𝗦◗q ϵ ▵t →
-      ∃∃v,u. v ϵ 𝐃𝛗 & u ϵ 𝐃𝛗 & q ϵ ▵v & @v.u ⇔ t
+      ∀t,q. t ϵ 𝐃𝛕 → 𝗦◗q ϵ ▵t →
+      ∃∃v,u. v ϵ 𝐃𝛕 & u ϵ 𝐃𝛕 & q ϵ ▵v & @v.u ⇔ t
 .
 #t #q #Ht * #r #Hq
 elim (bdd_inv_in_comp_S … Ht Hq) -Ht -Hq
@@ -168,7 +168,7 @@ qed-.
 (* Advanced inversions ******************************************************)
 
 lemma bbd_mono_in_root_d:
-      ∀l,n,p,t. t ϵ 𝐃𝛗 → p◖𝗱n ϵ ▵t → p◖l ϵ ▵t → 𝗱n = l.
+      ∀l,n,p,t. t ϵ 𝐃𝛕 → p◖𝗱n ϵ ▵t → p◖l ϵ ▵t → 𝗱n = l.
 #l #n #p elim p -p
 [ #t #Ht <list_cons_comm <list_cons_comm #Hn #Hl
   elim (bdd_inv_in_root_d … Ht Hn) -Ht -Hn *
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 434f1e810..f026c769e 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm_constructors.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm_constructors.ma
@@ -15,7 +15,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/tau_2.ma".
 include "delayed_updating/notation/functions/lamda_1.ma".
 include "delayed_updating/notation/functions/at_2.ma".
 
@@ -45,7 +45,7 @@ interpretation
 
 interpretation
   "inner variable reference by depth (prototerm)"
-  'Phi n t = (prototerm_node_1_2 (label_d n) label_m t).
+  'Tau n t = (prototerm_node_1_2 (label_d n) label_m t).
 
 interpretation
   "name-free functional abstraction (prototerm)"
@@ -58,13 +58,13 @@ interpretation
 (* Basic constructions *******************************************************)
 
 lemma in_comp_iref (t) (q) (n):
-      q ϵ t → 𝗱n◗𝗺◗q ϵ 𝛗n.t.
+      q ϵ t → 𝗱n◗𝗺◗q ϵ 𝛕n.t.
 /2 width=3 by ex2_intro/ qed.
 
 (* Basic inversions *********************************************************)
 
 lemma in_comp_inv_iref (t) (p) (n):
-      p ϵ 𝛗n.t →
+      p ϵ 𝛕n.t →
       ∃∃q. 𝗱n◗𝗺◗q = p & q ϵ t.
 #t #p #n * #q #Hq #Hp
 /2 width=3 by ex2_intro/
@@ -80,7 +80,7 @@ elim (eq_inv_list_empty_append … e0) -e0 #H0 #_
 qed-.
 
 lemma prototerm_in_root_inv_lcons_iref:
-      ∀t,p,l,n. l◗p ϵ ▵𝛗n.t →
+      ∀t,p,l,n. l◗p ϵ ▵𝛕n.t →
       ∧∧ 𝗱n = l & p ϵ ▵ɱ.t.
 #t #p #l #n * #q * #r #Hr
 <list_append_lcons_sn #H0 destruct -H0
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm_constructors_eq.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm_constructors_eq.ma
index 88f567214..46e945ede 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm_constructors_eq.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm_constructors_eq.ma
@@ -20,6 +20,6 @@ include "ground/lib/subset_ext_equivalence.ma".
 (* Constructions with equivalence for prototerm *****************************)
 
 lemma iref_eq_repl (t1) (t2) (n):
-      t1 ⇔ t2 → 𝛗n.t1 ⇔ 𝛗n.t2.
+      t1 ⇔ t2 → 𝛕n.t1 ⇔ 𝛕n.t2.
 /2 width=1 by subset_equivalence_ext_f1_bi/
 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
index c7bb79244..309eb0024 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm_proper_constructors.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm_proper_constructors.ma
@@ -20,6 +20,6 @@ include "delayed_updating/syntax/prototerm_constructors.ma".
 (* Constructions with prototerm constructors ********************************)
 
 lemma ppc_iref (t) (n):
-      (𝛗n.t) ϵ 𝐏.
+      (𝛕n.t) ϵ 𝐏.
 #t #n #p * #q #Hq #H0 destruct //
 qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_constructors.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_constructors.ma
index c70e09e1a..8cdfb5bf9 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_constructors.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_constructors.ma
@@ -20,20 +20,20 @@ include "delayed_updating/syntax/prototerm_constructors.ma".
 (* Constructions with constructors ******************************************)
 
 lemma unwind2_term_iref_sn (f) (t) (n:pnat):
-      ▼[f∘𝐮❨n❩]t ⊆ ▼[f](𝛗n.t).
+      ▼[f∘𝐮❨n❩]t ⊆ ▼[f](𝛕n.t).
 #f #t #n #p * #q #Hq #H0 destruct
 @(ex2_intro … (𝗱n◗𝗺◗q))
 /2 width=1 by in_comp_iref/
 qed-.
 
 lemma unwind2_term_iref_dx (f) (t) (n:pnat):
-      ▼[f](𝛗n.t) ⊆ ▼[f∘𝐮❨n❩]t.
+      ▼[f](𝛕n.t) ⊆ ▼[f∘𝐮❨n❩]t.
 #f #t #n #p * #q #Hq #H0 destruct
 elim (in_comp_inv_iref … Hq) -Hq #p #Hp #Ht destruct
 /2 width=1 by in_comp_unwind2_path_term/
 qed-.
 
 lemma unwind2_term_iref (f) (t) (n:pnat):
-      ▼[f∘𝐮❨n❩]t ⇔ ▼[f](𝛗n.t).
+      ▼[f∘𝐮❨n❩]t ⇔ ▼[f](𝛕n.t).
 /3 width=2 by conj, unwind2_term_iref_sn, unwind2_term_iref_dx/
 qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_preterm_fsubst.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_preterm_fsubst.ma
index 522ad9455..452c913e5 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_preterm_fsubst.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_preterm_fsubst.ma
@@ -18,7 +18,7 @@ include "delayed_updating/substitution/fsubst.ma".
 include "delayed_updating/syntax/preterm.ma".
 include "delayed_updating/syntax/prototerm_proper.ma".
 
-(* UNWIND FOR PRETERM ******************************************************)
+(* UNWIND FOR PRETERM *******************************************************)
 
 (* Constructions with fsubst ************************************************)
 
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind_gen_structure.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind_gen_structure.ma
index d8a44810c..5c92a9af5 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind_gen_structure.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind_gen_structure.ma
@@ -19,9 +19,9 @@ include "delayed_updating/syntax/path_proper.ma".
 include "ground/xoa/ex_4_2.ma".
 include "ground/xoa/ex_3_2.ma".
 
-(* GENERIC UNWIND FOR PATH *************************************************)
+(* GENERIC UNWIND FOR PATH **************************************************)
 
-(* Basic constructions with structure **************************************)
+(* Basic constructions with structure ***************************************)
 
 lemma structure_unwind_gen (p) (f):
       ⊗p = ⊗◆[f]p.
-- 
2.39.2