1> next_tac ([],``x*x>=x``);
2.
3SIMP_TAC bool_ss [arithmeticTheory.GREATER_DEF, arithmeticTheory.GREATER_OR_EQ]
4  ([],``x < x * x ��� (x * x = x)``)
5..
6SRW_TAC [ARITH_ss] [arithmeticTheory.GREATER_OR_EQ]
7  ([],``x�� > x ��� (x�� = x)``)
8
9SRW_TAC [] [arithmeticTheory.GREATER_OR_EQ]
10  ([],``x * x > x ��� (x * x = x)``)
11...
12REWRITE_TAC [arithmeticTheory.GREATER_EQ]
13  ([],``x ��� x * x``)
14...
15Q.SPEC_THEN [QUOTE " (*#loc 1 38348*)x"] FULL_STRUCT_CASES_TAC arithmeticTheory.num_CASES
16  ([],``0 * 0 ��� 0``)
17  ([],``SUC n * SUC n ��� SUC n``)
18val it = (): unit
19
20> val (gl,_) = next 4 ([],``x*x>=x``);
21val gl = [([], ���0 * 0 ��� 0���), ([], ���SUC n * SUC n ��� SUC n���)]: goal list
22 
23> next_tac ([],``0 * 0 ��� 0``);
24.
25ASM_REWRITE_TAC [arithmeticTheory.MULT_CLAUSES]
26  ([],``0 ��� 0``)
27
28ASM_REWRITE_TAC [...]
29  solved
30val it = (): unit
31
32> next_tac ([],``SUC n * SUC n ��� SUC n``);
33.
34RW_TAC bool_ss [arithmeticTheory.MULT_CLAUSES, arithmeticTheory.ADD_CLAUSES]
35  ([],``SUC (n + n * n + n) ��� SUC n``)
36
37ASM_REWRITE_TAC [arithmeticTheory.MULT, arithmeticTheory.ADD_CLAUSES]
38  ([],``SUC (n * SUC n + n) ��� SUC n``)
39
40ASM_REWRITE_TAC [arithmeticTheory.MULT_CLAUSES, arithmeticTheory.GREATER_OR_EQ]
41  ([],``n + n * n + SUC n > SUC n ��� (n + n * n + SUC n = SUC n)``)
42...
43SIMP_TAC bool_ss [arithmeticTheory.GREATER_DEF, arithmeticTheory.GREATER_OR_EQ, arithmeticTheory.ADD_CLAUSES, arithmeticTheory.MULT_CLAUSES]
44  ([],``SUC n < SUC (n + n * n + n) ��� (SUC (n + n * n + n) = SUC n)``)
45
46REWRITE_TAC [arithmeticTheory.GREATER_EQ]
47  ([],``SUC n ��� SUC n * SUC n``)
48val it = (): unit
49
50> next_tac ([],``SUC n * SUC n ��� SUC n``);
51.
52RW_TAC bool_ss [arithmeticTheory.MULT_CLAUSES, arithmeticTheory.ADD_CLAUSES]
53  ([],``SUC (n + n * n + n) ��� SUC n``)
54
55ASM_REWRITE_TAC [arithmeticTheory.MULT, arithmeticTheory.ADD_CLAUSES]
56  ([],``SUC (n * SUC n + n) ��� SUC n``)
57
58ASM_REWRITE_TAC [arithmeticTheory.MULT_CLAUSES, arithmeticTheory.GREATER_OR_EQ]
59  ([],``n + n * n + SUC n > SUC n ��� (n + n * n + SUC n = SUC n)``)
60...
61SIMP_TAC bool_ss [arithmeticTheory.GREATER_DEF, arithmeticTheory.GREATER_OR_EQ, arithmeticTheory.ADD_CLAUSES, arithmeticTheory.MULT_CLAUSES]
62  ([],``SUC n < SUC (n + n * n + n) ��� (SUC (n + n * n + n) = SUC n)``)
63
64REWRITE_TAC [arithmeticTheory.GREATER_EQ]
65  ([],``SUC n ��� SUC n * SUC n``)
66val it = (): unit
67
68> next_tac ([],``SUC n ��� SUC n * SUC n``);
69METIS_TAC [...]
70  solved
71val it = (): unit
72
73