partial update in delayed_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 0db6d2f65327310a9a7d5d6ba2765fcde15ded56..25678301b5951bb84b6edaf188cbf9d2f05ebbc5 100644 (file)
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_inner.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_inner.ma
@@ -15,81 +15,54 @@
 include "delayed_updating/syntax/path.ma".
 include "delayed_updating/notation/functions/class_i_0.ma".
 include "ground/lib/subset.ma".
+include "ground/generated/insert_eq_1.ma".
 
 (* INNER CONDITION FOR PATH *************************************************)
 
-definition pic: predicate path ≝
-           λp. ∀q,k. q◖𝗱k = p → ⊥
+inductive pic: predicate path ≝
+| pic_empty: (𝐞) ϵ pic
+| pic_m_dx (p): p◖𝗺 ϵ pic
+| pic_L_dx (p): p◖𝗟 ϵ pic
+| pic_A_dx (p): p◖𝗔 ϵ pic
+| pic_S_dx (p): p◖𝗦 ϵ pic
 .
 
 interpretation
   "inner condition (path)"
   'ClassI = (pic).
 
-(* Basic constructions ******************************************************)
-
-lemma pic_empty:
-      (𝐞) ϵ 𝐈.
-#q #k #H0 destruct
-qed.
-
-lemma pic_m_dx (p):
-      p◖𝗺 ϵ 𝐈.
-#p #q #k #H0 destruct
-qed.
-
-lemma pic_L_dx (p):
-      p◖𝗟 ϵ 𝐈.
-#p #q #k #H0 destruct
-qed.
-
-lemma pic_A_dx (p):
-      p◖𝗔 ϵ 𝐈.
-#p #q #k #H0 destruct
-qed.
-
-lemma pic_S_dx (p):
-      p◖𝗦 ϵ 𝐈.
-#p #q #k #H0 destruct
-qed.
-
 (* Basic inversions ********************************************************)
 
 lemma pic_inv_d_dx (p) (k):
       p◖𝗱k ϵ 𝐈 → ⊥.
-#p #k #H0 @H0 -H0 //
+#p #k @(insert_eq_1 … (p◖𝗱k))
+#q * -q [|*: #q ] #H0 destruct
+qed-.
+
+lemma pic_inv_d2_dx (p) (k) (d):
+      p◖𝗱❨k,d❩ ϵ 𝐈 → ⊥.
+#p #k #d @(insert_eq_1 … (p◖𝗱❨k,d❩))
+#q * -q [|*: #q ] #H0 destruct
 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)
-]
+#p * -p //
 qed.
 
 lemma pic_L_sn (p):
       p ϵ 𝐈 → 𝗟◗p ϵ 𝐈.
-* [| * [ #k ] #p #Hp <list_cons_shift ] //
-[ #_ <list_cons_comm //
-| elim (pic_inv_d_dx … Hp)
-]
+#p * -p //
 qed.
 
 lemma pic_A_sn (p):
       p ϵ 𝐈 → 𝗔◗p ϵ 𝐈.
-* [| * [ #k ] #p #Hp <list_cons_shift ] //
-[ #_ <list_cons_comm //
-| elim (pic_inv_d_dx … Hp)
-]
+#p * -p //
 qed.
 
 lemma pic_S_sn (p):
       p ϵ 𝐈 → 𝗦◗p ϵ 𝐈.
-* [| * [ #k ] #p #Hp <list_cons_shift ] //
-[ #_ <list_cons_comm //
-| elim (pic_inv_d_dx … Hp)
-]
+#p * -p //
 qed.