---

Step * 1 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 : ⋂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)
BY
{ (Assert ∀m:ℕ. ((F^m Void) ⊆r Base) BY
         (InductionOnNat
          THEN Reduce 0
          THEN Try ((D 0 THEN Complete (Auto)))
          THEN FHyp 3 [-1]
          THEN Auto
          THEN Unfold `so_apply` -1
          THEN RWO "fun_exp_add1" (-1)
          THEN Auto))⋅ }

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 ∈ ℤ)
11. ∀m:ℕ. ((F^m Void) ⊆r Base)
⊢ 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  :  \mcap{}T:\{T:Type|  T  \msubseteq{}r  Base\}  .  (x:F[T]  {}\mrightarrow{}  decomp\{i:l\}(T.F[T];T;x))
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.  m  :  \mBbbN{}
9.  x  :  F\^{}m  Void
10.  \mneg{}(m  =  0)
\mvdash{}  urec-level(f;x)  <  n  {}\mRightarrow{}  (x  \mmember{}  F\^{}urec-level(f;x)  Void)


By

---

Latex:
(Assert  \mforall{}m:\mBbbN{}.  ((F\^{}m  Void)  \msubseteq{}r  Base)  BY
              (InductionOnNat
                THEN  Reduce  0
                THEN  Try  ((D  0  THEN  Complete  (Auto)))
                THEN  FHyp  3  [-1]
                THEN  Auto
                THEN  Unfold  `so\_apply`  -1
                THEN  RWO  "fun\_exp\_add1"  (-1)
                THEN  Auto))\mcdot{}

---

Home Index