---

Step * of Lemma bag-combine-no-repeats

∀[T1,T2:Type]. ∀[f:T1 ⟶ bag(T2)]. ∀[eq1:EqDecider(T1)]. ∀[eq2:EqDecider(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]))))
BY
{ (Auto
   THEN (InstLemma `bag-no-repeats-count` [⌜T1⌝;⌜eq1⌝]⋅ THENA Auto)
   THEN (RWO "-1" (-2) THENA Auto)
   THEN Thin (-1)
   THEN ((InstLemma `bag-no-repeats-count` [⌜T2⌝;⌜eq2⌝]⋅ THENA Auto)
         THEN (RWO "-1" (-3) THENA Auto)
         THEN (RWO "-1" 0 THENA Auto)
         THEN Thin (-1)
         THEN (Auto
               THEN (SupposeNot THEN (Assert 1 < (#x in ⋃x∈bs.f[x]) BY Auto))
               THEN Assert ⌜False⌝⋅
               THEN Auto
               THEN RepeatFor 2 (Thin (-2))
               THEN RWO "bag-count-combine" (-1)
               THEN Auto
               THEN TACTIC:RWO "bag-sum-count" (-1)
               THEN Auto)⋅)⋅) }

1
1. T1 : Type
2. T2 : Type
3. f : T1 ⟶ bag(T2)
4. eq1 : EqDecider(T1)
5. eq2 : EqDecider(T2)
6. bs : bag(T1)
7. ∀x,y:T1. ∀z:T2.  (z ↓∈ f[x] ⇒ z ↓∈ f[y] ⇒ (x = y ∈ T1))
8. ∀x:T1. ∀[x1:T2]. uiff(1 ≤ (#x1 in f[x]);(#x1 in f[x]) = 1 ∈ ℤ)
9. ∀[x:T1]. uiff(1 ≤ (#x in bs);(#x in bs) = 1 ∈ ℤ)
10. x : T2
11. 1 < bag-sum([x1∈bs|1 ≤z (#x in f[x1])];x1.(#x in f[x1]))
⊢ False

---

Latex:

---

Latex:
\mforall{}[T1,T2:Type].  \mforall{}[f:T1  {}\mrightarrow{}  bag(T2)].  \mforall{}[eq1:EqDecider(T1)].  \mforall{}[eq2:EqDecider(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]))))


By

---

Latex:
(Auto
  THEN  (InstLemma  `bag-no-repeats-count`  [\mkleeneopen{}T1\mkleeneclose{};\mkleeneopen{}eq1\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (RWO  "-1"  (-2)  THENA  Auto)
  THEN  Thin  (-1)
  THEN  ((InstLemma  `bag-no-repeats-count`  [\mkleeneopen{}T2\mkleeneclose{};\mkleeneopen{}eq2\mkleeneclose{}]\mcdot{}  THENA  Auto)
              THEN  (RWO  "-1"  (-3)  THENA  Auto)
              THEN  (RWO  "-1"  0  THENA  Auto)
              THEN  Thin  (-1)
              THEN  (Auto
                          THEN  (SupposeNot  THEN  (Assert  1  <  (\#x  in  \mcup{}x\mmember{}bs.f[x])  BY  Auto))
                          THEN  Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}
                          THEN  Auto
                          THEN  RepeatFor  2  (Thin  (-2))
                          THEN  RWO  "bag-count-combine"  (-1)
                          THEN  Auto
                          THEN  TACTIC:RWO  "bag-sum-count"  (-1)
                          THEN  Auto)\mcdot{})\mcdot{})

---

Home Index