---

Step * of Lemma select-bag-rep

∀[T:Type]. ∀[n:ℕ]. ∀[x:T]. ∀[i:ℕn].  (bag-rep(n;x)[i] = x ∈ T)
BY
{ (Auto
   THEN InstLemma `member-bag-rep` [⌜T⌝;⌜n⌝;⌜x⌝;⌜bag-rep(n;x)[i]⌝]⋅
   THEN Auto
   THEN Try (Complete ((Fold `bag-size` 0 THEN RWO "bag-size-rep" 0 THEN Auto)))
   THEN (BLemma `list-member-bag-member` THENA Auto)
   THEN Try (Complete ((Fold `bag-size` 0 THEN RWO "bag-size-rep" 0 THEN Auto)))
   THEN With ⌜i⌝ (D 0)⋅
   THEN Auto
   THEN Try (Complete ((Fold `bag-size` 0 THEN RWO "bag-size-rep" 0 THEN Auto)))) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[n:\mBbbN{}].  \mforall{}[x:T].  \mforall{}[i:\mBbbN{}n].    (bag-rep(n;x)[i]  =  x)


By

---

Latex:
(Auto
  THEN  InstLemma  `member-bag-rep`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}bag-rep(n;x)[i]\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  Try  (Complete  ((Fold  `bag-size`  0  THEN  RWO  "bag-size-rep"  0  THEN  Auto)))
  THEN  (BLemma  `list-member-bag-member`  THENA  Auto)
  THEN  Try  (Complete  ((Fold  `bag-size`  0  THEN  RWO  "bag-size-rep"  0  THEN  Auto)))
  THEN  With  \mkleeneopen{}i\mkleeneclose{}  (D  0)\mcdot{}
  THEN  Auto
  THEN  Try  (Complete  ((Fold  `bag-size`  0  THEN  RWO  "bag-size-rep"  0  THEN  Auto))))

---

Home Index