(* *)
(**************************************************************************)
-include "delayed_updating/syntax/path_structure.ma".
include "delayed_updating/substitution/lift_eq.ma".
+include "delayed_updating/syntax/path_structure.ma".
+include "delayed_updating/syntax/path_proper.ma".
(* LIFT FOR PATH ***********************************************************)
-(* Constructions with structure ********************************************)
+(* Basic constructions with structure **************************************)
-lemma lift_d_empty_dx (n) (p) (f):
- (āp)āš±āØ(ā[pāš±āØnā©]f)@āØnā©ā© = ā[f](pāš±āØnā©).
-#n #p @(path_ind_lift ā¦ p) -p // [ #m #l #p |*: #p ] #IH #f
-[ <lift_rmap_d_lcons_sn <lift_path_d_lcons_sn //
-| <lift_rmap_L_sn <lift_path_L_sn <IH //
-| <lift_rmap_A_sn <lift_path_A_sn <IH //
-| <lift_rmap_S_sn <lift_path_S_sn <IH //
+lemma structure_lift (p) (f):
+ āp = āā[f]p.
+#p @(path_ind_lift ā¦ p) -p // #p #IH #f
+<lift_path_L_sn //
+qed.
+
+lemma lift_structure (p) (f):
+ āp = ā[f]āp.
+#p @(path_ind_lift ā¦ p) -p //
+qed.
+
+(* Properties with proper condition for path ********************************)
+
+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_L_sn <IH //
+| <lift_path_A_sn <IH //
+| <lift_path_S_sn <IH //
]
+qed-.
+
+(* Advanced constructions with structure ************************************)
+
+lemma lift_d_empty_dx (n) (p) (f):
+ (āp)āš±((ā[p]f)@āØnā©) = ā[f](pāš±n).
+/3 width=3 by ppc_lcons, lift_append_proper_dx/
qed.
lemma lift_L_dx (p) (f):
(āp)āš = ā[f](pāš).
-#p @(path_ind_lift ā¦ p) -p // #m #l #p #IH #f
-<lift_path_d_lcons_sn //
+/3 width=3 by ppc_lcons, lift_append_proper_dx/
qed.
lemma lift_A_dx (p) (f):
(āp)āš = ā[f](pāš).
-#p @(path_ind_lift ā¦ p) -p // #m #l #p #IH #f
-<lift_path_d_lcons_sn //
+/3 width=3 by ppc_lcons, lift_append_proper_dx/
qed.
lemma lift_S_dx (p) (f):
(āp)āš¦ = ā[f](pāš¦).
-#p @(path_ind_lift ā¦ p) -p // #m #l #p #IH #f
-<lift_path_d_lcons_sn //
-qed.
-
-lemma structure_lift (p) (f):
- āp = āā[f]p.
-#p @(path_ind_lift ā¦ p) -p // #p #IH #f
-<lift_path_L_sn //
-qed.
-
-lemma lift_structure (p) (f):
- āp = ā[f]āp.
-#p @(path_ind_lift ā¦ p) -p //
+/3 width=3 by ppc_lcons, lift_append_proper_dx/
qed.