---

Step * 1 1 1 2 of Lemma rat-complex-boundary-iter-subdiv

.....upcase..... 
1. k : ℕ
2. j : ℤ
3. 0 < j
4. primrec(j - 1;[];λi,c. (c)') ~ []
⊢ primrec(j;[];λi,c. (c)') ~ []
BY
{ ((RWO "primrec-unroll" 0 THENA Auto) THEN HypSubst' (-1) 0 THEN Reduce 0 THEN (OReduce 0 THENA Auto)) }

1
1. k : ℕ
2. j : ℤ
3. 0 < j
4. primrec(j - 1;[];λi,c. (c)') ~ []
⊢ ([])' ~ []

---

Latex:

---

Latex:
.....upcase..... 
1.  k  :  \mBbbN{}
2.  j  :  \mBbbZ{}
3.  0  <  j
4.  primrec(j  -  1;[];\mlambda{}i,c.  (c)')  \msim{}  []
\mvdash{}  primrec(j;[];\mlambda{}i,c.  (c)')  \msim{}  []


By

---

Latex:
((RWO  "primrec-unroll"  0  THENA  Auto)
  THEN  HypSubst'  (-1)  0
  THEN  Reduce  0
  THEN  (OReduce  0  THENA  Auto))

---

Home Index