---

Step * 1 of Lemma poset-cat-dist-add


1. I : Cname List
2. x : name-morph(I;[])
3. y : name-morph(I;[])
4. z : name-morph(I;[])
5. ∀x:nameset(I). (↑y x ≤z z x)
6. ∀x@0:nameset(I). (↑x x@0 ≤z y x@0)
⊢ ||filter(λi.((x i =z 0) ∧b (z i =z 1));I)||
= (||filter(λi.((x i =z 0) ∧b (y i =z 1));I)|| + ||filter(λi.((y i =z 0) ∧b (z i =z 1));I)||)
∈ ℤ
BY
{ (Assert ⌜∀i:nameset(I). ((((y i) = 0 ∈ ℤ) ⇒ ((x i) = 0 ∈ ℤ)) ∧ (((y i) = 1 ∈ ℤ) ⇒ ((z i) = 1 ∈ ℤ)))⌝⋅ THENA Auto) }

1
1. I : Cname List
2. x : name-morph(I;[])
3. y : name-morph(I;[])
4. z : name-morph(I;[])
5. ∀x:nameset(I). (↑y x ≤z z x)
6. ∀x@0:nameset(I). (↑x x@0 ≤z y x@0)
7. i : nameset(I)
8. (y i) = 0 ∈ ℤ
⊢ (x i) = 0 ∈ ℤ

2
1. I : Cname List
2. x : name-morph(I;[])
3. y : name-morph(I;[])
4. z : name-morph(I;[])
5. ∀x:nameset(I). (↑y x ≤z z x)
6. ∀x@0:nameset(I). (↑x x@0 ≤z y x@0)
7. i : nameset(I)
8. ((y i) = 0 ∈ ℤ) ⇒ ((x i) = 0 ∈ ℤ)
9. (y i) = 1 ∈ ℤ
⊢ (z i) = 1 ∈ ℤ

3
1. I : Cname List
2. x : name-morph(I;[])
3. y : name-morph(I;[])
4. z : name-morph(I;[])
5. ∀x:nameset(I). (↑y x ≤z z x)
6. ∀x@0:nameset(I). (↑x x@0 ≤z y x@0)
7. ∀i:nameset(I). ((((y i) = 0 ∈ ℤ) ⇒ ((x i) = 0 ∈ ℤ)) ∧ (((y i) = 1 ∈ ℤ) ⇒ ((z i) = 1 ∈ ℤ)))
⊢ ||filter(λi.((x i =z 0) ∧b (z i =z 1));I)||
= (||filter(λi.((x i =z 0) ∧b (y i =z 1));I)|| + ||filter(λi.((y i =z 0) ∧b (z i =z 1));I)||)
∈ ℤ

---

Latex:

---

Latex:

1.  I  :  Cname  List
2.  x  :  name-morph(I;[])
3.  y  :  name-morph(I;[])
4.  z  :  name-morph(I;[])
5.  \mforall{}x:nameset(I).  (\muparrow{}y  x  \mleq{}z  z  x)
6.  \mforall{}x@0:nameset(I).  (\muparrow{}x  x@0  \mleq{}z  y  x@0)
\mvdash{}  ||filter(\mlambda{}i.((x  i  =\msubz{}  0)  \mwedge{}\msubb{}  (z  i  =\msubz{}  1));I)||
=  (||filter(\mlambda{}i.((x  i  =\msubz{}  0)  \mwedge{}\msubb{}  (y  i  =\msubz{}  1));I)||  +  ||filter(\mlambda{}i.((y  i  =\msubz{}  0)  \mwedge{}\msubb{}  (z  i  =\msubz{}  1));I)||)


By

---

Latex:
(Assert  \mkleeneopen{}\mforall{}i:nameset(I).  ((((y  i)  =  0)  {}\mRightarrow{}  ((x  i)  =  0))  \mwedge{}  (((y  i)  =  1)  {}\mRightarrow{}  ((z  i)  =  1)))\mkleeneclose{}\mcdot{}  THENA  Auto)

---

Home Index