---

Step * 2 of Lemma stump-bars


1. T : Type
2. f : T ⟶ wfd-tree(T)
3. ∀b:T. ∀alpha:ℕ ⟶ T.  ∃n:ℕ. (¬↑(stump(f b) n alpha))
4. alpha : ℕ ⟶ T
⊢ ∃n:ℕ. (¬↑if (n =z 0) then tt else stump(f (alpha 0)) (n - 1) (λi.(alpha (i + 1))) fi )
BY
{ ((InstHyp [⌜alpha 0⌝;⌜λi.(alpha (i + 1))⌝] 3⋅ THENA Auto)
   THEN ExRepD
   THEN With ⌜n + 1⌝ (D 0)⋅
   THEN Auto
   THEN AutoSplit
   THEN NthHypSq (-1)
   THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  f  :  T  {}\mrightarrow{}  wfd-tree(T)
3.  \mforall{}b:T.  \mforall{}alpha:\mBbbN{}  {}\mrightarrow{}  T.    \mexists{}n:\mBbbN{}.  (\mneg{}\muparrow{}(stump(f  b)  n  alpha))
4.  alpha  :  \mBbbN{}  {}\mrightarrow{}  T
\mvdash{}  \mexists{}n:\mBbbN{}.  (\mneg{}\muparrow{}if  (n  =\msubz{}  0)  then  tt  else  stump(f  (alpha  0))  (n  -  1)  (\mlambda{}i.(alpha  (i  +  1)))  fi  )


By

---

Latex:
((InstHyp  [\mkleeneopen{}alpha  0\mkleeneclose{};\mkleeneopen{}\mlambda{}i.(alpha  (i  +  1))\mkleeneclose{}]  3\mcdot{}  THENA  Auto)
  THEN  ExRepD
  THEN  With  \mkleeneopen{}n  +  1\mkleeneclose{}  (D  0)\mcdot{}
  THEN  Auto
  THEN  AutoSplit
  THEN  NthHypSq  (-1)
  THEN  Auto)

---

Home Index