Step
*
1
2
1
of Lemma
strong-continuity-test-sp_wf
1. M : n:ℕ ⟶ (ℕn ⟶ ℕ) ⟶ (ℕ?)
2. k : ℕ
3. n : ℤ
4. 0 < n
5. ∀f:ℕn - 1 ⟶ ℕ. (strong-continuity-test-sp(M;n - 1;f;k) ∈ ℕ?)
⊢ ∀f:ℕn ⟶ ℕ. (primrec(n;inl k;λi,r. case M i f of inl(m) => if (m =z k) then inr Ax else r fi | inr(x) => r) ∈ ℕ?)
BY
{ (RWO "primrec-unroll-1" 0⋅ THEN Auto) }
Latex:
Latex:
1. M : n:\mBbbN{} {}\mrightarrow{} (\mBbbN{}n {}\mrightarrow{} \mBbbN{}) {}\mrightarrow{} (\mBbbN{}?)
2. k : \mBbbN{}
3. n : \mBbbZ{}
4. 0 < n
5. \mforall{}f:\mBbbN{}n - 1 {}\mrightarrow{} \mBbbN{}. (strong-continuity-test-sp(M;n - 1;f;k) \mmember{} \mBbbN{}?)
\mvdash{} \mforall{}f:\mBbbN{}n {}\mrightarrow{} \mBbbN{}
(primrec(n;inl k;\mlambda{}i,r. case M i f of inl(m) => if (m =\msubz{} k) then inr Ax else r fi | inr(x) => r\000C)
\mmember{} \mBbbN{}?)
By
Latex:
(RWO "primrec-unroll-1" 0\mcdot{} THEN Auto)
Home
Index