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