---

Step * of Lemma bag-remove1-member

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[x:T]. ∀[bs:bag(T)].  (bag-remove1(eq;{x} + bs;x) = (inl bs) ∈ (bag(T)?))
BY
{ ((TACTIC:Auto THEN (InstLemma `bag-remove1-property` [⌜T⌝;⌜eq⌝;⌜x⌝;⌜{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 : Base
5. b1 : Base
6. bs = b1 ∈ pertype(λas,bs. ((as ∈ T List) ∧ (bs ∈ T List) ∧ permutation(T;as;bs)))
7. bs ∈ T List
8. b1 ∈ T List
9. permutation(T;bs;b1)
10. as : bag(T)
11. ({x} + bs) = ({x} + as) ∈ bag(T)
12. bag-remove1(eq;{x} + bs;x) = (inl as) ∈ (bag(T)?)
⊢ bag-remove1(eq;{x} + bs;x) = (inl b1) ∈ (bag(T)?)

2
1. T : Type
2. eq : EqDecider(T)
3. x : T
4. bs : bag(T)
5. bag-remove1(eq;{x} + bs;x) = (inr ⋅ ) ∈ (bag(T)?)
⊢ x ↓∈ {x} + bs

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[x:T].  \mforall{}[bs:bag(T)].    (bag-remove1(eq;\{x\}  +  bs;x)  =  (inl  bs))


By

---

Latex:
((TACTIC:Auto  THEN  (InstLemma  `bag-remove1-property`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}eq\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}\{x\}  +  bs\mkleeneclose{}]\mcdot{}  THENA  Auto))
  THEN  D  -1
  THEN  Auto
  THEN  D  -2
  THEN  ExRepD)

---

Home Index