update in delayd_updating

+ introduction of path_closed complete

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/etc/head/unwind2_rmap_head.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/head/unwind2_rmap_head.etc
new file mode 100644 (file)
index 0000000..416c6e7
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/etc/head/unwind2_rmap_head.etc
@@ -0,0 +1,134 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/unwind/unwind2_rmap_labels.ma".
+include "delayed_updating/unwind/unwind2_rmap_eq.ma".
+include "delayed_updating/syntax/path_head_depth.ma".
+include "ground/relocation/xap.ma".
+include "ground/lib/stream_eq_eq.ma".
+include "ground/arith/nat_le_plus.ma".
+
+(* TAILED UNWIND FOR RELOCATION MAP *****************************************)
+
+(* Constructions with path_head *********************************************)
+
+lemma unwind2_rmap_head_xap_le_closed (f) (p) (q) (n) (m):
+      q = ↳[n]q → m ≤ n →
+      ▶[f](p●q)＠❨m❩ = ▶[f]↳[n](p●q)＠❨m❩.
+#f #p #q elim q -q
+[ #n #m #Hq
+  <(eq_inv_path_empty_head … Hq) -n #Hm
+  <(nle_inv_zero_dx … Hm) -m //
+| #l #q #IH #n @(nat_ind_succ … n) -n
+  [ #m #_ #Hm <(nle_inv_zero_dx … Hm) -m -IH //
+  | #n #_ #m cases l [ #k ]
+    [ <path_head_d_dx #Hq #Hm
+      elim (eq_inv_list_lcons_bi ????? Hq) -Hq #_ #Hq
+      <unwind2_rmap_d_dx <unwind2_rmap_d_dx
+      <tr_compose_xap <tr_compose_xap
+      @(IH … Hq) -IH -Hq (**) (* auto too slow *)
+      @nle_trans [| @tr_uni_xap ]
+      /2 width=1 by nle_plus_bi_dx/
+    | <path_head_m_dx #Hq #Hm
+      elim (eq_inv_list_lcons_bi ????? Hq) -Hq #_ #Hq
+      <unwind2_rmap_m_dx <unwind2_rmap_m_dx
+      /2 width=2 by/
+    | <path_head_L_dx #Hq
+      @(nat_ind_succ … m) -m // #m #_ #Hm
+      lapply (nle_inv_succ_bi … Hm) -Hm #Hm
+      elim (eq_inv_list_lcons_bi ????? Hq) -Hq #_ #Hq
+      <unwind2_rmap_L_dx <unwind2_rmap_L_dx
+      <tr_xap_push <tr_xap_push
+      /3 width=2 by eq_f/
+    | <path_head_A_dx #Hq #Hm
+      elim (eq_inv_list_lcons_bi ????? Hq) -Hq #_ #Hq
+      <unwind2_rmap_A_dx <unwind2_rmap_A_dx
+      /2 width=2 by/
+    | <path_head_S_dx #Hq #Hm
+      elim (eq_inv_list_lcons_bi ????? Hq) -Hq #_ #Hq
+      <unwind2_rmap_S_dx <unwind2_rmap_S_dx
+      /2 width=2 by/
+    ]
+  ]
+]
+qed-.
+
+lemma unwind2_rmap_head_xap_closed (f) (p) (q) (n):
+      q = ↳[n]q →
+      ▶[f](p●q)＠❨n❩ = ▶[f]↳[n](p●q)＠❨n❩.
+/2 width=2 by unwind2_rmap_head_xap_le_closed/
+qed-.
+
+lemma unwind2_rmap_head_xap (f) (p) (n):
+      n + ♯(↳[n]p) = (▶[f]↳[n]p)＠❨n❩.
+#f #p elim p -p
+[ #n <path_head_empty <unwind2_rmap_labels_L <height_labels_L
+  <tr_xap_pushs_le //
+| #l #p #IH #n @(nat_ind_succ … n) -n //
+  #n #_ cases l [ #k ]
+  [ <unwind2_rmap_d_dx <path_head_d_dx <height_d_dx
+    <nplus_comm in ⊢ (??(??%)?); <nplus_assoc
+    >IH -IH <tr_compose_xap <tr_uni_xap_succ //
+  | <unwind2_rmap_m_dx <path_head_m_dx <height_m_dx //
+  | <unwind2_rmap_L_dx <path_head_L_dx <height_L_dx
+    <tr_xap_push <npred_succ <nplus_succ_sn //
+  | <unwind2_rmap_A_dx <path_head_A_dx <height_A_dx //
+  | <unwind2_rmap_S_dx <path_head_S_dx <height_S_dx //
+  ]
+]
+qed.
+
+lemma unwind2_rmap_append_pap_closed (f) (p) (q) (h:pnat):
+      q = ↳[h]q →
+      ♭q = ninj (▶[f](p●q)＠⧣❨h❩).
+#f #p #q #h #Hh
+>tr_xap_ninj >(path_head_refl_append_sn p … Hh) in ⊢ (??%?);
+>(unwind2_rmap_head_xap_closed … Hh) -Hh
+<path_head_depth //
+qed.
+
+lemma tls_unwind2_rmap_plus_closed (f) (p) (q) (n) (m):
+      q = ↳[n]q →
+      ⇂*[m]▶[f]p ≗ ⇂*[n+m]▶[f](p●q).
+#f #p #q elim q -q
+[ #n #m #Hq
+  <(eq_inv_path_empty_head … Hq) -n //
+| #l #q #IH #n @(nat_ind_succ … n) -n //
+  #n #_ #m cases l [ #k ]
+  [ <path_head_d_dx #Hq
+    elim (eq_inv_list_lcons_bi ????? Hq) -Hq #_ #Hq <nrplus_inj_sn
+    @(stream_eq_trans … (tls_unwind2_rmap_d_dx …))
+    >nrplus_inj_dx >nrplus_inj_sn >nrplus_inj_sn <nplus_plus_comm_23
+    /2 width=1 by/
+  | <path_head_m_dx #Hq
+    elim (eq_inv_list_lcons_bi ????? Hq) -Hq #_ #Hq
+    <unwind2_rmap_m_sn /2 width=1 by/
+  | <path_head_L_dx #Hq
+    elim (eq_inv_list_lcons_bi ????? Hq) -Hq #_ #Hq
+    <unwind2_rmap_L_dx <nplus_succ_sn /2 width=1 by/
+  | <path_head_A_dx #Hq
+    elim (eq_inv_list_lcons_bi ????? Hq) -Hq #_ #Hq
+    <unwind2_rmap_A_dx /2 width=2 by/
+  | <path_head_S_dx #Hq
+    elim (eq_inv_list_lcons_bi ????? Hq) -Hq #_ #Hq
+    <unwind2_rmap_S_dx /2 width=2 by/
+  ]
+]
+qed-.
+
+lemma tls_unwind2_rmap_closed (f) (p) (q) (n):
+      q = ↳[n]q →
+      ▶[f]p ≗ ⇂*[n]▶[f](p●q).
+/2 width=1 by tls_unwind2_rmap_plus_closed/
+qed.

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/etc/head/unwind2_rmap_labels.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/head/unwind2_rmap_labels.etc
new file mode 100644 (file)
index 0000000..d139018
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/etc/head/unwind2_rmap_labels.etc
@@ -0,0 +1,28 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/unwind/unwind2_rmap.ma".
+include "delayed_updating/syntax/path_labels.ma".
+include "ground/relocation/tr_pushs.ma".
+
+(* TAILED UNWIND FOR RELOCATION MAP *****************************************)
+
+(* Constructions with labels ************************************************)
+
+lemma unwind2_rmap_labels_L (f) (n):
+      (⫯*[n]f) = ▶[f](𝗟∗∗n).
+#f #n @(nat_ind_succ … n) -n //
+#n #IH
+<labels_succ <unwind2_rmap_L_dx //
+qed.

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr.ma
index d0dcf4eee46d82e5b652d446ae486eeac26843b8..27468022ad4c4e22109173830d80a04d6498f657 100644 (file)
--- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr.ma
@@ -15,18 +15,17 @@
 include "delayed_updating/substitution/fsubst.ma".
 include "delayed_updating/syntax/prototerm_constructors.ma".
 include "delayed_updating/syntax/prototerm_eq.ma".
 include "delayed_updating/substitution/fsubst.ma".
 include "delayed_updating/syntax/prototerm_constructors.ma".
 include "delayed_updating/syntax/prototerm_eq.ma".

