---

Step * 1 1 1 of Lemma stump-monotone

.....falsecase..... 
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 ∈ ℤ)
⊢ ¬↑(stump(f (s 0)) ((n + 1) - 1) (λi.(s++x (i + 1))))
BY
{ (InstHyp [⌜s 0⌝;⌜n - 1⌝;⌜λi.(s (i + 1))⌝;⌜x⌝] 3⋅ THEN Auto THEN NthHypEq (-1) THEN RepeatFor 3 ((EqCD THEN Auto))) }

1
.....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)

---

Latex:

---

Latex:
.....falsecase..... 
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)
\mvdash{}  \mneg{}\muparrow{}(stump(f  (s  0))  ((n  +  1)  -  1)  (\mlambda{}i.(s++x  (i  +  1))))


By

---

Latex:
(InstHyp  [\mkleeneopen{}s  0\mkleeneclose{};\mkleeneopen{}n  -  1\mkleeneclose{};\mkleeneopen{}\mlambda{}i.(s  (i  +  1))\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]  3\mcdot{}
  THEN  Auto
  THEN  NthHypEq  (-1)
  THEN  RepeatFor  3  ((EqCD  THEN  Auto)))

---

Home Index