From 160b7f7385763d872b5f2632696d02fd540c4eae Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Mon, 6 Dec 2021 20:45:59 +0100
Subject: [PATCH] update in delayed_updating

+ wip on predicate for bdd terms
+ updated notation
+ additions to lists
---
 .../notation/functions/at_2.ma                |  19 ++++
 .../notation/functions/comma_2.ma             |  19 ++++
 .../notation/functions/hash_1.ma              |  19 ++++
 .../notation/functions/lamda_1.ma             |  19 ++++
 .../notation/functions/nodelabel_d_1.ma       |   2 +-
 .../notation/functions/phi_2.ma               |  19 ++++
 .../notation/functions/semicolon_2.ma         |  19 ++++
 .../relations/in_predicate_d_phi_1.ma         |  19 ++++
 .../notation/relations/up_arrow_epsilon_2.ma  |  19 ++++
 .../relations/up_down_arrow_epsilon_2.ma      |  19 ++++
 .../delayed_updating/syntax/bdd_term.ma       | 105 ++++++++++++++++++
 .../delayed_updating/syntax/label.ma          |   2 -
 .../delayed_updating/syntax/path.ma           |  22 +++-
 .../delayed_updating/syntax/term.ma           |  42 +++++++
 .../syntax/term_constructors.ma               |  67 +++++++++++
 .../lambdadelta/ground/lib/list_append.ma     |  11 ++
 .../lambdadelta/ground/lib/list_rcons.ma      |   8 ++
 matita/matita/predefined_virtuals.ml          |   8 +-
 18 files changed, 428 insertions(+), 10 deletions(-)
 create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/at_2.ma
 create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/comma_2.ma
 create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/hash_1.ma
 create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/lamda_1.ma
 create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/phi_2.ma
 create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/semicolon_2.ma
 create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/notation/relations/in_predicate_d_phi_1.ma
 create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/notation/relations/up_arrow_epsilon_2.ma
 create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/notation/relations/up_down_arrow_epsilon_2.ma
 create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/syntax/bdd_term.ma
 create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/syntax/term.ma
 create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/syntax/term_constructors.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
