---

Step * 2 1 1 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) ⟶ 𝔹))
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) ⟶ 𝔹)
7. stump'(f (s 0)) (n - 1) (λi.(s (i + 1))) 
= 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)))
8. (n - 1) = 0 ∈ ℤ
⊢ (¬b¬bempty-wfd-tree(f (s 0))) ∧b tt = empty-wfd-tree(f (s 0))
BY
{ (BoolCase ⌜empty-wfd-tree(f (s 0))⌝⋅ THEN Auto) }

---

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))
4.  n  :  \{1...\}
5.  s  :  \mBbbN{}n  {}\mrightarrow{}  T
6.  stump'(f  (s  0))
=  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  ;\000Cf  (s  0))
7.  stump'(f  (s  0))  (n  -  1)  (\mlambda{}i.(s  (i  +  1))) 
=  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  ;\000Cf 
                                                                                                                                                                                        (s  0)) 
    (n  -  1) 
    (\mlambda{}i.(s  (i  +  1)))
8.  (n  -  1)  =  0
\mvdash{}  (\mneg{}\msubb{}\mneg{}\msubb{}empty-wfd-tree(f  (s  0)))  \mwedge{}\msubb{}  tt  =  empty-wfd-tree(f  (s  0))


By

---

Latex:
(BoolCase  \mkleeneopen{}empty-wfd-tree(f  (s  0))\mkleeneclose{}\mcdot{}  THEN  Auto)

---

Home Index