From: Ferruccio Guidi Date: Wed, 14 Dec 2022 21:15:07 +0000 (+0100) Subject: update in delayed_updating X-Git-Tag: make_still_working~20 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=345b9054da93e11139d3dfe07f83e444e3022fc1;p=helm.git 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 index 000000000..c65fcbc5d --- /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 index 000000000..d2be3b32f --- /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 index 000000000..af57be335 --- /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 index 000000000..65bb51044 --- /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 index 000000000..8092cf8e3 --- /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 index 000000000..bdf843577 --- /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 index 4dd861087..000000000 --- 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 // 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 // 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 index 112a98c39..000000000 --- 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 // 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 // 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 index c65fcbc5d..000000000 --- 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 79d8698f9..079d44d8d 100644 --- 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 66d2a248f..776696b24 100644 --- 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 index 000000000..f0ffe995b --- /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 // 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 // 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 572b25097..387dc8f15 100644 --- 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 list_append_rcons_dx >list_append_assoc 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 974ceba5c..700440011 100644 --- 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 index 000000000..112a98c39 --- /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 // 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 // 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 0d569e6df..973a4570f 100644 --- 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 1b6bb9903..e08f3d419 100644 --- 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 list_append_assoc list_append_assoc >list_append_rcons_sn >(list_append_rcons_sn … b) @(stream_eq_trans … (tr_compose_uni_dx_pap …)) nsucc_unfold >nplus_succ_dx >nplus_succ_dx tr_nap_plus_dx nsucc_unfold >nplus_succ_dx >nplus_succ_dx tr_nap_plus_dx stream_tls_succ stream_tls_succ