---

Step * of Lemma bag-remove1-property1

∀[T:Type]
  ∀eq:EqDecider(T). ∀x:T. ∀L:T List.
    ((∃as,bs:T List. ((L = ((as @ [x]) @ bs) ∈ (T List)) ∧ (bag-remove1(eq;L;x) = (inl (rev(as) @ bs)) ∈ (T List?))))
    ∨ ((¬(x ∈ L)) ∧ (bag-remove1(eq;L;x) = (inr ⋅ ) ∈ (T List?))))
BY
{ xxx(xxxInstLemma `bag_remove1_aux_property` []xxx
      THEN RepeatFor 4 (ParallelLast')
      THEN (InstHyp [⌜[]⌝] (-1)⋅ THENA Auto)
      THEN Unfold `bag-remove1` 0
      THEN RepeatFor 4 (ParallelLast)
      THEN RWO "append-nil" (-1)
      THEN Auto)xxx }

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}eq:EqDecider(T).  \mforall{}x:T.  \mforall{}L:T  List.
        ((\mexists{}as,bs:T  List.  ((L  =  ((as  @  [x])  @  bs))  \mwedge{}  (bag-remove1(eq;L;x)  =  (inl  (rev(as)  @  bs)))))
        \mvee{}  ((\mneg{}(x  \mmember{}  L))  \mwedge{}  (bag-remove1(eq;L;x)  =  (inr  \mcdot{}  ))))


By

---

Latex:
xxx(xxxInstLemma  `bag\_remove1\_aux\_property`  []xxx
        THEN  RepeatFor  4  (ParallelLast')
        THEN  (InstHyp  [\mkleeneopen{}[]\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)
        THEN  Unfold  `bag-remove1`  0
        THEN  RepeatFor  4  (ParallelLast)
        THEN  RWO  "append-nil"  (-1)
        THEN  Auto)xxx

---

Home Index