-include "delayed_updating/syntax/path_head.ma".
+include "delayed_updating/syntax/path_closed.ma".

 include "delayed_updating/notation/relations/black_rightarrow_df_3.ma".
 include "ground/xoa/ex_4_3.ma".
 
 (* DELAYED FOCUSED REDUCTION ************************************************)
 
 include "delayed_updating/notation/relations/black_rightarrow_df_3.ma".
 include "ground/xoa/ex_4_3.ma".
 
 (* DELAYED FOCUSED REDUCTION ************************************************)
 

-(**) (* explicit ninj because we cannot declare the expectd type of k *)

 definition dfr (r): relation2 prototerm prototerm ≝
            λt1,t2.
 definition dfr (r): relation2 prototerm prototerm ≝
            λt1,t2.

-           ∃∃p,q,k. p●𝗔◗𝗟◗q = r &
-           (𝗟◗q) = ↳[ninj k](𝗟◗q) & r◖𝗱k ϵ t1 &
-           t1[⋔r←𝛕k.(t1⋔(p◖𝗦))] ⇔ t2
+           ∃∃p,q,n. p●𝗔◗𝗟◗q = r &
+           q ϵ 𝐂❨n❩ & r◖𝗱↑n ϵ t1 &
+           t1[⋔r←𝛕↑n.(t1⋔(p◖𝗦))] ⇔ t2

 .
 
 interpretation
 .
 
 interpretation

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_ifr.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_ifr.ma
index 68cea487c474ddaf6d9a0bff4f740a3e97953946..5f37abd5f1b81e78d8366eadbc747371bf72e54c 100644 (file)
--- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_ifr.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_ifr.ma
@@ -19,13 +19,13 @@ include "delayed_updating/unwind/unwind2_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".
 include "delayed_updating/unwind/unwind2_preterm_fsubst.ma".
 include "delayed_updating/unwind/unwind2_preterm_eq.ma".
 include "delayed_updating/unwind/unwind2_prototerm_lift.ma".

-include "delayed_updating/unwind/unwind2_rmap_head.ma".
+include "delayed_updating/unwind/unwind2_rmap_closed.ma".

 
 include "delayed_updating/substitution/fsubst_eq.ma".
 include "delayed_updating/substitution/lift_prototerm_eq.ma".
 
 include "delayed_updating/syntax/prototerm_proper_constructors.ma".
 
 include "delayed_updating/substitution/fsubst_eq.ma".
 include "delayed_updating/substitution/lift_prototerm_eq.ma".
 
 include "delayed_updating/syntax/prototerm_proper_constructors.ma".

-include "delayed_updating/syntax/path_head_structure.ma".
+include "delayed_updating/syntax/path_closed_structure.ma".

 include "delayed_updating/syntax/path_structure_depth.ma".
 
 (* DELAYED FOCUSED REDUCTION ************************************************)
 include "delayed_updating/syntax/path_structure_depth.ma".
 
 (* DELAYED FOCUSED REDUCTION ************************************************)


@@ -35,33 +35,29 @@ include "delayed_updating/syntax/path_structure_depth.ma".
 theorem dfr_des_ifr (f) (t1) (t2) (r): t1 ϵ 𝐓 →
         t1 ➡𝐝𝐟[r] t2 → ▼[f]t1 ➡𝐢𝐟[⊗r] ▼[f]t2.
 #f #t1 #t2 #r #H0t1
 theorem dfr_des_ifr (f) (t1) (t2) (r): t1 ϵ 𝐓 →
         t1 ➡𝐝𝐟[r] t2 → ▼[f]t1 ➡𝐢𝐟[⊗r] ▼[f]t2.
 #f #t1 #t2 #r #H0t1

