---

Step * of Lemma bag-combine-no-repeats2

∀[T1,T2:Type]. ∀[f:T1 ⟶ bag(T2)]. ∀[bs:bag(T1)].
  (bag-no-repeats(T2;⋃x∈bs.f[x])) supposing 
     (bag-no-repeats(T1;bs) and 
     ((∀x,y:T1. ∀z:T2.  (z ↓∈ f[x] ⇒ z ↓∈ f[y] ⇒ (x = y ∈ T1)))
     ∧ (∀x:T1. bag-no-repeats(T2;f[x]))
     ∧ (∀x,y:T1.  Dec(x = y ∈ T1))
     ∧ (∀x,y:T2.  Dec(x = y ∈ T2))))
BY
{ (Auto
   THEN ((FLemma `deq-exists` [-3] THENA Auto) THEN RenameVar `eq1' (-1))
   THEN (FLemma `deq-exists` [-3] THENA Auto)
   THEN RenameVar `eq2' (-1)
   THEN InstLemma `bag-combine-no-repeats` [⌜T1⌝;⌜T2⌝;⌜f⌝;⌜eq1⌝;⌜eq2⌝;⌜bs⌝]⋅
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T1,T2:Type].  \mforall{}[f:T1  {}\mrightarrow{}  bag(T2)].  \mforall{}[bs:bag(T1)].
    (bag-no-repeats(T2;\mcup{}x\mmember{}bs.f[x]))  supposing 
          (bag-no-repeats(T1;bs)  and 
          ((\mforall{}x,y:T1.  \mforall{}z:T2.    (z  \mdownarrow{}\mmember{}  f[x]  {}\mRightarrow{}  z  \mdownarrow{}\mmember{}  f[y]  {}\mRightarrow{}  (x  =  y)))
          \mwedge{}  (\mforall{}x:T1.  bag-no-repeats(T2;f[x]))
          \mwedge{}  (\mforall{}x,y:T1.    Dec(x  =  y))
          \mwedge{}  (\mforall{}x,y:T2.    Dec(x  =  y))))


By

---

Latex:
(Auto
  THEN  ((FLemma  `deq-exists`  [-3]  THENA  Auto)  THEN  RenameVar  `eq1'  (-1))
  THEN  (FLemma  `deq-exists`  [-3]  THENA  Auto)
  THEN  RenameVar  `eq2'  (-1)
  THEN  InstLemma  `bag-combine-no-repeats`  [\mkleeneopen{}T1\mkleeneclose{};\mkleeneopen{}T2\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}eq1\mkleeneclose{};\mkleeneopen{}eq2\mkleeneclose{};\mkleeneopen{}bs\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index