---

Step * 2 of Lemma stump'-inductive


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) ⟶ 𝔹)
BY
{ (Unfold `stump\'` 0
   THEN Unfold `stump` 0
   THEN Reduce 0
   THEN Fold `stump` 0
   THEN (EqCD THENA Auto)
   THEN AutoSplit
   THEN (EqCD THENA Auto)
   THEN (InstHyp [⌜s 0⌝] 3⋅ THENA Auto)) }

1
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) ⟶ 𝔹))
4. n : {1...}
5. s : ℕn ⟶ T
6. stump'(f (s 0))
= 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 (s 0))
∈ (n:ℕ ⟶ (ℕn ⟶ T) ⟶ 𝔹)
⊢ (¬b(stump(f (s 0)) (n - 1) (λi.(s (i + 1)))))
  ∧b if (n - 1 =z 0) then tt else stump(f (s 0)) (n - 1 - 1) (λi.(s (i + 1))) fi  
= 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 (s 0)) (n - 1) 
  (λi.(s (i + 1)))

---

Latex:

---

Latex:

1.  T  :  Type
2.  f  :  T  {}\mrightarrow{}  wfd-tree(T)
3.  \mforall{}b:T
          (stump'(f  b)
          =  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)))\000C  fi  ;f 
                                                                                                                                                                                                  b))
\mvdash{}  stump'(Wsup(ff;f))
=  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  ;Wsup(ff;f))


By

---

Latex:
(Unfold  `stump\mbackslash{}'`  0
  THEN  Unfold  `stump`  0
  THEN  Reduce  0
  THEN  Fold  `stump`  0
  THEN  (EqCD  THENA  Auto)
  THEN  AutoSplit
  THEN  (EqCD  THENA  Auto)
  THEN  (InstHyp  [\mkleeneopen{}s  0\mkleeneclose{}]  3\mcdot{}  THENA  Auto))

---

Home Index