include "delayed_updating/reduction/dfr.ma".
include "delayed_updating/reduction/ifr.ma".
+
include "delayed_updating/unwind1/unwind_fsubst.ma".
include "delayed_updating/unwind1/unwind_constructors.ma".
include "delayed_updating/unwind1/unwind_preterm_eq.ma".
include "delayed_updating/unwind1/unwind_structure_depth.ma".
include "delayed_updating/unwind1/unwind_depth.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_structure_depth.ma".
include "ground/relocation/tr_uni_compose.ma".
t1 โก๐๐[p,q] t2 โ โผ[๐ข]t1 โก๐[โp,โq] โผ[๐ข]t2.
#p #q #t1 #t2 #H0t1
* #b #n * #Hb #Hn #Ht1 #Ht2
-@(ex1_2_intro รข\80ยฆ (รข\8a\97b) (รข\86\91รข\9d\98รข\8a\97qรข\9d\98)) @and4_intro
+@(ex1_2_intro รข\80ยฆ (รข\8a\97b) (รข\86\91รข\99ยญรข\8a\97q)) @and4_intro
[ //
-| //
+| (*//*)
| lapply (in_comp_unwind_bi (๐ข) โฆ Ht1) -Ht1 -H0t1 -Hb -Ht2
<unwind_path_d_empty_dx <depth_structure //
| lapply (unwind_term_eq_repl_dx (๐ข) โฆ Ht2) -Ht2 #Ht2
<depth_append <depth_L_sn <depth_structure <depth_structure
@fsubst_eq_repl [ // ]
@(subset_eq_trans โฆ (unwind_iref โฆ))
+
+ elim Hb -Hb #Hb #H0 <H0 -H0 <nrplus_zero_dx <nplus_zero_dx <nsucc_unfold
+ >Hn
+ @(subset_eq_canc_sn โฆ (lift_term_eq_repl_dx โฆ))
+ [ @unwind_grafted_S /2 width=2 by ex_intro/ | skip ]
+ <Hn <Hn
+(*
+ @(subset_eq_trans โฆ (lift_term_eq_repl_dx โฆ))
+ [ @(unwind_term_eq_repl_sn โฆ (tls_succ_unwind q โฆ)) | skip ]
+*)
(*
+
+ @subset_eq_trans
+ [2: @unwind_term_eq_repl_dx
+ @(subset_eq_canc_sn โฆ (unwind_term_eq_repl_dx โฆ))
+
@(subset_eq_canc_sn โฆ (unwind_term_eq_repl_dx โฆ))
[ @unwind_grafted_S /2 width=2 by ex_intro/ | skip ]
---------------------------
โ[๐ฎโจโโqโ+โbโโฉ] โ[โ[p]๐ข] t โ โ[๐ฎโจโ[pโ๐โbโ๐โq]๐ข@โจn+โbโโฉโฉ] t
*)
+(*
+(โ[๐ฎโจโโqโโฉ]โผ[โ*[โโqโ]โผ[pโ๐โq]๐ข](t1โ(pโ๐ฆ))โโผ[๐ฎโจโโqโโฉโโผ[pโ๐โbโ๐โq]๐ข](t1โ(pโ๐ฆ))
+*)