---

Step * 1 of Lemma urec-level-property

.....assertion..... 
1. F : Type ⟶ Type
2. Monotone(T.F[T])
3. ∀T:Type. ((T ⊆r Base) ⇒ (F[T] ⊆r Base))
4. f : destructor{i:l}(T.F[T])
5. x : urec(F)
⊢ ∀n:ℕ. ∀x:urec(F).  (urec-level(f;x) < n ⇒ (x ∈ F^urec-level(f;x) Void))
BY
{ (Thin (-1) THEN InductionOnNat THEN Auto') }

1
1. F : Type ⟶ Type
2. Monotone(T.F[T])
3. ∀T:Type. ((T ⊆r Base) ⇒ (F[T] ⊆r Base))
4. f : destructor{i:l}(T.F[T])
5. n : ℤ
6. 0 < n
7. ∀x:urec(F). (urec-level(f;x) < n - 1 ⇒ (x ∈ F^urec-level(f;x) Void))
8. x : urec(F)
9. urec-level(f;x) < n
⊢ x ∈ F^urec-level(f;x) Void

---

Latex:

---

Latex:
.....assertion..... 
1.  F  :  Type  {}\mrightarrow{}  Type
2.  Monotone(T.F[T])
3.  \mforall{}T:Type.  ((T  \msubseteq{}r  Base)  {}\mRightarrow{}  (F[T]  \msubseteq{}r  Base))
4.  f  :  destructor\{i:l\}(T.F[T])
5.  x  :  urec(F)
\mvdash{}  \mforall{}n:\mBbbN{}.  \mforall{}x:urec(F).    (urec-level(f;x)  <  n  {}\mRightarrow{}  (x  \mmember{}  F\^{}urec-level(f;x)  Void))


By

---

Latex:
(Thin  (-1)  THEN  InductionOnNat  THEN  Auto')

---

Home Index