---

Step * of Lemma urec-level_wf

No Annotations
∀[F:Type ⟶ Type]
  ∀[f:destructor{i:l}(T.F[T])]. ∀[x:urec(F)].  (urec-level(f;x) ∈ ℕ) supposing ∀T:Type. ((T ⊆r Base) ⇒ (F[T] ⊆r Base))
BY
{ ((UnivCD THENA Auto)
   THEN Unfold `urec` -1
   THEN D_union (-1)
   THEN RenameVar `x' (-1)
   THEN Unfold `destructor` 3
   THEN NatInd (-2)
   THEN Reduce 0
   THEN (D 0 THENA Auto)
   THEN Try (Trivial)
   THEN ((GenConcl ⌜x = z ∈ (F (F^n - 1 Void))⌝⋅ THENA (Auto THEN RWO "fun_exp_add1" 0 THEN Auto))
         THEN Thin (-1)
         THEN Thin (-2))⋅) }

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

---

Latex:

---

Latex:
No  Annotations
\mforall{}[F:Type  {}\mrightarrow{}  Type]
    \mforall{}[f:destructor\{i:l\}(T.F[T])].  \mforall{}[x:urec(F)].    (urec-level(f;x)  \mmember{}  \mBbbN{}) 
    supposing  \mforall{}T:Type.  ((T  \msubseteq{}r  Base)  {}\mRightarrow{}  (F[T]  \msubseteq{}r  Base))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  Unfold  `urec`  -1
  THEN  D\_union  (-1)
  THEN  RenameVar  `x'  (-1)
  THEN  Unfold  `destructor`  3
  THEN  NatInd  (-2)
  THEN  Reduce  0
  THEN  (D  0  THENA  Auto)
  THEN  Try  (Trivial)
  THEN  ((GenConcl  \mkleeneopen{}x  =  z\mkleeneclose{}\mcdot{}  THENA  (Auto  THEN  RWO  "fun\_exp\_add1"  0  THEN  Auto))
              THEN  Thin  (-1)
              THEN  Thin  (-2))\mcdot{})

---

Home Index