---

Step * 1 of Lemma poset-cat-dist-non-zero


1. I : Cname List
2. x : cat-ob(poset-cat(I))
3. y : cat-ob(poset-cat(I))
4. cat-arrow(poset-cat(I)) x y
5. uiff(x = y ∈ cat-ob(poset-cat(I));poset-cat-dist(I;x;y) ≤ 0)
6. ¬(poset-cat-dist(I;x;y) ≤ 0)
⊢ null(filter(λx1.((x x1 =z 0) ∧b (y x1 =z 1));I)) ~ ff
BY
{ ((MoveToConcl (-1) THEN RepUR ``poset-cat-dist`` 0)
   THEN (GenConclTerm ⌜filter(λi.((x i =z 0) ∧b (y i =z 1));I)⌝⋅ THENA Auto)
   THEN (D -2 THEN Reduce 0)
   THEN Auto) }

---

Latex:

---

Latex:

1.  I  :  Cname  List
2.  x  :  cat-ob(poset-cat(I))
3.  y  :  cat-ob(poset-cat(I))
4.  cat-arrow(poset-cat(I))  x  y
5.  uiff(x  =  y;poset-cat-dist(I;x;y)  \mleq{}  0)
6.  \mneg{}(poset-cat-dist(I;x;y)  \mleq{}  0)
\mvdash{}  null(filter(\mlambda{}x1.((x  x1  =\msubz{}  0)  \mwedge{}\msubb{}  (y  x1  =\msubz{}  1));I))  \msim{}  ff


By

---

Latex:
((MoveToConcl  (-1)  THEN  RepUR  ``poset-cat-dist``  0)
  THEN  (GenConclTerm  \mkleeneopen{}filter(\mlambda{}i.((x  i  =\msubz{}  0)  \mwedge{}\msubb{}  (y  i  =\msubz{}  1));I)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (D  -2  THEN  Reduce  0)
  THEN  Auto)

---

Home Index