---

Step * 1 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. 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))))
BY
{ ((SplitOnHypITE -3  THENA Auto) THEN Auto') }

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

---

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.  n  +  1  \mneq{}  0
6.  s  :  \mBbbN{}n  {}\mrightarrow{}  T
7.  \mneg{}\muparrow{}if  (n  =\msubz{}  0)  then  tt  else  stump(f  (s  0))  (n  -  1)  (\mlambda{}i.(s  (i  +  1)))  fi 
8.  x  :  T
9.  0  <  n
\mvdash{}  \mneg{}\muparrow{}(stump(f  (s  0))  ((n  +  1)  -  1)  (\mlambda{}i.(s++x  (i  +  1))))


By

---

Latex:
((SplitOnHypITE  -3    THENA  Auto)  THEN  Auto')

---

Home Index