---

Step * 1 of Lemma member-disjoint-union-comb


∀[Info,A,B:Type]. ∀[X:EClass(A)]. ∀[Y:EClass(B)]. ∀[es:EO+(Info)]. ∀[e:E].
  uiff(↑¬b(#(X(e)) + #(Y(e)) =z 0);↑((¬b(#(X(e)) =z 0)) ∨b(¬b(#(Y(e)) =z 0))))
BY
{ (Auto THEN Repeat (AllPushDown)) }

1
1. Info : Type
2. A : Type
3. B : Type
4. X : EClass(A)
5. Y : EClass(B)
6. es : EO+(Info)
7. e : E
8. ¬((#(X(e)) + #(Y(e))) = 0 ∈ ℤ)
9. #(X(e)) = 0 ∈ ℤ
⊢ ¬(#(Y(e)) = 0 ∈ ℤ)

2
1. Info : Type
2. A : Type
3. B : Type
4. X : EClass(A)
5. Y : EClass(B)
6. es : EO+(Info)
7. e : E
8. (¬(#(X(e)) = 0 ∈ ℤ)) ∨ (¬(#(Y(e)) = 0 ∈ ℤ))
⊢ ¬((#(X(e)) + #(Y(e))) = 0 ∈ ℤ)

---

Latex:

---

Latex:

\mforall{}[Info,A,B:Type].  \mforall{}[X:EClass(A)].  \mforall{}[Y:EClass(B)].  \mforall{}[es:EO+(Info)].  \mforall{}[e:E].
    uiff(\muparrow{}\mneg{}\msubb{}(\#(X(e))  +  \#(Y(e))  =\msubz{}  0);\muparrow{}((\mneg{}\msubb{}(\#(X(e))  =\msubz{}  0))  \mvee{}\msubb{}(\mneg{}\msubb{}(\#(Y(e))  =\msubz{}  0))))


By

---

Latex:
(Auto  THEN  Repeat  (AllPushDown))

---

Home Index