---

Step * of Lemma stump-nil

∀T:Type. ∀t:wfd-tree(T). ∀s:ℕ0 ⟶ T.  (stump(t) 0 s ~ ¬bempty-wfd-tree(t))
BY
{ (Auto
   THEN RepeatFor 2 (MoveToConcl  (-1))
   THEN (BLemma `wfd-tree-induction` THENA Auto)
   THEN Unfold `stump` 0
   THEN Reduce 0
   THEN Try (Fold `stump` 0)
   THEN RepUR ``empty-wfd-tree`` 0
   THEN Try (Fold `empty-wfd-tree` 0)
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}T:Type.  \mforall{}t:wfd-tree(T).  \mforall{}s:\mBbbN{}0  {}\mrightarrow{}  T.    (stump(t)  0  s  \msim{}  \mneg{}\msubb{}empty-wfd-tree(t))


By

---

Latex:
(Auto
  THEN  RepeatFor  2  (MoveToConcl    (-1))
  THEN  (BLemma  `wfd-tree-induction`  THENA  Auto)
  THEN  Unfold  `stump`  0
  THEN  Reduce  0
  THEN  Try  (Fold  `stump`  0)
  THEN  RepUR  ``empty-wfd-tree``  0
  THEN  Try  (Fold  `empty-wfd-tree`  0)
  THEN  Auto)

---

Home Index