---

Step * 1 of Lemma stump-monotone


1. T : Type
2. f : T ⟶ wfd-tree(T)
3. ∀b:T. ∀n:ℕ. ∀s:ℕn ⟶ T.  ((¬↑(stump(f b) n s)) ⇒ (∀x:T. (¬↑(stump(f b) (n + 1) s++x))))
4. n : ℕ
5. s : ℕn ⟶ T
6. ¬↑if (n =z 0) then tt else stump(f (s 0)) (n - 1) (λi.(s (i + 1))) fi 
7. x : T
⊢ ¬↑if (n + 1 =z 0) then tt else stump(f (s++x 0)) ((n + 1) - 1) (λi.(s++x (i + 1))) fi 
BY
{ ((Subst' s++x 0 ~ if (0) < (n)  then s 0  else x 0 THENA (RepUR ``seq-adjoin seq-append`` 0 THEN AutoSplit))
   THEN RepeatFor 2 (AutoSplit)
   ) }

1
1. T : Type
2. f : T ⟶ wfd-tree(T)
3. ∀b:T. ∀n:ℕ. ∀s:ℕn ⟶ T.  ((¬↑(stump(f b) n s)) ⇒ (∀x:T. (¬↑(stump(f b) (n + 1) s++x))))
4. n : ℕ
5. n + 1 ≠ 0
6. s : ℕn ⟶ T
7. ¬↑if (n =z 0) then tt else stump(f (s 0)) (n - 1) (λi.(s (i + 1))) fi 
8. x : T
9. 0 < n
⊢ ¬↑(stump(f (s 0)) ((n + 1) - 1) (λi.(s++x (i + 1))))

---

Latex:

---

Latex:

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


By

---

Latex:
((Subst'  s++x  0  \msim{}  if  (0)  <  (n)    then  s  0    else  x  0
    THENA  (RepUR  ``seq-adjoin  seq-append``  0  THEN  AutoSplit)
    )
  THEN  RepeatFor  2  (AutoSplit)
  )

---

Home Index