---

Step * 1 of Lemma cWO-induction-extract-sqequal


1. f : Base
2. t : Base
⊢ fix((λF,t. (f t F))) ~ λs1.(fix((λbar_recursion,n,s. case if (0) < (n)
                                                           then if s (n - 1)
                                                                then inr (λp.let _,_ = p 
                                                                             in Ax) 
                                                                else inl <Ax, Ax>
                                                                fi 
                                                           else (inr (λp.let _,_ = p 
                                                                         in Ax) )
                                                   of inl(r) =>
                                                   λa.let _,_ = r 
                                                      in Ax
                                                   | inr(r) =>
                                                   λa.(f a 
                                                       (λs1.(bar_recursion (n + 1) (λm.if m=n  then inl a  else (s m)) 
                                                             s1))))) 
                          1 
                          (λm.if m=0  then inl t  else if (m) < (0)  then 0 m  else ⊥) 
                          s1)
BY
{ AbbreviateTerm ⌜λbar_recursion,n,s. case if (0) < (n)
                                              then if s (n - 1) then inr (λp.let _,_ = p in Ax)  else inl <Ax, Ax> fi 
                                              else (inr (λp.let _,_ = p 
                                                            in Ax) )
                                      of inl(r) =>
                                      λa.let _,_ = r 
                                         in Ax
                                      | inr(r) =>
                                      λa.(f a (λs1.(bar_recursion (n + 1) (λm.if m=n  then inl a  else (s m)) s1)))⌝ `G'\000C⋅ }

1
1. f : Base
2. t : Base
3. G : Base
4. G ~ λf,bar_recursion,n,s. case if (0) < (n)
                                     then if s (n - 1) then inr (λp.let _,_ = p in Ax)  else inl <Ax, Ax> fi 
                                     else (inr (λp.let _,_ = p 
                                                   in Ax) )
                             of inl(r) =>
                             λa.let _,_ = r 
                                in Ax
                             | inr(r) =>
                             λa.(f a (λs1.(bar_recursion (n + 1) (λm.if m=n  then inl a  else (s m)) s1)))
⊢ fix((λF,t. (f t F))) ~ λs1.(fix((G f)) 1 (λm.if m=0  then inl t  else if (m) < (0)  then 0 m  else ⊥) s1)

---

Latex:

---

Latex:

1.  f  :  Base
2.  t  :  Base
\mvdash{}  fix((\mlambda{}F,t.  (f  t  F)))  \msim{}  \mlambda{}s1.(fix((\mlambda{}bar$_{recursion}$,n,s.  case  if  (0)  <  (n)
                                                                                                                    then  if  s  (n  -  1)
                                                                                                                              then  inr  (\mlambda{}p.let  $_{}\000C$,$_{}$  =  p 
                                                                                                                                                        in  Ax) 
                                                                                                                              else  inl  <Ax,  Ax>
                                                                                                                              fi 
                                                                                                                    else  (inr  (\mlambda{}p.let  $_{}\mbackslash{}ff2\000C4,$_{}$  =  p 
                                                                                                                                                in  Ax)  )
                                                                                                    of  inl(r)  =>
                                                                                                    \mlambda{}a.let  $_{}$,$_{\mbackslash{}f\000Cf7d$  =  r 
                                                                                                          in  Ax
                                                                                                    |  inr(r)  =>
                                                                                                    \mlambda{}a.(f  a 
                                                                                                            (\mlambda{}s1.(bar$_{recursion}$  (n\000C  +  1) 
                                                                                                                        (\mlambda{}m.if  m=n    then  inl  a    else  (s  m)) 
                                                                                                                        s1))))) 
                                                    1 
                                                    (\mlambda{}m.if  m=0    then  inl  t    else  if  (m)  <  (0)    then  0  m    else  \mbot{}) 
                                                    s1)


By

---

Latex:
AbbreviateTerm  \mkleeneopen{}\mlambda{}bar$_{recursion}$,n,s.  case  if  (0)  <  (n)
                                                                                      then  if  s  (n  -  1)
                                                                                                then  inr  (\mlambda{}p.let  $_{}$,$\mbackslash{}ff5\000Cf{}$  =  p 
                                                                                                                          in  Ax) 
                                                                                                else  inl  <Ax,  Ax>
                                                                                                fi 
                                                                                      else  (inr  (\mlambda{}p.let  $_{}$,$_\mbackslash{}ff\000C7b}$  =  p 
                                                                                                                  in  Ax)  )
                                                                      of  inl(r)  =>
                                                                      \mlambda{}a.let  $_{}$,$_{}$  =  r 
                                                                            in  Ax
                                                                      |  inr(r)  =>
                                                                      \mlambda{}a.(f  a 
                                                                              (\mlambda{}s1.(bar$_{recursion}$  (n  +  1) 
                                                                                          (\mlambda{}m.if  m=n    then  inl  a    else  (s  m)) 
                                                                                          s1)))\mkleeneclose{}  `G'\mcdot{}

---

Home Index