---

Step * of Lemma tcWO-induction-ext

∀[T:Type]. ∀[>:T ⟶ T ⟶ ℙ].  ∀[Q:T ⟶ ℙ]. TI(T;x,y.>[x;y];t.Q[t]) supposing tcWO(T;x,y.>[x;y])
BY
{ Extract of Obid: tcWO-induction
  not unfolding bar_recursion
  finishing with xxx(Auto THEN Fold `bottom` 0 THEN Auto)xxx
  normalizes to:
  
  λF,t. (bar_recursion(λn,s. if (0) < (n)
                                then if s (n - 1) then inr (λ_.let _,_ = _ in Ax)  else inl <Ax, Ax> fi 
                                else (inr (λ_.let _,_ = _ 
                                              in Ax) );
                       λ_,_,_,_. Ax;
                       λn,s,g,a. (F a (λs.(g (inl a) s)));
                       0;λm.if (m) < (0)  then 0 m  else ⊥) 
         t) }

---

Latex:

---

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


By

---

Latex:
Extract  of  Obid:  tcWO-induction
not  unfolding  bar\_recursion
finishing  with  xxx(Auto  THEN  Fold  `bottom`  0  THEN  Auto)xxx
normalizes  to:

\mlambda{}F,t.  (bar\_recursion(\mlambda{}n,s.  if  (0)  <  (n)
                                                            then  if  s  (n  -  1)  then  inr  (\mlambda{}$_{}$.let  $_\mbackslash{}\000Cff7b}$,$_{}$  =  $_{}$  in  Ax)    else  inl  <Ax,  Ax>  fi 
                                                            else  (inr  (\mlambda{}$_{}$.let  $_{}$,\mbackslash{}f\000Cf24_{}$  =  $_{}$ 
                                                                                      in  Ax)  );
                                          \mlambda{}$_{}$,$_{}$,$_{}$,\000C$_{}$.  Ax;
                                          \mlambda{}n,s,g,a.  (F  a  (\mlambda{}s.(g  (inl  a)  s)));
                                          0;\mlambda{}m.if  (m)  <  (0)    then  0  m    else  \mbot{}) 
              t)

---

Home Index