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


1. Base
2. Base
3. Base
4. ~ λf,bar_recursion,n,s. case if (0) < (n)
                                     then if (n 1) then inr p.let _,_ in Ax)  else inl <Ax, Ax> fi 
                                     else (inr p.let _,_ 
                                                   in Ax) )
                             of inl(r) =>
                             λa.let _,_ 
                                in Ax
                             inr(r) =>
                             λa.(f s1.(bar_recursion (n 1) m.if m=n  then inl a  else (s m)) s1)))
5. s1 Base
⊢ s1 fix((λF,t. (f F))) fix((G f)) m.if m=0  then inl t  else if (m) < (0)  then m  else ⊥s1
BY
Assert ⌜∀n:ℕ+. ∀x:Base.  (G fix((G f)) m.if m=n 1  then inl t  else (x m)) s1 s1 fix((λF,t. (f F))))⌝⋅ }

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

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


Latex:


Latex:

1.  f  :  Base
2.  t  :  Base
3.  G  :  Base
4.  G  \msim{}  \mlambda{}f,bar$_{recursion}$,n,s.  case  if  (0)  <  (n)
                                                                        then  if  s  (n  -  1)
                                                                                  then  inr  (\mlambda{}p.let  $_{}$,$_{\mbackslash{}\000Cff7d$  =  p 
                                                                                                            in  Ax) 
                                                                                  else  inl  <Ax,  Ax>
                                                                                  fi 
                                                                        else  (inr  (\mlambda{}p.let  $_{}$,$_{}\000C$  =  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\000C  inl  a    else  (s  m))  s1)))
5.  s1  :  Base
\mvdash{}  f  s1  fix((\mlambda{}F,t.  (f  t  F)))  \msim{}  G  f  fix((G  f))  1 
                                                    (\mlambda{}m.if  m=0    then  inl  t    else  if  (m)  <  (0)    then  0  m    else  \mbot{}) 
                                                    s1


By


Latex:
Assert  \mkleeneopen{}\mforall{}n:\mBbbN{}\msupplus{}.  \mforall{}x:Base.
                    (G  f  fix((G  f))  n  (\mlambda{}m.if  m=n  -  1    then  inl  t    else  (x  m))  s1  \msim{}  f  s1  fix((\mlambda{}F,t.  (f  t  F))))\mkleeneclose{}\000C\mcdot{}




Home Index