---

Step * 2 of Lemma stump'_property


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)))
BY
{ (RW assert_pushdownC 0 THEN Auto) }

---

Latex:

---

Latex:

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


By

---

Latex:
(RW  assert\_pushdownC  0  THEN  Auto)

---

Home Index