---

Step * of Lemma bag-member-combine

∀[A,B:Type]. ∀[bs:bag(A)]. ∀[f:A ⟶ bag(B)]. ∀[b:B].  uiff(b ↓∈ ⋃x∈bs.f[x];↓∃x:A. (x ↓∈ bs ∧ b ↓∈ f[x]))
BY
{ ((UnivCD THENA Auto)
   THEN Assert ⌜∀n:ℕ. ∀bs:bag(A).  ((#(bs) ≤ n) ⇒ uiff(b ↓∈ ⋃x∈bs.f[x];↓∃x:A. (x ↓∈ bs ∧ b ↓∈ f[x])))⌝⋅
   THEN Try ((InstHyp [⌜#(bs)⌝;⌜bs⌝] (-1)⋅ THEN Auto))
   THEN ThinVar `bs'
   THEN CompleteInductionOnNat
   THEN (D 0 THENA Auto)
   THEN ((InstLemma `bag-cases` [⌜A⌝;⌜bs⌝]⋅ THENM D -1) THENA Auto)) }

1
1. A : Type
2. B : Type
3. f : A ⟶ bag(B)
4. b : B
5. n : ℕ
6. ∀n:ℕn. ∀bs:bag(A).  ((#(bs) ≤ n) ⇒ uiff(b ↓∈ ⋃x∈bs.f[x];↓∃x:A. (x ↓∈ bs ∧ b ↓∈ f[x])))
7. bs : bag(A)
8. bs = {} ∈ bag(A)
⊢ (#(bs) ≤ n) ⇒ uiff(b ↓∈ ⋃x∈bs.f[x];↓∃x:A. (x ↓∈ bs ∧ b ↓∈ f[x]))

2
1. A : Type
2. B : Type
3. f : A ⟶ bag(B)
4. b : B
5. n : ℕ
6. ∀n:ℕn. ∀bs:bag(A).  ((#(bs) ≤ n) ⇒ uiff(b ↓∈ ⋃x∈bs.f[x];↓∃x:A. (x ↓∈ bs ∧ b ↓∈ f[x])))
7. bs : bag(A)
8. ↓∃x:A. ∃bs':bag(A). (bs = ({x} + bs') ∈ bag(A))
⊢ (#(bs) ≤ n) ⇒ uiff(b ↓∈ ⋃x∈bs.f[x];↓∃x:A. (x ↓∈ bs ∧ b ↓∈ f[x]))

---

Latex:

---

Latex:
\mforall{}[A,B:Type].  \mforall{}[bs:bag(A)].  \mforall{}[f:A  {}\mrightarrow{}  bag(B)].  \mforall{}[b:B].
    uiff(b  \mdownarrow{}\mmember{}  \mcup{}x\mmember{}bs.f[x];\mdownarrow{}\mexists{}x:A.  (x  \mdownarrow{}\mmember{}  bs  \mwedge{}  b  \mdownarrow{}\mmember{}  f[x]))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  Assert 
  \mkleeneopen{}\mforall{}n:\mBbbN{}.  \mforall{}bs:bag(A).    ((\#(bs)  \mleq{}  n)  {}\mRightarrow{}  uiff(b  \mdownarrow{}\mmember{}  \mcup{}x\mmember{}bs.f[x];\mdownarrow{}\mexists{}x:A.  (x  \mdownarrow{}\mmember{}  bs  \mwedge{}  b  \mdownarrow{}\mmember{}  f[x])))\mkleeneclose{}\mcdot{}
  THEN  Try  ((InstHyp  [\mkleeneopen{}\#(bs)\mkleeneclose{};\mkleeneopen{}bs\mkleeneclose{}]  (-1)\mcdot{}  THEN  Auto))
  THEN  ThinVar  `bs'
  THEN  CompleteInductionOnNat
  THEN  (D  0  THENA  Auto)
  THEN  ((InstLemma  `bag-cases`  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}bs\mkleeneclose{}]\mcdot{}  THENM  D  -1)  THENA  Auto))

---

Home Index