---

Step * 1 2 1 1 1 of Lemma urec_induction


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)
6. x ∈ F^urec-level(f;x) Void
⊢ ∃n:ℕ. (x ∈ ⋃n:ℕn.(F^n Void))
BY
{ TACTIC:((InstLemma `urec-level_wf` [⌜F⌝;⌜f⌝;⌜x⌝]⋅ THENA Auto)
          THEN With ⌜urec-level(f;x) + 1⌝ (D 0)⋅
          THEN Try (Complete ((GenConclAtAddr [2;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 : destructor{i:l}(T.F[T])
5. x : urec(F)
6. x ∈ F^urec-level(f;x) Void
7. urec-level(f;x) ∈ ℕ
⊢ x ∈ ⋃n:ℕurec-level(f;x) + 1.(F^n Void)

2
.....wf..... 
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)
6. x ∈ F^urec-level(f;x) Void
7. urec-level(f;x) ∈ ℕ
8. n : ℕ
⊢ istype(x ∈ ⋃n:ℕn.(F^n 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.  x  :  urec(F)
6.  x  \mmember{}  F\^{}urec-level(f;x)  Void
\mvdash{}  \mexists{}n:\mBbbN{}.  (x  \mmember{}  \mcup{}n:\mBbbN{}n.(F\^{}n  Void))


By

---

Latex:
TACTIC:((InstLemma  `urec-level\_wf`  [\mkleeneopen{}F\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THENA  Auto)
                THEN  With  \mkleeneopen{}urec-level(f;x)  +  1\mkleeneclose{}  (D  0)\mcdot{}
                THEN  Try  (Complete  ((GenConclAtAddr  [2;1]  THEN  Auto))))

---

Home Index