---

Step * of Lemma decidable__sub-bag

∀[T:Type]. ((∀x,y:T.  Dec(x = y ∈ T)) ⇒ (∀as,bs:bag(T).  Dec(sub-bag(T;as;bs))))
BY
{ (Auto
   THEN (FLemma `deq-exists` [2] THENA Auto)
   THEN Thin 2
   THEN RenameVar `eq' (-1)
   THEN PromoteHyp (-1) 2
   THEN ((InstLemma `sub-bag-iff` [⌜T⌝;⌜eq⌝]⋅ THENA Auto) THEN RWO "-1" 0 THEN Auto)
   THEN Thin (-1)
   THEN (Assert Dec(↑bag-all(x.(#x in as) ≤z (#x in bs);as)) BY
               Auto)) }

1
1. [T] : Type
2. eq : EqDecider(T)
3. as : bag(T)@i
4. bs : bag(T)@i
5. Dec(↑bag-all(x.(#x in as) ≤z (#x in bs);as))
⊢ Dec(∀x:T. ((#x in as) ≤ (#x in bs)))

---

Latex:

---

Latex:
\mforall{}[T:Type].  ((\mforall{}x,y:T.    Dec(x  =  y))  {}\mRightarrow{}  (\mforall{}as,bs:bag(T).    Dec(sub-bag(T;as;bs))))


By

---

Latex:
(Auto
  THEN  (FLemma  `deq-exists`  [2]  THENA  Auto)
  THEN  Thin  2
  THEN  RenameVar  `eq'  (-1)
  THEN  PromoteHyp  (-1)  2
  THEN  ((InstLemma  `sub-bag-iff`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}eq\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  RWO  "-1"  0  THEN  Auto)
  THEN  Thin  (-1)
  THEN  (Assert  Dec(\muparrow{}bag-all(x.(\#x  in  as)  \mleq{}z  (\#x  in  bs);as))  BY
                          Auto))

---

Home Index