---

Step * of Lemma wfd-tree-induction

∀[T:Type]
  ∀P:wfd-tree(T) ⟶ ℙ
    (P[Wsup(tt;⋅)] ⇒ (∀f:T ⟶ wfd-tree(T). ((∀b:T. P[f b]) ⇒ P[Wsup(ff;f)])) ⇒ {∀t:wfd-tree(T). P[t]})
BY
{ ((Auto THEN Try (((Unfold `wfd-tree` 0 THEN MemCD) THEN Reduce 0 THEN Auto)))
   THEN (InstLemma `W-induction` [⌜𝔹⌝;⌜λ2z.if z then Void else T fi ⌝]⋅ THENA Auto)
   THEN Fold `wfd-tree` (-1)
   THEN (With ⌜P⌝ (D (-1))⋅ THENA Auto)
   THEN D -1
   THEN Try ((Unfold `guard` 0 THEN Trivial))
   THEN (D 0 THENA Auto)
   THEN D -1
   THEN Reduce 0
   THEN D -1
   THEN Fold `it` 0
   THEN Folds ``btrue bfalse`` 0
   THEN Auto) }

1
1. [T] : Type
2. P : wfd-tree(T) ⟶ ℙ
3. P[Wsup(tt;⋅)]
4. ∀f:T ⟶ wfd-tree(T). ((∀b:T. P[f b]) ⇒ P[Wsup(ff;f)])
5. x : 0 = 0 ∈ ℤ
6. f : Void ⟶ wfd-tree(T)
7. ∀b:Void. P[f b]
⊢ P[Wsup(tt;f)]

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}P:wfd-tree(T)  {}\mrightarrow{}  \mBbbP{}
        (P[Wsup(tt;\mcdot{})]
        {}\mRightarrow{}  (\mforall{}f:T  {}\mrightarrow{}  wfd-tree(T).  ((\mforall{}b:T.  P[f  b])  {}\mRightarrow{}  P[Wsup(ff;f)]))
        {}\mRightarrow{}  \{\mforall{}t:wfd-tree(T).  P[t]\})


By

---

Latex:
((Auto  THEN  Try  (((Unfold  `wfd-tree`  0  THEN  MemCD)  THEN  Reduce  0  THEN  Auto)))
  THEN  (InstLemma  `W-induction`  [\mkleeneopen{}\mBbbB{}\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}z.if  z  then  Void  else  T  fi  \mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  Fold  `wfd-tree`  (-1)
  THEN  (With  \mkleeneopen{}P\mkleeneclose{}  (D  (-1))\mcdot{}  THENA  Auto)
  THEN  D  -1
  THEN  Try  ((Unfold  `guard`  0  THEN  Trivial))
  THEN  (D  0  THENA  Auto)
  THEN  D  -1
  THEN  Reduce  0
  THEN  D  -1
  THEN  Fold  `it`  0
  THEN  Folds  ``btrue  bfalse``  0
  THEN  Auto)

---

Home Index