---

Step * 1 of Lemma stump'_property


1. T : Type
2. t : wfd-tree(T)
3. n : ℕ
4. s : ℕn ⟶ T
5. n = 0 ∈ ℤ
⊢ ↑empty-wfd-tree(t) ⇐⇒ (¬↑(stump(t) n s)) ∧ (0 < n ⇒ (↑(stump(t) (n - 1) s)))
BY
{ ((HypSubst' (-1) 0 THEN (RWO "stump-nil" 0 THENA Auto)) THEN BoolCase ⌜empty-wfd-tree(t)⌝⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  t  :  wfd-tree(T)
3.  n  :  \mBbbN{}
4.  s  :  \mBbbN{}n  {}\mrightarrow{}  T
5.  n  =  0
\mvdash{}  \muparrow{}empty-wfd-tree(t)  \mLeftarrow{}{}\mRightarrow{}  (\mneg{}\muparrow{}(stump(t)  n  s))  \mwedge{}  (0  <  n  {}\mRightarrow{}  (\muparrow{}(stump(t)  (n  -  1)  s)))


By

---

Latex:
((HypSubst'  (-1)  0  THEN  (RWO  "stump-nil"  0  THENA  Auto))
  THEN  BoolCase  \mkleeneopen{}empty-wfd-tree(t)\mkleeneclose{}\mcdot{}
  THEN  Auto)

---

Home Index