---

Step * 1 of Lemma mk_applies_split


1. F : Top
2. G : Top
3. n : ℕ
4. m : ℕ
⊢ primrec(n;primrec(m;F;λi,r. (r (G i)));λi,t. (t (G (i + m)))) ~ primrec(n;primrec(m;F;λi,r. (r (G i)));λi,r. (r (G (m \000C+ i))))
BY
{ (NatInd (-2)
   THEN Reduce 0
   THEN Try (Trivial)
   THEN (RW (SubC (LemmaC `primrec-unroll`)) 0 THENA Auto)
   THEN AutoSplit) }

---

Latex:

---

Latex:

1.  F  :  Top
2.  G  :  Top
3.  n  :  \mBbbN{}
4.  m  :  \mBbbN{}
\mvdash{}  primrec(n;primrec(m;F;\mlambda{}i,r.  (r  (G  i)));\mlambda{}i,t.  (t  (G  (i  +  m)))) 
\msim{}  primrec(n;primrec(m;F;\mlambda{}i,r.  (r  (G  i)));\mlambda{}i,r.  (r  (G  (m  +  i))))


By

---

Latex:
(NatInd  (-2)
  THEN  Reduce  0
  THEN  Try  (Trivial)
  THEN  (RW  (SubC  (LemmaC  `primrec-unroll`))  0  THENA  Auto)
  THEN  AutoSplit)

---

Home Index