---

Step * of Lemma equal_upto_mklist_eq

f,g:  . n:.  (equal_upto(n;f;g)  (m:. ((m  n)  (mklist(m;f) ~ mklist(m;g)))))
BY
{ (Unfold `equal_upto` (0) THEN Auto) }

1
1. f :   @i
2. g :   @i
3. n : @i
4. m:n. ((f m) = (g m))@i
5. m : @i
6. m  n@i
 mklist(m;f) = mklist(m;g)


\mforall{}f,g:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  \mforall{}n:\mBbbN{}.    (equal\_upto(n;f;g)  {}\mRightarrow{}  (\mforall{}m:\mBbbN{}.  ((m  \mleq{}  n)  {}\mRightarrow{}  (mklist(m;f)  \msim{}  mklist(m;g)))))


By

(Unfold  `equal\_upto`  (0)  THEN  Auto)



Home Index