---

Step * 1 1 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)
8. (y i) = 0 ∈ ℤ
⊢ (x i) = 0 ∈ ℤ
BY
{ OnMaybeHyp 6 (\h. ((InstHyp [⌜i⌝] h⋅ THENA Auto)
                     THEN (RW assert_pushdownC (-1) THENA Auto)
                     THEN HypSubst' (-2) (-1)
                     THEN MoveToConcl (-1)
                     THEN GenConcl ⌜(x i) = a ∈ ℕ2⌝⋅
                     THEN Auto)) }

---

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.  i  :  nameset(I)
8.  (y  i)  =  0
\mvdash{}  (x  i)  =  0


By

---

Latex:
OnMaybeHyp  6  (\mbackslash{}h.  ((InstHyp  [\mkleeneopen{}i\mkleeneclose{}]  h\mcdot{}  THENA  Auto)
                                      THEN  (RW  assert\_pushdownC  (-1)  THENA  Auto)
                                      THEN  HypSubst'  (-2)  (-1)
                                      THEN  MoveToConcl  (-1)
                                      THEN  GenConcl  \mkleeneopen{}(x  i)  =  a\mkleeneclose{}\mcdot{}
                                      THEN  Auto))

---

Home Index