---

Step * of Lemma stump'_property

∀T:Type. ∀t:wfd-tree(T). ∀n:ℕ. ∀s:ℕn ⟶ T.
  (↑(stump'(t) n s) ⇐⇒ (¬↑(stump(t) n s)) ∧ (0 < n ⇒ (↑(stump(t) (n - 1) s))))
BY
{ ((UnivCD THENA Auto) THEN Unfold `stump\'` 0 THEN Reduce 0 THEN AutoSplit) }

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

2
1. T : Type
2. t : wfd-tree(T)
3. n : {1...}
4. s : ℕn ⟶ T
⊢ ↑((¬b(stump(t) n s)) ∧b (stump(t) (n - 1) s)) ⇐⇒ (¬↑(stump(t) n s)) ∧ (0 < n ⇒ (↑(stump(t) (n - 1) s)))

---

Latex:

---

Latex:
\mforall{}T:Type.  \mforall{}t:wfd-tree(T).  \mforall{}n:\mBbbN{}.  \mforall{}s:\mBbbN{}n  {}\mrightarrow{}  T.
    (\muparrow{}(stump'(t)  n  s)  \mLeftarrow{}{}\mRightarrow{}  (\mneg{}\muparrow{}(stump(t)  n  s))  \mwedge{}  (0  <  n  {}\mRightarrow{}  (\muparrow{}(stump(t)  (n  -  1)  s))))


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  Unfold  `stump\mbackslash{}'`  0  THEN  Reduce  0  THEN  AutoSplit)

---

Home Index