update in delayed_updating

+ guard condition removed from reduction

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/etc/guard/class_g_0.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/guard/class_g_0.etc
new file mode 100644 (file)
index 0000000..c65fcbc
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/etc/guard/class_g_0.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( 𝐆 )"
+  non associative with precedence 70
+  for @{ 'ClassG }.

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/etc/guard/lift_path_guard.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/guard/lift_path_guard.etc
new file mode 100644 (file)
index 0000000..d2be3b3
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/etc/guard/lift_path_guard.etc
@@ -0,0 +1,25 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/lift_path.ma".
+include "delayed_updating/syntax/path_guard.ma".
+
+(* LIFT FOR PATH ************************************************************)
+
+(* Constructions with pgc ***************************************************)
+
+lemma lift_path_guard (f) (p):
+      p ϵ 𝐆 → 🠡[f]p ϵ 𝐆.
+#f #p #H0 elim H0 -p //
+qed.

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/etc/guard/path_closed_guard.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/guard/path_closed_guard.etc
new file mode 100644 (file)
index 0000000..af57be3
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/etc/guard/path_closed_guard.etc
@@ -0,0 +1,49 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/syntax/path_closed.ma".
+include "delayed_updating/syntax/path_guard.ma".
+
+(* CLOSED CONDITION FOR PATH ************************************************)
+
+axiom list_ind_pippo (A) (Q:predicate …):
+      (∀l. (∀m. (∃p. p⨁{A}m = l) → Q m) → Q l) → ∀l. Q l.
+
+(* Destructions with pgc ****************************************************)
+
+lemma path_closed_des_guard (x) (n):
+      x ϵ 𝐂❨Ⓕ,n❩ →
+      ∃∃p,q. p ϵ 𝐆 & q ϵ 𝐂❨Ⓕ,𝟎❩ & p●q = x.
+#x @(list_ind_pippo … x) -x
+#x #IH #n #H0 @(insert_eq_1 … x … H0) -H0
+#y * -y -n
+[|*: #y #n [ #k #_ ] #Hy ] #H0 destruct
+[ /2 width=5 by pgc_empty, pcc_empty, ex3_2_intro/
+| elim (pcc_false_inv_append_bi … Hy) -Hy #r #s #Hr #Hs #H0 destruct
+  elim (IH … Hr) -IH -Hr [| /2 width=2 by ex_intro/ ]
+  #p #q #Hp #Hq #H0 destruct
+  @(ex3_2_intro … Hp) -Hp [1,3: // ]
+  /3 width=2 by pcc_append_bi, pcc_false_d_dx/
+| elim (IH … Hy) -IH -Hy [| /2 width=2 by ex_intro/ ]
+  #p #q #Hp #Hq #H0 destruct
+  /3 width=5 by pcc_m_dx, ex3_2_intro/
+| @(ex3_2_intro … (y◖𝗟) (𝐞)) //
+| elim (IH … Hy) -IH -Hy [| /2 width=2 by ex_intro/ ]
+  #p #q #Hp #Hq #H0 destruct
+  /3 width=5 by pcc_A_dx, ex3_2_intro/
+| elim (IH … Hy) -IH -Hy [| /2 width=2 by ex_intro/ ]
+  #p #q #Hp #Hq #H0 destruct
+  /3 width=5 by pcc_S_dx, ex3_2_intro/
+]
+qed-.

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/etc/guard/path_guard.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/guard/path_guard.etc
new file mode 100644 (file)
index 0000000..65bb510
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/etc/guard/path_guard.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/syntax/path.ma".
+include "delayed_updating/notation/functions/class_g_0.ma".
+include "ground/lib/subset.ma".
+
+(* GUARD CONDITION FOR PATH *************************************************)
+
+inductive pgc: predicate path ≝
+| pgc_empty: (𝐞) ϵ pgc
+| pgc_L_dx (p): p◖𝗟 ϵ pgc
+.
+
+interpretation
+  "guard condition (path)"
+  'ClassG = (pgc).

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/etc/guard/path_guard_structure.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/guard/path_guard_structure.etc
new file mode 100644 (file)
index 0000000..8092cf8
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/etc/guard/path_guard_structure.etc
@@ -0,0 +1,25 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/syntax/path_guard.ma".
+include "delayed_updating/syntax/path_structure.ma".
+
+(* GUARD CONDITION FOR PATH *************************************************)
+
+(* Constructions with structure *********************************************)
+
+lemma path_guard_structure (p):
+      p ϵ 𝐆 → ⊗p ϵ 𝐆.
+#p #H0 elim H0 -p //
+qed.

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/etc/guard/unwind2_rmap_guard.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/guard/unwind2_rmap_guard.etc
new file mode 100644 (file)
index 0000000..bdf8435
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/etc/guard/unwind2_rmap_guard.etc
@@ -0,0 +1,32 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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_guard.ma".
+include "ground/relocation/nap.ma".
+
+(* TAILED UNWIND FOR RELOCATION MAP *****************************************)
+
+(* Destructions with pgc ****************************************************)
+
+lemma unwind2_rmap_push_guard (f) (p):
+      p ϵ 𝐆 → ⫯⇂▶[⫯f]p = ▶[⫯f]p.
+#f #p * //
+qed-.
+
+lemma nap_zero_unwind2_rmap_push_guard (f) (p):
+      p ϵ 𝐆 → 𝟎 = ▶[⫯f]p＠§❨𝟎❩.
+#f #p #Hp
+<(unwind2_rmap_push_guard … Hp) -Hp //
+qed-.

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/etc/reduction/dbfr_constructors.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/reduction/dbfr_constructors.etc
deleted file mode 100644 (file)
index 4dd8610..0000000
--- a/matita/matita/contribs/lambdadelta/delayed_updating/etc/reduction/dbfr_constructors.etc
+++ /dev/null
@@ -1,101 +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/reduction/dbfr.ma".
-include "delayed_updating/substitution/fsubst_constructors.ma".
-include "delayed_updating/substitution/fsubst_eq.ma".
-include "delayed_updating/syntax/prototerm_constructors_eq.ma".
-
-(* DELAYED BALANCED FOCUSED REDUCTION ***************************************)
-
-(* Constructions with constructors for prototerm ****************************)
-
-lemma dbfr_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 // @iref_eq_repl
-  >list_cons_shift @(subset_eq_canc_sn … (grafted_abst_hd … )) //
-]
-qed.
-
-lemma dbfr_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 // @iref_eq_repl
-  >list_cons_shift @(subset_eq_canc_sn … (grafted_appl_hd … )) //
-]
-qed.
-
-lemma dbfr_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 // @iref_eq_repl
-  >list_cons_shift @(subset_eq_canc_sn … (grafted_appl_sd … )) //
-]
-qed.
-
-lemma dbfr_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 @iref_eq_repl
-  >list_cons_comm @(subset_eq_canc_sn … (grafted_appl_sd … ))
-  @(subset_eq_canc_sn … (grafted_empty_dx … )) //
-]
-qed.
-(*
-lemma dbfr_beta_1 (v) (v1) (t) (q) (n):
-      q ϵ 𝐂❨Ⓕ,n❩ → q◖𝗱↑n ϵ t →
-      ＠v.＠v1.𝛌.𝛌.t ➡𝐝𝐛𝐟[𝗔◗𝗔◗𝗟◗𝗟◗q] ＠v.＠v1.𝛌.𝛌.(t[⋔q←🠡[𝐮❨↑↑n❩]v]).
-#v #v1 #t #q #n #Hn #Ht
-@(ex6_5_intro … (𝐞) (𝗔◗𝗟◗𝐞) q (𝟏) … Hn) -Hn
-[ //
-| /2 width=1 by pbc_empty, pbc_redex/
-| /3 width=1 by pcc_A_sn, pcc_L_sn, pcc_empty/
-| /5 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_appl_hd …)) @appl_eq_repl [ // ]
-  @(subset_eq_canc_sn … (fsubst_abst_hd …)) @abst_eq_repl
-  @(subset_eq_canc_sn … (fsubst_abst_hd …)) @abst_eq_repl
-  @fsubst_eq_repl // <nplus_unit_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/etc/reduction/ibfr_constructors.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/reduction/ibfr_constructors.etc
deleted file mode 100644 (file)
index 112a98c..0000000
--- a/matita/matita/contribs/lambdadelta/delayed_updating/etc/reduction/ibfr_constructors.etc
+++ /dev/null
@@ -1,101 +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/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.
-
-lemma ibfr_beta_1 (v) (v1) (t) (q) (n):
-      q ϵ 𝐂❨Ⓕ,n❩ → q◖𝗱↑n ϵ t →
-      ＠v.＠v1.𝛌.𝛌.t ➡𝐢𝐛𝐟[𝗔◗𝗔◗𝗟◗𝗟◗q] ＠v.＠v1.𝛌.𝛌.(t[⋔q←🠡[𝐮❨↑↑n❩]v]).
-#v #v1 #t #q #n #Hn #Ht
-@(ex6_5_intro … (𝐞) (𝗔◗𝗟◗𝐞) q (𝟏) … Hn) -Hn
-[ //
-| /2 width=1 by pbc_empty, pbc_redex/
-| /3 width=1 by pcc_A_sn, pcc_L_sn, pcc_empty/
-| /5 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_appl_hd …)) @appl_eq_repl [ // ]
-  @(subset_eq_canc_sn … (fsubst_abst_hd …)) @abst_eq_repl
-  @(subset_eq_canc_sn … (fsubst_abst_hd …)) @abst_eq_repl
-  @fsubst_eq_repl // <nplus_unit_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/notation/functions/class_g_0.ma b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/class_g_0.ma
deleted file mode 100644 (file)
index c65fcbc..0000000
--- a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/class_g_0.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( 𝐆 )"
-  non associative with precedence 70
-  for @{ 'ClassG }.

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notes.txt b/matita/matita/contribs/lambdadelta/delayed_updating/notes.txt
index 79d8698f97508071bcf21a0da735de3f464f9fd4..079d44d8d9b0eef3f7789fd27d10432a6656e23c 100644 (file)
--- a/matita/matita/contribs/lambdadelta/delayed_updating/notes.txt
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/notes.txt
@@ -8,5 +8,3 @@ lemma pr_pat_after_uni_tls (i2) (i1):
 266D;MUSIC FLAT SIGN;So;0;ON;;;;;N;FLAT;;;;
 266E;MUSIC NATURAL SIGN;So;0;ON;;;;;N;NATURAL;;;;
 266F;MUSIC SHARP SIGN;Sm;0;ON;;;;;N;SHARP;;;;
-
-include "ground/xoa/ex_6_5.ma".

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr.ma
index 66d2a248f98cda484743f9534f079258f9c106ff..776696b24b95b58c6c89bbe84d850ec3927ace77 100644 (file)
--- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr.ma
@@ -17,17 +17,16 @@ include "delayed_updating/syntax/prototerm_constructors.ma".
 include "delayed_updating/syntax/prototerm_eq.ma".
 include "delayed_updating/syntax/path_closed.ma".
 include "delayed_updating/syntax/path_balanced.ma".
-include "delayed_updating/syntax/path_guard.ma".
 include "delayed_updating/syntax/path_structure.ma".
 include "delayed_updating/notation/relations/black_rightarrow_dbf_3.ma".
-include "ground/xoa/ex_7_5.ma".
+include "ground/xoa/ex_6_5.ma".
 
 (* DELAYED BALANCED FOCUSED REDUCTION ***************************************)
 
 definition dbfr (r): relation2 prototerm prototerm ≝
            λt1,t2.
            ∃∃p,b,q,m,n. p●𝗔◗b●𝗟◗q = r &
-           p ϵ 𝐆 & ⊗b ϵ 𝐁 & b ϵ 𝐂❨Ⓕ,m❩ & q ϵ 𝐂❨Ⓕ,n❩ & r◖𝗱↑n ϵ t1 &
+           ⊗b ϵ 𝐁 & b ϵ 𝐂❨Ⓕ,m❩ & q ϵ 𝐂❨Ⓕ,n❩ & r◖𝗱↑n ϵ t1 &
            t1[⋔r←𝛕↑(m+n).(t1⋔(p◖𝗦))] ⇔ t2
 .
 
@@ -40,6 +39,6 @@ interpretation
 lemma dbfr_eq_trans (t) (t1) (t2) (r):
       t1 ➡𝐝𝐛𝐟[r] t → t ⇔ t2 → t1 ➡𝐝𝐛𝐟[r] t2.
 #t #t1 #t2 #r
-* #p #b #q #m #n #Hr #Hp #Hb #Hm #Hn #Ht1 #Ht #Ht2
-/3 width=14 by subset_eq_trans, ex7_5_intro/
+* #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/dbfr_constructors.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr_constructors.ma
new file mode 100644 (file)
index 0000000..f0ffe99
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr_constructors.ma
@@ -0,0 +1,101 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/dbfr.ma".
+include "delayed_updating/substitution/fsubst_constructors.ma".
+include "delayed_updating/substitution/fsubst_eq.ma".
+include "delayed_updating/syntax/prototerm_constructors_eq.ma".
+
+(* DELAYED BALANCED FOCUSED REDUCTION ***************************************)
+
+(* Constructions with constructors for prototerm ****************************)
+
+lemma dbfr_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 // @iref_eq_repl
+  >list_cons_shift @(subset_eq_canc_sn … (grafted_abst_hd … )) //
+]
+qed.
+
+lemma dbfr_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 // @iref_eq_repl
+  >list_cons_shift @(subset_eq_canc_sn … (grafted_appl_hd … )) //
+]
+qed.
+
+lemma dbfr_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 // @iref_eq_repl
+  >list_cons_shift @(subset_eq_canc_sn … (grafted_appl_sd … )) //
+]
+qed.
+
+lemma dbfr_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 @iref_eq_repl
+  >list_cons_comm @(subset_eq_canc_sn … (grafted_appl_sd … ))
+  @(subset_eq_canc_sn … (grafted_empty_dx … )) //
+]
+qed.
+(*
+lemma dbfr_beta_1 (v) (v1) (t) (q) (n):
+      q ϵ 𝐂❨Ⓕ,n❩ → q◖𝗱↑n ϵ t →
+      ＠v.＠v1.𝛌.𝛌.t ➡𝐝𝐛𝐟[𝗔◗𝗔◗𝗟◗𝗟◗q] ＠v.＠v1.𝛌.𝛌.(t[⋔q←𝛕↑↑n.v]).
+#v #v1 #t #q #n #Hn #Ht
+@(ex6_5_intro … (𝐞) (𝗔◗𝗟◗𝐞) q (𝟏) … Hn) -Hn
+[ //
+| /2 width=1 by pbc_empty, pbc_redex/
+| /3 width=1 by pcc_A_sn, pcc_L_sn, pcc_empty/
+| /5 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_appl_hd …)) @appl_eq_repl [ // ]
+  @(subset_eq_canc_sn … (fsubst_abst_hd …)) @abst_eq_repl
+  @(subset_eq_canc_sn … (fsubst_abst_hd …)) @abst_eq_repl
+  @fsubst_eq_repl // <nplus_unit_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/reduction/dbfr_ibfr.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr_ibfr.ma
index 572b250977bdac25373c6dc2258f03623784e0c1..387dc8f1562b89a3c7d8cafe19a00ed860455267 100644 (file)
--- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr_ibfr.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr_ibfr.ma
@@ -13,32 +13,40 @@
 (**************************************************************************)
 
 include "delayed_updating/reduction/dbfr.ma".
-include "delayed_updating/reduction/ibfr_unwind.ma".
+include "delayed_updating/reduction/ibfr.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".
+include "delayed_updating/unwind/unwind2_rmap_crux.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_closed_structure.ma".
+include "delayed_updating/syntax/path_structure_depth.ma".
 
 (* DELAYED BALANCED FOCUSED REDUCTION ***************************************)
 
 (* Main destructions with ibfr **********************************************)
 
-theorem dbfr_des_ibfr_push (f) (t1) (t2) (r): t1 ϵ 𝐓 →
-        t1 ➡𝐝𝐛𝐟[r] t2 → ▼[⫯f]t1 ➡𝐢𝐛𝐟[⊗r] ▼[⫯f]t2.
+theorem dbfr_des_ibfr (f) (t1) (t2) (r): t1 ϵ 𝐓 →
+        t1 ➡𝐝𝐛𝐟[r] t2 → ▼[f]t1 ➡𝐢𝐛𝐟[⊗r] ▼[f]t2.
 #f #t1 #t2 #r #H0t1
-* #p #b #q #m #n #Hr #Hp #Hb #Hm #Hn #Ht1 #Ht2 destruct
-@(ex7_5_intro … (⊗p) (⊗b) (⊗q) (♭b) (♭q))
-[ -H0t1 -Hp -Hb -Hm -Hn -Ht1 -Ht2 //
-| -H0t1 -Hb -Hm -Hn -Ht1 -Ht2 /2 width=1 by path_guard_structure/
-| -H0t1 -Hp -Hm -Hn -Ht1 -Ht2 //
-| -H0t1 -Hp -Hb -Hn -Ht1 -Ht2
+* #p #b #q #m #n #Hr #Hb #Hm #Hn #Ht1 #Ht2 destruct
+@(ex6_5_intro … (⊗p) (⊗b) (⊗q) (♭b) (♭q))
+[ -H0t1 -Hb -Hm -Hn -Ht1 -Ht2 //
+| -H0t1 -Hm -Hn -Ht1 -Ht2 //
+| -H0t1 -Hb -Hn -Ht1 -Ht2
   /2 width=2 by path_closed_structure_depth/
-| -H0t1 -Hp -Hb -Hm -Ht1 -Ht2
+| -H0t1 -Hb -Hm -Ht1 -Ht2
   /2 width=2 by path_closed_structure_depth/
-| lapply (in_comp_unwind2_path_term (⫯f) … Ht1) -H0t1 -Hp -Hb -Hm -Ht2 -Ht1
+| lapply (in_comp_unwind2_path_term f … Ht1) -H0t1 -Hb -Hm -Ht2 -Ht1
   <unwind2_path_d_dx <tr_pap_succ_nap >list_append_rcons_dx >list_append_assoc
   <nap_unwind2_rmap_append_closed_Lq_dx //
-| lapply (unwind2_term_eq_repl_dx (⫯f) … Ht2) -Ht2 #Ht2
+| 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 [ // | // ]
@@ -56,10 +64,3 @@ theorem dbfr_des_ibfr_push (f) (t1) (t2) (r): t1 ϵ 𝐓 →
   ]
 ]
 qed-.
-
-theorem dbfr_des_ibfr (f) (t1) (t2) (r): t1 ϵ 𝐓 →
-        t1 ➡𝐝𝐛𝐟[r] t2 → ▼[f]t1 ➡𝐢𝐛𝐟[⊗r] ▼[f]t2.
-#f #t1 #t2 #r #Ht1 #Ht12
-lapply (dbfr_des_ibfr_push (𝐢) … Ht1 Ht12) -Ht1 -Ht12 #Ht12
-/2 width=1 by ibfr_structure_unwind_bi/
-qed.

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 e1446df2df8328ed1aaeeffbf3946da82b8bbfa2..1f5c35a851d9c29726a1af037bc105c0a6361480 100644 (file)
--- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr_lift.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr_lift.ma
@@ -19,7 +19,6 @@ include "delayed_updating/substitution/fsubst_eq.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_path_guard.ma".
 include "delayed_updating/substitution/lift_rmap_closed.ma".
 
 (* DELAYED BALANCED FOCUSED REDUCTION ***************************************)
@@ -29,19 +28,17 @@ include "delayed_updating/substitution/lift_rmap_closed.ma".
 theorem dbfr_lift_bi (f) (t1) (t2) (r):
         t1 ➡𝐝𝐛𝐟[r] t2 → 🠡[f]t1 ➡𝐝𝐛𝐟[🠡[f]r] 🠡[f]t2.
 #f #t1 #t2 #r
-* #p #b #q #m #n #Hr #Hp #Hb #Hm #Hn #Ht1 #Ht2 destruct
-@(ex7_5_intro … (🠡[f]p) (🠡[🠢[f](p◖𝗔)]b) (🠡[🠢[f](p◖𝗔●b◖𝗟)]q) (🠢[f](p●𝗔◗b)＠❨m❩) (🠢[f](p●𝗔◗b●𝗟◗q)＠§❨n❩))
-[ -Hp -Hb -Hm -Hn -Ht1 -Ht2 //
-| -Hb -Hm -Hn -Ht1 -Ht2
-  /2 width=1 by lift_path_guard/
-| -Hp -Hm -Hn -Ht1 -Ht2 //
-| -Hp -Hb -Hn -Ht1 -Ht2
+* #p #b #q #m #n #Hr #Hb #Hm #Hn #Ht1 #Ht2 destruct
+@(ex6_5_intro … (🠡[f]p) (🠡[🠢[f](p◖𝗔)]b) (🠡[🠢[f](p◖𝗔●b◖𝗟)]q) (🠢[f](p●𝗔◗b)＠❨m❩) (🠢[f](p●𝗔◗b●𝗟◗q)＠§❨n❩))
+[ -Hb -Hm -Hn -Ht1 -Ht2 //
+| -Hm -Hn -Ht1 -Ht2 //
+| -Hb -Hn -Ht1 -Ht2
   /2 width=1 by lift_path_closed/
-| -Hp -Hb -Hm -Ht1 -Ht2
+| -Hb -Hm -Ht1 -Ht2
   /2 width=1 by lift_path_rmap_closed_L/
-| lapply (in_comp_lift_path_term f … Ht1) -Ht2 -Ht1 -Hn -Hp
+| 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 -Hp
+| 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 [ // | // ]
@@ -51,6 +48,7 @@ theorem dbfr_lift_bi (f) (t1) (t2) (r):
   @iref_eq_repl
   @(subset_eq_canc_sn … (lift_term_grafted_S …))
   @lift_term_eq_repl_sn
+(* 🠢[f]p ≗ ⇂*[↑(m+n)]🠢[f](((p◖𝗔)●b)●𝗟◗q) *)
 (* Note: crux of the proof begins *)
   >lift_rmap_A_dx
   /2 width=2 by tls_succ_plus_lift_rmap_append_closed_bLq_dx/

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ibfr.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ibfr.ma
index 974ceba5c8b6758c8a745c870c75625c85e59d50..700440011926ecc3fc22b55c9f5d69af4d7d107c 100644 (file)
--- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ibfr.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ibfr.ma
@@ -17,18 +17,17 @@ include "delayed_updating/substitution/lift_prototerm.ma".
 include "delayed_updating/syntax/prototerm_eq.ma".
 include "delayed_updating/syntax/path_closed.ma".
 include "delayed_updating/syntax/path_balanced.ma".
-include "delayed_updating/syntax/path_guard.ma".
 include "delayed_updating/syntax/path_structure.ma".
 include "delayed_updating/notation/relations/black_rightarrow_ibf_3.ma".
 include "ground/relocation/tr_uni.ma".
-include "ground/xoa/ex_7_5.ma".
+include "ground/xoa/ex_6_5.ma".
 
 (* IMMEDIATE BALANCED FOCUSED REDUCTION *************************************)
 
 definition ibfr (r): relation2 prototerm prototerm ≝
            λt1,t2.
            ∃∃p,b,q,m,n. p●𝗔◗b●𝗟◗q = r &
-           p ϵ 𝐆 & ⊗b ϵ 𝐁 & b ϵ 𝐂❨Ⓕ,m❩ & q ϵ 𝐂❨Ⓕ,n❩ & r◖𝗱↑n ϵ t1 &
+           ⊗b ϵ 𝐁 & b ϵ 𝐂❨Ⓕ,m❩ & q ϵ 𝐂❨Ⓕ,n❩ & r◖𝗱↑n ϵ t1 &
            t1[⋔r←🠡[𝐮❨↑(m+n)❩](t1⋔(p◖𝗦))] ⇔ t2
 .
 
@@ -41,6 +40,6 @@ interpretation
 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#Hp #Hb #Hm #Hn #Ht1 #Ht #Ht2
-/3 width=14 by subset_eq_trans, ex7_5_intro/
+* #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 (file)
index 0000000..112a98c
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ibfr_constructors.ma
@@ -0,0 +1,101 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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.
+
+lemma ibfr_beta_1 (v) (v1) (t) (q) (n):
+      q ϵ 𝐂❨Ⓕ,n❩ → q◖𝗱↑n ϵ t →
+      ＠v.＠v1.𝛌.𝛌.t ➡𝐢𝐛𝐟[𝗔◗𝗔◗𝗟◗𝗟◗q] ＠v.＠v1.𝛌.𝛌.(t[⋔q←🠡[𝐮❨↑↑n❩]v]).
+#v #v1 #t #q #n #Hn #Ht
+@(ex6_5_intro … (𝐞) (𝗔◗𝗟◗𝐞) q (𝟏) … Hn) -Hn
+[ //
+| /2 width=1 by pbc_empty, pbc_redex/
+| /3 width=1 by pcc_A_sn, pcc_L_sn, pcc_empty/
+| /5 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_appl_hd …)) @appl_eq_repl [ // ]
+  @(subset_eq_canc_sn … (fsubst_abst_hd …)) @abst_eq_repl
+  @(subset_eq_canc_sn … (fsubst_abst_hd …)) @abst_eq_repl
+  @fsubst_eq_repl // <nplus_unit_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/reduction/ibfr_eq.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ibfr_eq.ma
index 0d569e6df401615998a6a2424c4982ae62e8c004..973a4570fa187554fb10cbb094c16b07c432c227 100644 (file)
--- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ibfr_eq.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ibfr_eq.ma
@@ -23,8 +23,8 @@ include "delayed_updating/substitution/lift_prototerm_eq.ma".
 lemma ibfr_eq_canc_sn (t) (t1) (t2) (r):
       t ⇔ t1 → t ➡𝐢𝐛𝐟[r] t2 → t1 ➡𝐢𝐛𝐟[r] t2.
 #t #t1 #t2 #r #Ht1
-* #p #b #q #m #n #Hr#Hp #Hb #Hm #Hn #Ht #Ht2 destruct
-@(ex7_5_intro … Hp Hb Hm Hn) [ // ] -Hp -Hb -Hm -Hn
+* #p #b #q #m #n #Hr #Hb #Hm #Hn #Ht #Ht2 destruct
+@(ex6_5_intro … p … Hb Hm Hn) [ // ] -Hb -Hm -Hn
 [ /2 width=3 by subset_in_eq_repl_back/
 | /5 width=3 by subset_eq_canc_sn, fsubst_eq_repl, lift_term_eq_repl_dx, grafted_eq_repl/
 ]

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ibfr_lift.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ibfr_lift.ma
index 1b6bb9903a4ce30e9f758b585ed7de5deb550a3e..e08f3d41907c481d7f7c62a61314101ba1a6197a 100644 (file)
--- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ibfr_lift.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ibfr_lift.ma
@@ -19,7 +19,6 @@ include "delayed_updating/substitution/fsubst_eq.ma".
 include "delayed_updating/substitution/lift_prototerm_after.ma".
 include "delayed_updating/substitution/lift_path_structure.ma".
 include "delayed_updating/substitution/lift_path_closed.ma".
-include "delayed_updating/substitution/lift_path_guard.ma".
 include "delayed_updating/substitution/lift_rmap_closed.ma".
 
 include "ground/relocation/tr_uni_compose.ma".
@@ -32,19 +31,17 @@ include "ground/relocation/tr_compose_eq.ma".
 theorem ibfr_lift_bi (f) (t1) (t2) (r):
         t1 ➡𝐢𝐛𝐟[r] t2 → 🠡[f]t1 ➡𝐢𝐛𝐟[🠡[f]r] 🠡[f]t2.
 #f #t1 #t2 #r
-* #p #b #q #m #n #Hr #Hp #Hb #Hm #Hn #Ht1 #Ht2 destruct
-@(ex7_5_intro … (🠡[f]p) (🠡[🠢[f](p◖𝗔)]b) (🠡[🠢[f](p◖𝗔●b◖𝗟)]q) (🠢[f](p●𝗔◗b)＠❨m❩) (🠢[f](p●𝗔◗b●𝗟◗q)＠§❨n❩))
-[ -Hp -Hb -Hm -Hn -Ht1 -Ht2 //
-| -Hb -Hm -Hn -Ht1 -Ht2
-  /2 width=1 by lift_path_guard/
-| -Hp -Hm -Hn -Ht1 -Ht2 //
-| -Hp -Hb -Hn -Ht1 -Ht2
+* #p #b #q #m #n #Hr #Hb #Hm #Hn #Ht1 #Ht2 destruct
+@(ex6_5_intro … (🠡[f]p) (🠡[🠢[f](p◖𝗔)]b) (🠡[🠢[f](p◖𝗔●b◖𝗟)]q) (🠢[f](p●𝗔◗b)＠❨m❩) (🠢[f](p●𝗔◗b●𝗟◗q)＠§❨n❩))
+[ -Hb -Hm -Hn -Ht1 -Ht2 //
+| -Hm -Hn -Ht1 -Ht2 //
+| -Hb -Hn -Ht1 -Ht2
   /2 width=1 by lift_path_closed/
-| -Hp -Hb -Hm -Ht1 -Ht2
+| -Hb -Hm -Ht1 -Ht2
   /2 width=1 by lift_path_rmap_closed_L/
-| lapply (in_comp_lift_path_term f … Ht1) -Ht2 -Ht1 -Hp -Hn
+| 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 -Hp
+| 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_append // ]
@@ -53,6 +50,7 @@ theorem ibfr_lift_bi (f) (t1) (t2) (r):
   @(subset_eq_trans … (lift_term_after …))
   @(subset_eq_canc_dx … (lift_term_after …))
   @lift_term_eq_repl_sn
+(* 𝐮❨ ↑(🠢[f](p●𝗔◗b)＠❨m❩ + 🠢[f](p●𝗔◗b●𝗟◗q)＠§❨n❩) ❩ ∘ 🠢[f]p ≗ 🠢[f](p●𝗔◗b●𝗟◗q) ∘ 𝐮❨↑(m+n)❩ *)
 (* Note: crux of the proof begins *)
   @(stream_eq_trans … (tr_compose_uni_dx_pap …)) <tr_pap_succ_nap
   @tr_compose_eq_repl

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ibfr_unwind.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ibfr_unwind.ma
index 952ef252b7710982fe0d4d903b2e5679cc4f4bbd..34feec2432c419cfa282e917b6c92e56f71aaeb8 100644 (file)
--- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ibfr_unwind.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ibfr_unwind.ma
@@ -12,50 +12,39 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "delayed_updating/reduction/ibfr_lift.ma".
-include "delayed_updating/reduction/ibfr_eq.ma".
+include "delayed_updating/reduction/ibfr.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_crux.ma".
 
+include "delayed_updating/substitution/fsubst_eq.ma".
+include "delayed_updating/substitution/lift_prototerm_eq.ma".
+
 include "delayed_updating/syntax/path_closed_structure.ma".
-include "delayed_updating/syntax/path_guard_structure.ma".
 include "delayed_updating/syntax/path_structure_depth.ma".
 
 (* IMMEDIATE BALANCED FOCUSED REDUCTION *************************************)
 
 (* Constructions with unwind2 ***********************************************)
 
-lemma ibfr_structure_unwind_bi (f) (t1) (t2) (r):
-      ▼[⫯𝐢]t1 ➡𝐢𝐛𝐟[⊗r] ▼[⫯𝐢]t2 → ▼[f]t1 ➡𝐢𝐛𝐟[⊗r] ▼[f]t2.
-#f #t1 #t2 #r #Ht12
-lapply (ibfr_lift_bi (f) … Ht12) -Ht12
-<lift_path_structure #Ht12
-@(ibfr_eq_repl … Ht12) -r
-@(subset_eq_canc_dx … (lift_unwind2_term_after …))
-@unwind2_term_eq_repl_sn -t1 -t2 //
-qed-.
-
-lemma ibfr_unwind_bi_push (f) (t1) (t2) (r):
+lemma ibfr_unwind_bi (f) (t1) (t2) (r):
       t1 ϵ 𝐓 → r ϵ 𝐈 →
-      t1 ➡𝐢𝐛𝐟[r] t2 → ▼[⫯f]t1 ➡𝐢𝐛𝐟[⊗r] ▼[⫯f]t2.
+      t1 ➡𝐢𝐛𝐟[r] t2 → ▼[f]t1 ➡𝐢𝐛𝐟[⊗r] ▼[f]t2.
 #f #t1 #t2 #r #H1t1 #H2r
-* #p #b #q #m #n #Hr #Hp #Hb #Hm #Hn #Ht1 #Ht2 destruct
-@(ex7_5_intro … (⊗p) (⊗b) (⊗q) (♭b) (♭q))
-[ -H1t1 -H2r -Hp -Hb -Hm -Hn -Ht1 -Ht2 //
-| -H1t1 -H2r -Hb -Hm -Hn -Ht1 -Ht2
-  /2 width=1 by path_guard_structure/
-| -H1t1 -H2r -Hp -Hm -Hn -Ht1 -Ht2 //
-| -H1t1 -H2r -Hp -Hb -Hn -Ht1 -Ht2
+* #p #b #q #m #n #Hr #Hb #Hm #Hn #Ht1 #Ht2 destruct
+@(ex6_5_intro … (⊗p) (⊗b) (⊗q) (♭b) (♭q))
+[ -H1t1 -H2r -Hb -Hm -Hn -Ht1 -Ht2 //
+| -H1t1 -H2r -Hm -Hn -Ht1 -Ht2 //
+| -H1t1 -H2r -Hb -Hn -Ht1 -Ht2
   /2 width=2 by path_closed_structure_depth/
-| -H1t1 -H2r -Hp -Hb -Hm -Ht1 -Ht2
+| -H1t1 -H2r -Hb -Hm -Ht1 -Ht2
   /2 width=2 by path_closed_structure_depth/
-| lapply (in_comp_unwind2_path_term (⫯f) … Ht1) -Ht2 -Ht1 -H1t1 -H2r -Hp -Hb
+| lapply (in_comp_unwind2_path_term f … Ht1) -Ht2 -Ht1 -H1t1 -H2r -Hb
   <unwind2_path_d_dx <tr_pap_succ_nap <list_append_rcons_sn >list_append_assoc
   <nap_unwind2_rmap_append_closed_Lq_dx //
-| lapply (unwind2_term_eq_repl_dx (⫯f) … Ht2) -Ht2 #Ht2
+| lapply (unwind2_term_eq_repl_dx f … Ht2) -Ht2 #Ht2
   @(subset_eq_trans … Ht2) -t2
   @(subset_eq_trans … (unwind2_term_fsubst_pic …))
   [ @fsubst_eq_repl [ // | // ]
@@ -73,11 +62,3 @@ lemma ibfr_unwind_bi_push (f) (t1) (t2) (r):
   ]
 ]
 qed-.
-
-lemma ibfr_unwind_bi (f) (t1) (t2) (r):
-      t1 ϵ 𝐓 → r ϵ 𝐈 →
-      t1 ➡𝐢𝐛𝐟[r] t2 → ▼[f]t1 ➡𝐢𝐛𝐟[⊗r] ▼[f]t2.
-#f #t1 #t2 #r #Ht1 #Hr #Ht12
-lapply (ibfr_unwind_bi_push (𝐢) … Ht1 Hr Ht12) -Ht1 -Hr -Ht12 #Ht12
-/2 width=1 by ibfr_structure_unwind_bi/
-qed.

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_path_guard.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_path_guard.ma
deleted file mode 100644 (file)
index d2be3b3..0000000
--- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_path_guard.ma
+++ /dev/null
@@ -1,25 +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/substitution/lift_path.ma".
-include "delayed_updating/syntax/path_guard.ma".
-
-(* LIFT FOR PATH ************************************************************)
-
-(* Constructions with pgc ***************************************************)
-
-lemma lift_path_guard (f) (p):
-      p ϵ 𝐆 → 🠡[f]p ϵ 𝐆.
-#f #p #H0 elim H0 -p //
-qed.

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_rmap_structure.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_rmap_structure.ma
new file mode 100644 (file)
index 0000000..32b3924
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_rmap_structure.ma
@@ -0,0 +1,32 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/lift_rmap.ma".
+include "delayed_updating/syntax/path_structure.ma".
+include "delayed_updating/syntax/path_depth.ma".
+include "ground/relocation/tr_pushs.ma".
+
+(* LIFT FOR RELOCATION MAP **************************************************)
+
+(* Constructions with structure *********************************************)
+
+lemma lift_rmap_structure (f) (q):
+      (⫯*[♭q]f) = 🠢[f]⊗q.
+#f #q elim q -q //
+* [ #k ] #q #IH //
+[ <depth_L_dx <tr_pushs_succ <structure_L_dx <lift_rmap_L_dx //
+| <depth_A_dx <structure_A_dx <lift_rmap_A_dx //
+| <depth_S_dx <structure_S_dx <lift_rmap_S_dx //
+]
+qed.

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_closed_guard.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_closed_guard.ma
deleted file mode 100644 (file)
index af57be3..0000000
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_closed_guard.ma
+++ /dev/null
@@ -1,49 +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/syntax/path_closed.ma".
-include "delayed_updating/syntax/path_guard.ma".
-
-(* CLOSED CONDITION FOR PATH ************************************************)
-
-axiom list_ind_pippo (A) (Q:predicate …):
-      (∀l. (∀m. (∃p. p⨁{A}m = l) → Q m) → Q l) → ∀l. Q l.
-
-(* Destructions with pgc ****************************************************)
-
-lemma path_closed_des_guard (x) (n):
-      x ϵ 𝐂❨Ⓕ,n❩ →
-      ∃∃p,q. p ϵ 𝐆 & q ϵ 𝐂❨Ⓕ,𝟎❩ & p●q = x.
-#x @(list_ind_pippo … x) -x
-#x #IH #n #H0 @(insert_eq_1 … x … H0) -H0
-#y * -y -n
-[|*: #y #n [ #k #_ ] #Hy ] #H0 destruct
-[ /2 width=5 by pgc_empty, pcc_empty, ex3_2_intro/
-| elim (pcc_false_inv_append_bi … Hy) -Hy #r #s #Hr #Hs #H0 destruct
-  elim (IH … Hr) -IH -Hr [| /2 width=2 by ex_intro/ ]
-  #p #q #Hp #Hq #H0 destruct
-  @(ex3_2_intro … Hp) -Hp [1,3: // ]
-  /3 width=2 by pcc_append_bi, pcc_false_d_dx/
-| elim (IH … Hy) -IH -Hy [| /2 width=2 by ex_intro/ ]
-  #p #q #Hp #Hq #H0 destruct
-  /3 width=5 by pcc_m_dx, ex3_2_intro/
-| @(ex3_2_intro … (y◖𝗟) (𝐞)) //
-| elim (IH … Hy) -IH -Hy [| /2 width=2 by ex_intro/ ]
-  #p #q #Hp #Hq #H0 destruct
-  /3 width=5 by pcc_A_dx, ex3_2_intro/
-| elim (IH … Hy) -IH -Hy [| /2 width=2 by ex_intro/ ]
-  #p #q #Hp #Hq #H0 destruct
-  /3 width=5 by pcc_S_dx, ex3_2_intro/
-]
-qed-.

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_guard.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_guard.ma
deleted file mode 100644 (file)
index 65bb510..0000000
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_guard.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/syntax/path.ma".
-include "delayed_updating/notation/functions/class_g_0.ma".
-include "ground/lib/subset.ma".
-
-(* GUARD CONDITION FOR PATH *************************************************)
-
-inductive pgc: predicate path ≝
-| pgc_empty: (𝐞) ϵ pgc
-| pgc_L_dx (p): p◖𝗟 ϵ pgc
-.
-
-interpretation
-  "guard condition (path)"
-  'ClassG = (pgc).

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_guard_structure.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_guard_structure.ma
deleted file mode 100644 (file)
index 8092cf8..0000000
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_guard_structure.ma
+++ /dev/null
@@ -1,25 +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/syntax/path_guard.ma".
-include "delayed_updating/syntax/path_structure.ma".
-
-(* GUARD CONDITION FOR PATH *************************************************)
-
-(* Constructions with structure *********************************************)
-
-lemma path_guard_structure (p):
-      p ϵ 𝐆 → ⊗p ϵ 𝐆.
-#p #H0 elim H0 -p //
-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
index 7dd546a81e61feda56cca9bca770dcb672079ee0..55a1c3a288629cde9f745af4453b63c162b90ffc 100644 (file)
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_closed.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_closed.ma
@@ -12,10 +12,13 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "delayed_updating/unwind/unwind2_rmap_lift.ma".
 include "delayed_updating/unwind/unwind2_rmap_eq.ma".
+include "delayed_updating/substitution/lift_rmap_structure.ma".
 include "delayed_updating/syntax/path_closed.ma".
 include "delayed_updating/syntax/path_depth.ma".
 include "ground/relocation/nap.ma".
+include "ground/relocation/tr_pushs_tls.ma".
 include "ground/lib/stream_tls_plus.ma".
 include "ground/lib/stream_eq_eq.ma".
 
@@ -35,6 +38,13 @@ lemma nap_plus_unwind2_rmap_closed (o) (f) (q) (m) (n):
 ]
 qed-.
 
+lemma nap_unwind2_rmap_closed (o) (f) (q) (n):
+      q ϵ 𝐂❨o,n❩ →
+      f＠§❨𝟎❩+♭q = ▶[f]q＠§❨n❩.
+#o #f #q #n #Hn
+/2 width=2 by nap_plus_unwind2_rmap_closed/
+qed-.
+
 lemma nap_plus_unwind2_rmap_append_closed_Lq_dx (o) (f) (p) (q) (m) (n):
       q ϵ 𝐂❨o,n❩ →
       (⫯▶[f]p)＠§❨m❩+♭q = ▶[f](p●𝗟◗q)＠§❨m+n❩.
@@ -62,7 +72,7 @@ qed-.
 
 lemma tls_succ_unwind2_rmap_push_closed (o) (f) (q) (n):
       q ϵ 𝐂❨o,n❩ →
-      f ≗ ⇂*[↑n]▶[⫯f](q).
+      f ≗ ⇂*[↑n]▶[⫯f]q.
 #o #f #q #n #Hn
 /2 width=2 by tls_succ_plus_unwind2_rmap_push_closed/
 qed-.
@@ -73,3 +83,19 @@ lemma tls_succ_plus_unwind2_rmap_append_closed_Lq_dx (o) (f) (p) (q) (n):
 #o #f #p #q #n #Hn #m
 /2 width=2 by tls_succ_plus_unwind2_rmap_push_closed/
 qed-.
+
+lemma tls_succ_unwind2_rmap_closed (f) (q) (n):
+      q ϵ 𝐂❨Ⓕ,n❩ →
+      ⇂f ≗ ⇂*[↑n]▶[f]q.
+#f #q #n #Hn
+@(stream_eq_canc_dx … (stream_tls_eq_repl …))
+[| @(unwind2_rmap_eq_repl … (tr_compose_id_dx …)) | skip ]
+@(stream_eq_trans … (stream_tls_eq_repl …))
+[| @(lift_unwind2_rmap_after … ) | skip ]
+<tr_compose_tls <tr_id_unfold
+@(stream_eq_trans … (tr_compose_eq_repl …))
+[| @(tls_succ_unwind2_rmap_push_closed … Hn) | skip | // | skip ]
+@(stream_eq_trans ????? (tr_compose_id_dx …))
+<tr_pap_succ_nap <(nap_unwind2_rmap_closed … Hn) <nplus_zero_sn
+<lift_rmap_structure <stream_tls_succ <tr_tls_pushs //
+qed-.

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_crux.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_crux.ma
index c919221daa3728c37023e5d9cc6f6a04906154b5..32bc5f59469c34f53095483bd75cf285d9b5b3a1 100644 (file)
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_crux.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_crux.ma
@@ -13,7 +13,6 @@
 (**************************************************************************)
 
 include "delayed_updating/unwind/unwind2_rmap_closed.ma".
-include "delayed_updating/unwind/unwind2_rmap_guard.ma".
 
 (* TAILED UNWIND FOR RELOCATION MAP *****************************************)
 
@@ -21,9 +20,9 @@ include "delayed_updating/unwind/unwind2_rmap_guard.ma".
 
 (* Note: crux of the commutation between unwind and balanced focused reduction *)
 lemma unwind2_rmap_uni_crux (f) (p) (b) (q) (m) (n):
-      p ϵ 𝐆 → b ϵ 𝐂❨Ⓕ,m❩ → q ϵ 𝐂❨Ⓕ,n❩ →
-      (𝐮❨↑(♭b+♭q)❩ ∘ ▶[⫯f]p ≗ ▶[⫯f](p●𝗔◗b●𝗟◗q) ∘ 𝐮❨↑(m+n)❩).
-#f #p #b #q #m #n #Hp #Hm #Hn
+      b ϵ 𝐂❨Ⓕ,m❩ → q ϵ 𝐂❨Ⓕ,n❩ →
+      (𝐮❨↑(♭b+♭q)❩ ∘ ▶[f]p ≗ ▶[f](p●𝗔◗b●𝗟◗q) ∘ 𝐮❨↑(m+n)❩).
+#f #p #b #q #m #n #Hm #Hn
 <list_append_rcons_sn <list_append_rcons_sn >list_append_assoc
 >list_append_rcons_sn >(list_append_rcons_sn … b)
 @(stream_eq_trans … (tr_compose_uni_dx_pap …)) <tr_pap_succ_nap
@@ -33,14 +32,12 @@ lemma unwind2_rmap_uni_crux (f) (p) (b) (q) (m) (n):
 ] -Hn
 @tr_eq_inv_nap_zero_tl_bi
 [ <tr_compose_nap <tr_compose_nap <tr_uni_nap <tr_uni_nap
-  <nap_zero_unwind2_rmap_push_guard // <nplus_zero_sn
-  >nsucc_unfold >nplus_succ_dx >nplus_succ_dx <nplus_assoc
-  >tr_nap_plus_dx <unwind2_rmap_append
-  <nap_plus_unwind2_rmap_closed [|*: /2 width=2 by pcc_A_sn/ ]
-  <nap_zero_unwind2_rmap_push_guard //
+  >nsucc_unfold >nplus_succ_dx >nplus_succ_dx <nplus_assoc <nplus_assoc
+  >tr_nap_plus_dx <unwind2_rmap_append <nap_plus_unwind2_rmap_closed
+  /2 width=2 by pcc_A_sn/
 | @(stream_eq_canc_sn … (tr_tl_compose_uni_sn …))
   @(stream_eq_trans ????? (tr_tl_compose_uni_sn …))
-  >stream_tls_succ <unwind2_rmap_append <unwind2_rmap_push_guard
-  /2 width=2 by tls_succ_plus_unwind2_rmap_push_closed/
+  >stream_tls_succ <unwind2_rmap_append
+  /3 width=2 by tls_succ_unwind2_rmap_closed, pcc_A_sn/
 ]
 qed-.

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_guard.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_guard.ma
deleted file mode 100644 (file)
index bdf8435..0000000
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_guard.ma
+++ /dev/null
@@ -1,32 +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_guard.ma".
-include "ground/relocation/nap.ma".
-
-(* TAILED UNWIND FOR RELOCATION MAP *****************************************)
-
-(* Destructions with pgc ****************************************************)
-
-lemma unwind2_rmap_push_guard (f) (p):
-      p ϵ 𝐆 → ⫯⇂▶[⫯f]p = ▶[⫯f]p.
-#f #p * //
-qed-.
-
-lemma nap_zero_unwind2_rmap_push_guard (f) (p):
-      p ϵ 𝐆 → 𝟎 = ▶[⫯f]p＠§❨𝟎❩.
-#f #p #Hp
-<(unwind2_rmap_push_guard … Hp) -Hp //
-qed-.