Step * 1 2 of Lemma poset-cat-dist-add


1. Cname List
2. name-morph(I;[])
3. name-morph(I;[])
4. name-morph(I;[])
5. ∀x:nameset(I). (↑x ≤x)
6. ∀x@0:nameset(I). (↑x@0 ≤x@0)
7. nameset(I)
8. ((y i) 0 ∈ ℤ ((x i) 0 ∈ ℤ)
9. (y i) 1 ∈ ℤ
⊢ (z i) 1 ∈ ℤ
BY
OnMaybeHyp (\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