---

Step * 2 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) ⟶ 𝔹)
⊢ (¬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)))
BY
{ ((ApFunToHypEquands `Z' ⌜Z (n - 1) (λi.(s (i + 1)))⌝ ⌜𝔹⌝ (-1)⋅ THENA Auto)
   THEN RevHypSubst' (-1) 0
   THEN Unfold `stump\'` 0
   THEN Reduce 0
   THEN AutoSplit
   THEN HypSubst' (-1) 0
   THEN (RWO "stump-nil" 0 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) ⟶ 𝔹)
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))

---

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))
\mvdash{}  (\mneg{}\msubb{}(stump(f  (s  0))  (n  -  1)  (\mlambda{}i.(s  (i  +  1)))))
    \mwedge{}\msubb{}  if  (n  -  1  =\msubz{}  0)  then  tt  else  stump(f  (s  0))  (n  -  1  -  1)  (\mlambda{}i.(s  (i  +  1)))  fi   
=  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)))


By

---

Latex:
((ApFunToHypEquands  `Z'  \mkleeneopen{}Z  (n  -  1)  (\mlambda{}i.(s  (i  +  1)))\mkleeneclose{}  \mkleeneopen{}\mBbbB{}\mkleeneclose{}  (-1)\mcdot{}  THENA  Auto)
  THEN  RevHypSubst'  (-1)  0
  THEN  Unfold  `stump\mbackslash{}'`  0
  THEN  Reduce  0
  THEN  AutoSplit
  THEN  HypSubst'  (-1)  0
  THEN  (RWO  "stump-nil"  0  THENA  Auto))

---

Home Index