From: Ferruccio Guidi <fguidi@maelstrom.helm.cs.unibo.it>
Date: Fri, 10 Dec 2021 15:49:53 +0000 (+0100)
Subject: update in delayed updating
X-Git-Tag: make_still_working~126
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=3c257bf84769adf162510ed86a89872e3003629a;p=helm.git

update in delayed updating

+ WIP on dephi
+ some renaming
+ subset notation improved
---

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 5052f4cc9..e7d140231 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/bdd_term.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/bdd_term.ma
@@ -17,12 +17,12 @@ 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/syntax/preterm_constructors.ma".
 include "delayed_updating/notation/relations/in_predicate_d_phi_1.ma".
 
 (* BY-DEPTH DELAYED (BDD) TERM **********************************************)
 
-inductive bdd: predicate term ≝
+inductive bdd: predicate preterm ≝
 | bdd_oref: ∀n. bdd #n
 | bdd_iref: ∀t,n. bdd t → bdd 𝛗n.t
 | bdd_abst: ∀t. bdd t → bdd 𝛌.t
@@ -30,12 +30,12 @@ inductive bdd: predicate term ≝
 .
 
 interpretation
-  "well-formed by-depth delayed (term)"
+  "well-formed by-depth delayed (preterm)"
   'InPredicateDPhi t = (bdd t).
 
-(* Basic destructions *******************************************************)
+(* Basic inversions *********************************************************)
 
-lemma bdd_inv_in_com_gen:
+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
@@ -51,13 +51,13 @@ lemma bdd_inv_in_com_gen:
 ]
 qed-.
 
-lemma bdd_inv_in_com_d:
+lemma bdd_inv_in_comp_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 *
+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 #_ #_ #_ #H0 destruct
@@ -66,40 +66,125 @@ elim (bdd_inv_in_com_gen … Ht Hq) -Ht -Hq *
 ]
 qed-.
 
-lemma bdd_inv_in_ini_d:
+lemma bdd_inv_in_root_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 *
+elim (bdd_inv_in_comp_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
+| #u #Hu #Hq #H0 destruct
   /4 width=4 by ex3_intro, ex_intro, or_intror/
 ]
 qed-.
 
