読者です 読者をやめる 読者になる 読者になる

HOL(y) Hammer

リモートが動かなくなったと思っていたら,オンラインのインターフェイスが公開されていました.例えば,...

g `!n. &1 + &n <= &2 pow n` ;;

の証明スクリプト.人(私)が書くと

e( INDUCT_TAC THEN REWRITE_TAC [REAL;pow] THEN ASM_ARITH_TAC );;

といった感じですが,http://colo12-c703.uibk.ac.at/hh/

e( MESON_TAC[REAL_OF_NUM_POW;REAL_OF_NUM_LE;REAL_OF_NUM_ADD;NUMERAL;LT_POW2_REFL;LE_SUC_LT;ADD_SYM;ADD1] );;

と答えます.でも実は

# LT_POW2_REFL;;
val it : thm = |- !n. n < 2 EXP n

なので...