---

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


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 ||)
∈ ℤ
BY
{ (InstHyp [⌜x⌝;⌜y⌝;⌜z⌝] 3⋅ THENA 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 ∈ ℤ)))
8. ||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)||)
∈ ℤ
⊢ ||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.  u  :  Cname
2.  v  :  Cname  List
3.  \mforall{}x,y,z:name-morph(v;[]).
          ((\mforall{}i:nameset(v).  ((((y  i)  =  0)  {}\mRightarrow{}  ((x  i)  =  0))  \mwedge{}  (((y  i)  =  1)  {}\mRightarrow{}  ((z  i)  =  1))))
          {}\mRightarrow{}  (||filter(\mlambda{}i.((x  i  =\msubz{}  0)  \mwedge{}\msubb{}  (z  i  =\msubz{}  1));v)||
                =  (||filter(\mlambda{}i.((x  i  =\msubz{}  0)  \mwedge{}\msubb{}  (y  i  =\msubz{}  1));v)||
                    +  ||filter(\mlambda{}i.((y  i  =\msubz{}  0)  \mwedge{}\msubb{}  (z  i  =\msubz{}  1));v)||)))
4.  x  :  name-morph([u  /  v];[])
5.  y  :  name-morph([u  /  v];[])
6.  z  :  name-morph([u  /  v];[])
7.  \mforall{}i:nameset([u  /  v]).  ((((y  i)  =  0)  {}\mRightarrow{}  ((x  i)  =  0))  \mwedge{}  (((y  i)  =  1)  {}\mRightarrow{}  ((z  i)  =  1)))
\mvdash{}  ||if  (x  u  =\msubz{}  0)  \mwedge{}\msubb{}  (z  u  =\msubz{}  1)
then  [u  /  filter(\mlambda{}i.((x  i  =\msubz{}  0)  \mwedge{}\msubb{}  (z  i  =\msubz{}  1));v)]
else  filter(\mlambda{}i.((x  i  =\msubz{}  0)  \mwedge{}\msubb{}  (z  i  =\msubz{}  1));v)
fi  ||
=  (||if  (x  u  =\msubz{}  0)  \mwedge{}\msubb{}  (y  u  =\msubz{}  1)
    then  [u  /  filter(\mlambda{}i.((x  i  =\msubz{}  0)  \mwedge{}\msubb{}  (y  i  =\msubz{}  1));v)]
    else  filter(\mlambda{}i.((x  i  =\msubz{}  0)  \mwedge{}\msubb{}  (y  i  =\msubz{}  1));v)
    fi  ||
    +  ||if  (y  u  =\msubz{}  0)  \mwedge{}\msubb{}  (z  u  =\msubz{}  1)
        then  [u  /  filter(\mlambda{}i.((y  i  =\msubz{}  0)  \mwedge{}\msubb{}  (z  i  =\msubz{}  1));v)]
        else  filter(\mlambda{}i.((y  i  =\msubz{}  0)  \mwedge{}\msubb{}  (z  i  =\msubz{}  1));v)
        fi  ||)


By

---

Latex:
(InstHyp  [\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}z\mkleeneclose{}]  3\mcdot{}  THENA  Auto)

---

Home Index