update in delayed_updating

+ WIP on dfr_lift_bi
+ 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 839b4fdfad1a2d6028b644edc375af461d56fbf6..17fcd859888ef3d4413bdf10049a5a5e848e6ad7 100644 (file)
--- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_ifr.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_ifr.ma
@@ -21,8 +21,11 @@ include "delayed_updating/substitution/lift_preterm_eq.ma".
 include "delayed_updating/substitution/lift_structure_depth.ma".
 include "delayed_updating/syntax/prototerm_proper_constructors.ma".
 include "delayed_updating/syntax/path_structure_depth.ma".
+include "ground/relocation/tr_uni_compose.ma".
 include "ground/relocation/tr_pap_pushs.ma".
 
+include "ground/lib/stream_eq_eq.ma".
+
 (* DELAYED FOCUSED REDUCTION ************************************************)
 
 lemma dfr_lift_bi (f) (p) (q) (t1) (t2): t1 ϵ 𝐓 →
@@ -38,7 +41,9 @@ lemma dfr_lift_bi (f) (p) (q) (t1) (t2): t1 ϵ 𝐓 →
 | lapply (lift_term_eq_repl_dx f … Ht2) -Ht2 #Ht2
   @(subset_eq_trans … Ht2) -t2
   @(subset_eq_trans … (lift_fsubst …))
-  [ <structure_append <structure_A_sn <structure_append <structure_L_sn
+  [ <lift_rmap_append <lift_rmap_A_sn <lift_rmap_append <lift_rmap_L_sn
+    <structure_append <structure_A_sn <structure_append <structure_L_sn
+    <depth_plus <depth_L_sn <depth_structure <depth_structure
     @fsubst_eq_repl [ // ]
     @(subset_eq_trans … (lift_iref …))
     @(subset_eq_canc_sn … (lift_term_eq_repl_dx …))
@@ -46,6 +51,10 @@ lemma dfr_lift_bi (f) (p) (q) (t1) (t2): t1 ϵ 𝐓 →
     @(subset_eq_trans … (lift_term_after …))
     @(subset_eq_canc_dx … (lift_term_after …))
     @lift_term_eq_repl_sn -t1
+    @(stream_eq_trans … (tr_compose_uni_dx …))
+(*    
+    >nrplus_inj_dx <tr_pap_plus
+*)    
   | //
   | /2 width=2 by ex_intro/
   | //

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 1634678af36ecc77d57b90df7e0b6dddeb4fbab0..a85d74ef16e4f6b1e84a62db74e0119c0fdbd6ac 100644 (file)
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_depth.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_depth.ma
@@ -13,7 +13,7 @@
 (**************************************************************************)
 
 include "delayed_updating/syntax/path.ma".
-include "ground/arith/nat_succ.ma".
+include "ground/arith/nat_plus.ma".
 include "ground/notation/functions/verticalbars_1.ma".
 
 (* DEPTH FOR PATH ***********************************************************)
@@ -40,17 +40,31 @@ interpretation
 lemma depth_empty: 𝟎 = ❘𝐞❘.
 // qed.
 
-lemma depth_d (q) (n): ❘q❘ = ❘𝗱n◗q❘.
+lemma depth_d_sn (q) (n): ❘q❘ = ❘𝗱n◗q❘.
 // qed.
 
-lemma depth_m (q): ❘q❘ = ❘𝗺◗q❘.
+lemma depth_m_sn (q): ❘q❘ = ❘𝗺◗q❘.
 // qed.
 
-lemma depth_L (q): ↑❘q❘ = ❘𝗟◗q❘.
+lemma depth_L_sn (q): ↑❘q❘ = ❘𝗟◗q❘.
 // qed.
 
-lemma depth_A (q): ❘q❘ = ❘𝗔◗q❘.
+lemma depth_A_sn (q): ❘q❘ = ❘𝗔◗q❘.
 // qed.
 
-lemma depth_S (q): ❘q❘ = ❘𝗦◗q❘.
+lemma depth_S_sn (q): ❘q❘ = ❘𝗦◗q❘.
 // qed.
+
+(* Advanced constructions with nplus ****************************************)
+
+lemma depth_plus (p1) (p2):
+      ❘p2❘+❘p1❘ = ❘p1●p2❘.
+#p1 elim p1 -p1 //
+* [ #n ] #p1 #IH #p2 <list_append_lcons_sn
+[ <depth_d_sn <depth_d_sn //
+| <depth_m_sn <depth_m_sn //
+| <depth_L_sn <depth_L_sn //
+| <depth_A_sn <depth_A_sn //
+| <depth_S_sn <depth_S_sn //
+]
+qed.

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_structure_depth.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_structure_depth.ma
index 98583286b013534f56ffed50d27f0888767d13ab..700da6a46e26d3c6e5f8c6b4b3ac0be0425a571c 100644 (file)
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_structure_depth.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_structure_depth.ma
@@ -23,8 +23,8 @@ lemma depth_structure (p):
       ❘p❘ = ❘⊗p❘.
 #p elim p -p //
 * [ #n ] #p #IH //
-[ <structure_L_sn <depth_L <depth_L //
-| <structure_A_sn <depth_A <depth_A //
-| <structure_S_sn <depth_S <depth_S //
+[ <structure_L_sn <depth_L_sn <depth_L_sn //
+| <structure_A_sn <depth_A_sn <depth_A_sn //
+| <structure_S_sn <depth_S_sn <depth_S_sn //
 ]
 qed.