---

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


1. f : Base
2. G : Base
3. 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)))
4. j : ℤ
5. j ≠ 0
6. 0 < j
7. ∀t,s1:Base. ∀n:ℕ+. ∀x:Base.
     (G f (G f^j - 1 ⊥) n (λm.if m=n - 1  then inl t  else (x m)) s1 ≤ f s1 fix((λF,t. (f t F))))
8. t : Base
9. s1 : Base
10. n : ℕ+
11. x : Base
⊢ G f (G f (G f^j - 1 ⊥)) n (λm.if m=n - 1  then inl t  else (x m)) s1 ≤ f s1 fix((λF,t. (f t F)))
BY
{ Subst' G f (G f (G f^j - 1 ⊥)) n (λm.if m=n - 1  then inl t  else (x m)) s1 
~ (λ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)))) 
  f 
  (G f (G f^j - 1 ⊥)) 
  n 
  (λm.if m=n - 1  then inl t  else (x m)) 
  s1 0 }

1
.....equality..... 
1. f : Base
2. G : Base
3. 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)))
4. j : ℤ
5. j ≠ 0
6. 0 < j
7. ∀t,s1:Base. ∀n:ℕ+. ∀x:Base.
     (G f (G f^j - 1 ⊥) n (λm.if m=n - 1  then inl t  else (x m)) s1 ≤ f s1 fix((λF,t. (f t F))))
8. t : Base
9. s1 : Base
10. n : ℕ+
11. x : Base
⊢ G f (G f (G f^j - 1 ⊥)) n (λm.if m=n - 1  then inl t  else (x m)) s1 
~ (λ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)))) 
  f 
  (G f (G f^j - 1 ⊥)) 
  n 
  (λm.if m=n - 1  then inl t  else (x m)) 
  s1

2
1. f : Base
2. G : Base
3. 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)))
4. j : ℤ
5. j ≠ 0
6. 0 < j
7. ∀t,s1:Base. ∀n:ℕ+. ∀x:Base.
     (G f (G f^j - 1 ⊥) n (λm.if m=n - 1  then inl t  else (x m)) s1 ≤ f s1 fix((λF,t. (f t F))))
8. t : Base
9. s1 : Base
10. n : ℕ+
11. x : Base
⊢ (λ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)))) 
  f 
  (G f (G f^j - 1 ⊥)) 
  n 
  (λm.if m=n - 1  then inl t  else (x m)) 
  s1 ≤ f s1 fix((λF,t. (f t F)))

---

Latex:

---

Latex:

1.  f  :  Base
2.  G  :  Base
3.  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)))
4.  j  :  \mBbbZ{}
5.  j  \mneq{}  0
6.  0  <  j
7.  \mforall{}t,s1:Base.  \mforall{}n:\mBbbN{}\msupplus{}.  \mforall{}x:Base.
          (G  f  (G  f\^{}j  -  1  \mbot{})  n  (\mlambda{}m.if  m=n  -  1    then  inl  t    else  (x  m))  s1  \mleq{}  f  s1  fix((\mlambda{}F,t.  (f  t  F))))
8.  t  :  Base
9.  s1  :  Base
10.  n  :  \mBbbN{}\msupplus{}
11.  x  :  Base
\mvdash{}  G  f  (G  f  (G  f\^{}j  -  1  \mbot{}))  n  (\mlambda{}m.if  m=n  -  1    then  inl  t    else  (x  m))  s1  \mleq{}  f  s1  fix((\mlambda{}F,t.  (f  t  F)))


By

---

Latex:
Subst'  G  f  (G  f  (G  f\^{}j  -  1  \mbot{}))  n  (\mlambda{}m.if  m=n  -  1    then  inl  t    else  (x  m))  s1 
\msim{}  (\mlambda{}f,bar$_{recursion}$,n,s.  case  if  (0)  <  (n)
                                                                then  if  s  (n  -  1)  then  inr  (\mlambda{}p.let  $_{}$,$\mbackslash{}f\000Cf5f{}$  =  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  $_{}$,$_{}$  =  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)))) 
    f 
    (G  f  (G  f\^{}j  -  1  \mbot{})) 
    n 
    (\mlambda{}m.if  m=n  -  1    then  inl  t    else  (x  m)) 
    s1  0

---

Home Index