update in delayed_updating

+ ifr_lift proved
+ ifr corrected
+ minor corrections

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 fd5f76b54ba8ff80a7d68ca8f2f9f186112bdba4..92bd90699321b65cf9d5589fb69b21faf0a65060 100644 (file)
--- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_ifr.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_ifr.ma
@@ -18,9 +18,11 @@ include "delayed_updating/reduction/ifr.ma".
 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_rmap_head.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".
@@ -51,9 +53,9 @@ theorem dfr_des_ifr (f) (p) (q) (t1) (t2): t1 ϵ 𝐓 →
   @(subset_eq_trans … (unwind2_term_fsubst …))
   [ @fsubst_eq_repl [ // | // ]
     @(subset_eq_trans … (unwind2_term_iref …))
-    @(subset_eq_canc_sn … (unwind2_term_eq_repl_dx …))
+    @(subset_eq_canc_sn … (lift_term_eq_repl_dx …))
     [ @unwind2_term_grafted_S /2 width=2 by ex_intro/ | skip ] -Ht1
-    @(subset_eq_trans … (unwind2_term_after …))
+    @(subset_eq_trans … (lift_unwind2_term_after …))
     @unwind2_term_eq_repl_sn
 (* Note: crux of the proof begins *)
     @nstream_eq_inv_ext #m

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 f71d6974e2c6d7d939a1a225f906e4f32b5affa1..7273cd780dae13c2dc5359b91efea902d2c0437a 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,7 +17,6 @@ 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/lift_prototerm_eq.ma".
 include "delayed_updating/substitution/lift_path_head.ma".
 include "delayed_updating/substitution/lift_rmap_head.ma".
 

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr.ma
index fcc12edbf1c925c643b3e0839e3e13e41281c18b..8be4493b76a5fb2c9d3e37a2cb04f4e688af55e5 100644 (file)
--- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr.ma
@@ -12,10 +12,11 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "delayed_updating/unwind/unwind2_prototerm.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_reverse.ma".
 include "delayed_updating/notation/relations/black_rightarrow_if_4.ma".
 
 (* IMMEDIATE FOCUSED REDUCTION ************************************************)
@@ -24,7 +25,7 @@ definition ifr (p) (q): relation2 prototerm prototerm ≝
            λt1,t2. ∃n:pnat.
            let r ≝ p●𝗔◗𝗟◗q in
            ∧∧ (𝗟◗q)ᴿ = ↳[n](rᴿ) & r◖𝗱n ϵ t1 &
-              t1[â\8b\94râ\86\90â\96¼[𝐮❨n❩](t1⋔(p◖𝗦))] ⇔ t2
+              t1[â\8b\94râ\86\90â\86\91[𝐮❨n❩](t1⋔(p◖𝗦))] ⇔ t2
 .
 
 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 6d5cb47f0b093dd2a5d0f1fdf7ff6031f308f9ea..6eb354905fe8acd473a52b930d08ba7e72ec7522 100644 (file)
--- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr_lift.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr_lift.ma
@@ -14,14 +14,14 @@
 
 include "delayed_updating/reduction/ifr.ma".
 
-include "delayed_updating/unwind/unwind2_path_lift.ma".
-
 include "delayed_updating/substitution/fsubst_lift.ma".
 include "delayed_updating/substitution/fsubst_eq.ma".
-include "delayed_updating/substitution/lift_prototerm_eq.ma".
 include "delayed_updating/substitution/lift_path_head.ma".
 include "delayed_updating/substitution/lift_rmap_head.ma".
 
+include "ground/relocation/tr_uni_compose.ma".
+include "ground/relocation/tr_compose_eq.ma".
+
 (* IMMEDIATE FOCUSED REDUCTION **********************************************)
 
 (* Constructions with lift **************************************************)
@@ -41,15 +41,16 @@ theorem ifr_lift_bi (f) (p) (q) (t1) (t2):
   @(subset_eq_trans … Ht2) -t2
   @(subset_eq_trans … (lift_term_fsubst …))
   @fsubst_eq_repl [ // | <lift_path_append // ]
-(*  
-  @(subset_eq_trans … (lift_term_iref …))
-  @iref_eq_repl
-  @(subset_eq_canc_sn … (lift_term_grafted_S …))
+  @(subset_eq_canc_sn … (lift_term_eq_repl_dx …))
+  [ @lift_term_grafted_S | skip ]
+  @(subset_eq_trans … (lift_term_after …))
+  @(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 H1n; #H1n >lift_rmap_A_dx
   /2 width=1 by tls_lift_rmap_append_closed/
 (* Note: crux of the proof ends *)
 ]
 qed.
-*)
\ No newline at end of file

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 f05d86db3078678331cd649e9abe405996c383b1..13f6f3fa00dacfd3f309c42d7244165063cc239a 100644 (file)
--- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr_unwind.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr_unwind.ma
@@ -14,15 +14,15 @@
 
 include "delayed_updating/reduction/ifr.ma".
 
-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_inner.ma".
+include "delayed_updating/unwind/unwind2_prototerm_lift.ma".
 include "delayed_updating/unwind/unwind2_rmap_head.ma".
 
 include "delayed_updating/substitution/fsubst_eq.ma".
+include "delayed_updating/substitution/lift_prototerm_proper.ma".
+include "delayed_updating/substitution/lift_prototerm_eq.ma".
 
-include "delayed_updating/syntax/prototerm_proper_inner.ma".
 include "delayed_updating/syntax/path_head_structure.ma".
 include "delayed_updating/syntax/path_structure_depth.ma".
 include "delayed_updating/syntax/path_structure_reverse.ma".
@@ -33,7 +33,7 @@ include "delayed_updating/syntax/path_depth_reverse.ma".
 (* Constructions with unwind ************************************************)
 
 lemma ifr_unwind_bi (f) (p) (q) (t1) (t2):
-      t1 ϵ 𝐓 → t1⋔(p◖𝗦) ⧸≬ 𝐈 →
+      t1 ϵ 𝐓 → t1⋔(p◖𝗦) ϵ 𝐏 →
       t1 ➡𝐢𝐟[p,q] t2 → ▼[f]t1 ➡𝐢𝐟[⊗p,⊗q] ▼[f]t2.
 #f #p #q #t1 #t2 #H1t1 #H2t1
 * #n * #H1n #Ht1 #Ht2
@@ -51,10 +51,10 @@ lemma ifr_unwind_bi (f) (p) (q) (t1) (t2):
   @(subset_eq_trans … Ht2) -t2
   @(subset_eq_trans … (unwind2_term_fsubst …))
   [ @fsubst_eq_repl [ // | // ]
-    @(subset_eq_canc_dx … (unwind2_term_after …))
-    @(subset_eq_canc_sn … (unwind2_term_eq_repl_dx …))
+    @(subset_eq_canc_sn … (lift_term_eq_repl_dx …))
     [ @unwind2_term_grafted_S /2 width=2 by ex_intro/ | skip ] -Ht1
-    @(subset_eq_trans … (unwind2_term_after …))
+    @(subset_eq_trans … (lift_unwind2_term_after …))
+    @(subset_eq_canc_dx … (unwind2_term_after_lift …))
     @unwind2_term_eq_repl_sn
 (* Note: crux of the proof begins *)
     @nstream_eq_inv_ext #m
@@ -68,8 +68,7 @@ lemma ifr_unwind_bi (f) (p) (q) (t1) (t2):
 (* Note: crux of the proof ends *)
   | //
   | /2 width=2 by ex_intro/
-  | @term_proper_outer #H0 (**) (* full auto does not work *)
-    /3 width=2 by unwind2_term_des_inner/
+  | /2 width=6 by lift_term_proper/
   ]
 ]
 qed.

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_path_inner.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_path_inner.ma
deleted file mode 100644 (file)
index 2ec01a2..0000000
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_path_inner.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_path_structure.ma".
-include "delayed_updating/syntax/path_inner.ma".
-
-(* UNWIND FOR PATH **********************************************************)
-
-(* Destructions with inner condition for path *******************************)
-
-lemma unwind2_path_des_inner (f) (p):
-      ▼[f]p ϵ 𝐈 → p ϵ 𝐈.
-#f #p @(list_ind_rcons … p) -p //
-#p * [ #n ] #_ //
-<unwind2_path_d_dx #H0
-elim (pic_inv_d_dx … H0)
-qed-.

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_path_structure.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_path_structure.ma
index f01ac1de75c9cc572d0702351ede4238fc517b4e..9436b0c2aa7521c951e240302dc291dc789307d9 100644 (file)
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_path_structure.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_path_structure.ma
@@ -111,3 +111,13 @@ elim (unwind_gen_inv_append_inner_sn … Hq1 H0) -Hq1 -H0
 <reverse_rcons <list_tl_lcons <unwind2_rmap_append
 @ex3_2_intro [4: |*: // ] <unwind2_path_unfold // (**) (* auto fails *)
 qed-.
+
+(* Destructions with inner condition for path *******************************)
+
+lemma unwind2_path_des_inner (f) (p):
+      ▼[f]p ϵ 𝐈 → p ϵ 𝐈.
+#f #p @(list_ind_rcons … p) -p //
+#p * [ #n ] #_ //
+<unwind2_path_d_dx #H0
+elim (pic_inv_d_dx … H0)
+qed-.

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_prototerm_inner.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_prototerm_inner.ma
index 7cbe69e0cf47e8705469b0e7d89c998eb9cbd4bd..828f9905be6b57891e40278c62d50b8a681a149e 100644 (file)
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_prototerm_inner.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_prototerm_inner.ma
@@ -13,7 +13,7 @@
 (**************************************************************************)
 
 include "delayed_updating/unwind/unwind2_prototerm.ma".
-include "delayed_updating/unwind/unwind2_path_inner.ma".
+include "delayed_updating/unwind/unwind2_path_structure.ma".
 include "ground/lib/subset_overlap.ma".
 
 (* UNWIND FOR PROTOTERM *****************************************************)