---

Step * of Lemma bag-lub-property

∀[T:Type]
  ∀eq:EqDecider(T). ∀as,bs:bag(T).
    (sub-bag(T;as;bag-lub(eq;as;bs))
    ∧ sub-bag(T;bs;bag-lub(eq;as;bs))
    ∧ (∀cs:bag(T). (sub-bag(T;as;cs) ⇒ sub-bag(T;bs;cs) ⇒ sub-bag(T;bag-lub(eq;as;bs);cs))))
BY
{ (Auto⋅
   THEN (InstLemma `sub-bag-iff` [⌜T⌝;⌜eq⌝]⋅ THENA Auto)
   THEN RWO "-1" 0
   THEN Auto
   THEN Try (((RWO "-2" (-4) THENA Auto)
              THEN (RWO "-2" (-3) THENA Auto)
              THEN Thin (-2)
              THEN ∀h:hyp. (InstHyp [⌜x⌝] h⋅ THENA Auto) ))
   THEN (RWO "bag-count-bag-lub" 0 THEN Auto)⋅) }

1
1. T : Type
2. eq : EqDecider(T)@i
3. as : bag(T)@i
4. bs : bag(T)@i
5. sub-bag(T;as;bag-lub(eq;as;bs))
6. sub-bag(T;bs;bag-lub(eq;as;bs))
7. cs : bag(T)@i
8. ∀x:T. ((#x in as) ≤ (#x in cs))
9. ∀x:T. ((#x in bs) ≤ (#x in cs))
10. x : T@i
11. (#x in bs) ≤ (#x in cs)
12. (#x in as) ≤ (#x in cs)
⊢ imax((#x in as);(#x in bs)) ≤ (#x in cs)

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}eq:EqDecider(T).  \mforall{}as,bs:bag(T).
        (sub-bag(T;as;bag-lub(eq;as;bs))
        \mwedge{}  sub-bag(T;bs;bag-lub(eq;as;bs))
        \mwedge{}  (\mforall{}cs:bag(T).  (sub-bag(T;as;cs)  {}\mRightarrow{}  sub-bag(T;bs;cs)  {}\mRightarrow{}  sub-bag(T;bag-lub(eq;as;bs);cs))))


By

---

Latex:
(Auto\mcdot{}
  THEN  (InstLemma  `sub-bag-iff`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}eq\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  RWO  "-1"  0
  THEN  Auto
  THEN  Try  (((RWO  "-2"  (-4)  THENA  Auto)
                        THEN  (RWO  "-2"  (-3)  THENA  Auto)
                        THEN  Thin  (-2)
                        THEN  \mforall{}h:hyp.  (InstHyp  [\mkleeneopen{}x\mkleeneclose{}]  h\mcdot{}  THENA  Auto)  ))
  THEN  (RWO  "bag-count-bag-lub"  0  THEN  Auto)\mcdot{})

---

Home Index