-* #p #q #k #Hr #H1k #Ht1 #Ht2 destruct
-@(ex4_3_intro â\80¦ (â\8a\97p) (â\8a\97q) (â\86\91â\99­q))
-[ -H0t1 -H1k -Ht1 -Ht2 //
+* #p #q #n #Hr #Hn #Ht1 #Ht2 destruct
+@(ex4_3_intro … (⊗p) (⊗q) (♭q))
+[ -H0t1 -Hn -Ht1 -Ht2 //

 | -H0t1 -Ht1 -Ht2
 | -H0t1 -Ht1 -Ht2

-  >structure_L_sn
-  >H1k in ⊢ (??%?); >path_head_structure_depth <H1k -H1k //
+  /2 width=2 by path_closed_structure_depth/

 | lapply (in_comp_unwind2_path_term f … Ht1) -Ht2 -Ht1 -H0t1
 | lapply (in_comp_unwind2_path_term f … Ht1) -Ht2 -Ht1 -H0t1

-  <unwind2_path_d_dx <list_append_rcons_sn
-  lapply (unwind2_rmap_append_pap_closed f … (p◖𝗔) … H1k) -H1k
-  <depth_L_sn #H2k
-  lapply (eq_inv_ninj_bi … H2k) -H2k #H2k <H2k -H2k #Ht1 //
+  <unwind2_path_d_dx <tr_pap_succ_nap <list_append_rcons_sn
+  <unwind2_rmap_append_closed_nap //

 | lapply (unwind2_term_eq_repl_dx f … Ht2) -Ht2 #Ht2
   @(subset_eq_trans … Ht2) -t2
   @(subset_eq_trans … (unwind2_term_fsubst_ppc …))
   [ @fsubst_eq_repl [ // | // ]
 | lapply (unwind2_term_eq_repl_dx f … Ht2) -Ht2 #Ht2
   @(subset_eq_trans … Ht2) -t2
   @(subset_eq_trans … (unwind2_term_fsubst_ppc …))
   [ @fsubst_eq_repl [ // | // ]

-    @(subset_eq_trans … (unwind2_term_iref …))
+    @(subset_eq_trans … (unwind2_term_iref…))

     @(subset_eq_canc_sn … (lift_term_eq_repl_dx …))
     [ @unwind2_term_grafted_S /2 width=2 by ex_intro/ | skip ] -Ht1
     @(subset_eq_trans … (lift_unwind2_term_after …))
     @unwind2_term_eq_repl_sn
 (* Note: crux of the proof begins *)
     <list_append_rcons_sn
     @(subset_eq_canc_sn … (lift_term_eq_repl_dx …))
     [ @unwind2_term_grafted_S /2 width=2 by ex_intro/ | skip ] -Ht1
     @(subset_eq_trans … (lift_unwind2_term_after …))
     @unwind2_term_eq_repl_sn
 (* Note: crux of the proof begins *)
     <list_append_rcons_sn

-    @(stream_eq_trans … (tr_compose_uni_dx …))
+    @(stream_eq_trans … (tr_compose_uni_dx_pap …)) <tr_pap_succ_nap

     @tr_compose_eq_repl
     @tr_compose_eq_repl

-    [ <unwind2_rmap_append_pap_closed //
-    | >unwind2_rmap_A_dx
-      /2 width=1 by tls_unwind2_rmap_closed/
+    [ <unwind2_rmap_append_closed_nap //
+    | /2 width=1 by tls_succ_unwind2_rmap_append_L_closed_dx/

     ]
 (* Note: crux of the proof ends *)
   | //
     ]
 (* Note: crux of the proof ends *)
   | //

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_lift.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_lift.ma
index b60bd708c681b172e2f4c4ebbfdc3b403abe2879..830dbd640339a7b8711d7197d46aeeccfc84006c 100644 (file)
--- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_lift.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_lift.ma
@@ -17,8 +17,8 @@ include "delayed_updating/reduction/dfr.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/fsubst_lift.ma".
 include "delayed_updating/substitution/fsubst_eq.ma".
 include "delayed_updating/substitution/lift_constructors.ma".

-include "delayed_updating/substitution/lift_path_head.ma".
-include "delayed_updating/substitution/lift_rmap_head.ma".
+include "delayed_updating/substitution/lift_path_closed.ma".
+include "delayed_updating/substitution/lift_rmap_closed.ma".

 
 (* DELAYED FOCUSED REDUCTION ************************************************)
 
 
 (* DELAYED FOCUSED REDUCTION ************************************************)
 


@@ -27,25 +27,23 @@ include "delayed_updating/substitution/lift_rmap_head.ma".
 theorem dfr_lift_bi (f) (t1) (t2) (r):
         t1 ➡𝐝𝐟[r] t2 → ↑[f]t1 ➡𝐝𝐟[↑[f]r] ↑[f]t2.
 #f #t1 #t2 #r
 theorem dfr_lift_bi (f) (t1) (t2) (r):
         t1 ➡𝐝𝐟[r] t2 → ↑[f]t1 ➡𝐝𝐟[↑[f]r] ↑[f]t2.
 #f #t1 #t2 #r

-* #p #q #k #Hr #H1k #Ht1 #Ht2 destruct
-@(ex4_3_intro … (↑[f]p) (↑[↑[p◖𝗔◖𝗟]f]q) ((↑[p●𝗔◗𝗟◗q]f)＠⧣❨k❩))
-[ -H1k -Ht1 -Ht2 //
+* #p #q #n #Hr #Hn #Ht1 #Ht2 destruct
+@(ex4_3_intro … (↑[f]p) (↑[↑[p◖𝗔◖𝗟]f]q) ((↑[p●𝗔◗𝗟◗q]f)＠§❨n❩))
+[ -Hn -Ht1 -Ht2 //

 | -Ht1 -Ht2
 | -Ht1 -Ht2

-  <lift_rmap_L_dx >lift_path_L_sn
-  <(lift_path_head_closed … H1k) in ⊢ (??%?); -H1k //
-| lapply (in_comp_lift_path_term f … Ht1) -Ht2 -Ht1 -H1k
+  /2 width=1 by lift_path_rmap_closed_L/
+| lapply (in_comp_lift_path_term f … Ht1) -Ht2 -Ht1 -Hn

   <lift_path_d_dx #Ht1 //
 | lapply (lift_term_eq_repl_dx f … Ht2) -Ht2 #Ht2 -Ht1
   @(subset_eq_trans … Ht2) -t2
   @(subset_eq_trans … (lift_term_fsubst …))
   @fsubst_eq_repl [ // | // ]
   <lift_path_d_dx #Ht1 //
 | lapply (lift_term_eq_repl_dx f … Ht2) -Ht2 #Ht2 -Ht1
   @(subset_eq_trans … Ht2) -t2
   @(subset_eq_trans … (lift_term_fsubst …))
   @fsubst_eq_repl [ // | // ]

-  @(subset_eq_trans … (lift_term_iref …))
+  @(subset_eq_trans … (lift_term_iref_nap …))

   @iref_eq_repl
   @(subset_eq_canc_sn … (lift_term_grafted_S …))
   @lift_term_eq_repl_sn
 (* Note: crux of the proof begins *)
   @iref_eq_repl
   @(subset_eq_canc_sn … (lift_term_grafted_S …))
   @lift_term_eq_repl_sn
 (* Note: crux of the proof begins *)

-  >list_append_rcons_sn in H1k; #H1k >lift_rmap_A_dx
-  /2 width=1 by tls_lift_rmap_closed/
+  /2 width=1 by tls_succ_lift_rmap_append_L_closed_dx/

 (* Note: crux of the proof ends *)
 ]
 qed.
 (* Note: crux of the proof ends *)
 ]
 qed.

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr.ma
index b36038141c87ce356fb4296899ef3daac03269cf..92512b342ed50449745aa0fdec371d10bad5621e 100644 (file)
--- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr.ma
@@ -15,19 +15,18 @@
 include "delayed_updating/substitution/fsubst.ma".
 include "delayed_updating/substitution/lift_prototerm.ma".
 include "delayed_updating/syntax/prototerm_eq.ma".
 include "delayed_updating/substitution/fsubst.ma".
 include "delayed_updating/substitution/lift_prototerm.ma".
 include "delayed_updating/syntax/prototerm_eq.ma".

-include "delayed_updating/syntax/path_head.ma".
+include "delayed_updating/syntax/path_closed.ma".

 include "delayed_updating/notation/relations/black_rightarrow_if_3.ma".
 include "ground/relocation/tr_uni.ma".
 include "ground/xoa/ex_4_3.ma".
 
 (* IMMEDIATE FOCUSED REDUCTION ************************************************)
 
 include "delayed_updating/notation/relations/black_rightarrow_if_3.ma".
 include "ground/relocation/tr_uni.ma".
 include "ground/xoa/ex_4_3.ma".
 
 (* IMMEDIATE FOCUSED REDUCTION ************************************************)
 

-(**) (* explicit ninj because we cannot declare the expectd type of k *)

 definition ifr (r): relation2 prototerm prototerm ≝
            λt1,t2.
 definition ifr (r): relation2 prototerm prototerm ≝
            λt1,t2.

-           ∃∃p,q,k. p●𝗔◗𝗟◗q = r &
-           (𝗟◗q) = ↳[ninj k](𝗟◗q) & r◖𝗱k ϵ t1 &
-           t1[⋔r←↑[𝐮❨ninj k❩](t1⋔(p◖𝗦))] ⇔ t2
+           ∃∃p,q,n. p●𝗔◗𝗟◗q = r &
+           q ϵ 𝐂❨n❩ & r◖𝗱↑n ϵ t1 &
+           t1[⋔r←↑[𝐮❨↑n❩](t1⋔(p◖𝗦))] ⇔ t2

 .
 
 interpretation
 .
 
 interpretation

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr_lift.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr_lift.ma
index 7c4d11d73cdc452391e1627a058d93dc06a4fe48..1d8f5855a143beeb2e37eb06e8f8c3ef00e5dd5b 100644 (file)
--- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr_lift.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr_lift.ma
@@ -17,8 +17,8 @@ include "delayed_updating/reduction/ifr.ma".
 include "delayed_updating/substitution/fsubst_lift.ma".
 include "delayed_updating/substitution/fsubst_eq.ma".
 include "delayed_updating/substitution/lift_prototerm_after.ma".
 include "delayed_updating/substitution/fsubst_lift.ma".
 include "delayed_updating/substitution/fsubst_eq.ma".
 include "delayed_updating/substitution/lift_prototerm_after.ma".

-include "delayed_updating/substitution/lift_path_head.ma".
-include "delayed_updating/substitution/lift_rmap_head.ma".
+include "delayed_updating/substitution/lift_path_closed.ma".
+include "delayed_updating/substitution/lift_rmap_closed.ma".

 
 include "ground/relocation/tr_uni_compose.ma".
 include "ground/relocation/tr_compose_eq.ma".
 
 include "ground/relocation/tr_uni_compose.ma".
 include "ground/relocation/tr_compose_eq.ma".


@@ -30,13 +30,12 @@ include "ground/relocation/tr_compose_eq.ma".
 theorem ifr_lift_bi (f) (t1) (t2) (r):
         t1 ➡𝐢𝐟[r] t2 → ↑[f]t1 ➡𝐢𝐟[↑[f]r] ↑[f]t2.
 #f #t1 #t2 #r
 theorem ifr_lift_bi (f) (t1) (t2) (r):
         t1 ➡𝐢𝐟[r] t2 → ↑[f]t1 ➡𝐢𝐟[↑[f]r] ↑[f]t2.
 #f #t1 #t2 #r

-* #p #q #k #Hr #H1k #Ht1 #Ht2 destruct
-@(ex4_3_intro … (↑[f]p) (↑[↑[p◖𝗔◖𝗟]f]q) ((↑[p●𝗔◗𝗟◗q]f)＠⧣❨k❩))
-[ -H1k -Ht1 -Ht2 //
+* #p #q #n #Hr #Hn #Ht1 #Ht2 destruct
+@(ex4_3_intro … (↑[f]p) (↑[↑[p◖𝗔◖𝗟]f]q) ((↑[p●𝗔◗𝗟◗q]f)＠§❨n❩))
+[ -Hn -Ht1 -Ht2 //

 | -Ht1 -Ht2
 | -Ht1 -Ht2

-  <lift_rmap_L_dx >lift_path_L_sn
-  <(lift_path_head_closed … H1k) in ⊢ (??%?); -H1k //
-| lapply (in_comp_lift_path_term f … Ht1) -Ht2 -Ht1 -H1k
+  /2 width=1 by lift_path_rmap_closed_L/
+| lapply (in_comp_lift_path_term f … Ht1) -Ht2 -Ht1 -Hn

   <lift_path_d_dx #Ht1 //
 | lapply (lift_term_eq_repl_dx f … Ht2) -Ht2 #Ht2 -Ht1
   @(subset_eq_trans … Ht2) -t2
   <lift_path_d_dx #Ht1 //
 | lapply (lift_term_eq_repl_dx f … Ht2) -Ht2 #Ht2 -Ht1
   @(subset_eq_trans … Ht2) -t2


@@ -48,10 +47,9 @@ theorem ifr_lift_bi (f) (t1) (t2) (r):
   @(subset_eq_canc_dx … (lift_term_after …))
   @lift_term_eq_repl_sn
 (* Note: crux of the proof begins *)
   @(subset_eq_canc_dx … (lift_term_after …))
   @lift_term_eq_repl_sn
 (* Note: crux of the proof begins *)

-  @(stream_eq_trans … (tr_compose_uni_dx …))
-  @tr_compose_eq_repl //
-  >list_append_rcons_sn in H1k; #H1k >lift_rmap_A_dx
-  /2 width=1 by tls_lift_rmap_closed/
+  @(stream_eq_trans … (tr_compose_uni_dx_pap …)) <tr_pap_succ_nap
+  @tr_compose_eq_repl // >nsucc_unfold
+  /2 width=1 by tls_succ_lift_rmap_append_L_closed_dx/

 (* Note: crux of the proof ends *)
 ]
 qed.
 (* Note: crux of the proof ends *)
 ]
 qed.

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr_unwind.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr_unwind.ma
index e8cc51826179f68191c908417adedae47fd85353..077ff798e26298d93345e27bf014fed067b68f45 100644 (file)
--- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr_unwind.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr_unwind.ma
@@ -17,12 +17,12 @@ include "delayed_updating/reduction/ifr.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".
 include "delayed_updating/unwind/unwind2_preterm_fsubst.ma".
 include "delayed_updating/unwind/unwind2_preterm_eq.ma".
 include "delayed_updating/unwind/unwind2_prototerm_lift.ma".

-include "delayed_updating/unwind/unwind2_rmap_head.ma".
+include "delayed_updating/unwind/unwind2_rmap_closed.ma".

 
 include "delayed_updating/substitution/fsubst_eq.ma".
 include "delayed_updating/substitution/lift_prototerm_eq.ma".
 
 
 include "delayed_updating/substitution/fsubst_eq.ma".
 include "delayed_updating/substitution/lift_prototerm_eq.ma".
 

-include "delayed_updating/syntax/path_head_structure.ma".
+include "delayed_updating/syntax/path_closed_structure.ma".

 include "delayed_updating/syntax/path_structure_depth.ma".
 
 (* IMMEDIATE FOCUSED REDUCTION **********************************************)
 include "delayed_updating/syntax/path_structure_depth.ma".
 
 (* IMMEDIATE FOCUSED REDUCTION **********************************************)


@@ -33,17 +33,14 @@ lemma ifr_unwind_bi (f) (t1) (t2) (r):
       t1 ϵ 𝐓 → r ϵ 𝐈 →
       t1 ➡𝐢𝐟[r] t2 → ▼[f]t1 ➡𝐢𝐟[⊗r] ▼[f]t2.
 #f #t1 #t2 #r #H1t1 #H2r
       t1 ϵ 𝐓 → r ϵ 𝐈 →
       t1 ➡𝐢𝐟[r] t2 → ▼[f]t1 ➡𝐢𝐟[⊗r] ▼[f]t2.
 #f #t1 #t2 #r #H1t1 #H2r

-* #p #q #k #Hr #H1k #Ht1 #Ht2 destruct
-@(ex4_3_intro â\80¦ (â\8a\97p) (â\8a\97q) (â\86\91â\99­q))
-[ -H1t1 -H2r -H1k -Ht1 -Ht2 //
+* #p #q #n #Hr #Hn #Ht1 #Ht2 destruct
+@(ex4_3_intro … (⊗p) (⊗q) (♭q))
+[ -H1t1 -H2r -Hn -Ht1 -Ht2 //

 | -H1t1 -H2r -Ht1 -Ht2
 | -H1t1 -H2r -Ht1 -Ht2

-  >structure_L_sn
-  >H1k in ⊢ (??%?); >path_head_structure_depth <H1k -H1k //
+  /2 width=2 by path_closed_structure_depth/

 | lapply (in_comp_unwind2_path_term f … Ht1) -Ht2 -Ht1 -H1t1 -H2r
 | lapply (in_comp_unwind2_path_term f … Ht1) -Ht2 -Ht1 -H1t1 -H2r

-  <unwind2_path_d_dx <list_append_rcons_sn
-  lapply (unwind2_rmap_append_pap_closed f … (p◖𝗔) … H1k) -H1k
-  <depth_L_sn #H2k
-  lapply (eq_inv_ninj_bi … H2k) -H2k #H2k <H2k -H2k #Ht1 //
+  <unwind2_path_d_dx <tr_pap_succ_nap <list_append_rcons_sn
+  <unwind2_rmap_append_closed_nap //

 | lapply (unwind2_term_eq_repl_dx f … Ht2) -Ht2 #Ht2
   @(subset_eq_trans … Ht2) -t2
   @(subset_eq_trans … (unwind2_term_fsubst_pic …))
 | lapply (unwind2_term_eq_repl_dx f … Ht2) -Ht2 #Ht2
   @(subset_eq_trans … Ht2) -t2
   @(subset_eq_trans … (unwind2_term_fsubst_pic …))


@@ -55,11 +52,10 @@ lemma ifr_unwind_bi (f) (t1) (t2) (r):
     @unwind2_term_eq_repl_sn
 (* Note: crux of the proof begins *)
     <list_append_rcons_sn
     @unwind2_term_eq_repl_sn
 (* Note: crux of the proof begins *)
     <list_append_rcons_sn

-    @(stream_eq_trans … (tr_compose_uni_dx …))
+    @(stream_eq_trans … (tr_compose_uni_dx_pap …)) <tr_pap_succ_nap

     @tr_compose_eq_repl
     @tr_compose_eq_repl

-    [ <unwind2_rmap_append_pap_closed //
-    | >unwind2_rmap_A_dx
-      /2 width=1 by tls_unwind2_rmap_closed/
+    [ <unwind2_rmap_append_closed_nap //
+    | /2 width=1 by tls_succ_unwind2_rmap_append_L_closed_dx/

     ]
 (* Note: crux of the proof ends *)
   | //
     ]
 (* Note: crux of the proof ends *)
   | //

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_constructors.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_constructors.ma
index e87ccb21f0cb641bb48f4cf6ee666e8bc1ec455e..f263e2d140464896573bd1fddc5ebceaa2e322db 100644 (file)
--- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_constructors.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_constructors.ma
@@ -15,17 +15,18 @@
 include "delayed_updating/substitution/lift_prototerm_id.ma".
 include "delayed_updating/substitution/lift_path_uni.ma".
 include "delayed_updating/syntax/prototerm_constructors_eq.ma".
 include "delayed_updating/substitution/lift_prototerm_id.ma".
 include "delayed_updating/substitution/lift_path_uni.ma".
 include "delayed_updating/syntax/prototerm_constructors_eq.ma".

+include "ground/relocation/nap.ma".

 
 (* LIFT FOR PROTOTERM *******************************************************)
 
 
 (* LIFT FOR PROTOTERM *******************************************************)
 

-lemma lift_term_iref_sn (f) (t:prototerm) (k:pnat):
+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/
 qed-.
 
       (𝛕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/
 qed-.
 

-lemma lift_term_iref_dx (f) (t) (k:pnat):
+lemma lift_term_iref_pap_dx (f) (t) (k:pnat):

       ↑[f](𝛕k.t) ⊆ 𝛕f＠⧣❨k❩.↑[⇂*[k]f]t.
 #f #t #k #p * #q #Hq #H0 destruct
 elim (in_comp_inv_iref … Hq) -Hq #p #H0 #Hp destruct
       ↑[f](𝛕k.t) ⊆ 𝛕f＠⧣❨k❩.↑[⇂*[k]f]t.
 #f #t #k #p * #q #Hq #H0 destruct
 elim (in_comp_inv_iref … Hq) -Hq #p #H0 #Hp destruct


@@ -33,15 +34,21 @@ elim (in_comp_inv_iref … Hq) -Hq #p #H0 #Hp destruct
 /3 width=1 by in_comp_iref, in_comp_lift_path_term/
 qed-.
 
 /3 width=1 by in_comp_iref, in_comp_lift_path_term/
 qed-.
 

-lemma lift_term_iref (f) (t) (k:pnat):
+lemma lift_term_iref_pap (f) (t) (k:pnat):

       (𝛕f＠⧣❨k❩.↑[⇂*[k]f]t) ⇔ ↑[f](𝛕k.t).
       (𝛕f＠⧣❨k❩.↑[⇂*[k]f]t) ⇔ ↑[f](𝛕k.t).

-/3 width=1 by conj, lift_term_iref_sn, lift_term_iref_dx/
+/3 width=1 by conj, lift_term_iref_pap_sn, lift_term_iref_pap_dx/
+qed.
+
+lemma lift_term_iref_nap (f) (t) (n):
+      (𝛕↑(f＠§❨n❩).↑[⇂*[↑n]f]t) ⇔ ↑[f](𝛕↑n.t).
+#f #t #n
+>tr_pap_succ_nap //

 qed.
 
 lemma lift_term_iref_uni (t) (n) (k):
       (𝛕(k+n).t) ⇔ ↑[𝐮❨n❩](𝛕k.t).
 #t #n #k
 qed.
 
 lemma lift_term_iref_uni (t) (n) (k):
       (𝛕(k+n).t) ⇔ ↑[𝐮❨n❩](𝛕k.t).
 #t #n #k

-@(subset_eq_trans … (lift_term_iref …))
+@(subset_eq_trans … (lift_term_iref_pap …))

 <tr_uni_pap >nsucc_pnpred <tr_tls_succ_uni
 /3 width=1 by iref_eq_repl, lift_term_id/
 qed.
 <tr_uni_pap >nsucc_pnpred <tr_tls_succ_uni
 /3 width=1 by iref_eq_repl, lift_term_id/
 qed.

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_path_closed.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_path_closed.ma
index b332b841fb1f39929c857b39c01d8ce66da6d112..79443ca3ba9258b36eff07e4a2c27db3ba200865 100644 (file)
--- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_path_closed.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_path_closed.ma
@@ -31,3 +31,14 @@ lemma lift_path_rmap_closed (f) (p) (q) (n):
       q ϵ 𝐂❨n❩ → ↑[↑[p]f]q ϵ 𝐂❨↑[p●q]f＠❨n❩❩.
 /2 width=1 by lift_path_closed/
 qed.
       q ϵ 𝐂❨n❩ → ↑[↑[p]f]q ϵ 𝐂❨↑[p●q]f＠❨n❩❩.
 /2 width=1 by lift_path_closed/
 qed.

+
+lemma lift_path_rmap_closed_L (f) (p) (q) (n):
+      q ϵ 𝐂❨n❩ → ↑[↑[p◖𝗟]f]q ϵ 𝐂❨↑[p●𝗟◗q]f＠§❨n❩❩.
+#f #p #q #n #Hq
+lapply (lift_path_closed (↑[p◖𝗟]f) … Hq) #Hq0
+lapply (pcc_L_sn … Hq) -Hq #Hq1
+lapply (lift_path_rmap_closed f p … Hq1) -Hq1
+<lift_path_L_sn >lift_rmap_L_dx #Hq1
+elim (pcc_inv_L_sn … Hq1 Hq0) -Hq1 #H0 #_
+<H0 in Hq0; -H0 //
+qed.

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_rmap_closed.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_rmap_closed.ma
index 58bef8153e3ec21c96de6c4d00400402ac358b17..cc3e61bf7c5ebcfbf3097bff72a55b87e966c070 100644 (file)
--- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_rmap_closed.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_rmap_closed.ma
@@ -34,3 +34,10 @@ lemma tls_lift_rmap_closed (f) (q) (n):
 #f #q #n #H0
 /2 width=1 by tls_plus_lift_rmap_closed/
 qed-.
 #f #q #n #H0
 /2 width=1 by tls_plus_lift_rmap_closed/
 qed-.

+
+lemma tls_succ_lift_rmap_append_L_closed_dx (f) (p) (q) (n):
+      q ϵ 𝐂❨n❩ →
+      ↑[p]f ≗ ⇂*[↑n]↑[p●𝗟◗q]f.
+#f #p #q #n #Hq
+/3 width=1 by tls_lift_rmap_closed, pcc_L_sn/
+qed-.

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_closed.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_closed.ma
index fd7a9954fb8e94c3b6849f66070e4ac21eb4c842..620db955c30943a906f75ca63045380069e576e0 100644 (file)
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_closed.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_closed.ma
@@ -65,7 +65,7 @@ qed-.
 
 lemma pcc_inv_L_dx (p) (n):
       p◖𝗟 ϵ 𝐂❨n❩ →
 
 lemma pcc_inv_L_dx (p) (n):
       p◖𝗟 ϵ 𝐂❨n❩ →

-      ∧∧ p ϵ 𝐂❨↓n❩ & ↑↓n = n.
+      ∧∧ p ϵ 𝐂❨↓n❩ & n = ↑↓n.

 #p #n @(insert_eq_1 … (p◖𝗟))
 #x * -x -n
 [|*: #x #n [ #k ] #Hx ] #H0 destruct
 #p #n @(insert_eq_1 … (p◖𝗟))
 #x * -x -n
 [|*: #x #n [ #k ] #Hx ] #H0 destruct


@@ -99,7 +99,7 @@ lemma pcc_inv_L_dx_zero (p):
       p◖𝗟 ϵ 𝐂❨𝟎❩ → ⊥.
 #p #H0
 elim (pcc_inv_L_dx … H0) -H0 #_ #H0
       p◖𝗟 ϵ 𝐂❨𝟎❩ → ⊥.
 #p #H0
 elim (pcc_inv_L_dx … H0) -H0 #_ #H0

-/2 width=7 by eq_inv_nsucc_zero/
+/2 width=7 by eq_inv_zero_nsucc/

 qed-.
 
 lemma pcc_inv_L_dx_succ (p) (n):
 qed-.
 
 lemma pcc_inv_L_dx_succ (p) (n):


@@ -117,9 +117,39 @@ theorem pcc_append_bi (p) (q) (m) (n):
 /2 width=1 by pcc_d_dx, pcc_m_dx, pcc_L_dx, pcc_A_dx, pcc_S_dx/
 qed.
 
 /2 width=1 by pcc_d_dx, pcc_m_dx, pcc_L_dx, pcc_A_dx, pcc_S_dx/
 qed.
 

+(* Constructions with path_lcons ********************************************)
+
+lemma pcc_m_sn (q) (n):
+      q ϵ 𝐂❨n❩ → (𝗺◗q) ϵ 𝐂❨n❩.
+#q #n #Hq
+lapply (pcc_append_bi (𝐞◖𝗺) … Hq) -Hq
+/2 width=3 by pcc_m_dx/
+qed.
+
+lemma pcc_L_sn (q) (n):
+      q ϵ 𝐂❨n❩ → (𝗟◗q) ϵ 𝐂❨↑n❩.
+#q #n #Hq
+lapply (pcc_append_bi (𝐞◖𝗟) … Hq) -Hq
+/2 width=3 by pcc_L_dx/
+qed.
+
+lemma pcc_A_sn (q) (n):
+      q ϵ 𝐂❨n❩ → (𝗔◗q) ϵ 𝐂❨n❩.
+#q #n #Hq
+lapply (pcc_append_bi (𝐞◖𝗔) … Hq) -Hq
+/2 width=3 by pcc_A_dx/
+qed.
+
+lemma pcc_S_sn (q) (n):
+      q ϵ 𝐂❨n❩ → (𝗦◗q) ϵ 𝐂❨n❩.
+#q #n #Hq
+lapply (pcc_append_bi (𝐞◖𝗦) … Hq) -Hq
+/2 width=3 by pcc_S_dx/
+qed.
+

 (* Main inversions **********************************************************)
 
 (* Main inversions **********************************************************)
 

-theorem ppc_mono (q) (n1):
+theorem pcc_mono (q) (n1):

         q ϵ 𝐂❨n1❩ → ∀n2. q ϵ 𝐂❨n2❩ → n1 = n2.
 #q1 #n1 #Hn1 elim Hn1 -q1 -n1
 [|*: #q1 #n1 [ #k1 ] #_ #IH ] #n2 #Hn2
         q ϵ 𝐂❨n1❩ → ∀n2. q ϵ 𝐂❨n2❩ → n1 = n2.
 #q1 #n1 #Hn1 elim Hn1 -q1 -n1
 [|*: #q1 #n1 [ #k1 ] #_ #IH ] #n2 #Hn2


@@ -160,3 +190,12 @@ elim (eq_inv_list_lcons_bi ????? H0) -H0 #H0 #H1 destruct
 | elim (pcc_inv_empty_succ … Hq2)
 ]
 qed-.
 | elim (pcc_inv_empty_succ … Hq2)
 ]
 qed-.

+
+theorem pcc_inv_L_sn (q) (n) (m):
+        (𝗟◗q) ϵ 𝐂❨n❩ → q ϵ 𝐂❨m❩ →
+        ∧∧ ↓n = m & n = ↑↓n.
+#q #n #m #H1q #H2q
+lapply (pcc_L_sn … H2q) -H2q #H2q
+<(pcc_mono … H2q … H1q) -q -n
+/2 width=1 by conj/
+qed-.

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_closed.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_closed.ma
new file mode 100644 (file)
index 0000000..7c551ed
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_closed.ma
@@ -0,0 +1,92 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/unwind/unwind2_rmap_eq.ma".
+include "delayed_updating/syntax/path_closed.ma".
+include "delayed_updating/syntax/path_depth.ma".
+include "ground/relocation/xap.ma".
+include "ground/lib/stream_eq_eq.ma".
+include "ground/arith/nat_le_plus.ma".
+include "ground/arith/nat_le_pred.ma".
+
+(* TAILED UNWIND FOR RELOCATION MAP *****************************************)
+
+(* Destructions with cpp ****************************************************)
+
+lemma unwind2_rmap_append_closed_dx_xap_le (f) (p) (q) (n):
+      q ϵ 𝐂❨n❩ → ∀m. m ≤ n →
+      ▶[f]q＠❨m❩ = ▶[f](p●q)＠❨m❩.
+#f #p #q #n #Hq elim Hq -q -n
+[|*: #q #n [ #k ] #_ #IH ] #m #Hm
+[ <(nle_inv_zero_dx … Hm) -m //
+| <unwind2_rmap_d_dx <unwind2_rmap_d_dx
+  <tr_compose_xap <tr_compose_xap
+  @IH -IH (**) (* auto too slow *)
+  @nle_trans [| @tr_uni_xap ]
+  /2 width=1 by nle_plus_bi_dx/
+| <unwind2_rmap_m_dx <unwind2_rmap_m_dx
+  /2 width=2 by/
+| <unwind2_rmap_L_dx <unwind2_rmap_L_dx
+  elim (nle_inv_succ_dx … Hm) -Hm // * #Hm #H0
+  >H0 -H0 <tr_xap_push <tr_xap_push
+  /3 width=2 by eq_f/
+| <unwind2_rmap_A_dx <unwind2_rmap_A_dx
+  /2 width=2 by/
+| <unwind2_rmap_S_dx <unwind2_rmap_S_dx
+  /2 width=2 by/
+]
+qed-.
+
+lemma unwind2_rmap_append_L_closed_dx_nap (f) (p) (q) (n):
+      q ϵ 𝐂❨n❩ →
+      ▶[f](𝗟◗q)＠§❨n❩ = ▶[f](p●𝗟◗q)＠§❨n❩.
+#f #p #q #n #Hq
+lapply (pcc_L_sn … Hq) -Hq #Hq
+lapply (unwind2_rmap_append_closed_dx_xap_le f p … Hq (↑n) ?) -Hq //
+<tr_xap_succ_nap <tr_xap_succ_nap #Hq
+/2 width=1 by eq_inv_nsucc_bi/
+qed-.
+
+lemma unwind2_rmap_push_closed_nap (f) (q) (n):
+      q ϵ 𝐂❨n❩ →
+      ♭q = ▶[⫯f]q＠§❨n❩.
+#f #q #n #Hq elim Hq -q -n
+[|*: #q #n [ #k ] #_ #IH ] //
+<unwind2_rmap_d_dx <tr_compose_nap //
+qed-.
+
+lemma unwind2_rmap_append_closed_nap (f) (p) (q) (n):
+      q ϵ 𝐂❨n❩ →
+      ♭q = ▶[f](p●𝗟◗q)＠§❨n❩.
+#f #p #q #n #Hq
+<unwind2_rmap_append_L_closed_dx_nap //
+/2 width=1 by unwind2_rmap_push_closed_nap/
+qed-.
+
+lemma tls_succ_plus_unwind2_rmap_push_closed (f) (q) (n):
+      q ϵ 𝐂❨n❩ →
+      ∀m. ⇂*[m]f ≗ ⇂*[↑(m+n)]▶[⫯f]q.
+#f #q #n #Hq elim Hq -q -n //
+#q #n [ #k ] #_ #IH #m
+[ @(stream_eq_trans … (tls_unwind2_rmap_d_dx …))
+  >nrplus_inj_dx >nrplus_inj_sn >nsucc_unfold //
+| <unwind2_rmap_L_dx <nplus_succ_dx //
+]
+qed-.
+
+lemma tls_succ_unwind2_rmap_append_L_closed_dx (f) (p) (q) (n):
+      q ϵ 𝐂❨n❩ →
+      ▶[f]p ≗ ⇂*[↑n]▶[f](p●𝗟◗q).
+/2 width=1 by tls_succ_plus_unwind2_rmap_push_closed/
+qed-.

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_eq.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_eq.ma
index c075e2f250e8af9a1642edb561aa6b93186a26f7..b93aabf0ffb8316da2e18428b92a6a9b54798acd 100644 (file)
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_eq.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_eq.ma
@@ -28,9 +28,9 @@ lemma unwind2_rmap_eq_repl (p):
 /3 width=1 by preunwind2_rmap_eq_repl/
 qed-.
 
 /3 width=1 by preunwind2_rmap_eq_repl/
 qed-.
 

-lemma tls_unwind2_rmap_d_dx (f) (p) (n) (k):
-      ⇂*[n+k]▶[f]p ≗ ⇂*[n]▶[f](p◖𝗱k).
-#f #p #n #k
+lemma tls_unwind2_rmap_d_dx (f) (p) (h) (k):
+      ⇂*[h+k]▶[f]p ≗ ⇂*[h]▶[f](p◖𝗱k).
+#f #p #h #k

 <unwind2_rmap_d_dx >nrplus_inj_dx
 /2 width=1 by tr_tls_compose_uni_dx/
 qed.
 <unwind2_rmap_d_dx >nrplus_inj_dx
 /2 width=1 by tr_tls_compose_uni_dx/
 qed.

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_head.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_head.ma
deleted file mode 100644 (file)
index 416c6e7..0000000
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_head.ma
+++ /dev/null
@@ -1,134 +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/unwind/unwind2_rmap_labels.ma".
-include "delayed_updating/unwind/unwind2_rmap_eq.ma".
-include "delayed_updating/syntax/path_head_depth.ma".
-include "ground/relocation/xap.ma".
-include "ground/lib/stream_eq_eq.ma".
-include "ground/arith/nat_le_plus.ma".
-
-(* TAILED UNWIND FOR RELOCATION MAP *****************************************)
-
-(* Constructions with path_head *********************************************)
-
-lemma unwind2_rmap_head_xap_le_closed (f) (p) (q) (n) (m):
-      q = ↳[n]q → m ≤ n →
-      ▶[f](p●q)＠❨m❩ = ▶[f]↳[n](p●q)＠❨m❩.
-#f #p #q elim q -q
-[ #n #m #Hq
-  <(eq_inv_path_empty_head … Hq) -n #Hm
-  <(nle_inv_zero_dx … Hm) -m //
-| #l #q #IH #n @(nat_ind_succ … n) -n
-  [ #m #_ #Hm <(nle_inv_zero_dx … Hm) -m -IH //
-  | #n #_ #m cases l [ #k ]
-    [ <path_head_d_dx #Hq #Hm
-      elim (eq_inv_list_lcons_bi ????? Hq) -Hq #_ #Hq
-      <unwind2_rmap_d_dx <unwind2_rmap_d_dx
-      <tr_compose_xap <tr_compose_xap
-      @(IH … Hq) -IH -Hq (**) (* auto too slow *)
-      @nle_trans [| @tr_uni_xap ]
-      /2 width=1 by nle_plus_bi_dx/
-    | <path_head_m_dx #Hq #Hm
-      elim (eq_inv_list_lcons_bi ????? Hq) -Hq #_ #Hq
-      <unwind2_rmap_m_dx <unwind2_rmap_m_dx
-      /2 width=2 by/
-    | <path_head_L_dx #Hq
-      @(nat_ind_succ … m) -m // #m #_ #Hm
-      lapply (nle_inv_succ_bi … Hm) -Hm #Hm
-      elim (eq_inv_list_lcons_bi ????? Hq) -Hq #_ #Hq
-      <unwind2_rmap_L_dx <unwind2_rmap_L_dx
-      <tr_xap_push <tr_xap_push
-      /3 width=2 by eq_f/
-    | <path_head_A_dx #Hq #Hm
-      elim (eq_inv_list_lcons_bi ????? Hq) -Hq #_ #Hq
-      <unwind2_rmap_A_dx <unwind2_rmap_A_dx
-      /2 width=2 by/
-    | <path_head_S_dx #Hq #Hm
-      elim (eq_inv_list_lcons_bi ????? Hq) -Hq #_ #Hq
-      <unwind2_rmap_S_dx <unwind2_rmap_S_dx
-      /2 width=2 by/
-    ]
-  ]
-]
-qed-.
-
-lemma unwind2_rmap_head_xap_closed (f) (p) (q) (n):
-      q = ↳[n]q →
-      ▶[f](p●q)＠❨n❩ = ▶[f]↳[n](p●q)＠❨n❩.
-/2 width=2 by unwind2_rmap_head_xap_le_closed/
-qed-.
-
-lemma unwind2_rmap_head_xap (f) (p) (n):
-      n + ♯(↳[n]p) = (▶[f]↳[n]p)＠❨n❩.
-#f #p elim p -p
-[ #n <path_head_empty <unwind2_rmap_labels_L <height_labels_L
-  <tr_xap_pushs_le //
-| #l #p #IH #n @(nat_ind_succ … n) -n //
-  #n #_ cases l [ #k ]
-  [ <unwind2_rmap_d_dx <path_head_d_dx <height_d_dx
-    <nplus_comm in ⊢ (??(??%)?); <nplus_assoc
-    >IH -IH <tr_compose_xap <tr_uni_xap_succ //
-  | <unwind2_rmap_m_dx <path_head_m_dx <height_m_dx //
-  | <unwind2_rmap_L_dx <path_head_L_dx <height_L_dx
-    <tr_xap_push <npred_succ <nplus_succ_sn //
-  | <unwind2_rmap_A_dx <path_head_A_dx <height_A_dx //
-  | <unwind2_rmap_S_dx <path_head_S_dx <height_S_dx //
-  ]
-]
-qed.
-
-lemma unwind2_rmap_append_pap_closed (f) (p) (q) (h:pnat):
-      q = ↳[h]q →
-      ♭q = ninj (▶[f](p●q)＠⧣❨h❩).
-#f #p #q #h #Hh
->tr_xap_ninj >(path_head_refl_append_sn p … Hh) in ⊢ (??%?);
->(unwind2_rmap_head_xap_closed … Hh) -Hh
-<path_head_depth //
-qed.
-
-lemma tls_unwind2_rmap_plus_closed (f) (p) (q) (n) (m):
-      q = ↳[n]q →
-      ⇂*[m]▶[f]p ≗ ⇂*[n+m]▶[f](p●q).
-#f #p #q elim q -q
-[ #n #m #Hq
-  <(eq_inv_path_empty_head … Hq) -n //
-| #l #q #IH #n @(nat_ind_succ … n) -n //
-  #n #_ #m cases l [ #k ]
-  [ <path_head_d_dx #Hq
-    elim (eq_inv_list_lcons_bi ????? Hq) -Hq #_ #Hq <nrplus_inj_sn
-    @(stream_eq_trans … (tls_unwind2_rmap_d_dx …))
-    >nrplus_inj_dx >nrplus_inj_sn >nrplus_inj_sn <nplus_plus_comm_23
-    /2 width=1 by/
-  | <path_head_m_dx #Hq
-    elim (eq_inv_list_lcons_bi ????? Hq) -Hq #_ #Hq
-    <unwind2_rmap_m_sn /2 width=1 by/
-  | <path_head_L_dx #Hq
-    elim (eq_inv_list_lcons_bi ????? Hq) -Hq #_ #Hq
-    <unwind2_rmap_L_dx <nplus_succ_sn /2 width=1 by/
-  | <path_head_A_dx #Hq
-    elim (eq_inv_list_lcons_bi ????? Hq) -Hq #_ #Hq
-    <unwind2_rmap_A_dx /2 width=2 by/
-  | <path_head_S_dx #Hq
-    elim (eq_inv_list_lcons_bi ????? Hq) -Hq #_ #Hq
-    <unwind2_rmap_S_dx /2 width=2 by/
-  ]
-]
-qed-.
-
-lemma tls_unwind2_rmap_closed (f) (p) (q) (n):
-      q = ↳[n]q →
-      ▶[f]p ≗ ⇂*[n]▶[f](p●q).
-/2 width=1 by tls_unwind2_rmap_plus_closed/
-qed.

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_labels.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_labels.ma
deleted file mode 100644 (file)
index d139018..0000000
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_labels.ma
+++ /dev/null
@@ -1,28 +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/unwind/unwind2_rmap.ma".
-include "delayed_updating/syntax/path_labels.ma".
-include "ground/relocation/tr_pushs.ma".
-
-(* TAILED UNWIND FOR RELOCATION MAP *****************************************)
-
-(* Constructions with labels ************************************************)
-
-lemma unwind2_rmap_labels_L (f) (n):
-      (⫯*[n]f) = ▶[f](𝗟∗∗n).
-#f #n @(nat_ind_succ … n) -n //
-#n #IH
-<labels_succ <unwind2_rmap_L_dx //
-qed.