---

Step * of Lemma bag-drop-commutes

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[bs:bag(T)]. ∀[x,y:T].
  (bag-drop(eq;bag-drop(eq;bs;x);y) = bag-drop(eq;bag-drop(eq;bs;y);x) ∈ bag(T))
BY
{ TACTIC:(Auto
          THEN (Assert ∀x,y:T.  Dec(x = y ∈ T) BY
                      Auto)
          THEN (TACTIC: Decide ⌜x = y ∈ T⌝⋅⋅ THENA Auto)
          THEN Try ((HypSubst (-1) 0 THEN Auto))
          THEN Unfold `bag-drop` 0
          THEN (InstLemma `bag-remove1-property` [⌜T⌝;⌜eq⌝]⋅ THENA Auto)
          THEN (InstHyp [⌜x⌝;⌜bs⌝] 8⋅ THENA Auto)
          THEN D -1
          THEN ExRepD
          THEN ((HypSubst (-1) 0 THENA (D (-1) THEN Reduce 0 THEN Auto))
                THEN Reduce 0
                THEN ((InstHyp [⌜y⌝;⌜bs⌝] 8⋅ THENA Auto)
                      THEN D -1
                      THEN ExRepD
                      THEN ((HypSubst (-1) 0 THENA (D (-1) THEN Reduce 0 THEN Auto)) THEN Reduce 0)⋅)⋅)⋅) }

1
1. T : Type
2. eq : EqDecider(T)
3. bs : bag(T)
4. x : T
5. y : T
6. ∀x,y:T.  Dec(x = y ∈ T)
7. ¬(x = y ∈ T)
8. ∀x:T. ∀bs:bag(T).
     ((∃as:bag(T). ((bs = ({x} + as) ∈ bag(T)) ∧ (bag-remove1(eq;bs;x) = (inl as) ∈ (bag(T)?))))
     ∨ ((¬x ↓∈ bs) ∧ (bag-remove1(eq;bs;x) = (inr ⋅ ) ∈ (bag(T)?))))
9. as : bag(T)
10. bs = ({x} + as) ∈ bag(T)
11. bag-remove1(eq;bs;x) = (inl as) ∈ (bag(T)?)
12. a1 : bag(T)
13. bs = ({y} + a1) ∈ bag(T)
14. bag-remove1(eq;bs;y) = (inl a1) ∈ (bag(T)?)
⊢ case bag-remove1(eq;as;y) of inl(as) => as | inr(_) => as
= case bag-remove1(eq;a1;x) of inl(as) => as | inr(_) => a1
∈ bag(T)

2
1. T : Type
2. eq : EqDecider(T)
3. bs : bag(T)
4. x : T
5. y : T
6. ∀x,y:T.  Dec(x = y ∈ T)
7. ¬(x = y ∈ T)
8. ∀x:T. ∀bs:bag(T).
     ((∃as:bag(T). ((bs = ({x} + as) ∈ bag(T)) ∧ (bag-remove1(eq;bs;x) = (inl as) ∈ (bag(T)?))))
     ∨ ((¬x ↓∈ bs) ∧ (bag-remove1(eq;bs;x) = (inr ⋅ ) ∈ (bag(T)?))))
9. as : bag(T)
10. bs = ({x} + as) ∈ bag(T)
11. bag-remove1(eq;bs;x) = (inl as) ∈ (bag(T)?)
12. ¬y ↓∈ bs
13. bag-remove1(eq;bs;y) = (inr ⋅ ) ∈ (bag(T)?)
⊢ case bag-remove1(eq;as;y) of inl(as) => as | inr(_) => as
= case bag-remove1(eq;bs;x) of inl(as) => as | inr(_) => bs
∈ bag(T)

3
1. T : Type
2. eq : EqDecider(T)
3. bs : bag(T)
4. x : T
5. y : T
6. ∀x,y:T.  Dec(x = y ∈ T)
7. ¬(x = y ∈ T)
8. ∀x:T. ∀bs:bag(T).
     ((∃as:bag(T). ((bs = ({x} + as) ∈ bag(T)) ∧ (bag-remove1(eq;bs;x) = (inl as) ∈ (bag(T)?))))
     ∨ ((¬x ↓∈ bs) ∧ (bag-remove1(eq;bs;x) = (inr ⋅ ) ∈ (bag(T)?))))
9. ¬x ↓∈ bs
10. bag-remove1(eq;bs;x) = (inr ⋅ ) ∈ (bag(T)?)
11. as : bag(T)
12. bs = ({y} + as) ∈ bag(T)
13. bag-remove1(eq;bs;y) = (inl as) ∈ (bag(T)?)
⊢ as = case bag-remove1(eq;as;x) of inl(as) => as | inr(_) => as ∈ bag(T)

4
1. T : Type
2. eq : EqDecider(T)
3. bs : bag(T)
4. x : T
5. y : T
6. ∀x,y:T.  Dec(x = y ∈ T)
7. ¬(x = y ∈ T)
8. ∀x:T. ∀bs:bag(T).
     ((∃as:bag(T). ((bs = ({x} + as) ∈ bag(T)) ∧ (bag-remove1(eq;bs;x) = (inl as) ∈ (bag(T)?))))
     ∨ ((¬x ↓∈ bs) ∧ (bag-remove1(eq;bs;x) = (inr ⋅ ) ∈ (bag(T)?))))
9. ¬x ↓∈ bs
10. bag-remove1(eq;bs;x) = (inr ⋅ ) ∈ (bag(T)?)
11. ¬y ↓∈ bs
12. bag-remove1(eq;bs;y) = (inr ⋅ ) ∈ (bag(T)?)
⊢ bs = case bag-remove1(eq;bs;x) of inl(as) => as | inr(_) => bs ∈ bag(T)

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[bs:bag(T)].  \mforall{}[x,y:T].
    (bag-drop(eq;bag-drop(eq;bs;x);y)  =  bag-drop(eq;bag-drop(eq;bs;y);x))


By

---

Latex:
TACTIC:(Auto
                THEN  (Assert  \mforall{}x,y:T.    Dec(x  =  y)  BY
                                        Auto)
                THEN  (TACTIC:  Decide  \mkleeneopen{}x  =  y\mkleeneclose{}\mcdot{}\mcdot{}  THENA  Auto)
                THEN  Try  ((HypSubst  (-1)  0  THEN  Auto))
                THEN  Unfold  `bag-drop`  0
                THEN  (InstLemma  `bag-remove1-property`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}eq\mkleeneclose{}]\mcdot{}  THENA  Auto)
                THEN  (InstHyp  [\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}bs\mkleeneclose{}]  8\mcdot{}  THENA  Auto)
                THEN  D  -1
                THEN  ExRepD
                THEN  ((HypSubst  (-1)  0  THENA  (D  (-1)  THEN  Reduce  0  THEN  Auto))
                            THEN  Reduce  0
                            THEN  ((InstHyp  [\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}bs\mkleeneclose{}]  8\mcdot{}  THENA  Auto)
                                        THEN  D  -1
                                        THEN  ExRepD
                                        THEN  ((HypSubst  (-1)  0  THENA  (D  (-1)  THEN  Reduce  0  THEN  Auto))  THEN  Reduce  0)\mcdot{})
                            \mcdot{})\mcdot{})

---

Home Index