Step
*
of Lemma
mk_applies_roll
∀[F,G,x:Top]. ∀[m:ℕ]. (mk_applies(F;G;m) x ~ mk_applies(F;λi.if (i =z m) then x else G i fi ;m + 1))
BY
{ (Auto
THEN (RW (AddrC [2] (LemmaC `mk_applies_unroll`)) 0 THENA Auto)
THEN Reduce 0
THEN AutoSplit
THEN (Subst ⌜(m + 1) - 1 ~ m⌝ 0⋅ THENA Auto)
THEN RW (AddrC [2;1] (LemmaC `mk_applies_fun`)) 0
THEN Auto) }
Latex:
Latex:
\mforall{}[F,G,x:Top]. \mforall{}[m:\mBbbN{}].
(mk\_applies(F;G;m) x \msim{} mk\_applies(F;\mlambda{}i.if (i =\msubz{} m) then x else G i fi ;m + 1))
By
Latex:
(Auto
THEN (RW (AddrC [2] (LemmaC `mk\_applies\_unroll`)) 0 THENA Auto)
THEN Reduce 0
THEN AutoSplit
THEN (Subst \mkleeneopen{}(m + 1) - 1 \msim{} m\mkleeneclose{} 0\mcdot{} THENA Auto)
THEN RW (AddrC [2;1] (LemmaC `mk\_applies\_fun`)) 0
THEN Auto)
Home
Index