---

Step * 1 3 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)
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)||)
∈ ℤ
BY
{ (Lemmaize [-1] THEN InductionOnList THEN Reduce 0 THEN Auto) }

1
1. u : Cname
2. v : Cname List
3. ∀x,y,z:name-morph(v;[]).
     ((∀i:nameset(v). ((((y i) = 0 ∈ ℤ) ⇒ ((x i) = 0 ∈ ℤ)) ∧ (((y i) = 1 ∈ ℤ) ⇒ ((z i) = 1 ∈ ℤ))))
     ⇒ (||filter(λi.((x i =z 0) ∧b (z i =z 1));v)||
        = (||filter(λi.((x i =z 0) ∧b (y i =z 1));v)|| + ||filter(λi.((y i =z 0) ∧b (z i =z 1));v)||)
        ∈ ℤ))
4. x : name-morph([u / v];[])
5. y : name-morph([u / v];[])
6. z : name-morph([u / v];[])
7. ∀i:nameset([u / v]). ((((y i) = 0 ∈ ℤ) ⇒ ((x i) = 0 ∈ ℤ)) ∧ (((y i) = 1 ∈ ℤ) ⇒ ((z i) = 1 ∈ ℤ)))
⊢ ||if (x u =z 0) ∧b (z u =z 1)
then [u / filter(λi.((x i =z 0) ∧b (z i =z 1));v)]
else filter(λi.((x i =z 0) ∧b (z i =z 1));v)
fi ||
= (||if (x u =z 0) ∧b (y u =z 1)
  then [u / filter(λi.((x i =z 0) ∧b (y i =z 1));v)]
  else filter(λi.((x i =z 0) ∧b (y i =z 1));v)
  fi ||
  + ||if (y u =z 0) ∧b (z u =z 1)
    then [u / filter(λi.((y i =z 0) ∧b (z i =z 1));v)]
    else filter(λi.((y i =z 0) ∧b (z i =z 1));v)
    fi ||)
∈ ℤ

---

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)
7.  \mforall{}i:nameset(I).  ((((y  i)  =  0)  {}\mRightarrow{}  ((x  i)  =  0))  \mwedge{}  (((y  i)  =  1)  {}\mRightarrow{}  ((z  i)  =  1)))
\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:
(Lemmaize  [-1]  THEN  InductionOnList  THEN  Reduce  0  THEN  Auto)

---

Home Index