--- /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 *)
+(* *)
+(**************************************************************************)
+
+(* NOTATION FOR DELAYED UPDATING ********************************************)
+
+notation "hvbox( t1 โก๐๐[ break term 46 r ] break term 46 t2 )"
+ non associative with precedence 45
+ for @{ 'BlackRightArrowDF $t1 $r $t2 }.
+++ /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 *)
-(* *)
-(**************************************************************************)
-
-(* NOTATION FOR DELAYED UPDATING ********************************************)
-
-notation "hvbox( t1 โก๐๐[ break term 46 p, break term 46 q ] break term 46 t2 )"
- non associative with precedence 45
- for @{ 'BlackRightArrowDF $t1 $p $q $t2 }.
--- /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 *)
+(* *)
+(**************************************************************************)
+
+(* NOTATION FOR DELAYED UPDATING ********************************************)
+
+notation "hvbox( t1 โก๐ข๐[ break term 46 r ] break term 46 t2 )"
+ non associative with precedence 45
+ for @{ 'BlackRightArrowIF $t1 $r $t2 }.
+++ /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 *)
-(* *)
-(**************************************************************************)
-
-(* NOTATION FOR DELAYED UPDATING ********************************************)
-
-notation "hvbox( t1 โก๐ข๐[ break term 46 p, break term 46 q ] break term 46 t2 )"
- non associative with precedence 45
- for @{ 'BlackRightArrowIF $t1 $p $q $t2 }.
include "delayed_updating/syntax/prototerm_eq.ma".
include "delayed_updating/syntax/path_head.ma".
include "delayed_updating/syntax/path_depth.ma".
-include "delayed_updating/notation/relations/black_rightarrow_df_4.ma".
+include "delayed_updating/notation/relations/black_rightarrow_df_3.ma".
+include "ground/xoa/ex_4_3.ma".
(* DELAYED FOCUSED REDUCTION ************************************************)
-definition dfr (p) (q): relation2 prototerm prototerm โ
- ฮปt1,t2. โk:pnat.
- let r โ pโ๐โ๐โq in
- โงโง ๐โq = โณ[k](๐โq) & rโ๐ฑk ฯต t1 &
- t1[โrโ๐k.(t1โ(pโ๐ฆ))] โ t2
+(**) (* explicit ninj because we cannot declare the expectd type of k *)
+definition dfr (r): relation2 prototerm prototerm โ
+ ฮปt1,t2.
+ โโp,q,k. pโ๐โ๐โq = r &
+ (๐โq) = โณ[ninj k](๐โq) & rโ๐ฑk ฯต t1 &
+ t1[โrโ๐k.(t1โ(pโ๐ฆ))] โ t2
.
interpretation
"focused reduction with delayed updating (prototerm)"
- 'BlackRightArrowDF t1 p q t2 = (dfr p q t1 t2).
+ 'BlackRightArrowDF t1 r t2 = (dfr r t1 t2).
(* Main destructions with ifr ***********************************************)
-theorem dfr_des_ifr (f) (p) (q) (t1) (t2): t1 ฯต ๐ โ
- t1 โก๐๐[p,q] t2 โ โผ[f]t1 โก๐ข๐[โp,โq] โผ[f]t2.
-#f #p #q #t1 #t2 #H0t1
-* #k * #H1k #Ht1 #Ht2
-@(ex_intro โฆ (โโญq)) @and3_intro
-[ -H0t1 -Ht1 -Ht2
+theorem dfr_des_ifr (f) (t1) (t2) (r): t1 ฯต ๐ โ
+ t1 โก๐๐[r] t2 โ โผ[f]t1 โก๐ข๐[โr] โผ[f]t2.
+#f #t1 #t2 #r #H0t1
+* #p #q #k #Hr #H1k #Ht1 #Ht2 destruct
+@(ex4_3_intro โฆ (โp) (โq) (โโญq))
+[ -H0t1 -H1k -Ht1 -Ht2 //
+| -H0t1 -Ht1 -Ht2
>structure_L_sn
>H1k in โข (??%?); >path_head_structure_depth <H1k -H1k //
| lapply (in_comp_unwind2_path_term f โฆ Ht1) -Ht2 -Ht1 -H0t1
lapply (eq_inv_ninj_bi โฆ H2k) -H2k #H2k <H2k -H2k #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 โฆ (unwind2_term_fsubst_ppc โฆ))
[ @fsubst_eq_repl [ // | // ]
@(subset_eq_trans โฆ (unwind2_term_iref โฆ))
@(subset_eq_canc_sn โฆ (lift_term_eq_repl_dx โฆ))
(* Constructions with lift **************************************************)
-theorem dfr_lift_bi (f) (p) (q) (t1) (t2):
- t1 โก๐๐[p,q] t2 โ โ[f]t1 โก๐๐[โ[f]p,โ[โ[pโ๐โ๐]f]q] โ[f]t2.
-#f #p #q #t1 #t2
-* #k * #H1k #Ht1 #Ht2
-@(ex_intro โฆ ((โ[pโ๐โ๐โq]f)๏ผ โงฃโจkโฉ)) @and3_intro
-[ -Ht1 -Ht2
+(* โ[โ[pโ๐โ๐]f]q *)
+
+theorem dfr_lift_bi (f) (t1) (t2) (r):
+ t1 โก๐๐[r] t2 โ โ[f]t1 โก๐๐[โ[f]r] โ[f]t2.
+#f #t1 #t2 #r
+* #p #q #k #Hr #H1k #Ht1 #Ht2 destruct
+@(ex4_3_intro โฆ (โ[f]p) (โ[โ[pโ๐โ๐]f]q) ((โ[pโ๐โ๐โq]f)๏ผ โงฃโจkโฉ))
+[ -H1k -Ht1 -Ht2 //
+| -Ht1 -Ht2
<lift_rmap_L_dx >lift_path_L_sn
<(lift_path_head_closed โฆ H1k) in โข (??%?); -H1k //
| lapply (in_comp_lift_path_term f โฆ Ht1) -Ht2 -Ht1 -H1k
include "delayed_updating/substitution/lift_prototerm.ma".
include "delayed_updating/syntax/prototerm_eq.ma".
include "delayed_updating/syntax/path_head.ma".
-include "delayed_updating/notation/relations/black_rightarrow_if_4.ma".
+include "delayed_updating/notation/relations/black_rightarrow_if_3.ma".
include "ground/relocation/tr_uni.ma".
+include "ground/xoa/ex_4_3.ma".
(* IMMEDIATE FOCUSED REDUCTION ************************************************)
-definition ifr (p) (q): relation2 prototerm prototerm โ
- ฮปt1,t2. โk:pnat.
- let r โ pโ๐โ๐โq in
- โงโง ๐โq = โณ[k](๐โq) & rโ๐ฑk ฯต t1 &
- t1[โrโโ[๐ฎโจkโฉ](t1โ(pโ๐ฆ))] โ t2
+(**) (* explicit ninj because we cannot declare the expectd type of k *)
+definition ifr (r): relation2 prototerm prototerm โ
+ ฮปt1,t2.
+ โโp,q,k. pโ๐โ๐โq = r &
+ (๐โq) = โณ[ninj k](๐โq) & rโ๐ฑk ฯต t1 &
+ t1[โrโโ[๐ฎโจninj kโฉ](t1โ(pโ๐ฆ))] โ t2
.
interpretation
"focused reduction with immediate updating (prototerm)"
- 'BlackRightArrowIF t1 p q t2 = (ifr p q t1 t2).
+ 'BlackRightArrowIF t1 r t2 = (ifr r t1 t2).
(* Constructions with lift **************************************************)
-theorem ifr_lift_bi (f) (p) (q) (t1) (t2):
- t1 โก๐ข๐[p,q] t2 โ โ[f]t1 โก๐ข๐[โ[f]p,โ[โ[pโ๐โ๐]f]q] โ[f]t2.
-#f #p #q #t1 #t2
-* #k * #H1k #Ht1 #Ht2
-@(ex_intro โฆ ((โ[pโ๐โ๐โq]f)๏ผ โงฃโจkโฉ)) @and3_intro
-[ -Ht1 -Ht2
+theorem ifr_lift_bi (f) (t1) (t2) (r):
+ t1 โก๐ข๐[r] t2 โ โ[f]t1 โก๐ข๐[โ[f]r] โ[f]t2.
+#f #t1 #t2 #r
+* #p #q #k #Hr #H1k #Ht1 #Ht2 destruct
+@(ex4_3_intro โฆ (โ[f]p) (โ[โ[pโ๐โ๐]f]q) ((โ[pโ๐โ๐โq]f)๏ผ โงฃโจkโฉ))
+[ -H1k -Ht1 -Ht2 //
+| -Ht1 -Ht2
<lift_rmap_L_dx >lift_path_L_sn
<(lift_path_head_closed โฆ H1k) in โข (??%?); -H1k //
| lapply (in_comp_lift_path_term f โฆ Ht1) -Ht2 -Ht1 -H1k
include "delayed_updating/unwind/unwind2_rmap_head.ma".
include "delayed_updating/substitution/fsubst_eq.ma".
-include "delayed_updating/substitution/lift_prototerm_proper.ma".
include "delayed_updating/substitution/lift_prototerm_eq.ma".
include "delayed_updating/syntax/path_head_structure.ma".
(* Constructions with unwind2 ***********************************************)
-lemma ifr_unwind_bi (f) (p) (q) (t1) (t2):
- t1 ฯต ๐ โ t1โ(pโ๐ฆ) ฯต ๐ โ
- t1 โก๐ข๐[p,q] t2 โ โผ[f]t1 โก๐ข๐[โp,โq] โผ[f]t2.
-#f #p #q #t1 #t2 #H1t1 #H2t1
-* #k * #H1k #Ht1 #Ht2
-@(ex_intro โฆ (โโญq)) @and3_intro
-[ -H1t1 -H2t1 -Ht1 -Ht2
+lemma ifr_unwind_bi (f) (t1) (t2) (r):
+ t1 ฯต ๐ โ r ฯต ๐ โ
+ t1 โก๐ข๐[r] t2 โ โผ[f]t1 โก๐ข๐[โr] โผ[f]t2.
+#f #t1 #t2 #r #H1t1 #H2r
+* #p #q #k #Hr #H1k #Ht1 #Ht2 destruct
+@(ex4_3_intro โฆ (โp) (โq) (โโญq))
+[ -H1t1 -H2r -H1k -Ht1 -Ht2 //
+| -H1t1 -H2r -Ht1 -Ht2
>structure_L_sn
>H1k in โข (??%?); >path_head_structure_depth <H1k -H1k //
-| lapply (in_comp_unwind2_path_term f โฆ Ht1) -Ht2 -Ht1 -H1t1 -H2t1
+| lapply (in_comp_unwind2_path_term f โฆ Ht1) -Ht2 -Ht1 -H1t1 -H2r
<unwind2_path_d_dx <list_append_rcons_sn
lapply (unwind2_rmap_append_pap_closed f โฆ (pโ๐) โฆ H1k) -H1k
<depth_L_sn #H2k
lapply (eq_inv_ninj_bi โฆ H2k) -H2k #H2k <H2k -H2k #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 โฆ (unwind2_term_fsubst_pic โฆ))
[ @fsubst_eq_repl [ // | // ]
@(subset_eq_canc_sn โฆ (lift_term_eq_repl_dx โฆ))
[ @unwind2_term_grafted_S /2 width=2 by ex_intro/ | skip ] -Ht1
(* Note: crux of the proof ends *)
| //
| /2 width=2 by ex_intro/
- | /2 width=6 by lift_term_proper/
+ | //
]
]
qed.
(* PROPER CONDITION FOR PROTOTERM *******************************************)
-(* Constructions with inner condition for prototerm *************************)
+(* Constructions with pic ***************************************************)
lemma term_proper_outer (t):
t โงธโฌ ๐ โ t ฯต ๐.
(* TAILED UNWIND FOR PATH ***************************************************)
-(* Constructions with inner condition for path ******************************)
+(* Constructions with pic ***************************************************)
-lemma unwind2_path_inner (f) (p):
+lemma unwind2_path_pic (f) (p):
p ฯต ๐ โ โp = โผ[f]p.
#f * // * // #k #q #Hq
elim (pic_inv_d_dx โฆ Hq)
qed-.
-(* Constructions with append and inner condition for path *******************)
+(* Constructions with append and pic ****************************************)
-lemma unwind2_path_append_inner_sn (f) (p) (q): p ฯต ๐ โ
+lemma unwind2_path_append_pic_sn (f) (p) (q): p ฯต ๐ โ
(โp)โ(โผ[โถ[f]p]q) = โผ[f](pโq).
#f #p * [ #Hp | * [ #k ] #q #_ ] //
-[ <(unwind2_path_inner โฆ Hp) -Hp //
+[ <(unwind2_path_pic โฆ Hp) -Hp //
| <unwind2_path_d_dx <unwind2_path_d_dx
/2 width=3 by trans_eq/
| <unwind2_path_L_dx <unwind2_path_L_dx //
]
qed.
-(* Constructions with append and proper condition for path ******************)
+(* Constructions with append and ppc ****************************************)
-lemma unwind2_path_append_proper_dx (f) (p) (q): q ฯต ๐ โ
+lemma unwind2_path_append_ppc_dx (f) (p) (q): q ฯต ๐ โ
(โp)โ(โผ[โถ[f]p]q) = โผ[f](pโq).
#f #p * [ #Hq | * [ #k ] #q #_ ] //
[ elim (ppc_inv_empty โฆ Hq)
lemma unwind2_path_d_lcons (f) (p) (l) (k:pnat):
โผ[fโ๐ฎโจkโฉ](lโp) = โผ[f](๐ฑkโlโp).
-#f #p #l #k <unwind2_path_append_proper_dx in โข (???%); //
+#f #p #l #k <unwind2_path_append_ppc_dx in โข (???%); //
qed.
lemma unwind2_path_m_sn (f) (p):
โผ[f]p = โผ[f](๐บโp).
-#f #p <unwind2_path_append_inner_sn //
+#f #p <unwind2_path_append_pic_sn //
qed.
lemma unwind2_path_L_sn (f) (p):
(๐โโผ[โซฏf]p) = โผ[f](๐โp).
-#f #p <unwind2_path_append_inner_sn //
+#f #p <unwind2_path_append_pic_sn //
qed.
lemma unwind2_path_A_sn (f) (p):
(๐โโผ[f]p) = โผ[f](๐โp).
-#f #p <unwind2_path_append_inner_sn //
+#f #p <unwind2_path_append_pic_sn //
qed.
lemma unwind2_path_S_sn (f) (p):
(๐ฆโโผ[f]p) = โผ[f](๐ฆโp).
-#f #p <unwind2_path_append_inner_sn //
+#f #p <unwind2_path_append_pic_sn //
qed.
-(* Destructions with inner condition for path *******************************)
+(* Destructions with pic ****************************************************)
-lemma unwind2_path_des_inner (f) (p):
+lemma unwind2_path_des_pic (f) (p):
โผ[f]p ฯต ๐ โ p ฯต ๐.
#f * // * [ #k ] #p //
<unwind2_path_d_dx #H0
elim (pic_inv_d_dx โฆ H0)
qed-.
-(* Destructions with append and inner condition for path ********************)
+(* Destructions with append and pic *****************************************)
-lemma unwind2_path_des_append_inner_sn (f) (p) (q1) (q2):
+lemma unwind2_path_des_append_pic_sn (f) (p) (q1) (q2):
q1 ฯต ๐ โ q1โq2 = โผ[f]p โ
โโp1,p2. q1 = โp1 & q2 = โผ[โถ[f]p1]p2 & p1โp2 = p.
#f #p #q1 * [| * [ #k ] #q2 ] #Hq1
[ <list_append_empty_sn #H0 destruct
- lapply (unwind2_path_des_inner โฆ Hq1) -Hq1 #Hp
- <(unwind2_path_inner โฆ Hp) -Hp
+ lapply (unwind2_path_des_pic โฆ Hq1) -Hq1 #Hp
+ <(unwind2_path_pic โฆ Hp) -Hp
/2 width=5 by ex3_2_intro/
| #H0 elim (eq_inv_d_dx_unwind2_path โฆ H0) -H0 #r #h #Hr #H1 #H2 destruct
elim (eq_inv_append_structure โฆ Hr) -Hr #s1 #s2 #H1 #H2 #H3 destruct
| #H0 elim (eq_inv_L_dx_unwind2_path โฆ H0) -H0 #r1 #r2 #Hr1 #Hr2 #H0 destruct
elim (eq_inv_append_structure โฆ Hr1) -Hr1 #s1 #s2 #H1 #H2 #H3 destruct
@(ex3_2_intro โฆ s1 (s2โ๐โr2)) //
- <unwind2_path_append_proper_dx //
+ <unwind2_path_append_ppc_dx //
<unwind2_path_L_sn <Hr2 -Hr2 //
| #H0 elim (eq_inv_A_dx_unwind2_path โฆ H0) -H0 #r1 #r2 #Hr1 #Hr2 #H0 destruct
elim (eq_inv_append_structure โฆ Hr1) -Hr1 #s1 #s2 #H1 #H2 #H3 destruct
@(ex3_2_intro โฆ s1 (s2โ๐โr2)) //
- <unwind2_path_append_proper_dx //
+ <unwind2_path_append_ppc_dx //
<unwind2_path_A_sn <Hr2 -Hr2 //
| #H0 elim (eq_inv_S_dx_unwind2_path โฆ H0) -H0 #r1 #r2 #Hr1 #Hr2 #H0 destruct
elim (eq_inv_append_structure โฆ Hr1) -Hr1 #s1 #s2 #H1 #H2 #H3 destruct
@(ex3_2_intro โฆ s1 (s2โ๐ฆโr2)) //
- <unwind2_path_append_proper_dx //
+ <unwind2_path_append_ppc_dx //
<unwind2_path_S_sn <Hr2 -Hr2 //
]
qed-.
-(* Inversions with append and proper condition for path *********************)
+(* Inversions with append and ppc *******************************************)
-lemma unwind2_path_inv_append_proper_dx (f) (p) (q1) (q2):
+lemma unwind2_path_inv_append_ppc_dx (f) (p) (q1) (q2):
q2 ฯต ๐ โ q1โq2 = โผ[f]p โ
โโp1,p2. q1 = โp1 & q2 = โผ[โถ[f]p1]p2 & p1โp2 = p.
#f #p #q1 * [| * [ #k ] #q2 ] #Hq1
| #H0 elim (eq_inv_L_dx_unwind2_path โฆ H0) -H0 #r1 #r2 #Hr1 #Hr2 #H0 destruct
elim (eq_inv_append_structure โฆ Hr1) -Hr1 #s1 #s2 #H1 #H2 #H3 destruct
@(ex3_2_intro โฆ s1 (s2โ๐โr2)) //
- <unwind2_path_append_proper_dx //
+ <unwind2_path_append_ppc_dx //
<unwind2_path_L_sn <Hr2 -Hr2 //
| #H0 elim (eq_inv_A_dx_unwind2_path โฆ H0) -H0 #r1 #r2 #Hr1 #Hr2 #H0 destruct
elim (eq_inv_append_structure โฆ Hr1) -Hr1 #s1 #s2 #H1 #H2 #H3 destruct
@(ex3_2_intro โฆ s1 (s2โ๐โr2)) //
- <unwind2_path_append_proper_dx //
+ <unwind2_path_append_ppc_dx //
<unwind2_path_A_sn <Hr2 -Hr2 //
| #H0 elim (eq_inv_S_dx_unwind2_path โฆ H0) -H0 #r1 #r2 #Hr1 #Hr2 #H0 destruct
elim (eq_inv_append_structure โฆ Hr1) -Hr1 #s1 #s2 #H1 #H2 #H3 destruct
@(ex3_2_intro โฆ s1 (s2โ๐ฆโr2)) //
- <unwind2_path_append_proper_dx //
+ <unwind2_path_append_ppc_dx //
<unwind2_path_S_sn <Hr2 -Hr2 //
]
qed-.
elim (eq_inv_d_dx_unwind2_path โฆ H0) -H0 #r1 #r2 #Hr1 #H1 #H2 destruct
/2 width=5 by ex4_2_intro/
| >list_cons_comm #H0
- elim (unwind2_path_inv_append_proper_dx โฆ H0) -H0 // #r1 #r2 #Hr1 #_ #_ -r2
+ elim (unwind2_path_inv_append_ppc_dx โฆ H0) -H0 // #r1 #r2 #Hr1 #_ #_ -r2
elim (eq_inv_d_dx_structure โฆ Hr1)
]
qed-.
(๐บโq) = โผ[f]p โ โฅ.
#f #q #p
>list_cons_comm #H0
-elim (unwind2_path_des_append_inner_sn โฆ H0) <list_cons_comm in H0; //
+elim (unwind2_path_des_append_pic_sn โฆ H0) <list_cons_comm in H0; //
#H0 #r1 #r2 #Hr1 #H1 #H2 destruct
elim (eq_inv_m_dx_structure โฆ Hr1)
qed-.
โโr1,r2. ๐ = โr1 & q = โผ[โซฏโถ[f]r1]r2 & r1โ๐โr2 = p.
#f #q #p
>list_cons_comm #H0
-elim (unwind2_path_des_append_inner_sn โฆ H0) <list_cons_comm in H0; //
+elim (unwind2_path_des_append_pic_sn โฆ H0) <list_cons_comm in H0; //
#H0 #r1 #r2 #Hr1 #H1 #H2 destruct
elim (eq_inv_L_dx_structure โฆ Hr1) -Hr1 #s1 #s2 #H1 #_ #H3 destruct
<list_append_assoc in H0; <list_append_assoc
-<unwind2_path_append_proper_dx //
+<unwind2_path_append_ppc_dx //
<unwind2_path_L_sn <H1 <list_append_empty_dx #H0
elim (eq_inv_list_rcons_bi ????? H0) -H0 #H0 #_
/2 width=5 by ex3_2_intro/
โโr1,r2. ๐ = โr1 & q = โผ[โถ[f]r1]r2 & r1โ๐โr2 = p.
#f #q #p
>list_cons_comm #H0
-elim (unwind2_path_des_append_inner_sn โฆ H0) <list_cons_comm in H0; //
+elim (unwind2_path_des_append_pic_sn โฆ H0) <list_cons_comm in H0; //
#H0 #r1 #r2 #Hr1 #H1 #H2 destruct
elim (eq_inv_A_dx_structure โฆ Hr1) -Hr1 #s1 #s2 #H1 #_ #H3 destruct
<list_append_assoc in H0; <list_append_assoc
-<unwind2_path_append_proper_dx //
+<unwind2_path_append_ppc_dx //
<unwind2_path_A_sn <H1 <list_append_empty_dx #H0
elim (eq_inv_list_rcons_bi ????? H0) -H0 #H0 #_
/2 width=5 by ex3_2_intro/
โโr1,r2. ๐ = โr1 & q = โผ[โถ[f]r1]r2 & r1โ๐ฆโr2 = p.
#f #q #p
>list_cons_comm #H0
-elim (unwind2_path_des_append_inner_sn โฆ H0) <list_cons_comm in H0; //
+elim (unwind2_path_des_append_pic_sn โฆ H0) <list_cons_comm in H0; //
#H0 #r1 #r2 #Hr1 #H1 #H2 destruct
elim (eq_inv_S_dx_structure โฆ Hr1) -Hr1 #s1 #s2 #H1 #_ #H3 destruct
<list_append_assoc in H0; <list_append_assoc
-<unwind2_path_append_proper_dx //
+<unwind2_path_append_ppc_dx //
<unwind2_path_S_sn <H1 <list_append_empty_dx #H0
elim (eq_inv_list_rcons_bi ????? H0) -H0 #H0 #_
/2 width=5 by ex3_2_intro/
โผ[โถ[f]p](tโp) โ (โผ[f]t)โ(โp).
#f #t #p #Hp #q * #r #Hr #H0 destruct
@(ex2_intro โฆ Hr) -Hr
-<unwind2_path_append_inner_sn //
+<unwind2_path_append_pic_sn //
qed-.
lemma unwind2_term_grafted_dx (f) (t) (p): p ฯต ๐ โ p ฯต โตt โ t ฯต ๐ โ
(โผ[f]t)โ(โp) โ โผ[โถ[f]p](tโp).
#f #t #p #H1p #H2p #Ht #q * #r #Hr #H0
-elim (unwind2_path_des_append_inner_sn โฆ (sym_eq โฆ H0)) -H0 //
+elim (unwind2_path_des_append_pic_sn โฆ (sym_eq โฆ H0)) -H0 //
#p0 #q0 #Hp0 #Hq0 #H0 destruct
>(Ht โฆ Hp0) [|*: /2 width=2 by ex_intro/ ] -p
/2 width=1 by in_comp_unwind2_path_term/
(โผ[f]t)โ((โp)โ๐ฆ) โ โผ[โถ[f]p](tโ(pโ๐ฆ)).
#f #t #p #Hp #Ht #q * #r #Hr
>list_append_rcons_sn #H0
-elim (unwind2_path_inv_append_proper_dx โฆ (sym_eq โฆ H0)) -H0 //
+elim (unwind2_path_inv_append_ppc_dx โฆ (sym_eq โฆ H0)) -H0 //
#p0 #q0 #Hp0 #Hq0 #H0 destruct
>(Ht โฆ Hp0) [|*: /2 width=2 by ex_intro/ ] -p
elim (eq_inv_S_sn_unwind2_path โฆ Hq0) -Hq0
(* TAILED UNWIND FOR PRETERM ************************************************)
-(* Constructions with fsubst ************************************************)
+(* Constructions with fsubst and pic ****************************************)
-lemma unwind2_term_fsubst_sn (f) (t) (u) (p): u ฯต ๐ โ
+lemma unwind2_term_fsubst_pic_sn (f) (t) (u) (p): p ฯต ๐ โ
+ (โผ[f]t)[โ(โp)โโผ[โถ[f]p]u] โ โผ[f](t[โpโu]).
+#f #t #u #p #Hp #ql * *
+[ #rl * #r #Hr #H1 #H2 destruct
+ >unwind2_path_append_pic_sn
+ /4 width=3 by in_comp_unwind2_path_term, or_introl, ex2_intro/
+| * #q #Hq #H1 #H0
+ @(ex2_intro โฆ H1) @or_intror @conj // *
+ [ <list_append_empty_sn #H2 destruct
+ elim (unwind2_path_root f q) #r #_ #Hr /2 width=2 by/
+ | #l #r #H2 destruct
+ /3 width=2 by unwind2_path_append_pic_sn/
+ ]
+]
+qed-.
+
+lemma unwind2_term_fsubst_pic_dx (f) (t) (u) (p): p ฯต ๐ โ p ฯต โตt โ t ฯต ๐ โ
+ โผ[f](t[โpโu]) โ (โผ[f]t)[โ(โp)โโผ[โถ[f]p]u].
+#f #t #u #p #Hp #H1p #H2p #ql * #q * *
+[ #r #Hu #H1 #H2 destruct
+ /5 width=3 by unwind2_path_append_pic_sn, ex2_intro, or_introl/
+| #Hq #H0 #H1 destruct
+ @or_intror @conj [ /2 width=1 by in_comp_unwind2_path_term/ ] *
+ [ <list_append_empty_sn #Hr @(H0 โฆ (๐)) -H0
+ <list_append_empty_sn @H2p -H2p
+ /2 width=2 by unwind2_path_des_structure, prototerm_in_comp_root/
+ | #l #r #Hr
+ elim (unwind2_path_inv_append_ppc_dx โฆ Hr) -Hr // #s1 #s2 #Hs1 #_ #H1 destruct
+ lapply (H2p โฆ Hs1) -H2p -Hs1 /2 width=2 by ex_intro/
+ ]
+]
+qed-.
+
+lemma unwind2_term_fsubst_pic (f) (t) (u) (p): p ฯต ๐ โ p ฯต โตt โ t ฯต ๐ โ
+ (โผ[f]t)[โ(โp)โโผ[โถ[f]p]u] โ โผ[f](t[โpโu]).
+/4 width=3 by unwind2_term_fsubst_pic_sn, conj, unwind2_term_fsubst_pic_dx/ qed.
+
+(* Constructions with fsubst and ppc ****************************************)
+
+lemma unwind2_term_fsubst_ppc_sn (f) (t) (u) (p): u ฯต ๐ โ
(โผ[f]t)[โ(โp)โโผ[โถ[f]p]u] โ โผ[f](t[โpโu]).
#f #t #u #p #Hu #ql * *
[ #rl * #r #Hr #H1 #H2 destruct
- >unwind2_path_append_proper_dx
+ >unwind2_path_append_ppc_dx
/4 width=5 by in_comp_unwind2_path_term, in_comp_tpc_trans, or_introl, ex2_intro/
| * #q #Hq #H1 #H0
@(ex2_intro โฆ H1) @or_intror @conj // *
[ <list_append_empty_sn #H2 destruct
elim (unwind2_path_root f q) #r #_ #Hr /2 width=2 by/
| #l #r #H2 destruct
- @H0 -H0 [| <unwind2_path_append_proper_dx /2 width=3 by ppc_rcons/ ]
+ @H0 -H0 [| <unwind2_path_append_ppc_dx /2 width=3 by ppc_rcons/ ]
]
]
qed-.
-lemma unwind2_term_fsubst_dx (f) (t) (u) (p): u ฯต ๐ โ p ฯต โตt โ t ฯต ๐ โ
+lemma unwind2_term_fsubst_ppc_dx (f) (t) (u) (p): u ฯต ๐ โ p ฯต โตt โ t ฯต ๐ โ
โผ[f](t[โpโu]) โ (โผ[f]t)[โ(โp)โโผ[โถ[f]p]u].
#f #t #u #p #Hu #H1p #H2p #ql * #q * *
[ #r #Hu #H1 #H2 destruct
@or_introl @ex2_intro
- [|| <unwind2_path_append_proper_dx /2 width=5 by in_comp_tpc_trans/ ]
+ [|| <unwind2_path_append_ppc_dx /2 width=5 by in_comp_tpc_trans/ ]
/2 width=3 by ex2_intro/
| #Hq #H0 #H1 destruct
@or_intror @conj [ /2 width=1 by in_comp_unwind2_path_term/ ] *
<list_append_empty_sn @H2p -H2p
/2 width=2 by unwind2_path_des_structure, prototerm_in_comp_root/
| #l #r #Hr
- elim (unwind2_path_inv_append_proper_dx โฆ Hr) -Hr // #s1 #s2 #Hs1 #_ #H1 destruct
+ elim (unwind2_path_inv_append_ppc_dx โฆ Hr) -Hr // #s1 #s2 #Hs1 #_ #H1 destruct
lapply (H2p โฆ Hs1) -H2p -Hs1 /2 width=2 by ex_intro/
]
]
qed-.
-lemma unwind2_term_fsubst (f) (t) (u) (p): u ฯต ๐ โ p ฯต โตt โ t ฯต ๐ โ
+lemma unwind2_term_fsubst_ppc (f) (t) (u) (p): u ฯต ๐ โ p ฯต โตt โ t ฯต ๐ โ
(โผ[f]t)[โ(โp)โโผ[โถ[f]p]u] โ โผ[f](t[โpโu]).
-/4 width=3 by unwind2_term_fsubst_sn, conj, unwind2_term_fsubst_dx/ qed.
+/4 width=3 by unwind2_term_fsubst_ppc_sn, conj, unwind2_term_fsubst_ppc_dx/ qed.
(* TAILED UNWIND FOR PROTOTERM **********************************************)
-(* Destructions with inner condition for path *******************************)
+(* Destructions with pic ****************************************************)
-lemma unwind2_term_des_inner (f) (t):
+lemma unwind2_term_des_pic (f) (t):
โผ[f]t โฌ ๐ โ t โฌ ๐.
#f #t * #p * #q #Hq #H0 #Hp destruct
@(subset_ol_i โฆ Hq) -Hq (**) (* auto does not work *)
-@(unwind2_path_des_inner โฆ Hp)
+@(unwind2_path_des_pic โฆ Hp)
qed-.