---

Step * 1 1 1 1 of Lemma stump-monotone

.....subterm..... T:t
2:n
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. ¬↑(stump(f (s 0)) (n - 1) (λi.(s (i + 1))))
8. x : T
9. 0 < n
10. ¬(n = 0 ∈ ℤ)
11. ¬↑(stump(f (s 0)) ((n - 1) + 1) λi.(s (i + 1))++x)
⊢ (λi.(s++x (i + 1))) = λi.(s (i + 1))++x ∈ (ℕ(n + 1) - 1 ⟶ T)
BY
{ (RepUR ``seq-adjoin seq-append`` 0⋅ THEN EqCD THEN Auto THEN AutoSplit) }

---

Latex:

---

Latex:
.....subterm.....  T:t
2:n
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.  n  +  1  \mneq{}  0
6.  s  :  \mBbbN{}n  {}\mrightarrow{}  T
7.  \mneg{}\muparrow{}(stump(f  (s  0))  (n  -  1)  (\mlambda{}i.(s  (i  +  1))))
8.  x  :  T
9.  0  <  n
10.  \mneg{}(n  =  0)
11.  \mneg{}\muparrow{}(stump(f  (s  0))  ((n  -  1)  +  1)  \mlambda{}i.(s  (i  +  1))++x)
\mvdash{}  (\mlambda{}i.(s++x  (i  +  1)))  =  \mlambda{}i.(s  (i  +  1))++x


By

---

Latex:
(RepUR  ``seq-adjoin  seq-append``  0\mcdot{}  THEN  EqCD  THEN  Auto  THEN  AutoSplit)

---

Home Index