g(`!n. 3 < n ==> 2 EXP n < FACT n`);;
e(INDUCT_TAC);;
e(ARITH_TAC);;
e(SIMP_TAC[LT;EXP;FACT]);;
e(STRIP_TAC);;
e(POP_ASSUM (SUBST1_TAC o GSYM) THEN ARITH_TAC);;
e(MATCH_MP_TAC LESS_MULT);;
e(ASM_ARITH_TAC);;
prove
(`!n. 3 < n ==> 2 EXP n < FACT n`,
INDUCT_TAC THENL
[ARITH_TAC;
SIMP_TAC[LT;EXP;FACT] THEN STRIP_TAC THENL
[POP_ASSUM (SUBST1_TAC o GSYM) THEN ARITH_TAC;
MATCH_MP_TAC LESS_MULT THEN ASM_ARITH_TAC]]);;
dmtcp_checkpoint (DMTCP + MTCP) 1.2.5
Copyright (C) 2006-2011 Jason Ansel, Michael Rieker, Kapil Arya, and
Gene Cooperman
This program comes with ABSOLUTELY NO WARRANTY.
This is free software, and you are welcome to redistribute it
under certain conditions; see COPYING file for details.
(Use flag "-q" to hide this message.)
dmtcp_coordinator starting...
Port: 7779
Checkpoint Interval: disabled (checkpoint manually instead)
Exit on last client: 1
Backgrounding...
# g(`!n. 3 < n ==> 2 EXP n < FACT n`);;
val it : goalstack = 1 subgoal (1 total)
`!n. 3 < n ==> 2 EXP n < FACT n`
# e(INDUCT_TAC);;
val it : goalstack = 2 subgoals (2 total)
0 [`3 < n ==> 2 EXP n < FACT n`]
`3 < SUC n ==> 2 EXP SUC n < FACT (SUC n)`
`3 < 0 ==> 2 EXP 0 < FACT 0`
# e(ARITH_TAC);;
val it : goalstack = 1 subgoal (1 total)
0 [`3 < n ==> 2 EXP n < FACT n`]
`3 < SUC n ==> 2 EXP SUC n < FACT (SUC n)`
# e(SIMP_TAC[LT;EXP;FACT]);;
val it : goalstack = 1 subgoal (1 total)
0 [`3 < n ==> 2 EXP n < FACT n`]
`3 = n \/ 3 < n ==> 2 * 2 EXP n < SUC n * FACT n`
# e(STRIP_TAC);;
val it : goalstack = 2 subgoals (2 total)
0 [`3 < n ==> 2 EXP n < FACT n`]
1 [`3 < n`]
`2 * 2 EXP n < SUC n * FACT n`
0 [`3 < n ==> 2 EXP n < FACT n`]
1 [`3 = n`]
`2 * 2 EXP n < SUC n * FACT n`
# e(POP_ASSUM (SUBST1_TAC o GSYM) THEN ARITH_TAC);;
val it : goalstack = 1 subgoal (1 total)
0 [`3 < n ==> 2 EXP n < FACT n`]
1 [`3 < n`]
`2 * 2 EXP n < SUC n * FACT n`
# e(MATCH_MP_TAC LESS_MULT);;
val it : goalstack = 1 subgoal (1 total)
0 [`3 < n ==> 2 EXP n < FACT n`]
1 [`3 < n`]
`2 < SUC n /\ 2 EXP n < FACT n`
# e(ASM_ARITH_TAC);;
val it : goalstack = No subgoals