-lemma pippo:
+lemma bdd_inv_in_comp_L:
+      ∀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 *
+[ #n0 #_ #H0 destruct
+| #u0 #q0 #n0 #_ #_ #_ #H0 destruct
+| #u0 #q0 #Hu0 #Hq0 #H1 #H2 destruct /2 width=4 by ex3_intro/
+| #v0 #u0 #q0 #_ #_ #_ #_ #H0 destruct
+| #v0 #u0 #q0 #_ #_ #_ #_ #H0 destruct
+]
+qed-.
+
+lemma bdd_inv_in_root_L:
+      ∀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
+/3 width=4 by ex3_intro, ex_intro/
+qed-.
+
+lemma bdd_inv_in_comp_A:
+      ∀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 *
+[ #n0 #_ #H0 destruct
+| #u0 #q0 #n0 #_ #_ #_ #H0 destruct
+| #u0 #q0 #_ #_ #_ #H0 destruct
+| #v0 #u0 #q0 #Hv0 #Hu0 #Hq0 #H1 #H2 destruct /2 width=6 by ex4_2_intro/
+| #v0 #u0 #q0 #_ #_ #_ #_ #H0 destruct
+]
+qed-.
+
+lemma bdd_inv_in_root_A:
+      ∀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
+#v #u #Hv #Hu #Hq #H0 destruct
+/3 width=6 by ex4_2_intro, ex_intro/
+qed-.
+
+lemma bdd_inv_in_comp_S:
+      ∀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 *
+[ #n0 #_ #H0 destruct
+| #u0 #q0 #n0 #_ #_ #_ #H0 destruct
+| #u0 #q0 #_ #_ #_ #H0 destruct
+| #v0 #u0 #q0 #_ #_ #_ #_ #H0 destruct
+| #v0 #u0 #q0 #Hv0 #Hu0 #Hq0 #H1 #H2 destruct /2 width=6 by ex4_2_intro/
+]
+qed-.
+
+lemma bdd_inv_in_root_S:
+      ∀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
+#v #u #Hv #Hu #Hq #H0 destruct
+/3 width=6 by ex4_2_intro, ex_intro/
+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 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 //
+  elim (bdd_inv_in_root_d … Ht Hn) -Ht -Hn *
+  [ #H0 #_ destruct
+    elim (preterm_in_root_inv_lcons_oref … Hl) -Hl //
+  | #u #_ #_ #H0 destruct
+    elim (preterm_in_root_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) //
+  [ elim (bdd_inv_in_root_d … Ht Hn) -Ht -Hn *
+    [ #_ #H0
+      elim (eq_inv_list_empty_rcons ??? H0)
+    | #u #Hu #Hp #H0 destruct
+      elim (preterm_in_root_inv_lcons_iref … Hl) -Hl #_ #Hl
+      /2 width=4 by/
     ]
-  |
+  | elim (bdd_inv_in_root_L … Ht Hn) -Ht -Hn
+    #u #Hu #Hp #H0 destruct
+    elim (preterm_in_root_inv_lcons_abst … Hl) -Hl #_ #Hl
+    /2 width=4 by/
+  | elim (bdd_inv_in_root_A … Ht Hn) -Ht -Hn
+    #v #u #_ #Hu #Hp #H0 destruct
+    elim (preterm_in_root_inv_lcons_appl … Hl) -Hl * #H0 #Hl destruct
+    /2 width=4 by/
+  | elim (bdd_inv_in_root_S … Ht Hn) -Ht -Hn
+    #v #u #Hv #_ #Hp #H0 destruct
+    elim (preterm_in_root_inv_lcons_appl … Hl) -Hl * #H0 #Hl destruct
+    /2 width=4 by/
   ]
 ]
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/label.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/label.ma
index bdeaa9c20..d2a5c0783 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/label.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/label.ma
@@ -22,9 +22,9 @@ include "delayed_updating/notation/functions/edgelabel_s_0.ma".
 
 inductive label: Type[0] ≝
 | label_node_d: pnat → label
-| label_edge_l: label
-| label_edge_a: label
-| label_edge_s: label
+| label_edge_L: label
+| label_edge_A: label
+| label_edge_S: label
 .
 
 interpretation
@@ -33,12 +33,12 @@ interpretation
 
 interpretation
   "name-free functional abstruction (label)"
-  'EdgeLabelL = (label_edge_l).
+  'EdgeLabelL = (label_edge_L).
 
 interpretation
   "application (label)"
-  'EdgeLabelA = (label_edge_a).
+  'EdgeLabelA = (label_edge_A).
 
 interpretation
   "side branch (label)"
-  'EdgeLabelS = (label_edge_s).
+  'EdgeLabelS = (label_edge_S).
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path.ma
index a7d5e32c1..306c42a8c 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path.ma
@@ -19,7 +19,6 @@ include "delayed_updating/syntax/label.ma".
 include "delayed_updating/notation/functions/semicolon_2.ma".
 include "delayed_updating/notation/functions/comma_2.ma".
 
-
 (* PATH *********************************************************************)
 
 definition path ≝ list label.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_dephi.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_dephi.ma
