---

Step * 1 1 1 of Lemma strong-continuity-test-bound-unroll


1. T : Type
2. M : n:ℕ ⟶ (ℕn ⟶ T) ⟶ (ℕ?)
3. n : ℕ
4. f : Top
5. b : Top
⊢ if (n =z 0)
then inr Ax 
else (λi,r. if i <z b then inr Ax  if (i =z b) then inl b if isl(M i f) then inr Ax  else r fi ) (n - 1) 
     primrec(n - 1;inr Ax ;λi,r. if i <z b then inr Ax  if (i =z b) then inl b if isl(M i f) then inr Ax  else r fi )
fi  ~ if (n =z 0) then inr Ax 
if n - 1 <z b then inr Ax 
if (n - 1 =z b) then inl b
if isl(M (n - 1) f) then inr Ax 
else primrec(n - 1;inr Ax ;λi,r. if i <z b then inr Ax  if (i =z b) then inl b if isl(M i f) then inr Ax  else r fi )
fi 
BY
{ (Reduce 0 THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  M  :  n:\mBbbN{}  {}\mrightarrow{}  (\mBbbN{}n  {}\mrightarrow{}  T)  {}\mrightarrow{}  (\mBbbN{}?)
3.  n  :  \mBbbN{}
4.  f  :  Top
5.  b  :  Top
\mvdash{}  if  (n  =\msubz{}  0)
then  inr  Ax 
else  (\mlambda{}i,r.  if  i  <z  b  then  inr  Ax    if  (i  =\msubz{}  b)  then  inl  b  if  isl(M  i  f)  then  inr  Ax    else  r  fi  ) 
          (n  -  1) 
          primrec(n  -  1;inr  Ax  ;\mlambda{}i,r.  if  i  <z  b  then  inr  Ax 
                                                                if  (i  =\msubz{}  b)  then  inl  b
                                                                if  isl(M  i  f)  then  inr  Ax 
                                                                else  r
                                                                fi  )
fi    \msim{}  if  (n  =\msubz{}  0)  then  inr  Ax 
if  n  -  1  <z  b  then  inr  Ax 
if  (n  -  1  =\msubz{}  b)  then  inl  b
if  isl(M  (n  -  1)  f)  then  inr  Ax 
else  primrec(n  -  1;inr  Ax  ;\mlambda{}i,r.  if  i  <z  b  then  inr  Ax 
                                                                if  (i  =\msubz{}  b)  then  inl  b
                                                                if  isl(M  i  f)  then  inr  Ax 
                                                                else  r
                                                                fi  )
fi 


By

---

Latex:
(Reduce  0  THEN  Auto)

---

Home Index