From: Ferruccio Guidi <fguidi@maelstrom.helm.cs.unibo.it>
Date: Sun, 2 Jan 2022 18:07:48 +0000 (+0100)
Subject: update in delayed updating
X-Git-Tag: make_still_working~117
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=2bc0ba993e26ab77a792b38ba39da7a3dd03ad43;p=helm.git

update in delayed updating

+ some properties of lift
---

diff --git a/matita/matita/contribs/lambdadelta/Makefile b/matita/matita/contribs/lambdadelta/Makefile
index dc13cc156..bee981cbd 100644
--- a/matita/matita/contribs/lambdadelta/Makefile
+++ b/matita/matita/contribs/lambdadelta/Makefile
@@ -26,7 +26,7 @@ TAGS := all names xoa orig elim deps top leaf stats tbls odeps trim clean \
         pack-ground pack-2a pack-2b \
         home up-home \
 
-PACKAGES  := ground basic_2A static_2 basic_2 apps_2 alpha_1
+PACKAGES  := ground basic_2A static_2 basic_2 apps_2 alpha_1 delayed_updating
 
 LDWS := $(shell find -name "*.ldw.xml")
 TBLS := $(shell find -name "*.tbl")
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/etc/baruparrow_2.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/baruparrow_2.etc
new file mode 100644
index 000000000..f6e1cf8ab
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/etc/baruparrow_2.etc
@@ -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( ↥[ term 46 t1 ] break term 75 t2  )"
+  non associative with precedence 75
+  for @{ 'BarUpArrow $t1 $t2 }.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/etc/baruparrow_4.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/baruparrow_4.etc
new file mode 100644
index 000000000..425260d8f
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/etc/baruparrow_4.etc
@@ -0,0 +1,27 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* NOTATION FOR DELAYED UPDATING ********************************************)
+
+notation < "hvbox( ↥❨ term 46 k, break term 46 p, break term 46 f ❩ )"
+  non associative with precedence 75
+  for @{ 'BarUpArrow $S $k $p $f }.
+
+notation > "hvbox( ↥❨ term 46 k, break term 46 p, break term 46 f ❩ )"
+  non associative with precedence 75
+  for @{ 'BarUpArrow ? $k $p $f }.
+
+notation > "hvbox( ↥{ term 46 S }❨ break term 46 k, break term 46 p, break term 46 f ❩ )"
+  non associative with precedence 75
+  for @{ 'BarUpArrow $S $k $p $f }.
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
index e08c4ea27..cf5c8f623 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/at_2.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/at_2.ma
@@ -14,6 +14,6 @@
 
 (* NOTATION FOR DELAYED UPDATING ********************************************)
 
-notation "hvbox( @ break term 76 u. break term 75 t )"
+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/black_halfcircleleft_2.ma b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/black_halfcircleleft_2.ma
deleted file mode 100644
index fe9683834..000000000
--- a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/black_halfcircleleft_2.ma
+++ /dev/null
@@ -1,19 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-(* NOTATION FOR DELAYED UPDATING ********************************************)
-
-notation "hvbox( hd ◖ break tl )"
-  left associative with precedence 47
-  for @{ 'BlackHalfCircleLeft $hd $tl }.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/black_halfcircleright_2.ma b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/black_halfcircleright_2.ma
deleted file mode 100644
index c58a18653..000000000
--- a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/black_halfcircleright_2.ma
+++ /dev/null
@@ -1,19 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-(* NOTATION FOR DELAYED UPDATING ********************************************)
-
-notation "hvbox( hd ◗ break tl )"
-  right associative with precedence 47
-  for @{ 'BlackHalfCircleRight $hd $tl }.
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
index 379a9092d..6f8d020a9 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/lamda_1.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/lamda_1.ma
@@ -14,6 +14,6 @@
 
 (* NOTATION FOR DELAYED UPDATING ********************************************)
 
-notation "hvbox( 𝛌 . break term 75 t )"
+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/uparrow_2.ma b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/uparrow_2.ma
index ac803abae..c80ffe09f 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/uparrow_2.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/uparrow_2.ma
@@ -14,6 +14,6 @@
 
 (* NOTATION FOR DELAYED UPDATING ********************************************)
 
-notation "hvbox( ↑ [ term 46 t1 ] break term 75 t2  )"
+notation "hvbox( ↑[ term 46 t1 ] break term 75 t2  )"
   non associative with precedence 75
   for @{ 'UpArrow $t1 $t2 }.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/uparrow_4.ma b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/uparrow_4.ma
index e9a85f9a6..1f35274c9 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/uparrow_4.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/uparrow_4.ma
@@ -14,14 +14,14 @@
 
 (* NOTATION FOR DELAYED UPDATING ********************************************)
 
-notation < "hvbox( ↑ ❨ term 46 k, break term 46 p, break term 46 f ❩ )"
+notation < "hvbox( ↑❨ term 46 k, break term 46 p, break term 46 f ❩ )"
   non associative with precedence 75
   for @{ 'UpArrow $S $k $p $f }.
 
-notation > "hvbox( ↑ ❨ term 46 k, break term 46 p, break term 46 f ❩ )"
+notation > "hvbox( ↑❨ term 46 k, break term 46 p, break term 46 f ❩ )"
   non associative with precedence 75
   for @{ 'UpArrow ? $k $p $f }.
 
-notation > "hvbox( ↑ { term 46 S } ❨ break term 46 k, break term 46 p, break term 46 f ❩ )"
+notation > "hvbox( ↑{ term 46 S }❨ break term 46 k, break term 46 p, break term 46 f ❩ )"
   non associative with precedence 75
   for @{ 'UpArrow $S $k $p $f }.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/relations/black_rightarrow_4.ma b/matita/matita/contribs/lambdadelta/delayed_updating/notation/relations/black_rightarrow_4.ma
index 8622760f3..f27fa0bad 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/notation/relations/black_rightarrow_4.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/notation/relations/black_rightarrow_4.ma
@@ -14,6 +14,6 @@
 
 (* NOTATION FOR DELAYED UPDATING ********************************************)
 
-notation "hvbox( t1 ➡ 'd' 'f' [ break term 46 p, break term 46 q ] break term 46 t2 )"
+notation "hvbox( t1 ➡'d''f'[ break term 46 p, break term 46 q ] break term 46 t2 )"
    non associative with precedence 45
    for @{ 'BlackRightArrow $t1 $p $q $t2 }.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr.ma
index 724168bdf..a99d8ca06 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr.ma
@@ -12,7 +12,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "ground/xoa/ex_3_1.ma".
 include "delayed_updating/syntax/path_structure.ma".
 include "delayed_updating/syntax/path_balanced.ma".
 include "delayed_updating/substitution/fsubst.ma".
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift.ma
index 0b3dc7d5c..a396beb46 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift.ma
@@ -20,8 +20,11 @@ include "delayed_updating/notation/functions/uparrow_2.ma".
 
 (* LIFT FOR PATH ***********************************************************)
 
+definition lift_continuation (A:Type[0]) ≝
+           path → tr_map → A.
+
 (* Note: inner numeric labels are not liftable, so they are removed *)
-rec definition lift_gen (A:Type[0]) (k:?→?→A) (p) (f) on p ≝
+rec definition lift_gen (A:Type[0]) (k:lift_continuation A) (p) (f) on p ≝
 match p with
 [ list_empty     ⇒ k 𝐞 f
 | list_lcons l q ⇒
@@ -55,28 +58,26 @@ interpretation
 
 (* Basic constructions ******************************************************)
 
-lemma lift_L (A) (k) (p) (f):
+lemma lift_empty (A) (k) (f):
+      k 𝐞 f = ↑{A}❨k, 𝐞, f❩.
+// qed.
+
+lemma lift_d_empty_sn (A) (k) (n) (f):
+      ↑❨(λp. k (𝗱❨f@❨n❩❩◗p)), 𝐞, f❩ = ↑{A}❨k, 𝗱❨n❩◗𝐞, f❩.
+// qed.
+
+lemma lift_d_lcons_sn (A) (k) (p) (l) (n) (f):
+      ↑❨k, l◗p, f∘𝐮❨ninj n❩❩ = ↑{A}❨k, 𝗱❨n❩◗l◗p, f❩.
+// qed.
+
+lemma lift_L_sn (A) (k) (p) (f):
       ↑❨(λp. k (𝗟◗p)), p, ⫯f❩ = ↑{A}❨k, 𝗟◗p, f❩.
 // qed.
 
-(* Basic constructions with proj_path ***************************************)
-
-lemma lift_append (p) (f) (q):
-      q●↑[f]p = ↑❨(λp. proj_path (q●p)), p, f❩.
-#p elim p -p
-[ //
-| #l #p #IH #f #q cases l
-  [
-  | <lift_L in ⊢ (???%);
-    >(list_append_rcons_sn ? q) in ⊢ (???(??(λ_.%)??));
-    
-     <IH 
-  normalize >IH
-  | //   
-
-(* Constructions with append ************************************************)
-
-theorem lift_append_A (p2) (p1) (f):
-        (↑[f]p1)●𝗔◗↑[↑[p1]f]p2 = ↑[f](p1●𝗔◗p2).
-#p2 #p1 elim p1 -p1
-[ #f normalize 
+lemma lift_A_sn (A) (k) (p) (f):
+      ↑❨(λp. k (𝗔◗p)), p, f❩ = ↑{A}❨k, 𝗔◗p, f❩.
+// qed.
+
+lemma lift_S_sn (A) (k) (p) (f):
+      ↑❨(λp. k (𝗦◗p)), p, f❩ = ↑{A}❨k, 𝗦◗p, f❩.
+// qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_eq.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_eq.ma
new file mode 100644
index 000000000..c0d7dcbf5
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_eq.ma
@@ -0,0 +1,76 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/lift.ma".
+include "ground/notation/relations/ringeq_3.ma".
+
+(* LIFT FOR PATH ***********************************************************)
+
+definition lift_exteq (A): relation2 (lift_continuation A) (lift_continuation A) ≝
+           λk1,k2. ∀p,f. k1 p f = k2 p f.
+
+interpretation
+  "extensional equivalence (lift continuation)"
+  'RingEq A k1 k2 = (lift_exteq A k1 k2).
+
+(* Constructions with lift_exteq ********************************************)
+
+lemma lift_eq_repl_sn (A) (p) (k1) (k2) (f):
+      k1 ≗{A} k2 → ↑❨k1, p, f❩ = ↑❨k2, p, f❩.
+#A #p elim p -p
+[ #k1 #k2 #f #Hk <lift_empty <lift_empty //
+| * [ #n * [| #l0 ]] [|*: #q ] #IH #k1 #k2 #f #Hk /2 width=1 by/
+]
+qed-.
+
+(* Advanced constructions ***************************************************)
+
+lemma lift_lcons_alt (A) (k) (f) (p) (l):
+      ↑❨λp2.k(l◗p2),p,f❩ = ↑{A}❨λp2.k((l◗𝐞)●p2),p,f❩.
+#A #k #f #p #l
+@lift_eq_repl_sn #p2 #g // (**) (* auto fails with typechecker failure *)
+qed.
+
+lemma lift_append_rcons_sn (A) (k) (f) (p1) (p) (l):
+      ↑❨λp2.k(p1●l◗p2),p,f❩ = ↑{A}❨λp2.k(p1◖l●p2),p,f❩.
+#A #k #f #p1 #p #l
+@lift_eq_repl_sn #p2 #g
+<list_append_rcons_sn //
+qed.
+
+(* Basic constructions with proj_path ***************************************)
+
+lemma lift_append_sn (p) (f) (q):
+      q●↑[f]p = ↑❨(λp. proj_path (q●p)), p, f❩.
+#p elim p -p
+[ //
+| * [ #n * [| #l ]] [|*: #p ] #IH #f #q
+  [ <lift_d_empty_sn <lift_d_empty_sn >lift_lcons_alt >lift_append_rcons_sn
+    <IH <IH -IH <list_append_rcons_sn //
+  | <lift_d_lcons_sn <lift_d_lcons_sn <IH -IH //
+  | <lift_L_sn <lift_L_sn >lift_lcons_alt >lift_append_rcons_sn
+    <IH <IH -IH <list_append_rcons_sn //
+  | <lift_A_sn <lift_A_sn >lift_lcons_alt >lift_append_rcons_sn
+    <IH <IH -IH <list_append_rcons_sn //
+  | <lift_S_sn <lift_S_sn >lift_lcons_alt >lift_append_rcons_sn
+    <IH <IH -IH <list_append_rcons_sn //
+  ]
+]
+qed.
+
+lemma lift_lcons (f) (p) (l):
+      l◗↑[f]p = ↑❨(λp. proj_path (l◗p)), p, f❩.
+#f #p #l
+>lift_lcons_alt <lift_append_sn //
+qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_structure.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_structure.ma
new file mode 100644
index 000000000..50b35e654
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_structure.ma
@@ -0,0 +1,98 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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_structure.ma".
+include "delayed_updating/substitution/lift_eq.ma".
+
+(* LIFT FOR PATH ***********************************************************)
+
+(* Constructions with structure ********************************************)
+
+lemma lift_d_empty_dx (n) (p) (f):
+      (⊗p)◖𝗱❨(↑[p◖𝗱❨n❩]f)@❨n❩❩ = ↑[f](p◖𝗱❨n❩).
+#n #p elim p -p
+[| * [ #m * [| #l ]] [|*: #p ] #IH ] #f
+[ //
+| <list_cons_shift <list_cons_comm <list_cons_comm //
+| <lift_d_lcons_sn <lift_d_lcons_sn //
+| <lift_L_sn <lift_L_sn <lift_lcons <IH //
+| <lift_A_sn <lift_A_sn <lift_lcons <IH //
+| <lift_S_sn <lift_S_sn <lift_lcons <IH //
+]
+qed.
+
+lemma lift_L_dx (p) (f):
+      (⊗p)◖𝗟 = ↑[f](p◖𝗟).
+#p elim p -p
+[| * [ #m * [| #l ]] [|*: #p ] #IH ] #f
+[ //
+| //
+| <lift_d_lcons_sn //
+| <lift_L_sn <lift_lcons //
+| <lift_A_sn <lift_lcons //
+| <lift_S_sn <lift_lcons //
+]
+qed.
+
+lemma lift_A_dx (p) (f):
+      (⊗p)◖𝗔 = ↑[f](p◖𝗔).
+#p elim p -p
+[| * [ #m * [| #l ]] [|*: #p ] #IH ] #f
+[ //
+| //
+| <lift_d_lcons_sn //
+| <lift_L_sn <lift_lcons //
+| <lift_A_sn <lift_lcons //
+| <lift_S_sn <lift_lcons //
+]
+qed.
+
+lemma lift_S_dx (p) (f):
+      (⊗p)◖𝗦 = ↑[f](p◖𝗦).
+#p elim p -p
+[| * [ #m * [| #l ]] [|*: #p ] #IH ] #f
+[ //
+| //
+| <lift_d_lcons_sn //
+| <lift_L_sn <lift_lcons //
+| <lift_A_sn <lift_lcons //
+| <lift_S_sn <lift_lcons //
+]
+qed.
+
+lemma structure_lift (p) (f):
+      ⊗p = ⊗↑[f]p.
+#p elim p -p
+[| * [ #m * [| #l ]] [|*: #p ] #IH ] #f
+[ //
+| //
+| //
+| <lift_L_sn <lift_lcons //
+| <lift_A_sn <lift_lcons //
+| <lift_S_sn <lift_lcons //
+]
+qed.
+
+lemma lift_structure (p) (f):
+      ⊗p = ↑[f]⊗p.
+#p elim p -p
+[| * [ #m * [| #l ]] [|*: #p ] #IH ] #f
+[ //
+| //
+| //
+| <structure_L_sn <lift_L_sn <lift_lcons //
+| <structure_A_sn <lift_A_sn <lift_lcons //
+| <structure_S_sn <lift_S_sn <lift_lcons //
+]
+qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path.ma
index 3c2be9aa3..ed8036ba9 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path.ma
@@ -15,9 +15,9 @@
 include "ground/lib/list_rcons.ma".
 include "ground/notation/functions/element_e_0.ma".
 include "ground/notation/functions/black_circle_2.ma".
+include "ground/notation/functions/black_halfcircleright_2.ma".
+include "ground/notation/functions/black_halfcircleleft_2.ma".
 include "delayed_updating/syntax/label.ma".
-include "delayed_updating/notation/functions/black_halfcircleright_2.ma".
-include "delayed_updating/notation/functions/black_halfcircleleft_2.ma".
 
 (* PATH *********************************************************************)
 
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_structure.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_structure.ma
index 5bf678ebe..6ba6e937b 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_structure.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_structure.ma
@@ -17,18 +17,75 @@ include "delayed_updating/notation/functions/circled_times_1.ma".
 
 (* STRUCTURE FOR PATH *******************************************************)
 
-rec definition path_structure (p) on p ≝
+rec definition structure (p) on p ≝
 match p with
 [ list_empty     ⇒ 𝐞
 | list_lcons l q ⇒
    match l with
-   [ label_node_d n ⇒ path_structure q
-   | label_edge_L   ⇒ 𝗟◗path_structure q
-   | label_edge_A   ⇒ 𝗔◗path_structure q
-   | label_edge_S   ⇒ 𝗦◗path_structure q
+   [ label_node_d n ⇒ structure q
+   | label_edge_L   ⇒ 𝗟◗structure q
+   | label_edge_A   ⇒ 𝗔◗structure q
+   | label_edge_S   ⇒ 𝗦◗structure q
    ]
 ].
 
 interpretation
   "structure (path)"
-  'CircledTimes p = (path_structure p).
+  'CircledTimes p = (structure p).
+
+(* Basic constructions ******************************************************)
+
+lemma structure_empty:
+      𝐞 = ⊗𝐞.
+// qed.
+
+lemma structure_d_sn (p) (n):
+      ⊗p = ⊗(𝗱❨n❩◗p).
+// qed.
+
+lemma structure_L_sn (p):
+      𝗟◗⊗p = ⊗(𝗟◗p).
+// qed.
+
+lemma structure_A_sn (p):
+      𝗔◗⊗p = ⊗(𝗔◗p).
+// qed.
+
+lemma structure_S_sn (p):
+      𝗦◗⊗p = ⊗(𝗦◗p).
+// qed.
+
+(* Main constructions *******************************************************)
+
+theorem structure_idem (p):
+        ⊗p = ⊗⊗p.
+#p elim p -p [| * [ #n ] #p #IH ] //
+qed.
+
+theorem structure_append (p1) (p2):
+        ⊗p1●⊗p2 = ⊗(p1●p2).
+#p1 elim p1 -p1 [| * [ #n ] #p1 #IH ] #p2
+[||*: <list_append_lcons_sn ] //
+qed.
+
+(* Constructions with list_rcons ********************************************)
+
+lemma structure_d_dx (p) (n):
+      ⊗p = ⊗(p◖𝗱❨n❩).
+#p #n <structure_append //
+qed.
+
+lemma structure_L_dx (p):
+      (⊗p)◖𝗟 = ⊗(p◖𝗟).
+#p <structure_append //
+qed.
+
+lemma structure_A_dx (p):
+      (⊗p)◖𝗔 = ⊗(p◖𝗔).
+#p <structure_append //
+qed.
+
+lemma structure_S_dx (p):
+      (⊗p)◖𝗦 = ⊗(p◖𝗦).
+#p <structure_append //
+qed.
diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/black_halfcircleleft_2.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/black_halfcircleleft_2.ma
new file mode 100644
index 000000000..3b6a9d0d5
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/ground/notation/functions/black_halfcircleleft_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                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* GROUND NOTATION **********************************************************)
+
+notation "hvbox( hd ◖ break tl )"
+  left associative with precedence 47
+  for @{ 'BlackHalfCircleLeft $hd $tl }.
diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/black_halfcircleright_2.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/black_halfcircleright_2.ma
new file mode 100644
index 000000000..0427a6a93
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/ground/notation/functions/black_halfcircleright_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                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* GROUND NOTATION **********************************************************)
+
+notation "hvbox( hd ◗ break tl )"
+  right associative with precedence 47
+  for @{ 'BlackHalfCircleRight $hd $tl }.