2013-07-27から1日間の記事一覧
g `!(x:int). x <= &101 ==> (?n k. 91 <= k /\ k <= 101 /\ x = &k - &(11 * n))` ;; e( REPEAT STRIP_TAC );; e( SUBGOAL_THEN `?m:num. &101 - x:int = &m` MP_TAC );; e( ASM_CASES_TAC `&101 - x:int = &0` );; e( EXISTS_TAC `0` THEN ASM_SIMP_TAC []…