---

Step * 2 1 1 1 2 of Lemma fset-size-union


1. T : Type
2. valueall-type(T)
3. eq : EqDecider(T)
4. a : fset(T)
5. x : T
6. ∀b:fset(T). (||a ⋃ b|| = ((||a|| + ||b||) - ||a ⋂ b||) ∈ ℤ)
7. ¬x ∈ a
8. b : fset(T)
9. ||a ⋃ b|| = ((||a|| + ||b||) - ||a ⋂ b||) ∈ ℤ
10. x ∈ b
⊢ ||a ⋃ b|| = ((||fset-add(eq;x;a)|| + ||b||) - ||fset-add(eq;x;a) ⋂ b||) ∈ ℤ
BY
{ (Subst ⌜fset-add(eq;x;a) ⋂ b = fset-add(eq;x;a ⋂ b) ∈ fset(T)⌝ 0⋅ THEN Auto) }

1
.....equality..... 
1. T : Type
2. valueall-type(T)
3. eq : EqDecider(T)
4. a : fset(T)
5. x : T
6. ∀b:fset(T). (||a ⋃ b|| = ((||a|| + ||b||) - ||a ⋂ b||) ∈ ℤ)
7. ¬x ∈ a
8. b : fset(T)
9. ||a ⋃ b|| = ((||a|| + ||b||) - ||a ⋂ b||) ∈ ℤ
10. x ∈ b
⊢ fset-add(eq;x;a) ⋂ b = fset-add(eq;x;a ⋂ b) ∈ fset(T)

2
1. T : Type
2. valueall-type(T)
3. eq : EqDecider(T)
4. a : fset(T)
5. x : T
6. ∀b:fset(T). (||a ⋃ b|| = ((||a|| + ||b||) - ||a ⋂ b||) ∈ ℤ)
7. ¬x ∈ a
8. b : fset(T)
9. ||a ⋃ b|| = ((||a|| + ||b||) - ||a ⋂ b||) ∈ ℤ
10. x ∈ b
⊢ ||a ⋃ b|| = ((||fset-add(eq;x;a)|| + ||b||) - ||fset-add(eq;x;a ⋂ b)||) ∈ ℤ

---

Latex:

---

Latex:

1.  T  :  Type
2.  valueall-type(T)
3.  eq  :  EqDecider(T)
4.  a  :  fset(T)
5.  x  :  T
6.  \mforall{}b:fset(T).  (||a  \mcup{}  b||  =  ((||a||  +  ||b||)  -  ||a  \mcap{}  b||))
7.  \mneg{}x  \mmember{}  a
8.  b  :  fset(T)
9.  ||a  \mcup{}  b||  =  ((||a||  +  ||b||)  -  ||a  \mcap{}  b||)
10.  x  \mmember{}  b
\mvdash{}  ||a  \mcup{}  b||  =  ((||fset-add(eq;x;a)||  +  ||b||)  -  ||fset-add(eq;x;a)  \mcap{}  b||)


By

---

Latex:
(Subst  \mkleeneopen{}fset-add(eq;x;a)  \mcap{}  b  =  fset-add(eq;x;a  \mcap{}  b)\mkleeneclose{}  0\mcdot{}  THEN  Auto)

---

Home Index