---

Step * 1 of Lemma sub-bag_antisymmetry


1. T : Type
2. as : bag(T)
3. bs : bag(T)
4. c1 : bag(T)
5. as = (bs + c1) ∈ bag(T)
6. cs : bag(T)
7. bs = (as + cs) ∈ bag(T)
8. as = (bs + c1) ∈ bag(T)
9. #(as) = (#(bs) + #(c1)) ∈ ℤ
10. bs = (as + cs) ∈ bag(T)
11. #(bs) = (#(as) + #(cs)) ∈ ℤ
⊢ as = bs ∈ bag(T)
BY
{ Subst' cs ~ [] -2 }

1
.....equality..... 
1. T : Type
2. as : bag(T)
3. bs : bag(T)
4. c1 : bag(T)
5. as = (bs + c1) ∈ bag(T)
6. cs : bag(T)
7. bs = (as + cs) ∈ bag(T)
8. as = (bs + c1) ∈ bag(T)
9. #(as) = (#(bs) + #(c1)) ∈ ℤ
10. bs = (as + cs) ∈ bag(T)
11. #(bs) = (#(as) + #(cs)) ∈ ℤ
⊢ cs ~ []

2
1. T : Type
2. as : bag(T)
3. bs : bag(T)
4. c1 : bag(T)
5. as = (bs + c1) ∈ bag(T)
6. cs : bag(T)
7. bs = (as + cs) ∈ bag(T)
8. as = (bs + c1) ∈ bag(T)
9. #(as) = (#(bs) + #(c1)) ∈ ℤ
10. bs = (as + []) ∈ bag(T)
11. #(bs) = (#(as) + #(cs)) ∈ ℤ
⊢ as = bs ∈ bag(T)

---

Latex:

---

Latex:

1.  T  :  Type
2.  as  :  bag(T)
3.  bs  :  bag(T)
4.  c1  :  bag(T)
5.  as  =  (bs  +  c1)
6.  cs  :  bag(T)
7.  bs  =  (as  +  cs)
8.  as  =  (bs  +  c1)
9.  \#(as)  =  (\#(bs)  +  \#(c1))
10.  bs  =  (as  +  cs)
11.  \#(bs)  =  (\#(as)  +  \#(cs))
\mvdash{}  as  =  bs


By

---

Latex:
Subst'  cs  \msim{}  []  -2

---

Home Index