X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fdelayed_updating%2Fsyntax%2Fpath_inner.ma;h=b2b0cb03f9e6b681b1ab78ede143d96e27a8b42d;hb=9e31ac1f3f868349154b0ce2e550e2476aaf6a30;hp=8e9fccefefdda175bf27251e28d63101575540ba;hpb=80e953c112c66f884d167e7ff876c1f6289e1400;p=helm.git

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 8e9fccefe..b2b0cb03f 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_inner.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_inner.ma
@@ -15,47 +15,48 @@
 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,n. q◖𝗱n = 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 ******************************************************)
+(* Basic inversions ********************************************************)
 
-lemma pic_empty: 𝐞 ϵ 𝐈.
-#q #n #H0
-elim (eq_inv_list_empty_rcons ??? (sym_eq … H0))
-qed.
+lemma pic_inv_d_dx (p) (k):
+      p◖𝗱k ϵ 𝐈 → ⊥.
+#p #k @(insert_eq_1 … (p◖𝗱k))
+#q * -q [|*: #q ] #H0 destruct
+qed-.
 
-lemma pic_m_dx (p): p◖𝗺 ϵ 𝐈.
-#p #q #n #H0
-elim (eq_inv_list_rcons_bi ????? H0) -H0 #_ #H0 destruct
-qed.
+(* Constructions with path_lcons ********************************************)
 
-lemma pic_L_dx (p): p◖𝗟 ϵ 𝐈.
-#p #q #n #H0
-elim (eq_inv_list_rcons_bi ????? H0) -H0 #_ #H0 destruct
+lemma pic_m_sn (p):
+      p ϵ 𝐈 → 𝗺◗p ϵ 𝐈.
+#p * -p //
 qed.
 
-lemma pic_A_dx (p): p◖𝗔 ϵ 𝐈.
-#p #q #n #H0
-elim (eq_inv_list_rcons_bi ????? H0) -H0 #_ #H0 destruct
+lemma pic_L_sn (p):
+      p ϵ 𝐈 → 𝗟◗p ϵ 𝐈.
+#p * -p //
 qed.
 
-lemma pic_S_dx (p): p◖𝗦 ϵ 𝐈.
-#p #q #n #H0
-elim (eq_inv_list_rcons_bi ????? H0) -H0 #_ #H0 destruct
+lemma pic_A_sn (p):
+      p ϵ 𝐈 → 𝗔◗p ϵ 𝐈.
+#p * -p //
 qed.
 
-(* Basic inversions ********************************************************)
-
-lemma pic_inv_d_dx (p) (n):
-      p◖𝗱n ϵ 𝐈 → ⊥.
-#p #n #H0 @H0 -H0 //
-qed-.
+lemma pic_S_sn (p):
+      p ϵ 𝐈 → 𝗦◗p ϵ 𝐈.
+#p * -p //
+qed.