(* CLOSED CONDITION FOR PATH ************************************************)
-(* Constructions with height and depth **************************************)
+(* Destructions with height and depth ***************************************)
-lemma path_closed_depth (p) (n):
- p ϵ 𝐂❨n❩ → ♯p + n = ♭p.
-#p #n #Hn elim Hn -Hn //
-#p #n #_ #IH <nplus_succ_dx //
-qed.
+lemma path_closed_des_depth (o) (q) (n):
+ q ϵ 𝐂❨o,n❩ → ♯q + n = ♭q.
+#o #q #n #Hq elim Hq -q -n //
+#q #n #_ #IH <nplus_succ_dx //
+qed-.
+
+lemma path_closed_des_succ_depth (o) (q) (n):
+ q ϵ 𝐂❨o,↑n❩ → ♭q = ↑↓♭q.
+#o #q #n #Hq
+<(path_closed_des_depth … Hq) -Hq
+<nplus_succ_dx <npred_succ //
+qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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_closed.ma".
+include "delayed_updating/syntax/path_closed_height.ma".
+
+(* TAILED UNWIND FOR RELOCATION MAP *****************************************)
+
+(* Destructions with cpp and height *****************************************)
+
+lemma nap_depth_unwind2_rmap_closed (o) (f) (q) (n):
+ q ϵ 𝐂❨o,n❩ →
+ f＠§❨♯q❩+♭q = ▶[f]q＠§❨♭q❩.
+#o #f #q #n #Hq
+<(path_closed_des_depth … Hq) in ⊢ (???%);
+/2 width=2 by nap_plus_unwind2_rmap_closed_depth/
+qed-.
+
+lemma tls_depth_unwind2_rmap_closed (o) (f) (q) (n):
+ q ϵ 𝐂❨o,n❩ →
+ ⇂*[♯q]f ≗ ⇂*[♭q]▶[f]q.
+#o #f #q #n #Hq elim Hq -q -n //
+#q #n #k #_
+>(npsucc_pred k) in ⊢ (%→?); <nplus_succ_dx #Hq #IH
+<height_d_dx <depth_d_dx
+>(path_closed_des_succ_depth … Hq)
+@(stream_eq_trans … (tls_unwind2_rmap_d_dx …))
+>nrplus_inj_dx >nrplus_inj_sn >nsucc_unfold
+<(path_closed_des_succ_depth … Hq) -Hq
+<nplus_comm <stream_tls_plus
+<nplus_comm <stream_tls_plus
+/2 width=1 by stream_tls_eq_repl/
+qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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.
+*)
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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_constructors.ma".
+include "delayed_updating/reduction/ibfr_constructors.ma".
+include "delayed_updating/unwind/unwind2_prototerm_constructors.ma".
+include "delayed_updating/substitution/lift_prototerm_constructors.ma".
+include "ground/arith/pnat_two.ma".
+
+(* DELAYED BALANCED FOCUSED REDUCTION ***************************************)
+
+(* Example of unprotected balanced β-reduction ******************************)
+
+definition l3_t: prototerm ≝
+ (＠(⧣𝟏).＠(𝛌.⧣𝟏).𝛌.⧣𝟏).
+
+definition l3_i1: prototerm ≝
+ (＠(⧣𝟏).＠(𝛌.⧣𝟏).𝛌.𝛌.⧣𝟏).
+
+definition l3_i2: prototerm ≝
+ (＠(⧣𝟏).＠(𝛌.⧣𝟏).𝛌.𝛌.⧣↑𝟐).
+
+definition l3_d1: prototerm ≝
+ (＠(⧣𝟏).＠(𝛌.⧣𝟏).𝛌.𝛕𝟏.𝛌.⧣𝟏).
+
+definition l3_d2: prototerm ≝
+ (＠(⧣𝟏).＠(𝛌.⧣𝟏).𝛌.𝛕𝟏.𝛌.𝛕𝟏.⧣𝟏).
+
+lemma l3_ti1:
+ l3_t ➡𝐢𝐛𝐟[𝗔◗𝗔◗𝗟◗𝐞] l3_i1.
+@ibfr_appl_hd
+@ibfr_eq_trans [| @ibfr_beta_0 // ]
+@appl_eq_repl [ // ]
+@abst_eq_repl
+@(subset_eq_canc_sn … (fsubst_empty_rc …))
+@(subset_eq_canc_sn … (lift_term_abst …))
+@abst_eq_repl
+@(subset_eq_canc_sn … (lift_term_oref_pap … )) //
+qed.
+
+lemma l3_i12:
+ l3_i1 ➡𝐢𝐛𝐟[𝗔◗𝗔◗𝗟◗𝗟◗𝐞] l3_i2.
+@ibfr_eq_trans [| @ibfr_beta_1 // ]
+@appl_eq_repl [ // ]
+@appl_eq_repl [ // ]
+@abst_eq_repl
+@abst_eq_repl
+@(subset_eq_canc_sn … (fsubst_empty_rc …))
+@(subset_eq_canc_sn … (lift_term_oref_pap … )) //
+qed.
+
+lemma l3_td1:
+ l3_t ➡𝐝𝐛𝐟[𝗔◗𝗔◗𝗟◗𝐞] l3_d1.
+@dbfr_appl_hd
+@dbfr_eq_trans [| @dbfr_beta_0 // ]
+@appl_eq_repl [ // ]
+@abst_eq_repl
+@(subset_eq_canc_sn … (fsubst_empty_rc …)) //
+qed.
+
+lemma ld_di2:
+ l3_i2 ⇔ ▼[𝐢]l3_d2.
+@(subset_eq_canc_sn … (unwind2_term_appl …)) @appl_eq_repl
+[ @(subset_eq_canc_sn … (unwind2_term_oref_pap …)) // ]
+@(subset_eq_canc_sn … (unwind2_term_appl …)) @appl_eq_repl
+[ @(subset_eq_canc_sn … (unwind2_term_abst …)) @abst_eq_repl
+ @(subset_eq_canc_sn … (unwind2_term_oref_pap …)) //
+]
+@(subset_eq_canc_sn … (unwind2_term_abst …)) @abst_eq_repl
+@(subset_eq_canc_sn … (unwind2_term_iref …))
+@(subset_eq_canc_sn … (unwind2_term_abst …)) @abst_eq_repl
+@(subset_eq_canc_sn … (unwind2_term_iref …))
+@(subset_eq_canc_sn … (unwind2_term_oref_pap …)) //
+qed.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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.
--- /dev/null
+include "ground/arith/nat_le_plus.ma".
+include "ground/arith/nat_le_pred.ma".
+
+lemma tls_succ_unwind2_rmap_append_closed_Lq_dx (o) (f) (p) (q) (n):
+ q ϵ 𝐂❨o,n❩ →
+ ▶[f]p ≗ ⇂*[↑n]▶[f](p●𝗟◗q).
+/2 width=2 by tls_succ_plus_unwind2_rmap_push_closed/
+qed-.
+
+lemma xap_le_unwind2_rmap_append_closed_dx (o) (f) (p) (q) (n):
+ q ϵ 𝐂❨o,n❩ → ∀m. m ≤ n →
+ ▶[f]q＠❨m❩ = ▶[f](p●q)＠❨m❩.
+#o #f #p #q #n #Hq elim Hq -q -n
+[|*: #q #n [ #k #_ ] #_ #IH ] #m #Hm
+[ <(nle_inv_zero_dx … Hm) -m //
+| <unwind2_rmap_d_dx <unwind2_rmap_d_dx
+ <tr_compose_xap <tr_compose_xap
+ @IH -IH (**) (* auto too slow *)
+ @nle_trans [| @tr_uni_xap ]
+ /2 width=1 by nle_plus_bi_dx/
+| <unwind2_rmap_m_dx <unwind2_rmap_m_dx
+ /2 width=2 by/
+| <unwind2_rmap_L_dx <unwind2_rmap_L_dx
+ elim (nle_inv_succ_dx … Hm) -Hm // * #Hm #H0
+ >H0 -H0 <tr_xap_push <tr_xap_push
+ /3 width=2 by eq_f/
+| <unwind2_rmap_A_dx <unwind2_rmap_A_dx
+ /2 width=2 by/
+| <unwind2_rmap_S_dx <unwind2_rmap_S_dx
+ /2 width=2 by/
+]
+qed-.
+
+lemma nap_unwind2_rmap_append_closed_Lq_dx (o) (f) (p) (q) (n):
+ q ϵ 𝐂❨o,n❩ →
+ ▶[f](𝗟◗q)＠§❨n❩ = ▶[f](p●𝗟◗q)＠§❨n❩.
+#o #f #p #q #n #Hq
+lapply (pcc_L_sn … Hq) -Hq #Hq
+lapply (xap_le_unwind2_rmap_append_closed_dx o f p … Hq (↑n) ?) -Hq //
+<tr_xap_succ_nap <tr_xap_succ_nap #Hq
+/2 width=1 by eq_inv_nsucc_bi/
+qed-.
+
+lemma nap_unwind2_rmap_push_closed_depth (o) (f) (q) (n):
+ q ϵ 𝐂❨o,n❩ →
+ ♭q = ▶[⫯f]q＠§❨n❩.
+#o #f #q #n #Hq elim Hq -q -n
+[|*: #q #n [ #k #_ ] #_ #IH ] //
+<unwind2_rmap_d_dx <tr_compose_nap //
+qed-.
+
+lemma nap_unwind2_rmap_append_closed_Lq_dx_depth (o) (f) (p) (q) (n):
+ q ϵ 𝐂❨o,n❩ →
+ ♭q = ▶[f](p●𝗟◗q)＠§❨n❩.
+#o #f #p #q #n #Hq
+<nap_unwind2_rmap_append_closed_Lq_dx //
+/2 width=2 by nap_unwind2_rmap_push_closed_depth/
+qed-.
+
+lemma xap_unwind2_rmap_append_closed_true_dx_depth (f) (p) (q) (n):
+ q ϵ 𝐂❨Ⓣ,n❩ → ♭q = ▶[f](p●q)＠❨n❩.
+#f #p #q #n #Hq elim Hq -q -n //
+#q #n #k #Ho #_ #IH
+<unwind2_rmap_d_dx <tr_compose_xap
+>Ho // <tr_uni_xap_succ <Ho //
+qed-.
+
+lemma tls_plus_unwind2_rmap_closed_true (f) (q) (n):
+ q ϵ 𝐂❨Ⓣ,n❩ →
+ ∀m. ⇂*[m]f ≗ ⇂*[m+n]▶[f]q.
+#f #q #n #Hq elim Hq -q -n //
+#q #n #k #Ho #_ #IH #m
+>Ho // <nplus_succ_dx
+@(stream_eq_trans … (tls_unwind2_rmap_d_dx …))
+>nrplus_inj_dx >nrplus_inj_sn >nsucc_unfold
+>nplus_succ_dx <Ho //
+qed-.
+
+lemma tls_unwind2_rmap_append_closed_true_dx (f) (p) (q) (n):
+ q ϵ 𝐂❨Ⓣ,n❩ →
+ ▶[f]p ≗ ⇂*[n]▶[f](p●q).
+/2 width=1 by tls_plus_unwind2_rmap_closed_true/
+qed-.
+
+lemma nap_plus_unwind2_rmap_append_closed_Lq_dx_depth (o) (f) (p) (q) (m) (n):
+ q ϵ 𝐂❨o,n❩ →
+ ▶[f]p＠❨m❩+♭q = ▶[f](p●𝗟◗q)＠§❨m+n❩.
+#o #f #p #q #m #n #Hq
+<tr_nap_plus @eq_f2
+[ <(tr_xap_eq_repl … (tls_succ_unwind2_rmap_append_closed_Lq_dx …)) //
+| /2 width=2 by nap_unwind2_rmap_append_closed_Lq_dx_depth/
+]
+qed-.
+
+lemma nap_plus_unwind2_rmap_append_closed_bLq_dx_depth (o) (f) (p) (b) (q) (m) (n):
+ b ϵ 𝐂❨Ⓣ,m❩ → q ϵ 𝐂❨o,n❩ →
+ ♭b+♭q = ▶[f](p●b●𝗟◗q)＠§❨m+n❩.
+#o #f #p #b #q #m #n #Hb #Hq
+>(xap_unwind2_rmap_append_closed_true_dx_depth f p … Hb) -Hb
+>(nap_plus_unwind2_rmap_append_closed_Lq_dx_depth … Hq) -Hq //
+qed-.
+
+lemma tls_succ_plus_unwind2_rmap_append_closed_bLq_dx (o) (f) (p) (b) (q) (m) (n):
+ b ϵ 𝐂❨Ⓣ,m❩ → q ϵ 𝐂❨o,n❩ →
+ ▶[f]p ≗ ⇂*[↑(m+n)]▶[f](p●b●𝗟◗q).
+#o #f #p #b #q #m #n #Hb #Hq
+>nplus_succ_dx <stream_tls_plus >list_append_assoc
+@(stream_eq_trans … (tls_unwind2_rmap_append_closed_true_dx … Hb)) -Hb
+/3 width=2 by stream_tls_eq_repl, tls_succ_unwind2_rmap_append_closed_Lq_dx/
+qed-.
--- /dev/null
+include "delayed_updating/unwind/unwind2_rmap_closed.ma".
+
+lemma pippo (o) (q) (n):
+ (q◖𝗟) ϵ 𝐂❨o,n❩ →
+ (𝗟◗q) ϵ 𝐂❨o,n❩.
+#o #q elim q -q //
+* [ #k ] #q #IH #n #H0
+elim (pcc_inv_L_dx … H0) -H0 #H0 #Hn
+[ elim (pcc_inv_d_dx … H0) -H0 #_ #H0
+ >Hn -Hn /4 width=1 by pcc_d_dx, pcc_L_dx/
+| lapply (pcc_inv_m_dx … H0) -H0 #H0
+ >Hn -Hn /4 width=1 by pcc_m_dx, pcc_L_dx/
+| elim (pcc_inv_L_dx … H0) -H0 #H0 #Hnn
+ >Hn -Hn /4 width=1 by pcc_L_dx/
+| lapply (pcc_inv_A_dx … H0) -H0 #H0
+ >Hn -Hn /4 width=1 by pcc_A_dx, pcc_L_dx/
+| lapply (pcc_inv_S_dx … H0) -H0 #H0
+ >Hn -Hn /4 width=1 by pcc_S_dx, pcc_L_dx/
+]
+qed-.
+
+
+lemma pippo (o) (f) (q) (n):
+ q ϵ 𝐂❨o,n❩ → ♭q < ▶[f]q＠⧣❨↑n❩.
+#o #f #q #n #H0 elim H0 -q -n //
+#q #n [ #k #_ ] #_ #IH
+[ <depth_d_dx <unwind2_rmap_d_dx
+ <tr_compose_pap <tr_uni_pap //
+| <depth_L_dx <unwind2_rmap_L_dx
+ <tr_pap_push
+ /2 width=1 by nlt_succ_bi/
+]
+qed-.
+
+lemma pippo2 (o) (f) (q) (n):
+ q ϵ 𝐂❨o,n❩ → ▶[f]q＠❨n❩ ≤ ♭q.
+#o #f #q #n #H0 elim H0 -q -n //
+#q #n [ #k #_ ] #_ #IH
+[ <unwind2_rmap_d_dx <depth_d_dx
+ @(nle_trans … IH) -IH
+ <tr_compose_xap
+| <unwind2_rmap_L_dx <depth_L_dx
+ <tr_xap_push
+ /2 width=1 by nle_succ_bi/
+]
+qed-.
+
+lemma pippo (o) (f) (q) (n):
+ q ϵ 𝐂❨o,n❩ → n < ▶[f]q＠⧣❨↑♭q❩.
+#o #f #q #n #H0 elim H0 -q -n //
+#q #n [ #k #_ ] #_ #IH
+[ <unwind2_rmap_d_dx <depth_d_dx
+ <tr_compose_pap <tr_uni_pap
+ @(nlt_trans … (n+k)) [ // ]
+ @(nlt_trans … IH) -IH
+| <unwind2_rmap_L_dx <depth_L_dx <tr_pap_push
+ /2 width=1 by nlt_succ_bi/
METAVARIABLES
+ a : auxiliary path
b : balanced path
d : depth
+ e : excess
f, g : update function
h, k : reference index by depth
l : label
-1) (⫯f)@(1) = 1
-2) f@❨d-n❩ = k → n <= d → (f∘𝐮❨n❩)@❨d❩ = k
-3) f@❨d-1❩ = k-1 → 1 < d → 1 < k → (⫯f)@❨d❩ = k
-
-
lemma pr_pat_after_uni_tls (i2) (i1):
∀f2. @❨i1, f2❩ ≘ i2 →
∀f. 𝐮❨i2❩ ⊚ ⫰*[i2] f2 ≘ f → f2 ⊚ 𝐮❨i1❩ ≘ f.
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".
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/arith/nat_rplus.ma".
-include "ground/xoa/ex_6_5.ma".
+include "ground/xoa/ex_7_5.ma".
(* DELAYED BALANCED FOCUSED REDUCTION ***************************************)
definition dbfr (r): relation2 prototerm prototerm ≝
λt1,t2.
∃∃p,b,q,m,n. p●𝗔◗b●𝗟◗q = r &
- ⊗b ϵ 𝐁 & b ϵ 𝐂❨Ⓣ,m❩ & q ϵ 𝐂❨Ⓕ,n❩ & r◖𝗱↑n ϵ t1 &
+ p ϵ 𝐆 & ⊗b ϵ 𝐁 & b ϵ 𝐂❨Ⓕ,m❩ & q ϵ 𝐂❨Ⓕ,n❩ & r◖𝗱↑n ϵ t1 &
t1[⋔r←𝛕↑(m+n).(t1⋔(p◖𝗦))] ⇔ t2
.
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 #Hb #Hm #Hn #Ht1 #Ht #Ht2
-/3 width=13 by subset_eq_trans, ex6_5_intro/
+* #p #b #q #m #n #Hr #Hp #Hb #Hm #Hn #Ht1 #Ht #Ht2
+/3 width=14 by subset_eq_trans, ex7_5_intro/
qed-.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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.
-*)
(**************************************************************************)
include "delayed_updating/reduction/dbfr.ma".
-include "delayed_updating/reduction/ibfr.ma".
+include "delayed_updating/reduction/ibfr_unwind.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_closed.ma".
-
-include "delayed_updating/substitution/fsubst_eq.ma".
-include "delayed_updating/substitution/lift_prototerm_eq.ma".
include "delayed_updating/syntax/prototerm_proper_constructors.ma".
-include "delayed_updating/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 (f) (t1) (t2) (r): t1 ϵ 𝐓 →
- t1 ➡𝐝𝐛𝐟[r] t2 → ▼[f]t1 ➡𝐢𝐛𝐟[⊗r] ▼[f]t2.
+theorem dbfr_des_ibfr_push (f) (t1) (t2) (r): t1 ϵ 𝐓 →
+ t1 ➡𝐝𝐛𝐟[r] t2 → ▼[⫯f]t1 ➡𝐢𝐛𝐟[⊗r] ▼[⫯f]t2.
#f #t1 #t2 #r #H0t1
-* #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
+* #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
/2 width=2 by path_closed_structure_depth/
-| -H0t1 -Hb -Hm -Ht1 -Ht2
+| -H0t1 -Hp -Hb -Hm -Ht1 -Ht2
/2 width=2 by path_closed_structure_depth/
-| lapply (in_comp_unwind2_path_term f … Ht1) -H0t1 -Hb -Hm -Ht2 -Ht1
+| lapply (in_comp_unwind2_path_term (⫯f) … Ht1) -H0t1 -Hp -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_depth //
-| lapply (unwind2_term_eq_repl_dx f … Ht2) -Ht2 #Ht2
+ <nap_unwind2_rmap_append_closed_Lq_dx //
+| lapply (unwind2_term_eq_repl_dx (⫯f) … Ht2) -Ht2 #Ht2
@(subset_eq_trans … Ht2) -t2
@(subset_eq_trans … (unwind2_term_fsubst_ppc …))
[ @fsubst_eq_repl [ // | // ]
@(subset_eq_trans … (lift_unwind2_term_after …))
@unwind2_term_eq_repl_sn
(* Note: crux of the proof begins *)
- <list_append_rcons_sn
- @(stream_eq_trans … (tr_compose_uni_dx_pap …)) <tr_pap_succ_nap
- @tr_compose_eq_repl
- [ <nap_plus_unwind2_rmap_append_closed_bLq_dx_depth //
- | >unwind2_rmap_A_dx
- /2 width=2 by tls_succ_plus_unwind2_rmap_append_closed_bLq_dx/
- ]
+ /2 width=1 by unwind2_rmap_uni_crux/
(* Note: crux of the proof ends *)
| //
| /2 width=2 by ex_intro/
| //
]
]
+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.
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 ***************************************)
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 #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
+* #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
/2 width=1 by lift_path_closed/
-| -Hb -Hm -Ht1 -Ht2
+| -Hp -Hb -Hm -Ht1 -Ht2
/2 width=1 by lift_path_rmap_closed_L/
-| lapply (in_comp_lift_path_term f … Ht1) -Ht2 -Ht1 -Hn
+| lapply (in_comp_lift_path_term f … Ht1) -Ht2 -Ht1 -Hn -Hp
<lift_path_d_dx #Ht1 //
-| lapply (lift_term_eq_repl_dx f … Ht2) -Ht2 #Ht2 -Ht1
+| lapply (lift_term_eq_repl_dx f … Ht2) -Ht2 #Ht2 -Ht1 -Hp
@(subset_eq_trans … Ht2) -t2
@(subset_eq_trans … (lift_term_fsubst …))
@fsubst_eq_repl [ // | // ]
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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_constructors.ma".
-include "delayed_updating/reduction/ibfr_constructors.ma".
-include "delayed_updating/unwind/unwind2_prototerm_constructors.ma".
-include "delayed_updating/substitution/lift_prototerm_constructors.ma".
-include "ground/arith/pnat_two.ma".
-
-(* DELAYED BALANCED FOCUSED REDUCTION ***************************************)
-
-(* Example of unprotected balanced β-reduction ******************************)
-
-definition l3_t: prototerm ≝
- (＠(⧣𝟏).＠(𝛌.⧣𝟏).𝛌.⧣𝟏).
-
-definition l3_i1: prototerm ≝
- (＠(⧣𝟏).＠(𝛌.⧣𝟏).𝛌.𝛌.⧣𝟏).
-
-definition l3_i2: prototerm ≝
- (＠(⧣𝟏).＠(𝛌.⧣𝟏).𝛌.𝛌.⧣↑𝟐).
-
-definition l3_d1: prototerm ≝
- (＠(⧣𝟏).＠(𝛌.⧣𝟏).𝛌.𝛕𝟏.𝛌.⧣𝟏).
-
-definition l3_d2: prototerm ≝
- (＠(⧣𝟏).＠(𝛌.⧣𝟏).𝛌.𝛕𝟏.𝛌.𝛕𝟏.⧣𝟏).
-
-lemma l3_ti1:
- l3_t ➡𝐢𝐛𝐟[𝗔◗𝗔◗𝗟◗𝐞] l3_i1.
-@ibfr_appl_hd
-@ibfr_eq_trans [| @ibfr_beta_0 // ]
-@appl_eq_repl [ // ]
-@abst_eq_repl
-@(subset_eq_canc_sn … (fsubst_empty_rc …))
-@(subset_eq_canc_sn … (lift_term_abst …))
-@abst_eq_repl
-@(subset_eq_canc_sn … (lift_term_oref_pap … )) //
-qed.
-
-lemma l3_i12:
- l3_i1 ➡𝐢𝐛𝐟[𝗔◗𝗔◗𝗟◗𝗟◗𝐞] l3_i2.
-@ibfr_eq_trans [| @ibfr_beta_1 // ]
-@appl_eq_repl [ // ]
-@appl_eq_repl [ // ]
-@abst_eq_repl
-@abst_eq_repl
-@(subset_eq_canc_sn … (fsubst_empty_rc …))
-@(subset_eq_canc_sn … (lift_term_oref_pap … )) //
-qed.
-
-lemma l3_td1:
- l3_t ➡𝐝𝐛𝐟[𝗔◗𝗔◗𝗟◗𝐞] l3_d1.
-@dbfr_appl_hd
-@dbfr_eq_trans [| @dbfr_beta_0 // ]
-@appl_eq_repl [ // ]
-@abst_eq_repl
-@(subset_eq_canc_sn … (fsubst_empty_rc …)) //
-qed.
-
-lemma ld_di2:
- l3_i2 ⇔ ▼[𝐢]l3_d2.
-@(subset_eq_canc_sn … (unwind2_term_appl …)) @appl_eq_repl
-[ @(subset_eq_canc_sn … (unwind2_term_oref_pap …)) // ]
-@(subset_eq_canc_sn … (unwind2_term_appl …)) @appl_eq_repl
-[ @(subset_eq_canc_sn … (unwind2_term_abst …)) @abst_eq_repl
- @(subset_eq_canc_sn … (unwind2_term_oref_pap …)) //
-]
-@(subset_eq_canc_sn … (unwind2_term_abst …)) @abst_eq_repl
-@(subset_eq_canc_sn … (unwind2_term_iref …))
-@(subset_eq_canc_sn … (unwind2_term_abst …)) @abst_eq_repl
-@(subset_eq_canc_sn … (unwind2_term_iref …))
-@(subset_eq_canc_sn … (unwind2_term_oref_pap …)) //
-qed.
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/arith/nat_rplus.ma".
-include "ground/xoa/ex_6_5.ma".
+include "ground/xoa/ex_7_5.ma".
(* IMMEDIATE BALANCED FOCUSED REDUCTION *************************************)
definition ibfr (r): relation2 prototerm prototerm ≝
λt1,t2.
∃∃p,b,q,m,n. p●𝗔◗b●𝗟◗q = r &
- ⊗b ϵ 𝐁 & b ϵ 𝐂❨Ⓣ,m❩ & q ϵ 𝐂❨Ⓕ,n❩ & r◖𝗱↑n ϵ t1 &
+ p ϵ 𝐆 & ⊗b ϵ 𝐁 & b ϵ 𝐂❨Ⓕ,m❩ & q ϵ 𝐂❨Ⓕ,n❩ & r◖𝗱↑n ϵ t1 &
t1[⋔r←🠡[𝐮❨↑(m+n)❩](t1⋔(p◖𝗦))] ⇔ t2
.
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 #Hb #Hm #Hn #Ht1 #Ht #Ht2
-/3 width=13 by subset_eq_trans, ex6_5_intro/
+* #p #b #q #m #n #Hr#Hp #Hb #Hm #Hn #Ht1 #Ht #Ht2
+/3 width=14 by subset_eq_trans, ex7_5_intro/
qed-.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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 *)
+(* *)
+(**************************************************************************)
+
+(* IMMEDIATE BALANCED FOCUSED REDUCTION *************************************)
+
+include "delayed_updating/reduction/ibfr.ma".
+include "delayed_updating/substitution/fsubst_eq.ma".
+include "delayed_updating/substitution/lift_prototerm_eq.ma".
+
+(* Constructions with subset_equivalence ************************************)
+
+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
+[ /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/
+]
+qed-.
+
+lemma ibfr_eq_repl (t1) (t2) (u1) (u2) (r):
+ t1 ⇔ u1 → t2 ⇔ u2 → t1 ➡𝐢𝐛𝐟[r] t2 → u1 ➡𝐢𝐛𝐟[r] u2.
+/3 width=3 by ibfr_eq_canc_sn, ibfr_eq_trans/
+qed-.
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".
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 #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
+* #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
/2 width=1 by lift_path_closed/
-| -Hb -Hm -Ht1 -Ht2
+| -Hp -Hb -Hm -Ht1 -Ht2
/2 width=1 by lift_path_rmap_closed_L/
-| lapply (in_comp_lift_path_term f … Ht1) -Ht2 -Ht1 -Hn
+| lapply (in_comp_lift_path_term f … Ht1) -Ht2 -Ht1 -Hp -Hn
<lift_path_d_dx #Ht1 //
-| lapply (lift_term_eq_repl_dx f … Ht2) -Ht2 #Ht2 -Ht1
+| lapply (lift_term_eq_repl_dx f … Ht2) -Ht2 #Ht2 -Ht1 -Hp
@(subset_eq_trans … Ht2) -t2
@(subset_eq_trans … (lift_term_fsubst …))
@fsubst_eq_repl [ // | <lift_path_append // ]
(* *)
(**************************************************************************)
-include "delayed_updating/reduction/ibfr.ma".
+include "delayed_updating/reduction/ibfr_lift.ma".
+include "delayed_updating/reduction/ibfr_eq.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_closed.ma".
-
-include "delayed_updating/substitution/fsubst_eq.ma".
-include "delayed_updating/substitution/lift_prototerm_eq.ma".
+include "delayed_updating/unwind/unwind2_rmap_crux.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_unwind_bi (f) (t1) (t2) (r):
+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):
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 #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
+* #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
/2 width=2 by path_closed_structure_depth/
-| -H1t1 -H2r -Hb -Hm -Ht1 -Ht2
+| -H1t1 -H2r -Hp -Hb -Hm -Ht1 -Ht2
/2 width=2 by path_closed_structure_depth/
-| lapply (in_comp_unwind2_path_term f … Ht1) -Ht2 -Ht1 -H1t1 -H2r -Hb
+| lapply (in_comp_unwind2_path_term (⫯f) … Ht1) -Ht2 -Ht1 -H1t1 -H2r -Hp -Hb
<unwind2_path_d_dx <tr_pap_succ_nap <list_append_rcons_sn >list_append_assoc
- <nap_unwind2_rmap_append_closed_Lq_dx_depth //
-| lapply (unwind2_term_eq_repl_dx f … Ht2) -Ht2 #Ht2
+ <nap_unwind2_rmap_append_closed_Lq_dx //
+| 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 [ // | // ]
@(subset_eq_canc_dx … (unwind2_lift_term_after …))
@unwind2_term_eq_repl_sn
(* Note: crux of the proof begins *)
- <list_append_rcons_sn
- @(stream_eq_trans … (tr_compose_uni_dx_pap …)) <tr_pap_succ_nap
- @tr_compose_eq_repl
- [ <nap_plus_unwind2_rmap_append_closed_bLq_dx_depth //
- | >unwind2_rmap_A_dx
- /2 width=2 by tls_succ_plus_unwind2_rmap_append_closed_bLq_dx/
- ]
+ /2 width=1 by unwind2_rmap_uni_crux/
(* Note: crux of the proof ends *)
| //
| /2 width=2 by ex_intro/
| //
]
]
+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.
lemma nap_plus_lift_rmap_append_closed_Lq_dx (o) (f) (p) (q) (m) (n):
q ϵ 𝐂❨o,n❩ →
- 🠢[f](p)＠❨m❩+🠢[f](p●𝗟◗q)＠§❨n❩ = 🠢[f](p●𝗟◗q)＠§❨m+n❩.
+ 🠢[f]p＠❨m❩+🠢[f](p●𝗟◗q)＠§❨n❩ = 🠢[f](p●𝗟◗q)＠§❨m+n❩.
#o #f #p #q #m #n #Hq
+<tr_nap_plus_dx_xap
/4 width=2 by eq_f2, tr_xap_eq_repl, tls_succ_lift_rmap_append_closed_Lq_dx/
qed-.
/2 width=1 by conj/
qed.
+lemma grafted_incl_repl (t1) (t2) (p):
+ t1 ⊆ t2 → t1⋔p ⊆ t2⋔p.
+#t1 #t2 #p #Ht #q #Hq
+/2 width=1 by/
+qed.
+
+lemma grafted_eq_repl (t1) (t2) (p):
+ t1 ⇔ t2 → t1⋔p ⇔ t2⋔p.
+#t1 #t2 #p * #H1t #H2t
+/3 width=1 by conj, grafted_incl_repl/
+qed.
+
(* Constructions with prototerm_root ****************************************)
lemma prototerm_root_incl_repl:
include "delayed_updating/unwind/unwind2_rmap_eq.ma".
include "delayed_updating/syntax/path_closed.ma".
include "delayed_updating/syntax/path_depth.ma".
-include "ground/relocation/xap.ma".
+include "ground/relocation/nap.ma".
include "ground/lib/stream_tls_plus.ma".
include "ground/lib/stream_eq_eq.ma".
-include "ground/arith/nat_le_plus.ma".
-include "ground/arith/nat_le_pred.ma".
(* TAILED UNWIND FOR RELOCATION MAP *****************************************)
(* Destructions with cpp ****************************************************)
-lemma xap_le_unwind2_rmap_append_closed_dx (o) (f) (p) (q) (n):
- q ϵ 𝐂❨o,n❩ → ∀m. m ≤ n →
- ▶[f]q＠❨m❩ = ▶[f](p●q)＠❨m❩.
-#o #f #p #q #n #Hq elim Hq -q -n
-[|*: #q #n [ #k #_ ] #_ #IH ] #m #Hm
-[ <(nle_inv_zero_dx … Hm) -m //
-| <unwind2_rmap_d_dx <unwind2_rmap_d_dx
- <tr_compose_xap <tr_compose_xap
- @IH -IH (**) (* auto too slow *)
- @nle_trans [| @tr_uni_xap ]
- /2 width=1 by nle_plus_bi_dx/
-| <unwind2_rmap_m_dx <unwind2_rmap_m_dx
- /2 width=2 by/
-| <unwind2_rmap_L_dx <unwind2_rmap_L_dx
- elim (nle_inv_succ_dx … Hm) -Hm // * #Hm #H0
- >H0 -H0 <tr_xap_push <tr_xap_push
- /3 width=2 by eq_f/
-| <unwind2_rmap_A_dx <unwind2_rmap_A_dx
- /2 width=2 by/
-| <unwind2_rmap_S_dx <unwind2_rmap_S_dx
- /2 width=2 by/
-]
-qed-.
-
-lemma nap_unwind2_rmap_append_closed_Lq_dx (o) (f) (p) (q) (n):
+lemma nap_plus_unwind2_rmap_closed (o) (f) (q) (m) (n):
q ϵ 𝐂❨o,n❩ →
- ▶[f](𝗟◗q)＠§❨n❩ = ▶[f](p●𝗟◗q)＠§❨n❩.
-#o #f #p #q #n #Hq
-lapply (pcc_L_sn … Hq) -Hq #Hq
-lapply (xap_le_unwind2_rmap_append_closed_dx o f p … Hq (↑n) ?) -Hq //
-<tr_xap_succ_nap <tr_xap_succ_nap #Hq
-/2 width=1 by eq_inv_nsucc_bi/
+ f＠§❨m❩+♭q = ▶[f]q＠§❨m+n❩.
+#o #f #q #m #n #Hq elim Hq -q -n //
+#q #n [ #k #_ ] #_ #IH
+[ <depth_d_dx <unwind2_rmap_d_dx
+ <tr_compose_nap <tr_uni_nap //
+| <depth_L_dx <unwind2_rmap_L_dx
+ <tr_nap_push <nplus_succ_dx //
+]
qed-.
-lemma nap_unwind2_rmap_push_closed_depth (o) (f) (q) (n):
+lemma nap_plus_unwind2_rmap_append_closed_Lq_dx (o) (f) (p) (q) (m) (n):
q ϵ 𝐂❨o,n❩ →
- ♭q = ▶[⫯f]q＠§❨n❩.
-#o #f #q #n #Hq elim Hq -q -n
-[|*: #q #n [ #k #_ ] #_ #IH ] //
-<unwind2_rmap_d_dx <tr_compose_nap //
+ (⫯▶[f]p)＠§❨m❩+♭q = ▶[f](p●𝗟◗q)＠§❨m+n❩.
+#o #f #p #q #m #n #Hn
+/2 width=2 by nap_plus_unwind2_rmap_closed/
qed-.
-lemma nap_unwind2_rmap_append_closed_Lq_dx_depth (o) (f) (p) (q) (n):
+lemma nap_unwind2_rmap_append_closed_Lq_dx (o) (f) (p) (q) (n):
q ϵ 𝐂❨o,n❩ →
♭q = ▶[f](p●𝗟◗q)＠§❨n❩.
-#o #f #p #q #n #Hq
-<nap_unwind2_rmap_append_closed_Lq_dx //
-/2 width=2 by nap_unwind2_rmap_push_closed_depth/
-qed-.
-
-lemma xap_unwind2_rmap_append_closed_true_dx_depth (f) (p) (q) (n):
- q ϵ 𝐂❨Ⓣ,n❩ → ♭q = ▶[f](p●q)＠❨n❩.
-#f #p #q #n #Hq elim Hq -q -n //
-#q #n #k #Ho #_ #IH
-<unwind2_rmap_d_dx <tr_compose_xap
->Ho // <tr_uni_xap_succ <Ho //
+#o #f #p #q #n #Hn
+>(nplus_zero_sn n)
+<(nap_plus_unwind2_rmap_append_closed_Lq_dx … Hn) -Hn
+<nplus_zero_sn //
qed-.
lemma tls_succ_plus_unwind2_rmap_push_closed (o) (f) (q) (n):
q ϵ 𝐂❨o,n❩ →
∀m. ⇂*[m]f ≗ ⇂*[↑(m+n)]▶[⫯f]q.
-#o #f #q #n #Hq elim Hq -q -n //
+#o #f #q #n #Hn elim Hn -q -n //
#q #n #k #_ #_ #IH #m
@(stream_eq_trans … (tls_unwind2_rmap_d_dx …))
>nrplus_inj_dx >nrplus_inj_sn >nsucc_unfold //
qed-.
-lemma tls_plus_unwind2_rmap_closed_true (f) (q) (n):
- q ϵ 𝐂❨Ⓣ,n❩ →
- ∀m. ⇂*[m]f ≗ ⇂*[m+n]▶[f]q.
-#f #q #n #Hq elim Hq -q -n //
-#q #n #k #Ho #_ #IH #m
->Ho // <nplus_succ_dx
-@(stream_eq_trans … (tls_unwind2_rmap_d_dx …))
->nrplus_inj_dx >nrplus_inj_sn >nsucc_unfold
->nplus_succ_dx <Ho //
-qed-.
-
-lemma tls_succ_unwind2_rmap_append_closed_Lq_dx (o) (f) (p) (q) (n):
+lemma tls_succ_unwind2_rmap_push_closed (o) (f) (q) (n):
q ϵ 𝐂❨o,n❩ →
- ▶[f]p ≗ ⇂*[↑n]▶[f](p●𝗟◗q).
+ f ≗ ⇂*[↑n]▶[⫯f](q).
+#o #f #q #n #Hn
/2 width=2 by tls_succ_plus_unwind2_rmap_push_closed/
qed-.
-lemma tls_unwind2_rmap_append_closed_true_dx (f) (p) (q) (n):
- q ϵ 𝐂❨Ⓣ,n❩ →
- ▶[f]p ≗ ⇂*[n]▶[f](p●q).
-/2 width=1 by tls_plus_unwind2_rmap_closed_true/
-qed-.
-
-lemma nap_plus_unwind2_rmap_append_closed_Lq_dx_depth (o) (f) (p) (q) (m) (n):
+lemma tls_succ_plus_unwind2_rmap_append_closed_Lq_dx (o) (f) (p) (q) (n):
q ϵ 𝐂❨o,n❩ →
- ▶[f]p＠❨m❩+♭q = ▶[f](p●𝗟◗q)＠§❨m+n❩.
-#o #f #p #q #m #n #Hq
-<tr_nap_plus @eq_f2
-[ <(tr_xap_eq_repl … (tls_succ_unwind2_rmap_append_closed_Lq_dx …)) //
-| /2 width=2 by nap_unwind2_rmap_append_closed_Lq_dx_depth/
-]
-qed-.
-
-lemma nap_plus_unwind2_rmap_append_closed_bLq_dx_depth (o) (f) (p) (b) (q) (m) (n):
- b ϵ 𝐂❨Ⓣ,m❩ → q ϵ 𝐂❨o,n❩ →
- ♭b+♭q = ▶[f](p●b●𝗟◗q)＠§❨m+n❩.
-#o #f #p #b #q #m #n #Hb #Hq
->(xap_unwind2_rmap_append_closed_true_dx_depth f p … Hb) -Hb
->(nap_plus_unwind2_rmap_append_closed_Lq_dx_depth … Hq) -Hq //
-qed-.
-
-lemma tls_succ_plus_unwind2_rmap_append_closed_bLq_dx (o) (f) (p) (b) (q) (m) (n):
- b ϵ 𝐂❨Ⓣ,m❩ → q ϵ 𝐂❨o,n❩ →
- ▶[f]p ≗ ⇂*[↑(m+n)]▶[f](p●b●𝗟◗q).
-#o #f #p #b #q #m #n #Hb #Hq
->nplus_succ_dx <stream_tls_plus >list_append_assoc
-@(stream_eq_trans … (tls_unwind2_rmap_append_closed_true_dx … Hb)) -Hb
-/3 width=2 by stream_tls_eq_repl, tls_succ_unwind2_rmap_append_closed_Lq_dx/
+ ∀m. ⇂*[m]▶[f]p ≗ ⇂*[↑(m+n)]▶[f](p●𝗟◗q).
+#o #f #p #q #n #Hn #m
+/2 width=2 by tls_succ_plus_unwind2_rmap_push_closed/
qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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_closed.ma".
+include "delayed_updating/unwind/unwind2_rmap_guard.ma".
+
+(* TAILED UNWIND FOR RELOCATION MAP *****************************************)
+
+(* Crucial constructions with tr_uni ****************************************)
+
+(* 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
+<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
+@(stream_eq_trans ????? (tr_compose_eq_repl …))
+[| @tls_succ_plus_unwind2_rmap_append_closed_Lq_dx // | skip
+| <nap_plus_unwind2_rmap_append_closed_Lq_dx // | skip
+] -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 //
+| @(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/
+]
+qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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-.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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_closed.ma".
-include "delayed_updating/syntax/path_balanced.ma".
-include "delayed_updating/syntax/path_structure.ma".
-
-(* TAILED UNWIND FOR RELOCATION MAP *****************************************)
-
-(* Example of unprotected balanced path *************************************)
-
-definition l3_b: path ≝ 𝐞◖𝗔◖𝗟◖𝗱𝟏.
-
-lemma l3_b_unfold: 𝐞◖𝗔◖𝗟◖𝗱𝟏 = l3_b.
-// qed.
-
-lemma l3_b_balanced: ⊗l3_b ϵ 𝐁.
-<l3_b_unfold <structure_d_dx
-/2 width=1 by pbc_empty, pbc_redex/
-qed.
-
-lemma l3_b_closed: l3_b ϵ 𝐂❨Ⓕ,𝟎❩.
-/4 width=1 by pcc_A_sn, pcc_empty, pcc_false_d_dx, pcc_L_dx/
-qed.
-
-lemma l3_b_unwind2_rmap_unfold (f):
- (⫯f)∘𝐮❨𝟏❩ = ▶[f]l3_b.
-// qed.
-
-lemma l3_b_unwind2_rmap_pap_unit (f):
- ↑(f＠⧣❨𝟏❩) = ▶[f]l3_b＠⧣❨𝟏❩.
-// qed.
projects / helm.git / commitdiff