HOL Light vs PVS (3)
g `!n. 8 <= n ==> (?x y. n = 3 * x + 5 * y)` ;; e( INDUCT_TAC );; e( ARITH_TAC );; e( REWRITE_TAC [LE] THEN REPEAT STRIP_TAC );; e( EXISTS_TAC `1` THEN EXISTS_TAC `1` THEN ASM_ARITH_TAC );; e( FIRST_X_ASSUM (fun t -> FIRST_ASSUM (MP_TAC o (MATCH_MP t))) THEN STRIP_TAC );; e( ASM_CASES_TAC `y = 0` );; e( EXISTS_TAC `x - 3` THEN EXISTS_TAC `2` THEN ASM_ARITH_TAC );; e( EXISTS_TAC `x + 2` THEN EXISTS_TAC `y - 1` THEN ASM_ARITH_TAC );;
f01:lemma forall(n:nat): 8 <= n => exists(x,y:nat): n = 3 * x + 5 * y %|- f01 : PROOF %|- (spread (induct "n" 1) %|- ((ground) %|- (then (skeep*) %|- (spread (split) %|- ((then (skeep*) %|- (spread (case "y = 0") %|- ((spread (inst + "x - 3" "2") ((ground) (ground))) %|- (spread (inst + "x + 2" "y - 1") ((ground) (ground)))))) %|- (then (inst 2 "1" "1") (ground))))))) %|- QED
カットオフされない為の場合分け(y=0 のとき3<=x,および,not(y=0) のとき1<=y)について,HOL Light は黙って判ってくれますが,PVSは
f01.2.1.1.2 (TCC): [-1] y = 0 [-2] j = 3 * x + 5 * y [-3] 8 <= j + 1 |------- {1} x - 3 >= 0
f01.2.1.2.2 (TCC): [-1] j = 3 * x + 5 * y [-2] 8 <= j + 1 |------- {1} y - 1 >= 0 [2] y = 0
のように確認してきます.