---

Step * 2 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)
⊢ (x (f x1)) ≤ (z (f x1))
BY
{ ∀h:hyp. ((InstHyp [⌜f x1⌝] h⋅ THENA Trivial) THEN (RW assert_pushdownC (-1) THENA Auto))  }

1
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))

---

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)
\mvdash{}  (x  (f  x1))  \mleq{}  (z  (f  x1))


By

---

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

---

Home Index