---

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

∀[I:Cname List]. ∀[x,y:cat-ob(poset-cat(I))].
  (null(filter(λx1.((x x1 =z 0) ∧b (y x1 =z 1));I)) ~ ff) supposing 
     ((¬(x = y ∈ cat-ob(poset-cat(I)))) and 
     (cat-arrow(poset-cat(I)) x y))
BY
{ (InstLemma `poset-cat-dist-zero` []
   THEN RepeatFor 4 (ParallelLast')
   THEN (D 0 THENA Auto)
   THEN (RWO  "-2" (-1) THENA Auto)) }

1
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

---

Latex:

---

Latex:
\mforall{}[I:Cname  List].  \mforall{}[x,y:cat-ob(poset-cat(I))].
    (null(filter(\mlambda{}x1.((x  x1  =\msubz{}  0)  \mwedge{}\msubb{}  (y  x1  =\msubz{}  1));I))  \msim{}  ff)  supposing 
          ((\mneg{}(x  =  y))  and 
          (cat-arrow(poset-cat(I))  x  y))


By

---

Latex:
(InstLemma  `poset-cat-dist-zero`  []
  THEN  RepeatFor  4  (ParallelLast')
  THEN  (D  0  THENA  Auto)
  THEN  (RWO    "-2"  (-1)  THENA  Auto))

---

Home Index