---

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


1. T : Type
2. M : n:ℕ ⟶ (ℕn ⟶ T) ⟶ (ℕ?)
3. n : ℕ
4. f : Top
5. b : Top
⊢ strong-continuity-test-bound(M;n;f;b) ~ 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 strong-continuity-test-bound(M;n - 1;f;b)
fi 
BY
{ Unfold `strong-continuity-test-bound` 0 }

1
1. T : Type
2. M : n:ℕ ⟶ (ℕn ⟶ T) ⟶ (ℕ?)
3. n : ℕ
4. f : Top
5. b : Top
⊢ primrec(n;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 ) 
~ 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 

---

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{}  strong-continuity-test-bound(M;n;f;b)  \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  strong-continuity-test-bound(M;n  -  1;f;b)
fi 


By

---

Latex:
Unfold  `strong-continuity-test-bound`  0

---

Home Index