---

Step * 1 3 1 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 ∈ ℤ)))
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 ||)
∈ ℤ
BY
{ ((InstHyp [⌜u⌝] (-2)⋅ THENA Auto)
   THEN MoveToConcl (-1)
   THEN ((GenConcl ⌜(y u) = a ∈ ℕ2⌝⋅ THENA Auto) THEN IntSegCases (-2))
   THEN ((GenConcl ⌜(x u) = b ∈ ℕ2⌝⋅ THENA Auto) THEN IntSegCases (-2))
   THEN (GenConcl ⌜(z u) = c ∈ ℕ2⌝⋅ THENA Auto)
   THEN IntSegCases (-2)
   THEN Reduce 0
   THEN Auto) }

---

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)))
8.  ||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)||)
\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{}u\mkleeneclose{}]  (-2)\mcdot{}  THENA  Auto)
  THEN  MoveToConcl  (-1)
  THEN  ((GenConcl  \mkleeneopen{}(y  u)  =  a\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  IntSegCases  (-2))
  THEN  ((GenConcl  \mkleeneopen{}(x  u)  =  b\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  IntSegCases  (-2))
  THEN  (GenConcl  \mkleeneopen{}(z  u)  =  c\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  IntSegCases  (-2)
  THEN  Reduce  0
  THEN  Auto)

---

Home Index