---

Step * of Lemma stump'-inductive

∀T:Type. ∀t:wfd-tree(T).
  (stump'(t)
  = wfd-tree-rec(λn,s. (n =z 0);r.λn,s. if (n =z 0) then ff else r (s 0) (n - 1) (λi.(s (i + 1))) fi ;t)
  ∈ (n:ℕ ⟶ (ℕn ⟶ T) ⟶ 𝔹))
BY
{ ((D 0 THENA Auto) THEN BLemma `wfd-tree-induction` THEN Auto) }

1
1. T : Type
⊢ stump'(Wsup(tt;⋅))
= wfd-tree-rec(λn,s. (n =z 0);r.λn,s. if (n =z 0) then ff else r (s 0) (n - 1) (λi.(s (i + 1))) fi ;Wsup(tt;⋅))
∈ (n:ℕ ⟶ (ℕn ⟶ T) ⟶ 𝔹)

2
1. T : Type
2. f : T ⟶ wfd-tree(T)
3. ∀b:T
     (stump'(f b)
     = wfd-tree-rec(λn,s. (n =z 0);r.λn,s. if (n =z 0) then ff else r (s 0) (n - 1) (λi.(s (i + 1))) fi ;f b)
     ∈ (n:ℕ ⟶ (ℕn ⟶ T) ⟶ 𝔹))
⊢ stump'(Wsup(ff;f))
= wfd-tree-rec(λn,s. (n =z 0);r.λn,s. if (n =z 0) then ff else r (s 0) (n - 1) (λi.(s (i + 1))) fi ;Wsup(ff;f))
∈ (n:ℕ ⟶ (ℕn ⟶ T) ⟶ 𝔹)

---

Latex:

---

Latex:
\mforall{}T:Type.  \mforall{}t:wfd-tree(T).
    (stump'(t)
    =  wfd-tree-rec(\mlambda{}n,s.  (n  =\msubz{}  0);r.\mlambda{}n,s.  if  (n  =\msubz{}  0)  then  ff  else  r  (s  0)  (n  -  1)  (\mlambda{}i.(s  (i  +  1)))  fi\000C  ;t))


By

---

Latex:
((D  0  THENA  Auto)  THEN  BLemma  `wfd-tree-induction`  THEN  Auto)

---

Home Index