---

Step * of Lemma stump-monotone

∀T:Type. ∀t:wfd-tree(T). ∀n:ℕ. ∀s:ℕn ⟶ T.  ((¬↑(stump(t) n s)) ⇒ (∀x:T. (¬↑(stump(t) (n + 1) s++x))))
BY
{ ((D 0 THENA Auto)
   THEN (BLemma `wfd-tree-induction` THENA Auto)
   THEN Unfold `stump` 0
   THEN Reduce 0
   THEN Try (Fold `stump` 0)
   THEN Auto) }

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

---

Latex:

---

Latex:
\mforall{}T:Type.  \mforall{}t:wfd-tree(T).  \mforall{}n:\mBbbN{}.  \mforall{}s:\mBbbN{}n  {}\mrightarrow{}  T.
    ((\mneg{}\muparrow{}(stump(t)  n  s))  {}\mRightarrow{}  (\mforall{}x:T.  (\mneg{}\muparrow{}(stump(t)  (n  +  1)  s++x))))


By

---

Latex:
((D  0  THENA  Auto)
  THEN  (BLemma  `wfd-tree-induction`  THENA  Auto)
  THEN  Unfold  `stump`  0
  THEN  Reduce  0
  THEN  Try  (Fold  `stump`  0)
  THEN  Auto)

---

Home Index