---

Step * 1 of Lemma mk_applies_fun2


1. F : Top
2. K : Top
3. v : Top
4. p : ℕ
5. n : ℕ
6. m : ℕ
7. m < n + 1
⊢ mk_applies(F;λk.if (p + k =z p + n) then v else K (p + k) fi ;m) ~ mk_applies(F;λi.(K (p + i));m)
BY
{ (NatInd (-2)
   THEN (UnivCD THENA Auto)
   THEN Try (Complete (Auto))
   THEN Try (Complete ((RepUR ``mk_applies`` 0 THEN Auto)))
   THEN (D (-2) THENA Auto)
   THEN RepUR ``mk_applies`` 0
   THEN (RWO "primrec-unroll" 0 THENA Auto)
   THEN AutoSplit
   THEN RepUR ``mk_applies`` (-1)
   THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  F  :  Top
2.  K  :  Top
3.  v  :  Top
4.  p  :  \mBbbN{}
5.  n  :  \mBbbN{}
6.  m  :  \mBbbN{}
7.  m  <  n  +  1
\mvdash{}  mk\_applies(F;\mlambda{}k.if  (p  +  k  =\msubz{}  p  +  n)  then  v  else  K  (p  +  k)  fi  ;m)  \msim{}  mk\_applies(F;\mlambda{}i.(K  (p  +  i));m)


By

---

Latex:
(NatInd  (-2)
  THEN  (UnivCD  THENA  Auto)
  THEN  Try  (Complete  (Auto))
  THEN  Try  (Complete  ((RepUR  ``mk\_applies``  0  THEN  Auto)))
  THEN  (D  (-2)  THENA  Auto)
  THEN  RepUR  ``mk\_applies``  0
  THEN  (RWO  "primrec-unroll"  0  THENA  Auto)
  THEN  AutoSplit
  THEN  RepUR  ``mk\_applies``  (-1)
  THEN  Auto)\mcdot{}

---

Home Index