new file mode 100644
index 000000000..e08c4ea27
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/at_2.ma
@@ -0,0 +1,19 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* NOTATION FOR DELAYED UPDATING ********************************************)
+
+notation "hvbox( @ break term 76 u. break term 75 t )"
+  non associative with precedence 75
+  for @{ 'At $u $t }.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/comma_2.ma b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/comma_2.ma
new file mode 100644
index 000000000..f2f318da5
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/comma_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( hd , break tl )"
+  right associative with precedence 50
+  for @{ 'Comma $hd $tl }.
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
new file mode 100644
index 000000000..8d85b354a
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/hash_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 90 n )"
+  non associative with precedence 75
+  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
new file mode 100644
index 000000000..379a9092d
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/lamda_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 75 t )"
+  non associative with precedence 75
+  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 8412e58e4..919edaa64 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
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-(* GROUND NOTATION **********************************************************)
+(* NOTATION FOR DELAYED UPDATING ********************************************)
 
 notation "hvbox( 𝗱❨ break term 46 a ❩ )"
   non associative with precedence 75
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
new file mode 100644
index 000000000..7d04cc37a
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/phi_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 75 t )"
+  non associative with precedence 75
+  for @{ 'Phi $n $t }.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/semicolon_2.ma b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/semicolon_2.ma
new file mode 100644
index 000000000..81c475923
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/semicolon_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( hd ; break tl )"
+  right associative with precedence 47
+  for @{ 'Semicolon $hd $tl }.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/relations/in_predicate_d_phi_1.ma b/matita/matita/contribs/lambdadelta/delayed_updating/notation/relations/in_predicate_d_phi_1.ma
new file mode 100644
index 000000000..7942fed3c
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/notation/relations/in_predicate_d_phi_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( t ϵ break 𝐃𝛗 )"
+  non associative with precedence 45
+  for @{ 'InPredicateDPhi $t }.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/relations/up_arrow_epsilon_2.ma b/matita/matita/contribs/lambdadelta/delayed_updating/notation/relations/up_arrow_epsilon_2.ma
new file mode 100644
index 000000000..1c4f842fe
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/notation/relations/up_arrow_epsilon_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( p ϵ▵ break term 46 t )"
+  non associative with precedence 45
+  for @{ 'UpArrowEpsilon $p $t }.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/relations/up_down_arrow_epsilon_2.ma b/matita/matita/contribs/lambdadelta/delayed_updating/notation/relations/up_down_arrow_epsilon_2.ma
new file mode 100644
index 000000000..ffef611a4
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/notation/relations/up_down_arrow_epsilon_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( p ϵ⬦ break term 46 t )"
+  non associative with precedence 45
+  for @{ 'UpDownArrowEpsilon $p $t }.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/bdd_term.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/bdd_term.ma
new file mode 100644
index 000000000..5052f4cc9
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/bdd_term.ma
@@ -0,0 +1,105 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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 "ground/xoa/or_5.ma".
+include "ground/xoa/ex_3_1.ma".
+include "ground/xoa/ex_4_2.ma".
+include "ground/xoa/ex_4_3.ma".
+include "ground/xoa/ex_5_3.ma".
+include "delayed_updating/syntax/term_constructors.ma".
+include "delayed_updating/notation/relations/in_predicate_d_phi_1.ma".
+
+(* BY-DEPTH DELAYED (BDD) TERM **********************************************)
+
+inductive bdd: predicate term ≝
+| 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
+.
+
+interpretation
+  "well-formed by-depth delayed (term)"
+  'InPredicateDPhi t = (bdd t).
+
+(* Basic destructions *******************************************************)
+
+lemma bdd_inv_in_com_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. 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 *
+[ #n * /3 width=3 by or5_intro0, ex2_intro/
+| #u #n #Hu * #q #Hq #Hp /3 width=7 by ex4_3_intro, or5_intro1/
+| #u #Hu * #q #Hq #Hp /3 width=6 by or5_intro2, ex4_2_intro/
+| #v #u #Hv #Hu * * #q #Hq #Hp /3 width=8 by ex5_3_intro, or5_intro3, or5_intro4/
+]
+qed-.
+
+lemma bdd_inv_in_com_d:
+      ∀t,q,n. t ϵ 𝐃𝛗 → 𝗱❨n❩;q ϵ⬦ t →
+      ∨∨ ∧∧ #n = t & 𝐞 = q
+       | ∃∃u. u ϵ 𝐃𝛗 & q ϵ⬦ u & 𝛗n.u = t
+.
+#t #q #n #Ht #Hq
+elim (bdd_inv_in_com_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 #_ #_ #_ #H0 destruct
+| #v0 #u0 #q0 #_ #_ #_ #_ #H0 destruct
+| #v0 #u0 #q0 #_ #_ #_ #_ #H0 destruct
+]
+qed-.
+
+lemma bdd_inv_in_ini_d:
+      ∀t,q,n. t ϵ 𝐃𝛗 → 𝗱❨n❩;q ϵ▵ t →
+      ∨∨ ∧∧ #n = t & 𝐞 = q
+       | ∃∃u. u ϵ 𝐃𝛗 & q ϵ▵ u & 𝛗n.u = t
+.
+#t #q #n #Ht * #r #Hq
+elim (bdd_inv_in_com_d … Ht Hq) -Ht -Hq *
+[ #H1 #H2
+  elim (eq_inv_list_empty_append … H2) -H2 #H2 #_ destruct
+  /3 width=1 by or_introl, conj/
+| #u #Hu #Hq #H1 destruct
+  /4 width=4 by ex3_intro, ex_intro, or_intror/
+]
+qed-.
+
+lemma pippo:
+      ∀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_ini_d … Ht Hn) -Ht -Hn *
+  [ #H1 #_ destruct
+    elim (term_in_ini_inv_lcons_oref … Hl) -Hl //
+  | #u #_ #_ #H1 destruct
+    elim (term_in_ini_inv_lcons_iref … Hl) -Hl //
+  ]
+| * [ #m ] #p #IH #t #Ht
+  <list_cons_shift <list_cons_shift #Hn #Hl
+  [ elim (bdd_inv_in_ini_d … Ht Hn) -Ht -Hn *
+    [ #_ #H
+      elim (eq_inv_list_empty_rcons ??? H)
+    | #u #Hu #Hp #H destruct
+      elim (term_in_ini_inv_lcons_iref … Hl) -Hl #_ #Hl
+      @(IH … Hu) //
+    ]
+  |
+  ]
+]
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/label.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/label.ma
index 1241db40a..bdeaa9c20 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/label.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/label.ma
@@ -27,8 +27,6 @@ inductive label: Type[0] ≝
 | label_edge_s: label
 .
 
-coercion label_node_d.
-
 interpretation
   "variable reference by depth (label)"
   'NodeLabelD p = (label_node_d p).
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path.ma
index 69355961c..a7d5e32c1 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path.ma
@@ -12,9 +12,13 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "ground/lib/list.ma".
-include "delayed_updating/notation/functions/element_e_0.ma".
+include "ground/lib/list_rcons.ma".
+include "ground/notation/functions/element_e_0.ma".
+include "ground/notation/functions/double_semicolon_2.ma".
 include "delayed_updating/syntax/label.ma".
+include "delayed_updating/notation/functions/semicolon_2.ma".
+include "delayed_updating/notation/functions/comma_2.ma".
+
 
 (* PATH *********************************************************************)
 
@@ -22,4 +26,16 @@ definition path ≝ list label.
 
 interpretation
   "empty (paths)"
-  'ElementE = (list_nil label).
+  'ElementE = (list_empty label).
+
+interpretation
+  "left cons (paths)"
+  'Semicolon l p = (list_lcons label l p).
+
+interpretation
+  "append (paths)"
+  'DoubleSemicolon l1 l2 = (list_append label l1 l2).
+
+interpretation
+  "right cons (paths)"
+  'Comma p l = (list_append label p (list_lcons label l (list_empty label))).
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/term.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/term.ma
new file mode 100644
index 000000000..98a8dbdbd
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/term.ma
@@ -0,0 +1,42 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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 "delayed_updating/notation/relations/up_down_arrow_epsilon_2.ma".
+include "delayed_updating/notation/relations/up_arrow_epsilon_2.ma".
+
+(* TERM *********************************************************************)
+
+definition term: Type[0] ≝ predicate path.
+
+definition term_in_com: relation2 path term ≝
+           λp,t. t p.
+
+interpretation
+  "belongs to complete (term)"
+  'UpDownArrowEpsilon p t = (term_in_com p t).
+
+definition term_in_ini: relation2 path term ≝
+           λp,t. ∃q. p;;q ϵ⬦ t.
+
+interpretation
+  "belongs to initial (term)"
+  'UpArrowEpsilon p t = (term_in_ini p t).
+
+(* Basic constructions ******************************************************)
+
+lemma term_in_com_ini (p) (t):
+      p ϵ⬦ t → p ϵ▵ t.
+/2 width=2 by ex_intro/
+qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/term_constructors.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/term_constructors.ma
new file mode 100644
index 000000000..b05473fd1
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/term_constructors.ma
@@ -0,0 +1,67 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/term.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".
+include "delayed_updating/notation/functions/at_2.ma".
+
+(* CONSTRUCTORS FOR TERM ****************************************************)
+
+definition term_node_0 (l): term ≝
+           λp. l;𝐞 = p.
+
+definition term_node_1 (l): term → term ≝
+           λt,p. ∃∃q. q ϵ⬦ t & l;q = p.
+
+definition term_node_2 (l1) (l2): term → term → term ≝
+           λt1,t2,p.
+           ∨∨ ∃∃q. q ϵ⬦ t1 & l1;q = p
+            | ∃∃q. q ϵ⬦ t2 & l2;q = p.
+
+interpretation
+  "outer variable reference by depth (term)"
+  'Hash n = (term_node_0 (label_node_d n)).
+
+interpretation
+  "inner variable reference by depth (term)"
+  'Phi n t = (term_node_1 (label_node_d n) t).
+
+interpretation
+  "name-free functional abstraction (term)"
+  'Lamda t = (term_node_1 label_edge_l t).
+
+interpretation
+  "application (term)"
+  'At u t = (term_node_2 label_edge_s label_edge_a u t).
+
+(* Basic Inversions *********************************************************)
+
+lemma term_in_ini_inv_lcons_oref:
+      ∀p,l,n. l;p ϵ▵ #n →
+      ∧∧ 𝗱❨n❩ = l & 𝐞 = p.
+#p #l #n * #q
+<list_append_lcons_sn #H destruct -H
+elim (eq_inv_list_empty_append … e0) -e0 #H1 #_
+/2 width=1 by conj/
+qed-.
+
+lemma term_in_ini_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 #H1 destruct
+/3 width=2 by ex_intro, conj/
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/ground/lib/list_append.ma b/matita/matita/contribs/lambdadelta/ground/lib/list_append.ma
index 13c68a33c..05fefceb3 100644
--- a/matita/matita/contribs/lambdadelta/ground/lib/list_append.ma
+++ b/matita/matita/contribs/lambdadelta/ground/lib/list_append.ma
@@ -56,3 +56,14 @@ lemma list_append_assoc (A):
   ]
 ]
 qed.
+
+(* Basic inversions *********************************************************)
+
+lemma eq_inv_list_empty_append (A):
+      ∀l1,l2. ⓔ = l1⨁{A}l2 →
+      ∧∧ ⓔ = l1 & ⓔ = l2.
+#A *
+[ #l2 /2 width=1 by conj/
+| #a1 #l1 #l2 <list_append_lcons_sn #H destruct
+]
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/ground/lib/list_rcons.ma b/matita/matita/contribs/lambdadelta/ground/lib/list_rcons.ma
index 2cf2e23bf..66910e1a9 100644
--- a/matita/matita/contribs/lambdadelta/ground/lib/list_rcons.ma
+++ b/matita/matita/contribs/lambdadelta/ground/lib/list_rcons.ma
@@ -41,3 +41,11 @@ lemma list_append_rcons_sn (A):
 lemma list_append_rcons_dx (A):
       ∀l1,l2,a. l1 ⨁ l2 ⨭ a = l1 ⨁{A} (l2 ⨭ a).
 // qed.
+
+(* Basic inversions *********************************************************)
+
+lemma eq_inv_list_empty_rcons (A):
+      ∀l,a. ⓔ = l⨭{A}a → ⊥.
+#A #l #a #H
+elim (eq_inv_list_empty_append … H) -H #_ #H destruct
+qed-.
diff --git a/matita/matita/predefined_virtuals.ml b/matita/matita/predefined_virtuals.ml
index 26a2656e3..a816099a6 100644
--- a/matita/matita/predefined_virtuals.ml
+++ b/matita/matita/predefined_virtuals.ml
@@ -1515,13 +1515,13 @@ let predefined_classes = [
  ["="; "≝"; "≡"; "≘"; "≗"; "≐"; "≑"; "≛"; "≚"; "≙"; "⌆"; "⧦"; "⊜"; "≋"; "⩳"; "≅"; "⩬"; "≂"; "≃"; "≈"; ];  
  ["→"; "⥲"; "↦"; "⇝"; "⤞"; "⇾"; "⤍"; "⤏"; "⤳"; ] ;
  ["⇒"; "⤇"; "➾"; "⇨"; "⬀"; "➡"; "⬈"; "➤"; "➸"; "⇉"; "⥰"; ] ;
- ["^"; "↑"; "⇡"; ] ;
+ ["^"; "↑"; "⇡"; "↥"; "▵"; ] ;
  ["⇑"; "⇧"; "⬆"; ] ; 
  ["⇓"; "⇩"; "⬂"; "⬇"; "⬊"; "➷"; ] ;
  ["⇕"; "⇳"; "⬍"; "↕"; ];
  ["↔"; "⇔"; "⬄"; "⬌"; ] ; 
  ["≤"; "≲"; "≼"; "≰"; "≴"; "⋠"; "⊆"; "⫃"; "⊑"; ] ;
- ["_"; "↓"; "↙"; "⇣"; "⇃"; "⇂"; "⎽"; "⎼"; "⎻"; "⎺"; ];
+ ["_"; "↓"; "↙"; "⇣"; "⇃"; "⇂"; "⎽"; "⎼"; "⎻"; "⎺"; "▿"; ];
  ["<"; "≺"; "≮"; "⊀"; "〈"; "«"; "❬"; "❮"; "❰"; ] ;
  ["("; "❨"; "❪"; "❲"; "（"; ];
  [")"; "❩"; "❫"; "❳"; "）"; ];
@@ -1530,7 +1530,7 @@ let predefined_classes = [
  ["{"; "❴"; "⦃" ] ;
  ["}"; "❵"; "⦄" ] ;
  ["□"; "◽"; "▪"; "◾"; ];
- ["◊"; "♢"; "⧫"; "♦"; "⟐"; "⟠"; ] ;
+ ["◊"; "⬦"; "♢"; "⧫"; "♦"; "⟐"; "⟠"; ] ;
  [">"; "⭃"; "⧁"; "〉"; "»"; "❭"; "❯"; "❱"; "▸"; "►"; "▶"; "⊃"; "⊐"; ] ;
  ["≥"; "⪀"; "≽"; "⪴"; "⥸"; "⊒"; ]; 
  ["∨"; "⩖"; "∪"; "∩"; "⋓"; "⋒" ] ;
@@ -1544,7 +1544,7 @@ let predefined_classes = [
  ["D"; "Δ"; "𝔻"; "ⅅ"; "𝐃"; "𝚫"; "Ⓓ"; "𝗗"; ] ;
  ["e"; "ɛ"; "ε"; "ϵ"; "Є"; "ℯ"; "𝕖"; "ⅇ"; "𝐞"; "𝛆"; "𝛜"; "ⓔ"; ] ;
  ["E"; "ℰ"; "𝔼"; "𝐄"; "Ⓔ"; ] ;
- ["f"; "φ"; "ψ"; "ϕ"; "⨍"; "𝕗"; "𝐟"; "𝛟"; "𝛙"; "ⓕ"; ] ;
+ ["f"; "φ"; "ψ"; "ϕ"; "⨍"; "𝕗"; "𝐟"; "𝛗"; "𝛟"; "𝛙"; "ⓕ"; ] ;
  ["F"; "Φ"; "Ψ"; "ℱ"; "𝔽"; "𝐅"; "𝚽"; "𝚿"; "Ⓕ"; "𝗙"; ] ;
  ["g"; "γ"; "ℊ"; "𝕘"; "𝐠"; "𝛄"; "ⓖ"; ] ;
  ["G"; "Γ"; "𝔾"; "𝐆"; "𝚪"; "Ⓖ"; ] ;
-- 
2.39.2