---

Step * of Lemma wfd-tree-induction

∀[A:Type]. ∀[P:wfd-tree(A) ⟶ ℙ].
  (P[w-nil()] ⇒ (∀f:A ⟶ wfd-tree(A). ((∀a:A. P[f a]) ⇒ P[mk-wfd-tree(f)])) ⇒ (∀w:wfd-tree(A). P[w]))
BY
{ Auto }

1
1. [A] : Type
2. [P] : wfd-tree(A) ⟶ ℙ
3. P[w-nil()]
4. ∀f:A ⟶ wfd-tree(A). ((∀a:A. P[f a]) ⇒ P[mk-wfd-tree(f)])
5. w : wfd-tree(A)
⊢ P[w]

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[P:wfd-tree(A)  {}\mrightarrow{}  \mBbbP{}].
    (P[w-nil()]
    {}\mRightarrow{}  (\mforall{}f:A  {}\mrightarrow{}  wfd-tree(A).  ((\mforall{}a:A.  P[f  a])  {}\mRightarrow{}  P[mk-wfd-tree(f)]))
    {}\mRightarrow{}  (\mforall{}w:wfd-tree(A).  P[w]))


By

---

Latex:
Auto

---

Home Index