---

Step * 1 2 2 of Lemma poset-cat_wf


1. J : Cname List
⊢ <λf,x. Ax, λf,g,h,p,q,x. Ax> ∈ x:name-morph(J;[]) ⟶ (∀x@0:nameset(J). (↑x x@0 ≤z x x@0)) × (x:name-morph(J;[])
                                                                              ⟶ y:name-morph(J;[])
                                                                              ⟶ z:name-morph(J;[])
                                                                              ⟶ (∀x@0:nameset(J). (↑x x@0 ≤z y x@0))
                                                                              ⟶ (∀x:nameset(J). (↑y x ≤z z x))
                                                                              ⟶ (∀x@0:nameset(J). (↑x x@0 ≤z z x@0)))
BY
{ MemCD }

1
.....subterm..... T:t
1:n
1. J : Cname List
⊢ λf,x. Ax ∈ x:name-morph(J;[]) ⟶ (∀x@0:nameset(J). (↑x x@0 ≤z x x@0))

2
.....subterm..... T:t
2:n
1. J : Cname List
⊢ λf,g,h,p,q,x. Ax ∈ x:name-morph(J;[])
  ⟶ y:name-morph(J;[])
  ⟶ z:name-morph(J;[])
  ⟶ (∀x@0:nameset(J). (↑x x@0 ≤z y x@0))
  ⟶ (∀x:nameset(J). (↑y x ≤z z x))
  ⟶ (∀x@0:nameset(J). (↑x x@0 ≤z z x@0))

---

Latex:

---

Latex:

1.  J  :  Cname  List
\mvdash{}  <\mlambda{}f,x.  Ax,  \mlambda{}f,g,h,p,q,x.  Ax>  \mmember{}  x:name-morph(J;[])  {}\mrightarrow{}  (\mforall{}x@0:nameset(J).  (\muparrow{}x  x@0  \mleq{}z  x  x@0))
    \mtimes{}  (x:name-morph(J;[])
        {}\mrightarrow{}  y:name-morph(J;[])
        {}\mrightarrow{}  z:name-morph(J;[])
        {}\mrightarrow{}  (\mforall{}x@0:nameset(J).  (\muparrow{}x  x@0  \mleq{}z  y  x@0))
        {}\mrightarrow{}  (\mforall{}x:nameset(J).  (\muparrow{}y  x  \mleq{}z  z  x))
        {}\mrightarrow{}  (\mforall{}x@0:nameset(J).  (\muparrow{}x  x@0  \mleq{}z  z  x@0)))


By

---

Latex:
MemCD

---

Home Index