Step
*
of Lemma
bag-remove1-non-member
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[x:T]. ∀[bs:bag(T)]. bag-remove1(eq;bs;x) = (inr ⋅ ) ∈ (bag(T)?) supposing ¬x ↓∈ bs
BY
{ ((TACTIC:Auto THEN (InstLemma `bag-remove1-property` [⌜T⌝;⌜eq⌝;⌜x⌝;⌜bs⌝]⋅ THENA Auto))
THEN D -1
THEN Auto
THEN D -2
THEN ExRepD) }
1
1. T : Type
2. eq : EqDecider(T)
3. x : T
4. bs : bag(T)
5. as : bag(T)
6. bs = ({x} + as) ∈ bag(T)
7. bag-remove1(eq;bs;x) = (inl as) ∈ (bag(T)?)
⊢ x ↓∈ bs
Latex:
Latex:
\mforall{}[T:Type]. \mforall{}[eq:EqDecider(T)]. \mforall{}[x:T]. \mforall{}[bs:bag(T)].
bag-remove1(eq;bs;x) = (inr \mcdot{} ) supposing \mneg{}x \mdownarrow{}\mmember{} bs
By
Latex:
((TACTIC:Auto THEN (InstLemma `bag-remove1-property` [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}eq\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}bs\mkleeneclose{}]\mcdot{} THENA Auto))
THEN D -1
THEN Auto
THEN D -2
THEN ExRepD)
Home
Index