include "delayed_updating/substitution/lift_eq.ma".
include "delayed_updating/syntax/path_structure.ma".
+include "delayed_updating/syntax/path_inner.ma".
include "delayed_updating/syntax/path_proper.ma".
include "ground/xoa/ex_4_2.ma".
-include "ground/xoa/ex_3_2.ma".
(* LIFT FOR PATH ***********************************************************)
(* Constructions with proper condition for path *****************************)
-lemma lift_append_proper_dx (p2) (p1) (f): źp2 ā
+lemma lift_append_proper_dx (p2) (p1) (f): p2 Ļµ š ā
(āp1)ā(ā[ā[p1]f]p2) = ā[f](p1āp2).
#p2 #p1 @(path_ind_lift ā¦ p1) -p1 //
[ #n | #n #l #p1 |*: #p1 ] #IH #f #Hp2
[ elim (ppc_inv_lcons ā¦ Hp2) -Hp2 #l #q #H destruct //
| <lift_path_d_lcons_sn <IH //
+| <lift_path_m_sn <IH //
| <lift_path_L_sn <IH //
| <lift_path_A_sn <IH //
| <lift_path_S_sn <IH //
]
qed-.
-(* Advanced constructions with structure ************************************)
+(* Constructions with inner condition for path ******************************)
-lemma lift_d_empty_dx (n) (p) (f):
+lemma lift_append_inner_sn (p1) (p2) (f): p1 Ļµ š ā
+ (āp1)ā(ā[ā[p1]f]p2) = ā[f](p1āp2).
+#p1 @(list_ind_rcons ā¦ p1) -p1 // #p1 *
+[ #n ] #_ #p2 #f #Hp1
+[ elim (pic_inv_d_dx ā¦ Hp1)
+| <list_append_rcons_sn <lift_append_proper_dx //
+| <list_append_rcons_sn <lift_append_proper_dx //
+ <structure_L_dx <list_append_rcons_sn //
+| <list_append_rcons_sn <lift_append_proper_dx //
+ <structure_A_dx <list_append_rcons_sn //
+| <list_append_rcons_sn <lift_append_proper_dx //
+ <structure_S_dx <list_append_rcons_sn //
+]
+qed-.
+
+(* Advanced constructions with proj_path ************************************)
+
+lemma lift_path_d_empty_dx (n) (p) (f):
(āp)āš±((ā[p]f)@āØnā©) = ā[f](pāš±n).
#n #p #f <lift_append_proper_dx //
qed.
-lemma lift_L_dx (p) (f):
+lemma lift_path_m_dx (p) (f):
+ āp = ā[f](pāšŗ).
+#p #f <lift_append_proper_dx //
+qed.
+
+lemma lift_path_L_dx (p) (f):
(āp)āš = ā[f](pāš).
#p #f <lift_append_proper_dx //
qed.
-lemma lift_A_dx (p) (f):
+lemma lift_path_A_dx (p) (f):
(āp)āš = ā[f](pāš).
#p #f <lift_append_proper_dx //
qed.
-lemma lift_S_dx (p) (f):
+lemma lift_path_S_dx (p) (f):
(āp)āš¦ = ā[f](pāš¦).
#p #f <lift_append_proper_dx //
qed.
-lemma lift_root (f) (p):
+lemma lift_path_root (f) (p):
āār. š = ār & āpār = ā[f]p.
#f #p @(list_ind_rcons ā¦ p) -p
[ /2 width=3 by ex2_intro/
| <lift_path_d_lcons_sn #H
elim (IH ā¦ H) -IH -H #r #h #Hr #Hh #Hq #Hp destruct
/2 width=5 by ex4_2_intro/
+| <lift_path_m_sn #H
+ elim (IH ā¦ H) -IH -H #r #h #Hr #Hh #Hq #Hp destruct
+ /2 width=5 by ex4_2_intro/
+| <lift_path_L_sn #H destruct
+| <lift_path_A_sn #H destruct
+| <lift_path_S_sn #H destruct
+]
+qed-.
+
+lemma lift_path_inv_m_sn (q) (p) (f):
+ (šŗāq) = ā[f]p ā ā„.
+#q #p @(path_ind_lift ā¦ p) -p
+[| #n | #n #l #p |*: #p ] [|*: #IH ] #f
+[ <lift_path_empty #H destruct
+| <lift_path_d_empty_sn #H destruct
+| <lift_path_d_lcons_sn #H /2 width=2 by/
+| <lift_path_m_sn #H /2 width=2 by/
| <lift_path_L_sn #H destruct
| <lift_path_A_sn #H destruct
| <lift_path_S_sn #H destruct
| <lift_path_d_lcons_sn #H
elim (IH ā¦ H) -IH -H #r1 #r2 #Hr1 #Hq #Hp destruct
/2 width=5 by ex3_2_intro/
+| <lift_path_m_sn #H
+ elim (IH ā¦ H) -IH -H #r1 #r2 #Hr1 #Hq #Hp destruct
+ /2 width=5 by ex3_2_intro/
| <lift_path_L_sn #H destruct -IH
/2 width=5 by ex3_2_intro/
| <lift_path_A_sn #H destruct
| <lift_path_d_lcons_sn #H
elim (IH ā¦ H) -IH -H #r1 #r2 #Hr1 #Hq #Hp destruct
/2 width=5 by ex3_2_intro/
+| <lift_path_m_sn #H
+ elim (IH ā¦ H) -IH -H #r1 #r2 #Hr1 #Hq #Hp destruct
+ /2 width=5 by ex3_2_intro/
| <lift_path_L_sn #H destruct
| <lift_path_A_sn #H destruct -IH
/2 width=5 by ex3_2_intro/
| <lift_path_d_lcons_sn #H
elim (IH ā¦ H) -IH -H #r1 #r2 #Hr1 #Hq #Hp destruct
/2 width=5 by ex3_2_intro/
-| <lift_path_L_sn #H destruct
+| <lift_path_m_sn #H
+ elim (IH ā¦ H) -IH -H #r1 #r2 #Hr1 #Hq #Hp destruct
+ /2 width=5 by ex3_2_intro/| <lift_path_L_sn #H destruct
| <lift_path_A_sn #H destruct
| <lift_path_S_sn #H destruct -IH
/2 width=5 by ex3_2_intro/
(* Inversions with proper condition for path ********************************)
-lemma lift_inv_append_proper_dx (q2) (q1) (p) (f): źq2 ā
- q1āq2 = ā[f]p ā
+lemma lift_inv_append_proper_dx (q2) (q1) (p) (f):
+ q2 Ļµ š ā q1āq2 = ā[f]p ā
āāp1,p2. āp1 = q1 & ā[ā[p1]f]p2 = q2 & p1āp2 = p.
#q2 #q1 elim q1 -q1
[ #p #f #Hq2 <list_append_empty_sn #H destruct
[ elim (lift_path_inv_d_sn ā¦ H) -H #r1 #m1 #_ #_ #H0 #_ -IH
elim (eq_inv_list_empty_append ā¦ H0) -H0 #_ #H0 destruct
elim Hq2 -Hq2 //
+ | elim (lift_path_inv_m_sn ā¦ H)
| elim (lift_path_inv_L_sn ā¦ H) -H #r1 #s1 #Hr1 #Hs1 #H0 destruct
elim (IH ā¦ Hs1) -IH -Hs1 // -Hq2 #p1 #p2 #H1 #H2 #H3 destruct
@(ex3_2_intro ā¦ (r1āšāp1)) //
]
]
qed-.
+
+(* Inversions with inner condition for path *********************************)
+
+lemma lift_inv_append_inner_sn (q1) (q2) (p) (f):
+ q1 Ļµ š ā q1āq2 = ā[f]p ā
+ āāp1,p2. āp1 = q1 & ā[ā[p1]f]p2 = q2 & p1āp2 = p.
+#q1 @(list_ind_rcons ā¦ q1) -q1
+[ #q2 #p #f #Hq1 <list_append_empty_sn #H destruct
+ /2 width=5 by ex3_2_intro/
+| #q1 * [ #n1 ] #_ #q2 #p #f #Hq2
+ [ elim (pic_inv_d_dx ā¦ Hq2)
+ | <list_append_rcons_sn #H0
+ elim (lift_inv_append_proper_dx ā¦ H0) -H0 // #p1 #p2 #H1 #H2 #H3 destruct
+ elim (lift_path_inv_m_sn ā¦ (sym_eq ā¦ H2))
+ | <list_append_rcons_sn #H0
+ elim (lift_inv_append_proper_dx ā¦ H0) -H0 // #p1 #p2 #H1 #H2 #H3 destruct
+ elim (lift_path_inv_L_sn ā¦ (sym_eq ā¦ H2)) -H2 #r2 #s2 #Hr2 #Hs2 #H0 destruct
+ @(ex3_2_intro ā¦ (p1ār2āš)) [1,3: // ]
+ [ <structure_append <structure_L_dx <Hr2 -Hr2 //
+ | <list_append_assoc <list_append_rcons_sn //
+ ]
+ | <list_append_rcons_sn #H0
+ elim (lift_inv_append_proper_dx ā¦ H0) -H0 // #p1 #p2 #H1 #H2 #H3 destruct
+ elim (lift_path_inv_A_sn ā¦ (sym_eq ā¦ H2)) -H2 #r2 #s2 #Hr2 #Hs2 #H0 destruct
+ @(ex3_2_intro ā¦ (p1ār2āš)) [1,3: // ]
+ [ <structure_append <structure_A_dx <Hr2 -Hr2 //
+ | <list_append_assoc <list_append_rcons_sn //
+ ]
+ | <list_append_rcons_sn #H0
+ elim (lift_inv_append_proper_dx ā¦ H0) -H0 // #p1 #p2 #H1 #H2 #H3 destruct
+ elim (lift_path_inv_S_sn ā¦ (sym_eq ā¦ H2)) -H2 #r2 #s2 #Hr2 #Hs2 #H0 destruct
+ @(ex3_2_intro ā¦ (p1ār2āš¦)) [1,3: // ]
+ [ <structure_append <structure_S_dx <Hr2 -Hr2 //
+ | <list_append_assoc <list_append_rcons_sn //
+ ]
+ ]
+]
+qed-.