---

Step * of Lemma mk_applies_fun

No Annotations
∀[F,K,v:Top]. ∀[n:ℕ]. ∀[m:ℕn + 1].  (mk_applies(F;λk.if (k =z n) then v else K k fi ;m) ~ mk_applies(F;K;m))
BY
{ ((UnivCD THENA Auto)
   THEN SqEqualTopToBase
   THEN (Assert m ≤ n BY
               Auto)
   THEN MoveToConcl (-1)
   THEN (GenConcl ⌜m = M ∈ ℕ⌝⋅ THENA Auto)
   THEN ThinVar `m'
   THEN RenameVar `m' (-1)
   THEN NatInd (-1)
   THEN (D 0 THENA Auto)
   THEN RepUR ``mk_applies`` 0
   THEN Try (Complete (Auto))
   THEN ((RWO "primrec-unroll" 0 THENA Auto)
         THEN AutoSplit
         THEN Fold `mk_applies` 0
         THEN RWO "-2<" 0
         THEN RepUR ``mk_applies`` 0
         THEN Auto)⋅) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[F,K,v:Top].  \mforall{}[n:\mBbbN{}].  \mforall{}[m:\mBbbN{}n  +  1].
    (mk\_applies(F;\mlambda{}k.if  (k  =\msubz{}  n)  then  v  else  K  k  fi  ;m)  \msim{}  mk\_applies(F;K;m))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  SqEqualTopToBase
  THEN  (Assert  m  \mleq{}  n  BY
                          Auto)
  THEN  MoveToConcl  (-1)
  THEN  (GenConcl  \mkleeneopen{}m  =  M\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  ThinVar  `m'
  THEN  RenameVar  `m'  (-1)
  THEN  NatInd  (-1)
  THEN  (D  0  THENA  Auto)
  THEN  RepUR  ``mk\_applies``  0
  THEN  Try  (Complete  (Auto))
  THEN  ((RWO  "primrec-unroll"  0  THENA  Auto)
              THEN  AutoSplit
              THEN  Fold  `mk\_applies`  0
              THEN  RWO  "-2<"  0
              THEN  RepUR  ``mk\_applies``  0
              THEN  Auto)\mcdot{})

---

Home Index