---

Step * of Lemma cWO-induction_1-ext

∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  ∀[Q:T ⟶ ℙ]. TI(T;x,y.R[x;y];t.Q[t]) supposing cWO(T;x,y.R[x;y])
BY
{ Extract of Obid: cWO-induction_1
  normalizes to:
  
  λF,t. (bar_recursion(λn,s. 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) );
                       λn,s,p,a. let _,_ = p in Ax;
                       λn,s,g,a. (F a (λs1.(g (inl a) s1)));
                       0;λm.if (m) < (0)  then 0 m  else ⊥) 
         t)
  
  not unfolding bar_recursion
  finishing with (Try (Fold `bottom` 0) THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].    \mforall{}[Q:T  {}\mrightarrow{}  \mBbbP{}].  TI(T;x,y.R[x;y];t.Q[t])  supposing  cWO(T;x,y.R[x;y])


By

---

Latex:
Extract  of  Obid:  cWO-induction\_1
normalizes  to:

\mlambda{}F,t.  (bar\_recursion(\mlambda{}n,s.  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  $_{}$,$_{}$  \000C=  p 
                                                                                        in  Ax)  );
                                          \mlambda{}n,s,p,a.  let  $_{}$,$_{}$  =  p  in  Ax;
                                          \mlambda{}n,s,g,a.  (F  a  (\mlambda{}s1.(g  (inl  a)  s1)));
                                          0;\mlambda{}m.if  (m)  <  (0)    then  0  m    else  \mbot{}) 
              t)

not  unfolding  bar\_recursion
finishing  with  (Try  (Fold  `bottom`  0)  THEN  Auto)

---

Home Index