---

Step * 1 1 1 1 1 3 1 1 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. t : Base
6. s1 : Base
7. n : ℕ+
8. x : Base
9. X : Base
10. X ~ λx,t,n,f,a. (f a 
                     (λ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))))) 
                           (n + 1) 
                           (λm.if m=n  then inl a  else if m=n - 1  then inl t  else (x m)) 
                           s1)))
⊢ f s1 ⊥ ≤ case if (0) < (n)  then inr (λp.let _,_ = p in Ax)   else (inr (λp.let _,_ = p in Ax) )
            of inl(r) =>
            λa.let _,_ = r 
               in Ax
            | inr(r) =>
            X x t n f 
           s1
BY
{ (AutoSplit THEN UnAbbreviate 9 THEN (Thin (-1) THEN Reduce 0) THEN Auto) }

---

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.  t  :  Base
6.  s1  :  Base
7.  n  :  \mBbbN{}\msupplus{}
8.  x  :  Base
9.  X  :  Base
10.  X  \msim{}  \mlambda{}x,t,n,f,a.  (f  a 
                                          (\mlambda{}s1.(fix((\mlambda{}bar$_{recursion}$,n,s.  case  if  (0)  <  (n)
                                                                                                                      then  if  s  (n  -  1)
                                                                                                                                then  inr  (\mlambda{}p.let  $_{\mbackslash{}ff7\000Cd$,$_{}$  =  p 
                                                                                                                                                          in  Ax) 
                                                                                                                                else  inl  <Ax,  Ax>
                                                                                                                                fi 
                                                                                                                      else  (inr  (\mlambda{}p.let  $_{}\mbackslash{}ff\000C24,$_{}$  =  p 
                                                                                                                                                  in  Ax)  )
                                                                                                      of  inl(r)  =>
                                                                                                      \mlambda{}a.let  $_{}$,$_{\mbackslash{}\000Cff7d$  =  r 
                                                                                                            in  Ax
                                                                                                      |  inr(r)  =>
                                                                                                      \mlambda{}a.(f  a 
                                                                                                              (\mlambda{}s1.(bar$_{recursion}$  (\000Cn  +  1) 
                                                                                                                          (\mlambda{}m.if  m=n    then  inl  a    else  (s  m)) 
                                                                                                                          s1))))) 
                                                      (n  +  1) 
                                                      (\mlambda{}m.if  m=n    then  inl  a    else  if  m=n  -  1    then  inl  t    else  (x  m)) 
                                                      s1)))
\mvdash{}  f  s1  \mbot{}  \mleq{}  case  if  (0)  <  (n)    then  inr  (\mlambda{}p.let  $_{}$,$_{}$  =\000C  p  in  Ax)      else  (inr  (\mlambda{}p.let  $_{}$,$_{}$  =  p  in  Ax)  )
                        of  inl(r)  =>
                        \mlambda{}a.let  $_{}$,$_{}$  =  r 
                              in  Ax
                        |  inr(r)  =>
                        X  x  t  n  f 
                      s1


By

---

Latex:
(AutoSplit  THEN  UnAbbreviate  9  THEN  (Thin  (-1)  THEN  Reduce  0)  THEN  Auto)

---

Home Index