---

Step * 1 1 1 of Lemma W_iterate_functor_wf

.....assertion..... 
1. A : Type
2. B : A ⟶ Type
3. F : Type ⟶ Type
4. a : A
5. f : B[a] ⟶ W(A;a.B[a])
6. ∀b:B[a]. ∀x:W(A;a.B[a]).  ((x ≤  (f b)) ⇒ (W_iterate_functor(A;a.B[a];T.F[T];x) ∈ Type))
7. x : W(A;a.B[a])
8. v : x ≤  Wsup(a;f)
9. ∀b:W(A;a.B[a]). (b <  x ∈ Type)
10. x1 : W(A;a.B[a])
11. x1 <  x
⊢ x1 <  Wsup(a;f)
BY
{ (InstLemma `Wcmp_transitivity` [⌜A⌝;⌜B⌝;⌜x1⌝;⌜x⌝;⌜Wsup(a;f)⌝]⋅ THEN Auto) }

---

Latex:

---

Latex:
.....assertion..... 
1.  A  :  Type
2.  B  :  A  {}\mrightarrow{}  Type
3.  F  :  Type  {}\mrightarrow{}  Type
4.  a  :  A
5.  f  :  B[a]  {}\mrightarrow{}  W(A;a.B[a])
6.  \mforall{}b:B[a].  \mforall{}x:W(A;a.B[a]).    ((x  \mleq{}    (f  b))  {}\mRightarrow{}  (W\_iterate\_functor(A;a.B[a];T.F[T];x)  \mmember{}  Type))
7.  x  :  W(A;a.B[a])
8.  v  :  x  \mleq{}    Wsup(a;f)
9.  \mforall{}b:W(A;a.B[a]).  (b  <    x  \mmember{}  Type)
10.  x1  :  W(A;a.B[a])
11.  x1  <    x
\mvdash{}  x1  <    Wsup(a;f)


By

---

Latex:
(InstLemma  `Wcmp\_transitivity`  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{};\mkleeneopen{}x1\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}Wsup(a;f)\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index