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