---

Step * 2 1 1 of Lemma poset-functor_wf


1. J : Cname List
2. K : Cname List
3. f : name-morph(J;K)
4. ∀x:name-morph(K;[]). ((λx.Ax) = (λx.Ax) ∈ (∀x@0:nameset(J). (↑(f o x) x@0 ≤z (f o x) x@0)))
5. x : name-morph(K;[])
6. y : name-morph(K;[])
7. z : name-morph(K;[])
8. f@0 : ∀x@0:nameset(K). (↑x x@0 ≤z y x@0)
9. g : ∀x:nameset(K). (↑y x ≤z z x)
10. x1 : nameset(J)
11. ↑isname(f x1)
12. f x1 ∈ nameset(K)
13. (y (f x1)) ≤ (z (f x1))
14. (x (f x1)) ≤ (y (f x1))
⊢ (x (f x1)) ≤ (z (f x1))
BY
{ (RWO "-1" 0 THEN Try (Trivial) THEN DoSubsume THEN Auto) }

---

Latex:

---

Latex:

1.  J  :  Cname  List
2.  K  :  Cname  List
3.  f  :  name-morph(J;K)
4.  \mforall{}x:name-morph(K;[]).  ((\mlambda{}x.Ax)  =  (\mlambda{}x.Ax))
5.  x  :  name-morph(K;[])
6.  y  :  name-morph(K;[])
7.  z  :  name-morph(K;[])
8.  f@0  :  \mforall{}x@0:nameset(K).  (\muparrow{}x  x@0  \mleq{}z  y  x@0)
9.  g  :  \mforall{}x:nameset(K).  (\muparrow{}y  x  \mleq{}z  z  x)
10.  x1  :  nameset(J)
11.  \muparrow{}isname(f  x1)
12.  f  x1  \mmember{}  nameset(K)
13.  (y  (f  x1))  \mleq{}  (z  (f  x1))
14.  (x  (f  x1))  \mleq{}  (y  (f  x1))
\mvdash{}  (x  (f  x1))  \mleq{}  (z  (f  x1))


By

---

Latex:
(RWO  "-1"  0  THEN  Try  (Trivial)  THEN  DoSubsume  THEN  Auto)

---

Home Index