definition dfr (p) (q): relation2 prototerm prototerm ≝
λt1,t2. ∃n:pnat.
let r ≝ p●𝗔◗𝗟◗q in
- ∧∧ (𝗟◗q)ᴿ = ↳[n](rᴿ) & r◖𝗱n ϵ t1 &
+ ∧∧ (𝗟◗q)ᴿ = ↳[n](𝗟◗q)ᴿ & r◖𝗱n ϵ t1 &
t1[⋔r←𝛕n.(t1⋔(p◖𝗦))] ⇔ t2
.
@(ex_intro … (↑♭q)) @and3_intro
[ -H0t1 -Ht1 -Ht2
>structure_L_sn >structure_reverse
- >H1n >path_head_structure_depth <H1n -H1n //
+ >H1n in ⊢ (??%?); >path_head_structure_depth <H1n -H1n //
| lapply (in_comp_unwind2_path_term f … Ht1) -Ht2 -Ht1 -H0t1
- <unwind2_path_d_dx
- >list_append_rcons_sn in H1n; <reverse_append #H1n
- lapply (unwind2_rmap_append_pap_closed f … H1n)
+ <unwind2_path_d_dx >(list_append_rcons_sn … p) <reverse_append
+ lapply (unwind2_rmap_append_pap_closed f … (p◖𝗔)ᴿ … H1n) -H1n
<reverse_lcons <depth_L_dx #H2n
- lapply (eq_inv_ninj_bi … H2n) -H2n #H2n <H2n -H2n -H1n #Ht1 //
+ lapply (eq_inv_ninj_bi … H2n) -H2n #H2n <H2n -H2n #Ht1 //
| lapply (unwind2_term_eq_repl_dx f … Ht2) -Ht2 #Ht2
@(subset_eq_trans … Ht2) -t2
@(subset_eq_trans … (unwind2_term_fsubst …))
@(subset_eq_trans … (lift_unwind2_term_after …))
@unwind2_term_eq_repl_sn
(* Note: crux of the proof begins *)
- >list_append_rcons_sn in H1n; <reverse_append #H1n
+ >list_append_rcons_sn <reverse_append
@(stream_eq_trans … (tr_compose_uni_dx …))
@tr_compose_eq_repl
[ <unwind2_rmap_append_pap_closed //
| >unwind2_rmap_A_sn <reverse_rcons
- /2 width=1 by tls_unwind2_rmap_append_closed/
+ /2 width=1 by tls_unwind2_rmap_closed/
]
(* Note: crux of the proof ends *)
| //
@(ex_intro … ((↑[p●𝗔◗𝗟◗q]f)@⧣❨n❩)) @and3_intro
[ -Ht1 -Ht2
<lift_rmap_L_dx >lift_path_L_sn
- >list_append_rcons_sn in H1n; <reverse_append #H1n
- <(lift_path_head … H1n) -H1n //
+ <(lift_path_head … H1n) in ⊢ (??%?); -H1n //
| lapply (in_comp_lift_path_term f … Ht1) -Ht2 -Ht1 -H1n
<lift_path_d_dx #Ht1 //
| lapply (lift_term_eq_repl_dx f … Ht2) -Ht2 #Ht2 -Ht1
@lift_term_eq_repl_sn
(* Note: crux of the proof begins *)
>list_append_rcons_sn in H1n; #H1n >lift_rmap_A_dx
- /2 width=1 by tls_lift_rmap_append_closed/
+ /2 width=1 by tls_lift_rmap_closed/
(* Note: crux of the proof ends *)
]
qed.
definition ifr (p) (q): relation2 prototerm prototerm ≝
λt1,t2. ∃n:pnat.
let r ≝ p●𝗔◗𝗟◗q in
- ∧∧ (𝗟◗q)ᴿ = ↳[n](rᴿ) & r◖𝗱n ϵ t1 &
+ ∧∧ (𝗟◗q)ᴿ = ↳[n](𝗟◗q)ᴿ & r◖𝗱n ϵ t1 &
t1[⋔r←↑[𝐮❨n❩](t1⋔(p◖𝗦))] ⇔ t2
.
@(ex_intro … ((↑[p●𝗔◗𝗟◗q]f)@⧣❨n❩)) @and3_intro
[ -Ht1 -Ht2
<lift_rmap_L_dx >lift_path_L_sn
- >list_append_rcons_sn in H1n; <reverse_append #H1n
- <(lift_path_head … H1n) -H1n //
+ <(lift_path_head … H1n) in ⊢ (??%?); -H1n //
| lapply (in_comp_lift_path_term f … Ht1) -Ht2 -Ht1 -H1n
<lift_path_d_dx #Ht1 //
| lapply (lift_term_eq_repl_dx f … Ht2) -Ht2 #Ht2 -Ht1
@(stream_eq_trans … (tr_compose_uni_dx …))
@tr_compose_eq_repl //
>list_append_rcons_sn in H1n; #H1n >lift_rmap_A_dx
- /2 width=1 by tls_lift_rmap_append_closed/
+ /2 width=1 by tls_lift_rmap_closed/
(* Note: crux of the proof ends *)
]
qed.
@(ex_intro … (↑♭q)) @and3_intro
[ -H1t1 -H2t1 -Ht1 -Ht2
>structure_L_sn >structure_reverse
- >H1n >path_head_structure_depth <H1n -H1n //
+ >H1n in ⊢ (??%?); >path_head_structure_depth <H1n -H1n //
| lapply (in_comp_unwind2_path_term f … Ht1) -Ht2 -Ht1 -H1t1 -H2t1
- <unwind2_path_d_dx
- >list_append_rcons_sn in H1n; <reverse_append #H1n
- lapply (unwind2_rmap_append_pap_closed f … H1n)
+ <unwind2_path_d_dx >(list_append_rcons_sn … p) <reverse_append
+ lapply (unwind2_rmap_append_pap_closed f … (p◖𝗔)ᴿ … H1n) -H1n
<reverse_lcons <depth_L_dx #H2n
- lapply (eq_inv_ninj_bi … H2n) -H2n #H2n <H2n -H2n -H1n #Ht1 //
+ lapply (eq_inv_ninj_bi … H2n) -H2n #H2n <H2n -H2n #Ht1 //
| lapply (unwind2_term_eq_repl_dx f … Ht2) -Ht2 #Ht2
@(subset_eq_trans … Ht2) -t2
@(subset_eq_trans … (unwind2_term_fsubst …))
@(subset_eq_canc_dx … (unwind2_term_after_lift …))
@unwind2_term_eq_repl_sn
(* Note: crux of the proof begins *)
- >list_append_rcons_sn in H1n; <reverse_append #H1n
+ >list_append_rcons_sn <reverse_append
@(stream_eq_trans … (tr_compose_uni_dx …))
@tr_compose_eq_repl
[ <unwind2_rmap_append_pap_closed //
| >unwind2_rmap_A_sn <reverse_rcons
- /2 width=1 by tls_unwind2_rmap_append_closed/
+ /2 width=1 by tls_unwind2_rmap_closed/
]
(* Note: crux of the proof ends *)
| //
(* Constructions with head for path *****************************************)
lemma lift_path_head (f) (p) (q) (n):
- pᴿ = ↳[n](pᴿ●qᴿ) →
- ↳[↑[q●p]f@❨n❩](↑[f](q●p))ᴿ = (↑[↑[q]f]p)ᴿ.
+ pᴿ = ↳[n](pᴿ) →
+ ↳[↑[q●p]f@❨n❩](↑[↑[q]f]p)ᴿ = (↑[↑[q]f]p)ᴿ.
#f #p @(list_ind_rcons … p) -p
[ #q #n #H0
<(eq_inv_path_empty_head … H0) -H0
[ <reverse_rcons <path_head_d_sn #H0
elim (eq_inv_list_lcons_bi ????? H0) -H0 #_ #H0
<list_append_assoc <lift_rmap_d_dx <lift_path_d_dx <reverse_rcons
- <tr_xap_succ_nap <path_head_d_sn >tr_xap_succ_nap
- <lift_path_d_dx >lift_rmap_append <reverse_rcons
- <(IH … H0) -IH -H0 <tr_xap_plus //
+ <tr_xap_succ_nap <path_head_d_sn
+ <(IH … H0) in ⊢ (???%); -IH -H0 <tr_xap_plus //
| <reverse_rcons <path_head_m_sn #H0
elim (eq_inv_list_lcons_bi ????? H0) -H0 #_ #H0
<list_append_assoc <lift_rmap_m_dx <lift_path_m_dx <reverse_rcons
- <tr_xap_succ_nap <path_head_m_sn >tr_xap_succ_nap
- <lift_path_m_dx <reverse_rcons
- <(IH … H0) -IH -H0 //
+ <tr_xap_succ_nap <path_head_m_sn
+ <(IH … H0) in ⊢ (???%); -IH -H0 //
| <reverse_rcons <path_head_L_sn #H0
elim (eq_inv_list_lcons_bi ????? H0) -H0 #_ #H0
<list_append_assoc <lift_rmap_L_dx <lift_path_L_dx <reverse_rcons
- <tr_xap_succ_nap <path_head_L_sn >tr_xap_succ_nap
- <lift_path_L_dx <reverse_rcons
- <(IH … H0) -IH -H0 //
+ <tr_xap_succ_nap <path_head_L_sn
+ <(IH … H0) in ⊢ (???%); -IH -H0 //
| <reverse_rcons <path_head_A_sn #H0
elim (eq_inv_list_lcons_bi ????? H0) -H0 #_ #H0
<list_append_assoc <lift_rmap_A_dx <lift_path_A_dx <reverse_rcons
- <tr_xap_succ_nap <path_head_A_sn >tr_xap_succ_nap
- <lift_path_A_dx <reverse_rcons
- <(IH … H0) -IH -H0 //
+ <tr_xap_succ_nap <path_head_A_sn
+ <(IH … H0) in ⊢ (???%); -IH -H0 //
| <reverse_rcons <path_head_S_sn #H0
elim (eq_inv_list_lcons_bi ????? H0) -H0 #_ #H0
<list_append_assoc <lift_rmap_S_dx <lift_path_S_dx <reverse_rcons
- <tr_xap_succ_nap <path_head_S_sn >tr_xap_succ_nap
- <lift_path_S_dx <reverse_rcons
- <(IH … H0) -IH -H0 //
+ <tr_xap_succ_nap <path_head_S_sn
+ <(IH … H0) in ⊢ (???%); -IH -H0 //
]
]
]
(* Constructions with path_head *********************************************)
-lemma tls_plus_lift_rmap_reverse_closed (f) (q) (p) (n) (k):
- q = (↳[n]q)●p →
- ⇂*[k]↑[pᴿ]f ≗ ⇂*[n+k]↑[qᴿ]f.
+lemma tls_plus_lift_rmap_reverse_closed (f) (q) (n) (k):
+ q = ↳[n]q →
+ ⇂*[k]f ≗ ⇂*[n+k]↑[qᴿ]f.
#f #q elim q -q
-[ #p #n #k #Hp
- elim (eq_inv_list_empty_append … Hp) -Hp #Hn #H0 destruct
- <path_head_empty in Hn; #Hn
- <(eq_inv_empty_labels … Hn) -n //
-| #l #q #IH #p #n @(nat_ind_succ … n) -n //
+[ #n #k #Hq
+ <(eq_inv_path_empty_head … Hq) -n //
+| #l #q #IH #n @(nat_ind_succ … n) -n //
#n #_ #k cases l [ #m ]
- [ <path_head_d_sn <list_append_lcons_sn #Hp
- elim (eq_inv_list_lcons_bi ????? Hp) -Hp #_ #Hp <nrplus_inj_sn
+ [ <path_head_d_sn #Hq
+ elim (eq_inv_list_lcons_bi ????? Hq) -Hq #_ #Hp <nrplus_inj_sn
<reverse_lcons
@(stream_eq_trans … (tls_lift_rmap_d_dx …))
>nrplus_inj_dx >nrplus_inj_sn >nrplus_inj_sn <nplus_plus_comm_23
>nsucc_unfold /2 width=1 by/
- | <path_head_m_sn <list_append_lcons_sn #Hp
- elim (eq_inv_list_lcons_bi ????? Hp) -Hp #_ #Hp
+ | <path_head_m_sn #Hq
+ elim (eq_inv_list_lcons_bi ????? Hq) -Hq #_ #Hq
<reverse_lcons <lift_rmap_m_dx /2 width=1 by/
- | <path_head_L_sn <list_append_lcons_sn #Hp
- elim (eq_inv_list_lcons_bi ????? Hp) -Hp #_ #Hp
+ | <path_head_L_sn #Hq
+ elim (eq_inv_list_lcons_bi ????? Hq) -Hq #_ #Hq
<reverse_lcons <lift_rmap_L_dx <nplus_succ_sn /2 width=1 by/
- | <path_head_A_sn <list_append_lcons_sn #Hp
- elim (eq_inv_list_lcons_bi ????? Hp) -Hp #_ #Hp
+ | <path_head_A_sn #Hq
+ elim (eq_inv_list_lcons_bi ????? Hq) -Hq #_ #Hq
<reverse_lcons <lift_rmap_A_dx /2 width=2 by/
- | <path_head_S_sn <list_append_lcons_sn #Hp
- elim (eq_inv_list_lcons_bi ????? Hp) -Hp #_ #Hp
+ | <path_head_S_sn #Hq
+ elim (eq_inv_list_lcons_bi ????? Hq) -Hq #_ #Hq
<reverse_lcons <lift_rmap_S_dx /2 width=2 by/
]
]
qed-.
-lemma tls_lift_rmap_append_closed (f) (p) (q) (n):
- qᴿ = ↳[n](p●q)ᴿ →
- ↑[p]f ≗ ⇂*[n]↑[p●q]f.
-#f #p #q #n #H0
->(reverse_reverse p) >(reverse_reverse q)
+lemma tls_lift_rmap_closed (f) (q) (n):
+ qᴿ = ↳[n](qᴿ) →
+ f ≗ ⇂*[n]↑[q]f.
+#f #q #n #H0
+>(reverse_reverse q)
/2 width=1 by tls_plus_lift_rmap_reverse_closed/
qed.
(* Constructions with path_head *********************************************)
lemma unwind2_rmap_head_xap_le_closed (f) (p) (q) (n) (k):
- p = (↳[n]p)●q → k ≤ n →
- (▶[f]p)@❨k❩ = (▶[f]↳[n]p)@❨k❩.
+ p = ↳[n]p → k ≤ n →
+ ▶[f](p●q)@❨k❩ = ▶[f]↳[n](p●q)@❨k❩.
#f #p elim p -p
-[ #q #n #k #Hq #Hk
- elim (eq_inv_list_empty_append … Hq) -Hq * #_ //
+[ #q #n #k #Hq
+ <(eq_inv_path_empty_head … Hq) -n #Hk
+ <(nle_inv_zero_dx … Hk) -k //
| #l #p #IH #q #n @(nat_ind_succ … n) -n
- [ #k #_ #Hk <(nle_inv_zero_dx … Hk) -k -IH
- <path_head_zero <unwind2_rmap_empty //
+ [ #k #_ #Hk <(nle_inv_zero_dx … Hk) -k -IH //
| #n #_ #k cases l [ #m ]
- [ <path_head_d_sn <list_append_lcons_sn #Hq #Hk
+ [ <path_head_d_sn #Hq #Hk
elim (eq_inv_list_lcons_bi ????? Hq) -Hq #_ #Hq
<unwind2_rmap_d_sn <unwind2_rmap_d_sn
<tr_compose_xap <tr_compose_xap
@(IH … Hq) -IH -Hq (**) (* auto too slow *)
@nle_trans [| @tr_uni_xap ]
/2 width=1 by nle_plus_bi_dx/
- | <path_head_m_sn <list_append_lcons_sn #Hq #Hk
+ | <path_head_m_sn #Hq #Hk
elim (eq_inv_list_lcons_bi ????? Hq) -Hq #_ #Hq
<unwind2_rmap_m_sn <unwind2_rmap_m_sn
/2 width=2 by/
- | <path_head_L_sn <list_append_lcons_sn #Hq
+ | <path_head_L_sn #Hq
@(nat_ind_succ … k) -k // #k #_ #Hk
lapply (nle_inv_succ_bi … Hk) -Hk #Hk
elim (eq_inv_list_lcons_bi ????? Hq) -Hq #_ #Hq
<unwind2_rmap_L_sn <unwind2_rmap_L_sn
<tr_xap_push <tr_xap_push
/3 width=2 by eq_f/
- | <path_head_A_sn <list_append_lcons_sn #Hq #Hk
+ | <path_head_A_sn #Hq #Hk
elim (eq_inv_list_lcons_bi ????? Hq) -Hq #_ #Hq
<unwind2_rmap_A_sn <unwind2_rmap_A_sn
/2 width=2 by/
- | <path_head_S_sn <list_append_lcons_sn #Hq #Hk
+ | <path_head_S_sn #Hq #Hk
elim (eq_inv_list_lcons_bi ????? Hq) -Hq #_ #Hq
<unwind2_rmap_S_sn <unwind2_rmap_S_sn
/2 width=2 by/
]
qed-.
-lemma unwind2_rmap_head_append_xap_closed (f) (p) (q) (n):
- p = ↳[n](p●q) →
+lemma unwind2_rmap_head_xap_closed (f) (p) (q) (n):
+ p = ↳[n]p →
▶[f](p●q)@❨n❩ = ▶[f]↳[n](p●q)@❨n❩.
/2 width=2 by unwind2_rmap_head_xap_le_closed/
qed-.
qed.
lemma unwind2_rmap_append_pap_closed (f) (p) (q) (n:pnat):
- p = ↳[n](p●q) →
+ p = ↳[n]p →
♭p = ninj (▶[f](p●q)@⧣❨n❩).
#f #p #q #n #Hn
->tr_xap_ninj >Hn in ⊢ (??%?);
->(unwind2_rmap_head_append_xap_closed … Hn) -Hn
+>tr_xap_ninj >(path_head_refl_append q … Hn) in ⊢ (??%?);
+>(unwind2_rmap_head_xap_closed … Hn) -Hn
<path_head_depth //
qed.
lemma tls_unwind2_rmap_plus_closed (f) (p) (q) (n) (k):
- p = (↳[n]p)●q →
- ⇂*[k]▶[f]q ≗ ⇂*[n+k]▶[f]p.
+ p = ↳[n]p →
+ ⇂*[k]▶[f]q ≗ ⇂*[n+k]▶[f](p●q).
#f #p elim p -p
[ #q #n #k #Hq
- elim (eq_inv_list_empty_append … Hq) -Hq #Hn #H0 destruct
- <path_head_empty in Hn; #Hn
- <(eq_inv_empty_labels … Hn) -n //
+ <(eq_inv_path_empty_head … Hq) -n //
| #l #p #IH #q #n @(nat_ind_succ … n) -n //
#n #_ #k cases l [ #m ]
- [ <path_head_d_sn <list_append_lcons_sn #Hq
+ [ <path_head_d_sn #Hq
elim (eq_inv_list_lcons_bi ????? Hq) -Hq #_ #Hq <nrplus_inj_sn
@(stream_eq_trans … (tls_unwind2_rmap_d_sn …))
>nrplus_inj_dx >nrplus_inj_sn >nrplus_inj_sn <nplus_plus_comm_23
/2 width=1 by/
- | <path_head_m_sn <list_append_lcons_sn #Hq
+ | <path_head_m_sn #Hq
elim (eq_inv_list_lcons_bi ????? Hq) -Hq #_ #Hq
<unwind2_rmap_m_sn /2 width=1 by/
- | <path_head_L_sn <list_append_lcons_sn #Hq
+ | <path_head_L_sn #Hq
elim (eq_inv_list_lcons_bi ????? Hq) -Hq #_ #Hq
<unwind2_rmap_L_sn <nplus_succ_sn /2 width=1 by/
- | <path_head_A_sn <list_append_lcons_sn #Hq
+ | <path_head_A_sn #Hq
elim (eq_inv_list_lcons_bi ????? Hq) -Hq #_ #Hq
<unwind2_rmap_A_sn /2 width=2 by/
- | <path_head_S_sn <list_append_lcons_sn #Hq
+ | <path_head_S_sn #Hq
elim (eq_inv_list_lcons_bi ????? Hq) -Hq #_ #Hq
<unwind2_rmap_S_sn /2 width=2 by/
]
]
qed-.
-lemma tls_unwind2_rmap_append_closed (f) (p) (q) (n):
- p = ↳[n](p●q) →
+lemma tls_unwind2_rmap_closed (f) (p) (q) (n):
+ p = ↳[n]p →
▶[f]q ≗ ⇂*[n]▶[f](p●q).
/2 width=1 by tls_unwind2_rmap_plus_closed/
qed.