---

Step * of Lemma mk_applies_split

∀[F,G:Top]. ∀[n,m:ℕ].  (mk_applies(F;G;m + n) ~ mk_applies(mk_applies(F;G;m);λk.(G (m + k));n))
BY
{ ((UnivCD THENA Auto)
   THEN Subst' m + n ~ n + m 0
   THEN Try (Complete (Auto))
   THEN Unfold `mk_applies` 0
   THEN ((RWO "primrec_add" 0 THENM Reduce 0) THENA Auto)) }

1
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))))

---

Latex:

---

Latex:
\mforall{}[F,G:Top].  \mforall{}[n,m:\mBbbN{}].    (mk\_applies(F;G;m  +  n)  \msim{}  mk\_applies(mk\_applies(F;G;m);\mlambda{}k.(G  (m  +  k));n))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  Subst'  m  +  n  \msim{}  n  +  m  0
  THEN  Try  (Complete  (Auto))
  THEN  Unfold  `mk\_applies`  0
  THEN  ((RWO  "primrec\_add"  0  THENM  Reduce  0)  THENA  Auto))

---

Home Index