---

Step * 1 1 of Lemma urec-level-property


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
BY
{ (Unfold `urec` -2
   THEN D_union (-2)
   THEN RenameVar `m' (-3)
   THEN All Reduce
   THEN RenameVar `x' (-2)
   THEN Unfold `destructor` 4
   THEN CaseNat 0 `m'
   THEN Try ((HypSubst' (-1) (-3) THEN Reduce (-3) THEN Auto)⋅)
   THEN MoveToConcl (-2)) }

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

---

Latex:

---

Latex:

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.  n  :  \mBbbZ{}
6.  0  <  n
7.  \mforall{}x:urec(F).  (urec-level(f;x)  <  n  -  1  {}\mRightarrow{}  (x  \mmember{}  F\^{}urec-level(f;x)  Void))
8.  x  :  urec(F)
9.  urec-level(f;x)  <  n
\mvdash{}  x  \mmember{}  F\^{}urec-level(f;x)  Void


By

---

Latex:
(Unfold  `urec`  -2
  THEN  D\_union  (-2)
  THEN  RenameVar  `m'  (-3)
  THEN  All  Reduce
  THEN  RenameVar  `x'  (-2)
  THEN  Unfold  `destructor`  4
  THEN  CaseNat  0  `m'
  THEN  Try  ((HypSubst'  (-1)  (-3)  THEN  Reduce  (-3)  THEN  Auto)\mcdot{})
  THEN  MoveToConcl  (-2))

---

Home Index