---

Step * of Lemma bag-cases

∀[T:Type]. ∀bs:bag(T). ((bs = {} ∈ bag(T)) ∨ (↓∃x:T. ∃bs':bag(T). (bs = ({x} + bs') ∈ bag(T))))
BY
{ (Auto
   THEN ((Decide #(bs) ≤ 0 THENA Auto) THENL [OrLeft; OrRight  ⋅])
   THEN Auto
   THEN Try (((FLemma `bag-size-zero` [-1] THEN Auto) THEN RWO "-1" 0 THEN Auto))
   THEN (BagToList 2 THENA Auto)
   THEN D 2
   THEN RepUR ``bag-size`` -1
   THEN Auto
   THEN D 0
   THEN InstConcl [⌜u⌝;⌜v⌝]⋅
   THEN Auto
   THEN RepUR ``single-bag bag-append`` 0⋅
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}bs:bag(T).  ((bs  =  \{\})  \mvee{}  (\mdownarrow{}\mexists{}x:T.  \mexists{}bs':bag(T).  (bs  =  (\{x\}  +  bs'))))


By

---

Latex:
(Auto
  THEN  ((Decide  \#(bs)  \mleq{}  0  THENA  Auto)  THENL  [OrLeft;  OrRight    \mcdot{}])
  THEN  Auto
  THEN  Try  (((FLemma  `bag-size-zero`  [-1]  THEN  Auto)  THEN  RWO  "-1"  0  THEN  Auto))
  THEN  (BagToList  2  THENA  Auto)
  THEN  D  2
  THEN  RepUR  ``bag-size``  -1
  THEN  Auto
  THEN  D  0
  THEN  InstConcl  [\mkleeneopen{}u\mkleeneclose{};\mkleeneopen{}v\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  RepUR  ``single-bag  bag-append``  0\mcdot{}
  THEN  Auto)

---

Home Index