new file mode 100644
index 000000000..f51295ecf
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_dephi.ma
@@ -0,0 +1,30 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/relocation/tr_pap.ma".
+include "delayed_updating/syntax/path.ma".
+
+(* DEPHI FOR PATH ***********************************************************)
+
+rec definition path_dephi (f) (p) on p ≝
+match p with
+[ list_empty     ⇒ 𝐞
+| list_lcons l q ⇒
+   match l with
+   [ label_node_d n ⇒ 𝗱❨f@❨n❩❩;path_dephi f q
+   | label_edge_L   ⇒ 𝗟;path_dephi (𝟏⨮f) q
+   | label_edge_A   ⇒ 𝗔;path_dephi f q
+   | label_edge_S   ⇒ 𝗦;path_dephi f q
+   ]
+].
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/preterm.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/preterm.ma
new file mode 100644
index 000000000..1da2d0174
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/preterm.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".
+
+(* PRETERM ******************************************************************)
+
+definition preterm: Type[0] ≝ predicate path.
+
+definition preterm_in_comp: relation2 path preterm ≝
+           λp,t. t p.
+
+interpretation
+  "belongs to complete (preterm)"
+  'UpDownArrowEpsilon p t = (preterm_in_comp p t).
+
+definition preterm_in_root: relation2 path preterm ≝
+           λp,t. ∃q. p;;q ϵ⬦ t.
+
+interpretation
+  "belongs to root (preterm)"
+  'UpArrowEpsilon p t = (preterm_in_root p t).
+
+(* Basic constructions ******************************************************)
+
+lemma preterm_in_comp_root (p) (t):
+      p ϵ⬦ t → p ϵ▵ t.
+/2 width=2 by ex_intro/
+qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/preterm_constructors.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/preterm_constructors.ma
new file mode 100644
index 000000000..03394c5bf
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/preterm_constructors.ma
@@ -0,0 +1,84 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/preterm.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 PRETERM *************************************************)
+
+definition preterm_node_0 (l): preterm ≝
+           λp. l;𝐞 = p.
+
+definition preterm_node_1 (l): preterm → preterm ≝
+           λt,p. ∃∃q. q ϵ⬦ t & l;q = p.
+
+definition preterm_node_2 (l1) (l2): preterm → preterm → preterm ≝
+           λt1,t2,p.
+           ∨∨ ∃∃q. q ϵ⬦ t1 & l1;q = p
+            | ∃∃q. q ϵ⬦ t2 & l2;q = p.
+
+interpretation
+  "outer variable reference by depth (preterm)"
+  'Hash n = (preterm_node_0 (label_node_d n)).
+
+interpretation
+  "inner variable reference by depth (preterm)"
+  'Phi n t = (preterm_node_1 (label_node_d n) t).
+
+interpretation
+  "name-free functional abstraction (preterm)"
+  'Lamda t = (preterm_node_1 label_edge_L t).
+
+interpretation
+  "application (preterm)"
+  'At u t = (preterm_node_2 label_edge_S label_edge_A u t).
+
+(* Basic Inversions *********************************************************)
+
+lemma preterm_in_root_inv_lcons_oref:
+      ∀p,l,n. l;p ϵ▵ #n →
+      ∧∧ 𝗱❨n❩ = l & 𝐞 = p.
+#p #l #n * #q
+<list_append_lcons_sn #H0 destruct -H0
+elim (eq_inv_list_empty_append … e0) -e0 #H0 #_
+/2 width=1 by conj/
+qed-.
+
+lemma preterm_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
+/3 width=2 by ex_intro, conj/
+qed-.
+
+lemma preterm_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
+/3 width=2 by ex_intro, conj/
+qed-.
+
+lemma preterm_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
+/4 width=2 by ex_intro, or_introl, or_intror, conj/
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/preterm_dephi.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/preterm_dephi.ma
new file mode 100644
index 000000000..67aa029d7
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/preterm_dephi.ma
@@ -0,0 +1,20 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/preterm_constructors.ma".
+
+(* DEPHI FOR PRETERM ********************************************************)
+
+definition preterm_dephi (f) (t) ≝
+           λp. ∃∃q. q ϵ⬦ t & p = path_dephi f q. 
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/term.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/term.ma
deleted file mode 100644
index 98a8dbdbd..000000000
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/term.ma
+++ /dev/null
@@ -1,42 +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/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
deleted file mode 100644
index b05473fd1..000000000
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/term_constructors.ma
+++ /dev/null
@@ -1,67 +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/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/lib/basics/core_notation/subseteq_2.ma b/matita/matita/lib/basics/core_notation/subseteq_2.ma
index bbfe6f527..09c630041 100644
--- a/matita/matita/lib/basics/core_notation/subseteq_2.ma
+++ b/matita/matita/lib/basics/core_notation/subseteq_2.ma
@@ -11,5 +11,6 @@
 
 (* Core notation *******************************************************)
 
-notation "hvbox(a break ⊆ b)" non associative with precedence 45
-for @{ 'subseteq $a $b }. (* \subseteq *)
+notation "hvbox( a ⊆ break term 46 b )"
+ non associative with precedence 45
+ for @{ 'subseteq $a $b }. (* \subseteq *)