From 513c4a61f11ce03888a8a0f9d8e513de6e3a7c8b Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Sun, 13 Nov 2022 23:34:18 +0100
Subject: [PATCH] update in delayed_updating
MIME-Version: 1.0
Content-Type: text/plain; charset=utf8
Content-Transfer-Encoding: 8bit

+ example of unprotected balanced β-reduction started
+ some corrections and additions
---
 .../etc/prototerm_constructors.etc            |  43 +++++++
 .../delayed_updating/reduction/dbfr_ibfr.ma   |   2 +-
 .../delayed_updating/reduction/dbfr_lift.ma   |   2 +-
 .../reduction/dbfr_unprotected.ma             |  42 +++++++
 .../delayed_updating/reduction/ibfr.ma        |   9 ++
 .../reduction/ibfr_constructors.ma            |  79 +++++++++++++
 .../substitution/fsubst_constructors.ma       | 105 ++++++++++++++++++
 .../substitution/fsubst_eq.ma                 |   9 ++
 ...tors.ma => lift_prototerm_constructors.ma} |  36 +++++-
 .../delayed_updating/syntax/prototerm.ma      |   8 +-
 .../syntax/prototerm_constructors.ma          |  90 ++++++++-------
 .../syntax/prototerm_constructors_eq.ma       |  39 +++++++
 .../delayed_updating/syntax/prototerm_eq.ma   |   7 ++
 ...s.ma => unwind2_prototerm_constructors.ma} |   4 +-
 .../unwind/unwind2_rmap_unprotected.ma        |  18 +--
 15 files changed, 437 insertions(+), 56 deletions(-)
 create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/etc/prototerm_constructors.etc
 create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr_unprotected.ma
 create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/reduction/ibfr_constructors.ma
 create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/substitution/fsubst_constructors.ma
 rename matita/matita/contribs/lambdadelta/delayed_updating/substitution/{lift_constructors.ma => lift_prototerm_constructors.ma} (67%)
 rename matita/matita/contribs/lambdadelta/delayed_updating/unwind/{unwind2_constructors.ma => unwind2_prototerm_constructors.ma} (95%)

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/etc/prototerm_constructors.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/prototerm_constructors.etc
new file mode 100644
index 000000000..a3e29bd4e
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/etc/prototerm_constructors.etc
@@ -0,0 +1,43 @@
+(* COMMENT
+lemma prototerm_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 prototerm_in_root_inv_lcons_iref:
+      ∀t,p,l,n. l◗p ϵ ▵𝛕n.t →
+      ∧∧ 𝗱n = l & p ϵ ▵ɱ.t.
+#t #p #l #n * #q * #r #Hr
+<list_append_lcons_sn #H0 destruct -H0
+/4 width=4 by ex2_intro, ex_intro, conj/
+qed-.
+
+lemma prototerm_in_root_inv_lcons_mark:
+      ∀t,p,l. l◗p ϵ ▵ɱ.t →
+      ∧∧ 𝗺 = l & p ϵ ▵t.
+#t #p #l * #q * #r #Hr
+<list_append_lcons_sn #H0 destruct
+/3 width=2 by ex_intro, conj/
+qed-.
+
+lemma prototerm_in_root_inv_lcons_abst:
+      ∀t,p,l. l◗p ϵ ▵𝛌.t →
+      ∧∧ 𝗟 = l & p ϵ ▵t.
+#t #p #l * #q * #r #Hr
+<list_append_lcons_sn #H0 destruct
+/3 width=2 by ex_intro, conj/
+qed-.
+
+lemma prototerm_in_root_inv_lcons_appl:
+      ∀u,t,p,l. l◗p ϵ ▵@u.t →
+      ∨∨ ∧∧ 𝗦 = l & p ϵ ▵u
+       | ∧∧ 𝗔 = l & p ϵ ▵t.
+#u #t #p #l * #q * * #r #Hr
+<list_append_lcons_sn #H0 destruct
+/4 width=2 by ex_intro, or_introl, or_intror, conj/
+qed-.
+*)
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr_ibfr.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr_ibfr.ma
index eee619916..35966d9f7 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr_ibfr.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr_ibfr.ma
@@ -15,7 +15,7 @@
 include "delayed_updating/reduction/dbfr.ma".
 include "delayed_updating/reduction/ibfr.ma".
 
