---

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


1. T : Type
2. M : n:ℕ ⟶ (ℕn ⟶ T) ⟶ (ℕ?)
3. n : ℕ
4. f : Top
5. b : Top
⊢ strong-continuity-test(M;n;f;b) ~ if (n =z 0) then b
if isl(M (n - 1) f) then inr Ax 
else strong-continuity-test(M;n - 1;f;b)
fi 
BY
{ TACTIC:Unfold `strong-continuity-test` 0 }

1
1. T : Type
2. M : n:ℕ ⟶ (ℕn ⟶ T) ⟶ (ℕ?)
3. n : ℕ
4. f : Top
5. b : Top
⊢ primrec(n;b;λi,r. if isl(M i f) then inr Ax  else r fi ) ~ if (n =z 0) then b
if isl(M (n - 1) f) then inr Ax 
else primrec(n - 1;b;λi,r. 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(M;n;f;b)  \msim{}  if  (n  =\msubz{}  0)  then  b
if  isl(M  (n  -  1)  f)  then  inr  Ax 
else  strong-continuity-test(M;n  -  1;f;b)
fi 


By

---

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

---

Home Index