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-.
(* 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.