Step
*
1
2
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 ∈ ℤ)
9. (y i) = 1 ∈ ℤ
⊢ (z i) = 1 ∈ ℤ
BY
{ OnMaybeHyp 5 (\h. ((InstHyp [⌜i⌝] h⋅ THENA Auto)
                     THEN (RW assert_pushdownC (-1) THENA Auto)
                     THEN HypSubst' (-2) (-1)
                     THEN MoveToConcl (-1)
                     THEN GenConcl ⌜(z 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)  {}\mRightarrow{}  ((x  i)  =  0)
9.  (y  i)  =  1
\mvdash{}  (z  i)  =  1
By
Latex:
OnMaybeHyp  5  (\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{}(z  i)  =  a\mkleeneclose{}\mcdot{}
                                      THEN  Auto))
Home
Index