2013-03-25から1日間の記事一覧
EXPAND_CASES_CONV http://www.cl.cam.ac.uk/~jrh13/hol-light/HTML/EXPAND_CASES_CONV.html は `!n. n<N ==> P(n)`;; を「n # EXPAND_CASES_CONV`!n.n<5==>0<(n EXP 2+n+1)MOD 5`;; val it : thm = |- (!n. n < 5 ==> 0 < (n EXP 2 + n + 1) MOD 5) <=> 0 < (0 EX</n>…