---

Step * 1 2 2 2 1 of Lemma poset-cat_wf


1. J : Cname List
2. f : name-morph(J;[])
3. g : name-morph(J;[])
4. h : name-morph(J;[])
5. p : ∀x@0:nameset(J). (↑f x@0 ≤z g x@0)
6. q : ∀x:nameset(J). (↑g x ≤z h x)
7. x : nameset(J)
⊢ (f x) ≤ (h x)
BY
{ (RepeatFor 2 (((InstHyp [⌜x⌝] (-3)⋅ THENA Auto) THEN (RW assert_pushdownC (-1) THENA Auto))) THEN Auto) }

---

Latex:

---

Latex:

1.  J  :  Cname  List
2.  f  :  name-morph(J;[])
3.  g  :  name-morph(J;[])
4.  h  :  name-morph(J;[])
5.  p  :  \mforall{}x@0:nameset(J).  (\muparrow{}f  x@0  \mleq{}z  g  x@0)
6.  q  :  \mforall{}x:nameset(J).  (\muparrow{}g  x  \mleq{}z  h  x)
7.  x  :  nameset(J)
\mvdash{}  (f  x)  \mleq{}  (h  x)


By

---

Latex:
(RepeatFor  2  (((InstHyp  [\mkleeneopen{}x\mkleeneclose{}]  (-3)\mcdot{}  THENA  Auto)  THEN  (RW  assert\_pushdownC  (-1)  THENA  Auto)))
  THEN  Auto
  )

---

Home Index