---

Step * 2 2 of Lemma poset-cat_wf


1. J : Cname List
2. ∀x,y:name-morph(J;[]). ∀f:∀x@0:nameset(J). (↑x x@0 ≤z y x@0).
     (((λx.Ax) = f ∈ (∀x@0:nameset(J). (↑x x@0 ≤z y x@0))) ∧ ((λx.Ax) = f ∈ (∀x@0:nameset(J). (↑x x@0 ≤z y x@0))))
3. x : name-morph(J;[])
4. y : name-morph(J;[])
5. z : name-morph(J;[])
6. w : name-morph(J;[])
7. f : ∀x@0:nameset(J). (↑x x@0 ≤z y x@0)
8. g : ∀x:nameset(J). (↑y x ≤z z x)
9. h : ∀x:nameset(J). (↑z x ≤z w x)
10. x1 : nameset(J)
⊢ (x x1) ≤ (w x1)
BY
{ (∀h:hyp. ((InstHyp [⌜x1⌝] h⋅ THENA Declaration) THEN (RW assert_pushdownC (-1) THENA Auto))  THEN Auto) }

---

Latex:

---

Latex:

1.  J  :  Cname  List
2.  \mforall{}x,y:name-morph(J;[]).  \mforall{}f:\mforall{}x@0:nameset(J).  (\muparrow{}x  x@0  \mleq{}z  y  x@0).    (((\mlambda{}x.Ax)  =  f)  \mwedge{}  ((\mlambda{}x.Ax)  =  f))
3.  x  :  name-morph(J;[])
4.  y  :  name-morph(J;[])
5.  z  :  name-morph(J;[])
6.  w  :  name-morph(J;[])
7.  f  :  \mforall{}x@0:nameset(J).  (\muparrow{}x  x@0  \mleq{}z  y  x@0)
8.  g  :  \mforall{}x:nameset(J).  (\muparrow{}y  x  \mleq{}z  z  x)
9.  h  :  \mforall{}x:nameset(J).  (\muparrow{}z  x  \mleq{}z  w  x)
10.  x1  :  nameset(J)
\mvdash{}  (x  x1)  \mleq{}  (w  x1)


By

---

Latex:
(\mforall{}h:hyp.  ((InstHyp  [\mkleeneopen{}x1\mkleeneclose{}]  h\mcdot{}  THENA  Declaration)  THEN  (RW  assert\_pushdownC  (-1)  THENA  Auto)) 
  THEN  Auto
  )

---

Home Index