---

Step * 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
⊢ 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 
BY
{ (RW (AddrC [1] (LemmaC `primrec-unroll`)) 0 THENA Auto) }

1
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 

---

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{}  primrec(n;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  )  \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:
(RW  (AddrC  [1]  (LemmaC  `primrec-unroll`))  0  THENA  Auto)

---

Home Index