update in delayd_updating

[helm.git] / matita / matita / contribs / lambdadelta / delayed_updating / syntax / path_inner.ma

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_inner.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_inner.ma
index 8e9fccefefdda175bf27251e28d63101575540ba..0db6d2f65327310a9a7d5d6ba2765fcde15ded56 100644 (file)
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_inner.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_inner.ma
@@ -19,7 +19,7 @@ include "ground/lib/subset.ma".
 (* INNER CONDITION FOR PATH *************************************************)
 
 definition pic: predicate path ≝
 (* INNER CONDITION FOR PATH *************************************************)
 
 definition pic: predicate path ≝

-           λp. ∀q,n. q◖𝗱n = p → ⊥
+           λp. ∀q,k. q◖𝗱k = p → ⊥

 .
 
 interpretation
 .
 
 interpretation


@@ -28,34 +28,68 @@ interpretation
 
 (* Basic constructions ******************************************************)
 
 
 (* Basic constructions ******************************************************)
 

-lemma pic_empty: 𝐞 ϵ 𝐈.
-#q #n #H0
-elim (eq_inv_list_empty_rcons ??? (sym_eq … H0))
+lemma pic_empty:
+      (𝐞) ϵ 𝐈.
+#q #k #H0 destruct

 qed.
 
 qed.
 

-lemma pic_m_dx (p): p◖𝗺 ϵ 𝐈.
-#p #q #n #H0
-elim (eq_inv_list_rcons_bi ????? H0) -H0 #_ #H0 destruct
+lemma pic_m_dx (p):
+      p◖𝗺 ϵ 𝐈.
+#p #q #k #H0 destruct

 qed.
 
 qed.
 

-lemma pic_L_dx (p): p◖𝗟 ϵ 𝐈.
-#p #q #n #H0
-elim (eq_inv_list_rcons_bi ????? H0) -H0 #_ #H0 destruct
+lemma pic_L_dx (p):
+      p◖𝗟 ϵ 𝐈.
+#p #q #k #H0 destruct

 qed.
 
 qed.
 

-lemma pic_A_dx (p): p◖𝗔 ϵ 𝐈.
-#p #q #n #H0
-elim (eq_inv_list_rcons_bi ????? H0) -H0 #_ #H0 destruct
+lemma pic_A_dx (p):
+      p◖𝗔 ϵ 𝐈.
+#p #q #k #H0 destruct

 qed.
 
 qed.
 

-lemma pic_S_dx (p): p◖𝗦 ϵ 𝐈.
-#p #q #n #H0
-elim (eq_inv_list_rcons_bi ????? H0) -H0 #_ #H0 destruct
+lemma pic_S_dx (p):
+      p◖𝗦 ϵ 𝐈.
+#p #q #k #H0 destruct

 qed.
 
 (* Basic inversions ********************************************************)
 
 qed.
 
 (* Basic inversions ********************************************************)
 

-lemma pic_inv_d_dx (p) (n):
-      p◖𝗱n ϵ 𝐈 → ⊥.
-#p #n #H0 @H0 -H0 //
+lemma pic_inv_d_dx (p) (k):
+      p◖𝗱k ϵ 𝐈 → ⊥.
+#p #k #H0 @H0 -H0 //

 qed-.
 qed-.

+
+(* Constructions with path_lcons ********************************************)
+
+lemma pic_m_sn (p):
+      p ϵ 𝐈 → 𝗺◗p ϵ 𝐈.
+* [| * [ #k ] #p #Hp <list_cons_shift ] //
+[ #_ <list_cons_comm //
+| elim (pic_inv_d_dx … Hp)
+]
+qed.
+
+lemma pic_L_sn (p):
+      p ϵ 𝐈 → 𝗟◗p ϵ 𝐈.
+* [| * [ #k ] #p #Hp <list_cons_shift ] //
+[ #_ <list_cons_comm //
+| elim (pic_inv_d_dx … Hp)
+]
+qed.
+
+lemma pic_A_sn (p):
+      p ϵ 𝐈 → 𝗔◗p ϵ 𝐈.
+* [| * [ #k ] #p #Hp <list_cons_shift ] //
+[ #_ <list_cons_comm //
+| elim (pic_inv_d_dx … Hp)
+]
+qed.
+
+lemma pic_S_sn (p):
+      p ϵ 𝐈 → 𝗦◗p ϵ 𝐈.
+* [| * [ #k ] #p #Hp <list_cons_shift ] //
+[ #_ <list_cons_comm //
+| elim (pic_inv_d_dx … Hp)
+]
+qed.