---

Step * 2 of Lemma enumerate_wf

.....upcase..... 
1. P : ℕ ⟶ 𝔹
2. n : ℤ
3. 0 < n
4. primrec(n - 1;mu(P);λi,r. eval r' = r + 1 in r' + mu(λk.(P (r' + k)))) ∈ {k:ℕ| ↑(P k)}  supposing ∀n:ℕ. ∃k:ℕ. ((↑(P k\000C)) ∧ (n ≤ k))
⊢ primrec(n;mu(P);λi,r. eval r' = r + 1 in r' + mu(λk.(P (r' + k)))) ∈ {k:ℕ| ↑(P k)}  supposing ∀n:ℕ. ∃k:ℕ. ((↑(P k)) ∧ \000C(n ≤ k))
BY
{ xxx(ParallelLast THEN (RWO "primrec-unroll" 0 THENA Auto) THEN OldAutoSplit)xxx }

1
1. P : ℕ ⟶ 𝔹
2. n : ℤ
3. 0 < n
4. ∀n:ℕ. ∃k:ℕ. ((↑(P k)) ∧ (n ≤ k))
5. primrec(n - 1;mu(P);λi,r. eval r' = r + 1 in r' + mu(λk.(P (r' + k)))) ∈ {k:ℕ| ↑(P k)} 
6. ¬(n = 0 ∈ ℤ)
⊢ eval r' = primrec(n - 1;mu(P);λi,r. eval r' = r + 1 in r' + mu(λk.(P (r' + k)))) + 1 in
  r' + mu(λk.(P (r' + k))) ∈ {k:ℕ| ↑(P k)} 

---

Latex:

---

Latex:
.....upcase..... 
1.  P  :  \mBbbN{}  {}\mrightarrow{}  \mBbbB{}
2.  n  :  \mBbbZ{}
3.  0  <  n
4.  primrec(n  -  1;mu(P);\mlambda{}i,r.  eval  r'  =  r  +  1  in  r'  +  mu(\mlambda{}k.(P  (r'  +  k))))  \mmember{}  \{k:\mBbbN{}|  \muparrow{}(P  k)\}    supposing\000C  \mforall{}n:\mBbbN{}.  \mexists{}k:\mBbbN{}.  ((\muparrow{}(P  k))  \mwedge{}  (n  \mleq{}  k))
\mvdash{}  primrec(n;mu(P);\mlambda{}i,r.  eval  r'  =  r  +  1  in  r'  +  mu(\mlambda{}k.(P  (r'  +  k))))  \mmember{}  \{k:\mBbbN{}|  \muparrow{}(P  k)\}    supposing  \mforall{}n:\mBbbN{}\000C.  \mexists{}k:\mBbbN{}.  ((\muparrow{}(P  k))  \mwedge{}  (n  \mleq{}  k))


By

---

Latex:
xxx(ParallelLast  THEN  (RWO  "primrec-unroll"  0  THENA  Auto)  THEN  OldAutoSplit)xxx

---

Home Index