---

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


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 
BY
{ TACTIC:(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 1
then b
else (λi,r. if isl(M i f) then inr Ax  else r fi ) (n - 1) primrec(n - 1;b;λi,r. if isl(M i f) then inr Ax  else r fi )
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{}  primrec(n;b;\mlambda{}i,r.  if  isl(M  i  f)  then  inr  Ax    else  r  fi  )  \msim{}  if  (n  =\msubz{}  0)  then  b
if  isl(M  (n  -  1)  f)  then  inr  Ax 
else  primrec(n  -  1;b;\mlambda{}i,r.  if  isl(M  i  f)  then  inr  Ax    else  r  fi  )
fi 


By

---

Latex:
TACTIC:(RW  (AddrC  [1]  (LemmaC  `primrec-unroll`))  0  THENA  Auto)

---

Home Index