-include "delayed_updating/unwind/unwind2_constructors.ma".
+include "delayed_updating/unwind/unwind2_prototerm_constructors.ma".
 include "delayed_updating/unwind/unwind2_preterm_fsubst.ma".
 include "delayed_updating/unwind/unwind2_preterm_eq.ma".
 include "delayed_updating/unwind/unwind2_prototerm_lift.ma".
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr_lift.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr_lift.ma
index fc67c5779..0c6ab932f 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr_lift.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr_lift.ma
@@ -16,7 +16,7 @@ include "delayed_updating/reduction/dbfr.ma".
 
 include "delayed_updating/substitution/fsubst_lift.ma".
 include "delayed_updating/substitution/fsubst_eq.ma".
-include "delayed_updating/substitution/lift_constructors.ma".
+include "delayed_updating/substitution/lift_prototerm_constructors.ma".
 include "delayed_updating/substitution/lift_path_structure.ma".
 include "delayed_updating/substitution/lift_path_closed.ma".
 include "delayed_updating/substitution/lift_rmap_closed.ma".
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr_unprotected.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr_unprotected.ma
new file mode 100644
index 000000000..a0e5a6944
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr_unprotected.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/reduction/ibfr_constructors.ma".
+include "delayed_updating/substitution/lift_prototerm_constructors.ma".
+include "ground/arith/pnat_two.ma".
+
+(* DELAYED BALANCED FOCUSED REDUCTION ***************************************)
+
+(* Example of unprotected balanced β-reduction ******************************)
+
+definition l3_t0: prototerm ≝
+           (𝛌.＠(⧣𝟏).＠(𝛌.＠(⧣𝟐).⧣𝟏).𝛌.⧣𝟏).
+
+definition l3_t1: prototerm ≝
+           (𝛌.＠(⧣𝟏).＠(𝛌.＠(⧣𝟐).⧣𝟏).𝛌.(𝛌.＠(⧣↑𝟐).⧣𝟏)).
+
+lemma l3_t01:
+      l3_t0 ➡𝐢𝐛𝐟[𝗟◗𝗔◗𝗔◗𝗟◗𝐞] l3_t1.
+@ibfr_abst_hd
+@ibfr_appl_hd
+@ibfr_eq_trans [| @ibfr_beta_0 // ]
+@appl_eq_repl [ // ]
+@abst_eq_repl
+@(subset_eq_canc_sn … (fsubst_empty_rc …))
+@(subset_eq_canc_sn … (lift_term_abst …))
+@abst_eq_repl
+@(subset_eq_canc_sn … (lift_term_appl … ))
+@appl_eq_repl
+@(subset_eq_canc_sn … (lift_term_oref_pap … )) //
+qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ibfr.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ibfr.ma
index 869ad5754..90b16d3de 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ibfr.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ibfr.ma
@@ -35,3 +35,12 @@ definition ibfr (r): relation2 prototerm prototerm ≝
 interpretation
   "balanced focused reduction with immediate updating (prototerm)"
   'BlackRightArrowIBF t1 r t2 = (ibfr r t1 t2).
+
+(* Constructions with subset_equivalence ************************************)
+
+lemma ibfr_eq_trans (t) (t1) (t2) (r):
+      t1 ➡𝐢𝐛𝐟[r] t → t ⇔ t2 → t1 ➡𝐢𝐛𝐟[r] t2.
+#t #t1 #t2 #r
+* #p #b #q #m #n #Hr #Hb #Hm #Hn #Ht1 #Ht #Ht2
+/3 width=13 by subset_eq_trans, ex6_5_intro/
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ibfr_constructors.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ibfr_constructors.ma
new file mode 100644
index 000000000..2a98609ad
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ibfr_constructors.ma
@@ -0,0 +1,79 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/reduction/ibfr.ma".
+include "delayed_updating/substitution/fsubst_constructors.ma".
+include "delayed_updating/substitution/fsubst_eq.ma".
+include "delayed_updating/substitution/lift_prototerm_eq.ma".
+include "delayed_updating/syntax/prototerm_constructors_eq.ma".
+
+(* IMMEDIATE BALANCED FOCUSED REDUCTION *************************************)
+
+(* Constructions with constructors for prototerm ****************************)
+
+lemma ibfr_abst_hd (t1) (t2) (r):
+      t1 ➡𝐢𝐛𝐟[r] t2 → 𝛌.t1 ➡𝐢𝐛𝐟[𝗟◗r] 𝛌.t2.
+#t1 #t2 #r *
+#p #b #q #m #n #Hr #Hb #Hm #Hn #Ht1 #Ht2 destruct
+@(ex6_5_intro … (𝗟◗p) … Hb Hm Hn) -Hb -Hm -Hn
+[ -Ht2 //
+| -Ht2 /2 width=1 by in_comp_abst_hd/
+| @(subset_eq_trans … (abst_eq_repl … Ht2)) -Ht1 -Ht2
+  @(subset_eq_canc_sn … (fsubst_abst_hd …)) @abst_eq_repl
+  @fsubst_eq_repl // @lift_term_eq_repl_dx
+  >list_cons_shift @(subset_eq_canc_sn … (grafted_abst_hd … )) //
+]
+qed.
+
+lemma ibfr_appl_hd (v) (t1) (t2) (r):
+      t1 ➡𝐢𝐛𝐟[r] t2 → ＠v.t1 ➡𝐢𝐛𝐟[𝗔◗r] ＠v.t2.
+#v #t1 #t2 #r *
+#p #b #q #m #n #Hr #Hb #Hm #Hn #Ht1 #Ht2 destruct
+@(ex6_5_intro … (𝗔◗p) … Hb Hm Hn) -Hb -Hm -Hn
+[ -Ht2 //
+| -Ht2 /2 width=1 by in_comp_appl_hd/
+| @(subset_eq_trans … (appl_eq_repl … Ht2)) -Ht1 -Ht2 [|*: // ]
+  @(subset_eq_canc_sn … (fsubst_appl_hd …)) @appl_eq_repl [ // ]
+  @fsubst_eq_repl // @lift_term_eq_repl_dx
+  >list_cons_shift @(subset_eq_canc_sn … (grafted_appl_hd … )) //
+]
+qed.
+
+lemma ibfr_appl_sd (v1) (v2) (t) (r):
+      v1 ➡𝐢𝐛𝐟[r] v2 → ＠v1.t ➡𝐢𝐛𝐟[𝗦◗r] ＠v2.t.
+#v1 #v2 #t #r *
+#p #b #q #m #n #Hr #Hb #Hm #Hn #Hv1 #Hv2 destruct
+@(ex6_5_intro … (𝗦◗p) … Hb Hm Hn) -Hb -Hm -Hn
+[ -Hv2 //
+| -Hv2 /2 width=1 by in_comp_appl_sd/
+| @(subset_eq_trans ????? (appl_eq_repl …)) [3: @Hv2 |2,4: // |5: skip ]
+  @(subset_eq_canc_sn … (fsubst_appl_sd …)) @appl_eq_repl [| // ]
+  @fsubst_eq_repl // @lift_term_eq_repl_dx
+  >list_cons_shift @(subset_eq_canc_sn … (grafted_appl_sd … )) //
+]
+qed.
+
+lemma ibfr_beta_0 (v) (t) (q) (n):
+      q ϵ 𝐂❨Ⓕ,n❩ → q◖𝗱↑n ϵ t →
+      ＠v.𝛌.t ➡𝐢𝐛𝐟[𝗔◗𝗟◗q] ＠v.𝛌.(t[⋔q←🠡[𝐮❨↑n❩]v]).
+#v #t #q #n #Hn #Ht
+@(ex6_5_intro … (𝐞) (𝐞) q (𝟎) … Hn) -Hn //
+[ /3 width=1 by in_comp_appl_hd, in_comp_abst_hd/
+| @(subset_eq_canc_sn … (fsubst_appl_hd …)) @appl_eq_repl [ // ]
+  @(subset_eq_canc_sn … (fsubst_abst_hd …)) @abst_eq_repl
+  @fsubst_eq_repl // <nplus_zero_sn @lift_term_eq_repl_dx
+  >list_cons_comm @(subset_eq_canc_sn … (grafted_appl_sd … ))
+  @(subset_eq_canc_sn … (grafted_empty_dx … )) //
+]
+qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/fsubst_constructors.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/fsubst_constructors.ma
new file mode 100644
index 000000000..7d69778c0
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/fsubst_constructors.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 "delayed_updating/substitution/fsubst.ma".
+include "delayed_updating/syntax/prototerm_constructors.ma".
+include "ground/lib/subset_equivalence.ma".
+
+(* FOCALIZED SUBSTITUTION ***************************************************)
+
+(* Constructions with constructors for prototerm ****************************)
+
+lemma fsubst_abst_hd (t) (u) (p):
+      𝛌.(t[⋔p←u]) ⇔ (𝛌.t)[⋔𝗟◗p←u].
+#t #u #p @conj #r
+[ #Hr
+  elim (in_comp_inv_abst … Hr) -Hr #s #H0 * *
+  [ #q #Hq #H1 destruct
+    /3 width=3 by ex2_intro, or_introl/
+  | #H1s #H2s destruct
+    @or_intror @conj
+    [ /2 width=1 by in_comp_abst_hd/ ]
+    #s0 <list_append_rcons_dx #Hs0
+    elim (eq_inv_list_rcons_bi ????? Hs0) -Hs0 #H1 #H2 destruct
+    /2 width=2 by/
+  ]
+| * *
+  [ #q #Hq #H0 destruct
+    /4 width=3 by in_comp_abst_hd, ex2_intro, or_introl/
+  | #H1r #H2r
+    elim (in_comp_inv_abst … H1r) -H1r #s #H0 #Hs destruct
+    /5 width=2 by in_comp_abst_hd, conj, or_intror/
+  ]
+]
+qed.
+
+lemma fsubst_appl_sd (v) (t) (u) (p):
+      ＠v[⋔p←u].t ⇔ (＠v.t)[⋔𝗦◗p←u].
+#v #t #u #p @conj #r
+[ #Hr
+  elim (in_comp_inv_appl … Hr) -Hr * #s #H0
+  [ * *
+    [ #q #Hq #H1 destruct
+      /3 width=3 by ex2_intro, or_introl/
+    | #H1s #H2s destruct
+      @or_intror @conj
+      [ /2 width=1 by in_comp_appl_sd/ ]
+      #s0 <list_append_rcons_dx #Hs0
+      elim (eq_inv_list_rcons_bi ????? Hs0) -Hs0 #H1 #H2 destruct
+      /2 width=2 by/
+    ]
+  | #Hs destruct
+    @or_intror @conj [ /2 width=1 by in_comp_appl_hd/ ]
+    #r <list_append_rcons_dx #H0
+    elim (eq_inv_list_rcons_bi ????? H0) -H0 #H1 #H2 destruct
+  ]
+| * *
+  [ #q #Hq #H0 destruct
+    /4 width=3 by in_comp_appl_sd, ex2_intro, or_introl/
+  | #H1r #H2r
+    elim (in_comp_inv_appl … H1r) -H1r * #s #H0 #Hs destruct
+    /5 width=2 by in_comp_appl_hd, in_comp_appl_sd, or_intror, conj/
+  ]
+]
+qed.
+
+lemma fsubst_appl_hd (v) (t) (u) (p):
+      ＠v.(t[⋔p←u]) ⇔ (＠v.t)[⋔𝗔◗p←u].
+#v #t #u #p @conj #r
+[ #Hr
+  elim (in_comp_inv_appl … Hr) -Hr * #s #H0
+  [ #Hs destruct
+    @or_intror @conj [ /2 width=1 by in_comp_appl_sd/ ]
+    #r <list_append_rcons_dx #H0
+    elim (eq_inv_list_rcons_bi ????? H0) -H0 #H1 #H2 destruct
+  | * *
+    [ #q #Hq #H1 destruct
+      /3 width=3 by ex2_intro, or_introl/
+    | #H1s #H2s destruct
+      @or_intror @conj
+      [ /2 width=1 by in_comp_appl_hd/ ]
+      #s0 <list_append_rcons_dx #Hs0
+      elim (eq_inv_list_rcons_bi ????? Hs0) -Hs0 #H1 #H2 destruct
+      /2 width=2 by/
+    ]
+  ]
+| * *
+  [ #q #Hq #H0 destruct
+    /4 width=3 by in_comp_appl_hd, ex2_intro, or_introl/
+  | #H1r #H2r
+    elim (in_comp_inv_appl … H1r) -H1r * #s #H0 #Hs destruct
+    /5 width=2 by in_comp_appl_hd, in_comp_appl_sd, or_intror, conj/
+  ]
+]
+qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/fsubst_eq.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/fsubst_eq.ma
index c3f6cfa11..c3a985716 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/fsubst_eq.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/fsubst_eq.ma
@@ -19,6 +19,15 @@ include "delayed_updating/syntax/prototerm_eq.ma".
 
 (* Constructions with subset_equivalence ************************************)
 
+lemma fsubst_empty_rc (t) (u):
+      u ⇔ t[⋔𝐞←u].
+#t #u @conj #p
+[ #Hp /3 width=3 by or_introl, ex2_intro/ ]
+* *
+[ #r #Hr #H0 destruct // ]
+#H1p #H2p elim H2p -H2p //
+qed.
+
 lemma subset_inclusion_fsubst_bi (t1) (t2) (u1) (u2) (p):
       t1 ⊆ t2 → u1 ⊆ u2 → t1[⋔p←u1] ⊆ t2[⋔p←u2].
 #t1 #t2 #u1 #u2 #p #Ht #Hu #q * *
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_constructors.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_prototerm_constructors.ma
similarity index 67%
rename from matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_constructors.ma
rename to matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_prototerm_constructors.ma
index 56f7b178a..8ed0399b9 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_constructors.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_prototerm_constructors.ma
@@ -19,11 +19,21 @@ include "ground/relocation/nap.ma".
 
 (* LIFT FOR PROTOTERM *******************************************************)
 
+(* Constructions with constructors for prototerm ****************************)
+
+lemma lift_term_oref_pap (f) (k):
+      (⧣(f＠⧣❨k❩)) ⇔ 🠡[f]⧣k.
+#f #k @conj #p *
+[ /2 width=1 by in_comp_lift_path_term/
+| #q * #H0 destruct //
+]
+qed.
+
 lemma lift_term_iref_pap_sn (f) (t:prototerm) (k:pnat):
       (𝛕f＠⧣❨k❩.🠡[⇂*[k]f]t) ⊆ 🠡[f](𝛕k.t).
 #f #t #k #p * #q * #r #Hr #H1 #H2 destruct
 @(ex2_intro … (𝗱k◗𝗺◗r))
-/2 width=1 by in_comp_iref/
+/2 width=1 by in_comp_iref_hd/
 qed-.
 
 lemma lift_term_iref_pap_dx (f) (t) (k:pnat):
@@ -31,7 +41,7 @@ lemma lift_term_iref_pap_dx (f) (t) (k:pnat):
 #f #t #k #p * #q #Hq #H0 destruct
 elim (in_comp_inv_iref … Hq) -Hq #p #H0 #Hp destruct
 <lift_path_d_sn <lift_path_m_sn
-/3 width=1 by in_comp_iref, in_comp_lift_path_term/
+/3 width=1 by in_comp_iref_hd, in_comp_lift_path_term/
 qed-.
 
 lemma lift_term_iref_pap (f) (t) (k:pnat):
@@ -52,3 +62,25 @@ lemma lift_term_iref_uni (t) (n) (k):
 <tr_uni_pap >nsucc_pnpred <tr_tls_succ_uni
 /3 width=1 by iref_eq_repl, lift_term_id/
 qed.
+
+lemma lift_term_abst (f) (t):
+      (𝛌.🠡[⫯f]t) ⇔ 🠡[f]𝛌.t.
+#f #t @conj #p #Hp
+[ elim (in_comp_inv_abst … Hp) -Hp #q #H1 * #r #Hr #H2 destruct
+  /3 width=1 by in_comp_lift_path_term, in_comp_abst_hd/
+| elim Hp -Hp #q #Hq #H0 destruct
+  elim (in_comp_inv_abst … Hq) -Hq #r #H0 #Hr destruct 
+  /3 width=1 by in_comp_lift_path_term, in_comp_abst_hd/
+]
+qed.
+
+lemma lift_term_appl (f) (v) (t):
+      ＠🠡[f]v.🠡[f]t ⇔ 🠡[f]＠v.t.
+#f #v #t @conj #p #Hp
+[ elim (in_comp_inv_appl … Hp) -Hp * #q #H1 * #r #Hr #H2 destruct
+  /3 width=1 by in_comp_lift_path_term, in_comp_appl_sd, in_comp_appl_hd/
+| elim Hp -Hp #q #Hq #H0 destruct
+  elim (in_comp_inv_appl … Hq) -Hq * #r #H0 #Hr destruct 
+  /3 width=1 by in_comp_lift_path_term, in_comp_appl_sd, in_comp_appl_hd/
+]
+qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm.ma
index 30a2770e2..be3b82e04 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm.ma
@@ -30,12 +30,18 @@ interpretation
   'Pitchfork t p = (prototerm_grafted p t).
 
 definition prototerm_root: prototerm → prototerm ≝
-           λt,q. ∃r. q●r ϵ t.
+           λt,q. ∃r. r ϵ t⋔q.
 
 interpretation
   "root (prototerm)"
   'UpTriangle t = (prototerm_root t).
 
+(* Basic inversions *********************************************************)
+
+lemma prototerm_grafted_inv_gen (t) (p) (q):
+      q ϵ t⋔p → p●q ϵ t.
+// qed-.
+
 (* Basic constructions ******************************************************)
 
 lemma prototerm_in_comp_root (p) (t):
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 5bb66e16a..f2526c2f6 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm_constructors.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm_constructors.ma
@@ -57,10 +57,26 @@ interpretation
 
 (* Basic constructions *******************************************************)
 
-lemma in_comp_iref (t) (q) (k):
+lemma in_comp_oref_hd (k):
+      (𝗱k◗𝐞) ϵ ⧣k.
+// qed.
+
+lemma in_comp_iref_hd (t) (q) (k):
       q ϵ t → 𝗱k◗𝗺◗q ϵ 𝛕k.t.
 /2 width=3 by ex2_intro/ qed.
 
+lemma in_comp_abst_hd (t) (q):
+      q ϵ t → 𝗟◗q ϵ 𝛌.t.
+/2 width=3 by ex2_intro/ qed.
+
+lemma in_comp_appl_sd (u) (t) (q):
+      q ϵ u → 𝗦◗q ϵ ＠u.t.
+/3 width=3 by ex2_intro, or_introl/ qed.
+
+lemma in_comp_appl_hd (u) (t) (q):
+      q ϵ t → 𝗔◗q ϵ ＠u.t.
+/3 width=3 by ex2_intro, or_intror/ qed.
+
 (* Basic inversions *********************************************************)
 
 lemma in_comp_inv_iref (t) (p) (k):
@@ -70,46 +86,40 @@ lemma in_comp_inv_iref (t) (p) (k):
 /2 width=3 by ex2_intro/
 qed-.
 
-(* COMMENT
-lemma prototerm_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 prototerm_in_root_inv_lcons_iref:
-      ∀t,p,l,n. l◗p ϵ ▵𝛕n.t →
-      ∧∧ 𝗱n = l & p ϵ ▵ɱ.t.
-#t #p #l #n * #q * #r #Hr
-<list_append_lcons_sn #H0 destruct -H0
-/4 width=4 by ex2_intro, ex_intro, conj/
-qed-.
-
-lemma prototerm_in_root_inv_lcons_mark:
-      ∀t,p,l. l◗p ϵ ▵ɱ.t →
-      ∧∧ 𝗺 = l & p ϵ ▵t.
-#t #p #l * #q * #r #Hr
-<list_append_lcons_sn #H0 destruct
-/3 width=2 by ex_intro, conj/
+lemma in_comp_inv_abst (t) (p):
+      p ϵ 𝛌.t →
+      ∃∃q. 𝗟◗q = p & q ϵ t.
+#t #p * #q #Hq #Hp
+/2 width=3 by ex2_intro/
 qed-.
 
-lemma prototerm_in_root_inv_lcons_abst:
-      ∀t,p,l. l◗p ϵ ▵𝛌.t →
-      ∧∧ 𝗟 = l & p ϵ ▵t.
-#t #p #l * #q * #r #Hr
-<list_append_lcons_sn #H0 destruct
-/3 width=2 by ex_intro, conj/
+lemma in_comp_inv_appl (u) (t) (p):
+      p ϵ ＠u.t →
+      ∨∨ ∃∃q. 𝗦◗q = p & q ϵ u
+       | ∃∃q. 𝗔◗q = p & q ϵ t.
+#u #t #p * * #q #Hq #Hp
+/3 width=3 by ex2_intro, or_introl, or_intror/
 qed-.
 
-lemma prototerm_in_root_inv_lcons_appl:
-      ∀u,t,p,l. l◗p ϵ ▵@u.t →
-      ∨∨ ∧∧ 𝗦 = l & p ϵ ▵u
-       | ∧∧ 𝗔 = l & p ϵ ▵t.
-#u #t #p #l * #q * * #r #Hr
-<list_append_lcons_sn #H0 destruct
-/4 width=2 by ex_intro, or_introl, or_intror, conj/
-qed-.
-*)
+(* Advanced inversions ******************************************************)
+
+lemma in_comp_inv_abst_hd (t) (p):
+      (𝗟◗p) ϵ 𝛌.t → p ϵ t.
+#t #p #H0
+elim (in_comp_inv_abst … H0) -H0 #q #H0 #Hq
+elim (eq_inv_list_rcons_bi ????? H0) -H0 #H1 #H2 destruct //
+qed-. 
+
+lemma in_comp_inv_appl_sd (u) (t) (p):
+      (𝗦◗p) ϵ ＠u.t → p ϵ u.
+#u #t #p #H0
+elim (in_comp_inv_appl … H0) -H0 * #q #H0 #Hq
+elim (eq_inv_list_rcons_bi ????? H0) -H0 #H1 #H2 destruct //
+qed-. 
+
+lemma in_comp_inv_appl_hd (u) (t) (p):
+      (𝗔◗p) ϵ ＠u.t → p ϵ t.
+#u #t #p #H0
+elim (in_comp_inv_appl … H0) -H0 * #q #H0 #Hq
+elim (eq_inv_list_rcons_bi ????? H0) -H0 #H1 #H2 destruct //
+qed-. 
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm_constructors_eq.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm_constructors_eq.ma
index 4a83b790e..c99cb5775 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm_constructors_eq.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm_constructors_eq.ma
@@ -23,3 +23,42 @@ lemma iref_eq_repl (t1) (t2) (k):
       t1 ⇔ t2 → 𝛕k.t1 ⇔ 𝛕k.t2.
 /2 width=1 by subset_equivalence_ext_f1_bi/
 qed.
+
+lemma abst_eq_repl (t1) (t2):
+      t1 ⇔ t2 → 𝛌.t1 ⇔ 𝛌.t2.
+/2 width=1 by subset_equivalence_ext_f1_bi/
+qed.
+
+lemma appl_eq_repl (u1) (u2) (t1) (t2):
+      u1 ⇔ u2 → t1 ⇔ t2 → ＠u1.t1 ⇔ ＠u2.t2.
+/2 width=1 by subset_equivalence_ext_f1_1_bi/
+qed.
+
+(* Constructions with prototerm_grafted *************************************)
+
+lemma grafted_abst_hd (t) (p):
+      t⋔p ⇔ (𝛌.t)⋔(𝗟◗p).
+#t #p @conj #r #Hr
+[ /2 width=3 by ex2_intro/
+| lapply (prototerm_grafted_inv_gen … Hr) -Hr
+  /2 width=1 by in_comp_inv_abst_hd/
+]
+qed.
+
+lemma grafted_appl_sd (v) (t) (p):
+      v⋔p ⇔ (＠v.t)⋔(𝗦◗p).
+#v #t #p @conj #r #Hr
+[ /3 width=3 by ex2_intro, or_introl/
+| lapply (prototerm_grafted_inv_gen … Hr) -Hr
+  /2 width=2 by in_comp_inv_appl_sd/
+]
+qed.
+
+lemma grafted_appl_hd (v) (t) (p):
+      t⋔p ⇔ (＠v.t)⋔(𝗔◗p).
+#v #t #p @conj #r #Hr
+[ /3 width=3 by ex2_intro, or_intror/
+| lapply (prototerm_grafted_inv_gen … Hr) -Hr
+  /2 width=2 by in_comp_inv_appl_hd/
+]
+qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm_eq.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm_eq.ma
index baffe070a..5604578e5 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm_eq.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm_eq.ma
@@ -17,6 +17,13 @@ include "ground/lib/subset_equivalence.ma".
 
 (* EQUIVALENCE FOR PROTOTERM ************************************************)
 
+(* Constructions with prototerm_grafted *************************************)
+
+lemma grafted_empty_dx (t):
+      t ⇔ t⋔𝐞.
+/2 width=1 by conj/
+qed.
+
 (* Constructions with prototerm_root ****************************************)
 
 lemma prototerm_root_incl_repl:
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_constructors.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_prototerm_constructors.ma
similarity index 95%
rename from matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_constructors.ma
rename to matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_prototerm_constructors.ma
index 35fa984b5..96fc1d02e 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_constructors.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_prototerm_constructors.ma
@@ -18,13 +18,13 @@ include "delayed_updating/syntax/prototerm_constructors.ma".
 
 (* TAILED UNWIND FOR PROTOTERM **********************************************)
 
-(* Constructions with constructors ******************************************)
+(* Constructions with constructors for prototerm ****************************)
 
 lemma unwind2_term_iref_sn (f) (t) (k:pnat):
       ▼[f∘𝐮❨k❩]t ⊆ ▼[f](𝛕k.t).
 #f #t #k #p * #q #Hq #H0 destruct
 @(ex2_intro … (𝗱k◗𝗺◗q))
-/2 width=1 by in_comp_iref/
+/2 width=1 by in_comp_iref_hd/
 qed-.
 
 lemma unwind2_term_iref_dx (f) (t) (k:pnat):
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_unprotected.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_unprotected.ma
index b8cb1d2cf..df93a6709 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_unprotected.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_unprotected.ma
@@ -20,24 +20,24 @@ include "delayed_updating/syntax/path_structure.ma".
 
 (* Example of unprotected balanced path *************************************)
 
-definition b: path ≝ 𝐞◖𝗔◖𝗟◖𝗱𝟏.
+definition l3_b: path ≝ 𝐞◖𝗔◖𝗟◖𝗱𝟏.
 
-lemma b_unfold: 𝐞◖𝗔◖𝗟◖𝗱𝟏 = b.
+lemma l3_b_unfold: 𝐞◖𝗔◖𝗟◖𝗱𝟏 = l3_b.
 // qed.
 
-lemma b_balanced: ⊗b ϵ 𝐁.
-<b_unfold <structure_d_dx
+lemma l3_b_balanced: ⊗l3_b ϵ 𝐁.
+<l3_b_unfold <structure_d_dx
 /2 width=1 by pbc_empty, pbc_redex/
 qed.
 
-lemma b_closed: b ϵ 𝐂❨Ⓕ,𝟎❩.
+lemma l3_b_closed: l3_b ϵ 𝐂❨Ⓕ,𝟎❩.
 /4 width=1 by pcc_A_sn, pcc_empty, pcc_false_d_dx, pcc_L_dx/
 qed.
 
-lemma b_unwind2_rmap_unfold (f):
-      (⫯f)∘𝐮❨𝟏❩ = ▶[f]b.
+lemma l3_b_unwind2_rmap_unfold (f):
+      (⫯f)∘𝐮❨𝟏❩ = ▶[f]l3_b.
 // qed.
 
-lemma b_unwind2_rmap_pap_unit (f):
-      ↑(f＠⧣❨𝟏❩) = ▶[f]b＠⧣❨𝟏❩.
+lemma l3_b_unwind2_rmap_pap_unit (f):
+      ↑(f＠⧣❨𝟏❩) = ▶[f]l3_b＠⧣❨𝟏❩.
 // qed.
-- 
2.39.2