update in delayed_updating

+ reference by depth with offset parked for now

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/etc/d2/d2.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/d2/d2.etc
new file mode 100644 (file)
index 0000000..32a628e
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/etc/d2/d2.etc
@@ -0,0 +1,77 @@
+include "delayed_updating/notation/functions/nodelabel_d_2.ma".
+
+| label_d2: pnat → nat → label
+
+interpretation
+  "variable reference by depth with offset (label)"
+  'NodeLabelD k d = (label_d2 k d).
+
+  | label_d2 k d ⇒ depth q
+
+lemma depth_d2_dx (p) (k) (d):
+      ♭p = ♭(p◖𝗱❨k,d❩).
+// qed.
+
+lemma depth_d2_sn (p) (k) (d):
+      ♭p = ♭(𝗱❨k,d❩◗p).
+// qed.
+
+   | label_d2 k d ⇒ structure q
+
+lemma structure_d2_dx (p) (k) (d):
+      ⊗p = ⊗(p◖𝗱❨k,d❩).
+// qed.
+
+lemma structure_d2_sn (p) (k) (d):
+      ⊗p = ⊗(𝗱❨k,d❩◗p).
+#p #k #d <structure_append //
+qed.
+
+lemma eq_inv_d2_dx_structure (d) (h) (q) (p):
+      q◖𝗱❨h,d❩ = ⊗p → ⊥.
+#d #h #q #p elim p -p [| * [ #k | #k #d ] #p #IH ]
+[ <structure_empty #H0 destruct
+| <structure_d_dx #H0 /2 width=1 by/
+| <structure_d2_dx #H0 /2 width=1 by/
+| <structure_m_dx #H0 /2 width=1 by/
+| <structure_L_dx #H0 destruct
+| <structure_A_dx #H0 destruct
+| <structure_S_dx #H0 destruct
+]
+qed-.
+
+lemma eq_inv_d2_sn_structure (d) (h) (q) (p):
+      (𝗱❨h,d❩◗q) = ⊗p → ⊥.
+#d #h #q #p >list_cons_comm #H0
+elim (eq_inv_append_structure … H0) -H0 #r1 #r2
+<list_cons_comm #H0 #H1 #H2 destruct
+elim (eq_inv_d2_dx_structure … H0)
+qed-.
+
+include "delayed_updating/notation/functions/tau_3.ma".
+
+interpretation
+  "inner variable reference by depth with offset (prototerm)"
+  'Tau k d t = (prototerm_node_1_2 (label_d2 k d) label_m t).
+
+lemma in_comp_iref2 (t) (q) (k) (d):
+      q ϵ t → 𝗱❨k,d❩◗𝗺◗q ϵ 𝛕❨k,d❩.t.
+/2 width=3 by ex2_intro/ qed.
+
+lemma in_comp_inv_iref2 (t) (p) (k) (d):
+      p ϵ 𝛕❨k,d❩.t →
+      ∃∃q. 𝗱❨k,d❩◗𝗺◗q = p & q ϵ t.
+#t #p #k #d * #q #Hq #Hp
+/2 width=3 by ex2_intro/
+qed-.
+
+lemma ppc_iref2 (t) (k) (d):
+      (𝛕❨k,d❩.t) ϵ 𝐏.
+#t #k #d #p * #q #Hq #H0 destruct //
+qed.
+
+lemma pic_inv_d2_dx (p) (k) (d):
+      p◖𝗱❨k,d❩ ϵ 𝐈 → ⊥.
+#p #k #d @(insert_eq_1 … (p◖𝗱❨k,d❩))
+#q * -q [|*: #q ] #H0 destruct
+qed-.

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/etc/d2/nodelabel_d_2.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/d2/nodelabel_d_2.etc
new file mode 100644 (file)
index 0000000..8239026
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/etc/d2/nodelabel_d_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( 𝗱 ❨ break term 46 k, break term 46 d ❩ )"
+  non associative with precedence 70
+  for @{ 'NodeLabelD $k $d }.

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/etc/d2/tau_3.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/d2/tau_3.etc
new file mode 100644 (file)
index 0000000..204dd89
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/etc/d2/tau_3.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( 𝛕 ❨ break term 46 k, break term 46 d ❩. break term 70 t )"
+  non associative with precedence 70
+  for @{ 'Tau $k $d $t }.

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/nodelabel_d_2.ma b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/nodelabel_d_2.ma
deleted file mode 100644 (file)
index 8239026..0000000
--- a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/nodelabel_d_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( 𝗱 ❨ break term 46 k, break term 46 d ❩ )"
-  non associative with precedence 70
-  for @{ 'NodeLabelD $k $d }.

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/tau_3.ma b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/tau_3.ma
deleted file mode 100644 (file)
index 204dd89..0000000
--- a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/tau_3.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( 𝛕 ❨ break term 46 k, break term 46 d ❩. break term 70 t )"
-  non associative with precedence 70
-  for @{ 'Tau $k $d $t }.

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/label.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/label.ma
index 7106e0b0b217021d7fdcae1eed404fc3533ff428..6a607559cae0c07e5aaccd85230a8261f422771f 100644 (file)
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/label.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/label.ma
@@ -16,9 +16,8 @@
  * Initial invocation: - Patience on me to gain peace and perfection! -
  *)
 
  * Initial invocation: - Patience on me to gain peace and perfection! -
  *)
 

-include "ground/arith/nat.ma".
+include "ground/arith/pnat.ma".

 include "delayed_updating/notation/functions/nodelabel_d_1.ma".
 include "delayed_updating/notation/functions/nodelabel_d_1.ma".

-include "delayed_updating/notation/functions/nodelabel_d_2.ma".

 include "delayed_updating/notation/functions/nodelabel_m_0.ma".
 include "delayed_updating/notation/functions/edgelabel_l_0.ma".
 include "delayed_updating/notation/functions/edgelabel_a_0.ma".
 include "delayed_updating/notation/functions/nodelabel_m_0.ma".
 include "delayed_updating/notation/functions/edgelabel_l_0.ma".
 include "delayed_updating/notation/functions/edgelabel_a_0.ma".


@@ -27,22 +26,17 @@ include "delayed_updating/notation/functions/edgelabel_s_0.ma".
 (* LABEL ********************************************************************)
 
 inductive label: Type[0] ≝
 (* LABEL ********************************************************************)
 
 inductive label: Type[0] ≝

-| label_d : pnat → label
-| label_d2: pnat → nat → label
-| label_m : label
-| label_L : label
-| label_A : label
-| label_S : label
+| label_d: pnat → label
+| label_m: label
+| label_L: label
+| label_A: label
+| label_S: label

 .
 
 interpretation
   "variable reference by depth (label)"
   'NodeLabelD k = (label_d k).
 
 .
 
 interpretation
   "variable reference by depth (label)"
   'NodeLabelD k = (label_d k).
 

-interpretation
-  "variable reference by depth with offset (label)"
-  'NodeLabelD k d = (label_d2 k d).
-

 interpretation
   "mark (label)"
   'NodeLabelM = (label_m).
 interpretation
   "mark (label)"
   'NodeLabelM = (label_m).

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_depth.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_depth.ma
index 2e638b8ac43bfba05ccc9783d2045d130d302a9d..a769327f65b218f655530102b435ca614b60eb22 100644 (file)
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_depth.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_depth.ma
@@ -23,12 +23,11 @@ match p with
 [ list_empty     ⇒ 𝟎
 | list_lcons l q ⇒
   match l with
 [ list_empty     ⇒ 𝟎
 | list_lcons l q ⇒
   match l with

-  [ label_d k    ⇒ depth q
-  | label_d2 k d ⇒ depth q
-  | label_m      ⇒ depth q
-  | label_L      ⇒ ↑(depth q)
-  | label_A      ⇒ depth q
-  | label_S      ⇒ depth q
+  [ label_d k ⇒ depth q
+  | label_m   ⇒ depth q
+  | label_L   ⇒ ↑(depth q)
+  | label_A   ⇒ depth q
+  | label_S   ⇒ depth q

   ]
 ].
 
   ]
 ].
 


@@ -45,10 +44,6 @@ lemma depth_d_dx (p) (k):
       ♭p = ♭(p◖𝗱k).
 // qed.
 
       ♭p = ♭(p◖𝗱k).
 // qed.
 

-lemma depth_d2_dx (p) (k) (d):
-      ♭p = ♭(p◖𝗱❨k,d❩).
-// qed.
-

 lemma depth_m_dx (p):
       ♭p = ♭(p◖𝗺).
 // qed.
 lemma depth_m_dx (p):
       ♭p = ♭(p◖𝗺).
 // qed.


@@ -70,9 +65,8 @@ lemma depth_S_dx (p):
 theorem depth_append (p) (q):
         (♭p)+(♭q) = ♭(p●q).
 #p #q elim q -q //
 theorem depth_append (p) (q):
         (♭p)+(♭q) = ♭(p●q).
 #p #q elim q -q //

-* [ #k | #k #d ] #q #IH <list_append_lcons_sn
+* [ #k ] #q #IH <list_append_lcons_sn

 [ <depth_d_dx <depth_d_dx //
 [ <depth_d_dx <depth_d_dx //

-| <depth_d2_dx <depth_d2_dx //

 | <depth_m_dx <depth_m_dx //
 | <depth_L_dx <depth_L_dx //
 | <depth_A_dx <depth_A_dx //
 | <depth_m_dx <depth_m_dx //
 | <depth_L_dx <depth_L_dx //
 | <depth_A_dx <depth_A_dx //


@@ -86,10 +80,6 @@ lemma depth_d_sn (p) (k):
       ♭p = ♭(𝗱k◗p).
 // qed.
 
       ♭p = ♭(𝗱k◗p).
 // qed.
 

-lemma depth_d2_sn (p) (k) (d):
-      ♭p = ♭(𝗱❨k,d❩◗p).
-// qed.
-

 lemma depth_m_sn (p):
       ♭p = ♭(𝗺◗p).
 // qed.
 lemma depth_m_sn (p):
       ♭p = ♭(𝗺◗p).
 // qed.

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_inner.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_inner.ma
index 25678301b5951bb84b6edaf188cbf9d2f05ebbc5..b2b0cb03f9e6b681b1ab78ede143d96e27a8b42d 100644 (file)
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_inner.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_inner.ma
@@ -39,12 +39,6 @@ lemma pic_inv_d_dx (p) (k):
 #q * -q [|*: #q ] #H0 destruct
 qed-.
 
 #q * -q [|*: #q ] #H0 destruct
 qed-.
 

-lemma pic_inv_d2_dx (p) (k) (d):
-      p◖𝗱❨k,d❩ ϵ 𝐈 → ⊥.
-#p #k #d @(insert_eq_1 … (p◖𝗱❨k,d❩))
-#q * -q [|*: #q ] #H0 destruct
-qed-.
-

 (* Constructions with path_lcons ********************************************)
 
 lemma pic_m_sn (p):
 (* Constructions with path_lcons ********************************************)
 
 lemma pic_m_sn (p):

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 95c728682db4058cc10f4caca52bb357be601634..288575c4e7680630668be3a61108478261a6d0c4 100644 (file)
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_structure.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_structure.ma
@@ -23,12 +23,11 @@ match p with
 [ list_empty     ⇒ 𝐞
 | list_lcons l q ⇒
    match l with
 [ list_empty     ⇒ 𝐞
 | list_lcons l q ⇒
    match l with

-   [ label_d k    ⇒ structure q
-   | label_d2 k d ⇒ structure q
-   | label_m      ⇒ structure q
-   | label_L      ⇒ (structure q)◖𝗟
-   | label_A      ⇒ (structure q)◖𝗔
-   | label_S      ⇒ (structure q)◖𝗦
+   [ label_d k ⇒ structure q
+   | label_m   ⇒ structure q
+   | label_L   ⇒ (structure q)◖𝗟
+   | label_A   ⇒ (structure q)◖𝗔
+   | label_S   ⇒ (structure q)◖𝗦

    ]
 ].
 
    ]
 ].
 


@@ -46,10 +45,6 @@ lemma structure_d_dx (p) (k):
       ⊗p = ⊗(p◖𝗱k).
 // qed.
 
       ⊗p = ⊗(p◖𝗱k).
 // qed.
 

-lemma structure_d2_dx (p) (k) (d):
-      ⊗p = ⊗(p◖𝗱❨k,d❩).
-// qed.
-

 lemma structure_m_dx (p):
       ⊗p = ⊗(p◖𝗺).
 // qed.
 lemma structure_m_dx (p):
       ⊗p = ⊗(p◖𝗺).
 // qed.


@@ -71,13 +66,13 @@ lemma structure_S_dx (p):
 theorem structure_idem (p):
         ⊗p = ⊗⊗p.
 #p elim p -p //
 theorem structure_idem (p):
         ⊗p = ⊗⊗p.
 #p elim p -p //

-* [ #k | #k #d ] #p #IH //
+* [ #k ] #p #IH //

 qed.
 
 theorem structure_append (p) (q):
         ⊗p●⊗q = ⊗(p●q).
 #p #q elim q -q //
 qed.
 
 theorem structure_append (p) (q):
         ⊗p●⊗q = ⊗(p●q).
 #p #q elim q -q //

-* [ #k | #k #d ] #q #IH //
+* [ #k ] #q #IH //

 <list_append_lcons_sn //
 qed.
 
 <list_append_lcons_sn //
 qed.
 


@@ -88,11 +83,6 @@ lemma structure_d_sn (p) (k):
 #p #k <structure_append //
 qed.
 
 #p #k <structure_append //
 qed.
 

-lemma structure_d2_sn (p) (k) (d):
-      ⊗p = ⊗(𝗱❨k,d❩◗p).
-#p #k #d <structure_append //
-qed.
-

 lemma structure_m_sn (p):
       ⊗p = ⊗(𝗺◗p).
 #p <structure_append //
 lemma structure_m_sn (p):
       ⊗p = ⊗(𝗺◗p).
 #p <structure_append //


@@ -117,23 +107,9 @@ qed.
 
 lemma eq_inv_d_dx_structure (h) (q) (p):
       q◖𝗱h = ⊗p → ⊥.
 
 lemma eq_inv_d_dx_structure (h) (q) (p):
       q◖𝗱h = ⊗p → ⊥.

-#h #q #p elim p -p [| * [ #k | #k #d ] #p #IH ]
+#h #q #p elim p -p [| * [ #k ] #p #IH ]

 [ <structure_empty #H0 destruct
 | <structure_d_dx #H0 /2 width=1 by/
 [ <structure_empty #H0 destruct
 | <structure_d_dx #H0 /2 width=1 by/

-| <structure_d2_dx #H0 /2 width=1 by/
-| <structure_m_dx #H0 /2 width=1 by/
-| <structure_L_dx #H0 destruct
-| <structure_A_dx #H0 destruct
-| <structure_S_dx #H0 destruct
-]
-qed-.
-
-lemma eq_inv_d2_dx_structure (d) (h) (q) (p):
-      q◖𝗱❨h,d❩ = ⊗p → ⊥.
-#d #h #q #p elim p -p [| * [ #k | #k #d ] #p #IH ]
-[ <structure_empty #H0 destruct
-| <structure_d_dx #H0 /2 width=1 by/
-| <structure_d2_dx #H0 /2 width=1 by/

 | <structure_m_dx #H0 /2 width=1 by/
 | <structure_L_dx #H0 destruct
 | <structure_A_dx #H0 destruct
 | <structure_m_dx #H0 /2 width=1 by/
 | <structure_L_dx #H0 destruct
 | <structure_A_dx #H0 destruct


@@ -143,10 +119,9 @@ qed-.
 
 lemma eq_inv_m_dx_structure (q) (p):
       q◖𝗺 = ⊗p → ⊥.
 
 lemma eq_inv_m_dx_structure (q) (p):
       q◖𝗺 = ⊗p → ⊥.

-#q #p elim p -p [| * [ #k | #k #d ] #p #IH ]
+#q #p elim p -p [| * [ #k ] #p #IH ]

 [ <structure_empty #H0 destruct
 | <structure_d_dx #H0 /2 width=1 by/
 [ <structure_empty #H0 destruct
 | <structure_d_dx #H0 /2 width=1 by/

-| <structure_d2_dx #H0 /2 width=1 by/

 | <structure_m_dx #H0 /2 width=1 by/
 | <structure_L_dx #H0 destruct
 | <structure_A_dx #H0 destruct
 | <structure_m_dx #H0 /2 width=1 by/
 | <structure_L_dx #H0 destruct
 | <structure_A_dx #H0 destruct


@@ -157,14 +132,11 @@ qed-.
 lemma eq_inv_L_dx_structure (q) (p):
       q◖𝗟 = ⊗p →
       ∃∃r1,r2. q = ⊗r1 & 𝐞 = ⊗r2 & r1●𝗟◗r2 = p.
 lemma eq_inv_L_dx_structure (q) (p):
       q◖𝗟 = ⊗p →
       ∃∃r1,r2. q = ⊗r1 & 𝐞 = ⊗r2 & r1●𝗟◗r2 = p.

-#q #p elim p -p [| * [ #k | #k #d ] #p #IH ]
+#q #p elim p -p [| * [ #k ] #p #IH ]

 [ <structure_empty #H0 destruct
 | <structure_d_dx #H0
   elim IH -IH // -H0 #r1 #r2 #H1 #H0 #H2 destruct
   /2 width=5 by ex3_2_intro/
 [ <structure_empty #H0 destruct
 | <structure_d_dx #H0
   elim IH -IH // -H0 #r1 #r2 #H1 #H0 #H2 destruct
   /2 width=5 by ex3_2_intro/

-| <structure_d2_dx #H0
-  elim IH -IH // -H0 #r1 #r2 #H1 #H0 #H2 destruct
-  /2 width=5 by ex3_2_intro/

 | <structure_m_dx #H0
   elim IH -IH // -H0 #r1 #r2 #H1 #H0 #H2 destruct
   /2 width=5 by ex3_2_intro/
 | <structure_m_dx #H0
   elim IH -IH // -H0 #r1 #r2 #H1 #H0 #H2 destruct
   /2 width=5 by ex3_2_intro/


@@ -178,14 +150,11 @@ qed-.
 lemma eq_inv_A_dx_structure (q) (p):
       q◖𝗔 = ⊗p →
       ∃∃r1,r2. q = ⊗r1 & 𝐞 = ⊗r2 & r1●𝗔◗r2 = p.
 lemma eq_inv_A_dx_structure (q) (p):
       q◖𝗔 = ⊗p →
       ∃∃r1,r2. q = ⊗r1 & 𝐞 = ⊗r2 & r1●𝗔◗r2 = p.

-#q #p elim p -p [| * [ #k | #k #d ] #p #IH ]
+#q #p elim p -p [| * [ #k ] #p #IH ]

 [ <structure_empty #H0 destruct
 | <structure_d_dx #H0
   elim IH -IH // -H0 #r1 #r2 #H1 #H0 #H2 destruct
   /2 width=5 by ex3_2_intro/
 [ <structure_empty #H0 destruct
 | <structure_d_dx #H0
   elim IH -IH // -H0 #r1 #r2 #H1 #H0 #H2 destruct
   /2 width=5 by ex3_2_intro/

-| <structure_d2_dx #H0
-  elim IH -IH // -H0 #r1 #r2 #H1 #H0 #H2 destruct
-  /2 width=5 by ex3_2_intro/

 | <structure_m_dx #H0
   elim IH -IH // -H0 #r1 #r2 #H1 #H0 #H2 destruct
   /2 width=5 by ex3_2_intro/
 | <structure_m_dx #H0
   elim IH -IH // -H0 #r1 #r2 #H1 #H0 #H2 destruct
   /2 width=5 by ex3_2_intro/


@@ -199,14 +168,11 @@ qed-.
 lemma eq_inv_S_dx_structure (q) (p):
       q◖𝗦 = ⊗p →
       ∃∃r1,r2. q = ⊗r1 & 𝐞 = ⊗r2 & r1●𝗦◗r2 = p.
 lemma eq_inv_S_dx_structure (q) (p):
       q◖𝗦 = ⊗p →
       ∃∃r1,r2. q = ⊗r1 & 𝐞 = ⊗r2 & r1●𝗦◗r2 = p.

-#q #p elim p -p [| * [ #k | #k #d ] #p #IH ]
+#q #p elim p -p [| * [ #k ] #p #IH ]

 [ <structure_empty #H0 destruct
 | <structure_d_dx #H0
   elim IH -IH // -H0 #r1 #r2 #H1 #H0 #H2 destruct
   /2 width=5 by ex3_2_intro/
 [ <structure_empty #H0 destruct
 | <structure_d_dx #H0
   elim IH -IH // -H0 #r1 #r2 #H1 #H0 #H2 destruct
   /2 width=5 by ex3_2_intro/

-| <structure_d2_dx #H0
-  elim IH -IH // -H0 #r1 #r2 #H1 #H0 #H2 destruct
-  /2 width=5 by ex3_2_intro/

 | <structure_m_dx #H0
   elim IH -IH // -H0 #r1 #r2 #H1 #H0 #H2 destruct
   /2 width=5 by ex3_2_intro/
 | <structure_m_dx #H0
   elim IH -IH // -H0 #r1 #r2 #H1 #H0 #H2 destruct
   /2 width=5 by ex3_2_intro/


@@ -222,11 +188,10 @@ qed-.
 theorem eq_inv_append_structure (p) (q) (r):
         p●q = ⊗r →
         ∃∃r1,r2.p = ⊗r1 & q = ⊗r2 & r1●r2 = r.
 theorem eq_inv_append_structure (p) (q) (r):
         p●q = ⊗r →
         ∃∃r1,r2.p = ⊗r1 & q = ⊗r2 & r1●r2 = r.

-#p #q elim q -q [| * [ #k | #k #d ] #q #IH ] #r
+#p #q elim q -q [| * [ #k ] #q #IH ] #r

 [ <list_append_empty_sn #H0 destruct
   /2 width=5 by ex3_2_intro/
 | #H0 elim (eq_inv_d_dx_structure … H0)
 [ <list_append_empty_sn #H0 destruct
   /2 width=5 by ex3_2_intro/
 | #H0 elim (eq_inv_d_dx_structure … H0)

-| #H0 elim (eq_inv_d2_dx_structure … H0)

 | #H0 elim (eq_inv_m_dx_structure … H0)
 | #H0 elim (eq_inv_L_dx_structure … H0) -H0 #r1 #r2 #Hr1 #Hr2 #H0 destruct
   elim (IH … Hr1) -IH -Hr1 #s1 #s2 #H1 #H2 #H3 destruct
 | #H0 elim (eq_inv_m_dx_structure … H0)
 | #H0 elim (eq_inv_L_dx_structure … H0) -H0 #r1 #r2 #Hr1 #Hr2 #H0 destruct
   elim (IH … Hr1) -IH -Hr1 #s1 #s2 #H1 #H2 #H3 destruct


@@ -253,14 +218,6 @@ elim (eq_inv_append_structure … H0) -H0 #r1 #r2
 elim (eq_inv_d_dx_structure … H0)
 qed-.
 
 elim (eq_inv_d_dx_structure … H0)
 qed-.
 

-lemma eq_inv_d2_sn_structure (d) (h) (q) (p):
-      (𝗱❨h,d❩◗q) = ⊗p → ⊥.
-#d #h #q #p >list_cons_comm #H0
-elim (eq_inv_append_structure … H0) -H0 #r1 #r2
-<list_cons_comm #H0 #H1 #H2 destruct
-elim (eq_inv_d2_dx_structure … H0)
-qed-.
-

 lemma eq_inv_m_sn_structure (q) (p):
       (𝗺 ◗q) = ⊗p → ⊥.
 #q #p >list_cons_comm #H0
 lemma eq_inv_m_sn_structure (q) (p):
       (𝗺 ◗q) = ⊗p → ⊥.
 #q #p >list_cons_comm #H0

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_structure_inner.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_structure_inner.ma
index 4de1097bb0b9662c6c76d3d30912cb3cf81849af..99ed6a323f59a60e7cba2473b40d4e270ed2aca5 100644 (file)
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_structure_inner.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_structure_inner.ma
@@ -23,9 +23,8 @@ lemma structure_pic (p):
       ⊗p ϵ 𝐈.
 #p elim p -p
 [ <structure_empty //
       ⊗p ϵ 𝐈.
 #p elim p -p
 [ <structure_empty //

-| * [ #k | #k #d ] #p #IH
+| * [ #k ] #p #IH

   [ <structure_d_dx //
   [ <structure_d_dx //

-  | <structure_d2_dx //

   | <structure_m_dx //
   | <structure_L_dx //
   | <structure_A_dx //
   | <structure_m_dx //
   | <structure_L_dx //
   | <structure_A_dx //

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 8bffdb64ae0555df03894b6793f712f21b92e81a..5bb66e16ab112f1ab94db7db70cba521bc150131 100644 (file)
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm_constructors.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm_constructors.ma
@@ -16,7 +16,6 @@ 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/tau_2.ma".
 include "delayed_updating/notation/functions/m_hook_1.ma".
 include "delayed_updating/notation/functions/hash_1.ma".
 include "delayed_updating/notation/functions/tau_2.ma".

-include "delayed_updating/notation/functions/tau_3.ma".

 include "delayed_updating/notation/functions/lamda_1.ma".
 include "delayed_updating/notation/functions/at_2.ma".
 
 include "delayed_updating/notation/functions/lamda_1.ma".
 include "delayed_updating/notation/functions/at_2.ma".
 


@@ -48,10 +47,6 @@ interpretation
   "inner variable reference by depth (prototerm)"
   'Tau k t = (prototerm_node_1_2 (label_d k) label_m t).
 
   "inner variable reference by depth (prototerm)"
   'Tau k t = (prototerm_node_1_2 (label_d k) label_m t).
 

-interpretation
-  "inner variable reference by depth with offset (prototerm)"
-  'Tau k d t = (prototerm_node_1_2 (label_d2 k d) label_m t).
-

 interpretation
   "name-free functional abstraction (prototerm)"
   'Lamda t = (prototerm_node_1 label_L t).
 interpretation
   "name-free functional abstraction (prototerm)"
   'Lamda t = (prototerm_node_1 label_L t).


@@ -66,10 +61,6 @@ lemma in_comp_iref (t) (q) (k):
       q ϵ t → 𝗱k◗𝗺◗q ϵ 𝛕k.t.
 /2 width=3 by ex2_intro/ qed.
 
       q ϵ t → 𝗱k◗𝗺◗q ϵ 𝛕k.t.
 /2 width=3 by ex2_intro/ qed.
 

-lemma in_comp_iref2 (t) (q) (k) (d):
-      q ϵ t → 𝗱❨k,d❩◗𝗺◗q ϵ 𝛕❨k,d❩.t.
-/2 width=3 by ex2_intro/ qed.
-

 (* Basic inversions *********************************************************)
 
 lemma in_comp_inv_iref (t) (p) (k):
 (* Basic inversions *********************************************************)
 
 lemma in_comp_inv_iref (t) (p) (k):


@@ -79,13 +70,6 @@ lemma in_comp_inv_iref (t) (p) (k):
 /2 width=3 by ex2_intro/
 qed-.
 
 /2 width=3 by ex2_intro/
 qed-.
 

-lemma in_comp_inv_iref2 (t) (p) (k) (d):
-      p ϵ 𝛕❨k,d❩.t →
-      ∃∃q. 𝗱❨k,d❩◗𝗺◗q = p & q ϵ t.
-#t #p #k #d * #q #Hq #Hp
-/2 width=3 by ex2_intro/
-qed-.
-

 (* COMMENT
 lemma prototerm_in_root_inv_lcons_oref:
       ∀p,l,n. l◗p ϵ ▵#n →
 (* COMMENT
 lemma prototerm_in_root_inv_lcons_oref:
       ∀p,l,n. l◗p ϵ ▵#n →

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 c5a27617ab02de792f623bf197962e0a60df4a11..f7f921bcfb5ee6152efad51bfe57eefbff2ed0b0 100644 (file)
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm_proper_constructors.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm_proper_constructors.ma
@@ -23,8 +23,3 @@ lemma ppc_iref (t) (k):
       (𝛕k.t) ϵ 𝐏.
 #t #k #p * #q #Hq #H0 destruct //
 qed.
       (𝛕k.t) ϵ 𝐏.
 #t #k #p * #q #Hq #H0 destruct //
 qed.

-
-lemma ppc_iref2 (t) (k) (d):
-      (𝛕❨k,d❩.t) ϵ 𝐏.
-#t #k #d #p * #q #Hq #H0 destruct //
-qed.