author  wenzelm 
Mon, 11 Feb 2008 21:32:12 +0100  
changeset 26059  b67a225b50fd 
parent 26056  6a0801279f4c 
child 26190  cf51a23c0cd0 
permissions  rwrr 
23146  1 
(* Title: ZF/int_arith.ML 
2 
ID: $Id$ 

3 
Author: Larry Paulson 

4 
Copyright 2000 University of Cambridge 

5 

6 
Simprocs for linear arithmetic. 

7 
*) 

8 

9 

10 
(** To simplify inequalities involving integer negation and literals, 

11 
such as x = #3 

12 
**) 

13 

24893  14 
Addsimps [inst "y" "integ_of(?w)" @{thm zminus_equation}, 
15 
inst "x" "integ_of(?w)" @{thm equation_zminus}]; 

23146  16 

24893  17 
AddIffs [inst "y" "integ_of(?w)" @{thm zminus_zless}, 
18 
inst "x" "integ_of(?w)" @{thm zless_zminus}]; 

23146  19 

24893  20 
AddIffs [inst "y" "integ_of(?w)" @{thm zminus_zle}, 
21 
inst "x" "integ_of(?w)" @{thm zle_zminus}]; 

23146  22 

24893  23 
Addsimps [inst "s" "integ_of(?w)" @{thm Let_def}]; 
23146  24 

25 
(*** Simprocs for numeric literals ***) 

26 

27 
(** Combining of literal coefficients in sums of products **) 

28 

29 
Goal "(x $< y) <> (x$y $< #0)"; 

24893  30 
by (simp_tac (simpset() addsimps @{thms zcompare_rls}) 1); 
23146  31 
qed "zless_iff_zdiff_zless_0"; 
32 

33 
Goal "[ x: int; y: int ] ==> (x = y) <> (x$y = #0)"; 

24893  34 
by (asm_simp_tac (simpset() addsimps @{thms zcompare_rls}) 1); 
23146  35 
qed "eq_iff_zdiff_eq_0"; 
36 

37 
Goal "(x $<= y) <> (x$y $<= #0)"; 

24893  38 
by (asm_simp_tac (simpset() addsimps @{thms zcompare_rls}) 1); 
23146  39 
qed "zle_iff_zdiff_zle_0"; 
40 

41 

42 
(** For combine_numerals **) 

43 

44 
Goal "i$*u $+ (j$*u $+ k) = (i$+j)$*u $+ k"; 

24893  45 
by (simp_tac (simpset() addsimps [@{thm zadd_zmult_distrib}]@ @{thms zadd_ac}) 1); 
23146  46 
qed "left_zadd_zmult_distrib"; 
47 

48 

49 
(** For cancel_numerals **) 

50 

51 
val rel_iff_rel_0_rls = map (inst "y" "?u$+?v") 

52 
[zless_iff_zdiff_zless_0, eq_iff_zdiff_eq_0, 

53 
zle_iff_zdiff_zle_0] @ 

54 
map (inst "y" "n") 

55 
[zless_iff_zdiff_zless_0, eq_iff_zdiff_eq_0, 

56 
zle_iff_zdiff_zle_0]; 

57 

58 
Goal "(i$*u $+ m = j$*u $+ n) <> ((i$j)$*u $+ m = intify(n))"; 

24893  59 
by (simp_tac (simpset() addsimps [@{thm zdiff_def}, @{thm zadd_zmult_distrib}]) 1); 
60 
by (simp_tac (simpset() addsimps @{thms zcompare_rls}) 1); 

61 
by (simp_tac (simpset() addsimps @{thms zadd_ac}) 1); 

23146  62 
qed "eq_add_iff1"; 
63 

64 
Goal "(i$*u $+ m = j$*u $+ n) <> (intify(m) = (j$i)$*u $+ n)"; 

24893  65 
by (simp_tac (simpset() addsimps [@{thm zdiff_def}, @{thm zadd_zmult_distrib}]) 1); 
66 
by (simp_tac (simpset() addsimps @{thms zcompare_rls}) 1); 

67 
by (simp_tac (simpset() addsimps @{thms zadd_ac}) 1); 

23146  68 
qed "eq_add_iff2"; 
69 

70 
Goal "(i$*u $+ m $< j$*u $+ n) <> ((i$j)$*u $+ m $< n)"; 

24893  71 
by (asm_simp_tac (simpset() addsimps [@{thm zdiff_def}, @{thm zadd_zmult_distrib}]@ 
72 
@{thms zadd_ac} @ rel_iff_rel_0_rls) 1); 

23146  73 
qed "less_add_iff1"; 
74 

75 
Goal "(i$*u $+ m $< j$*u $+ n) <> (m $< (j$i)$*u $+ n)"; 

24893  76 
by (asm_simp_tac (simpset() addsimps [@{thm zdiff_def}, @{thm zadd_zmult_distrib}]@ 
77 
@{thms zadd_ac} @ rel_iff_rel_0_rls) 1); 

23146  78 
qed "less_add_iff2"; 
79 

80 
Goal "(i$*u $+ m $<= j$*u $+ n) <> ((i$j)$*u $+ m $<= n)"; 

24893  81 
by (simp_tac (simpset() addsimps [@{thm zdiff_def}, @{thm zadd_zmult_distrib}]) 1); 
82 
by (simp_tac (simpset() addsimps @{thms zcompare_rls}) 1); 

83 
by (simp_tac (simpset() addsimps @{thms zadd_ac}) 1); 

23146  84 
qed "le_add_iff1"; 
85 

86 
Goal "(i$*u $+ m $<= j$*u $+ n) <> (m $<= (j$i)$*u $+ n)"; 

24893  87 
by (simp_tac (simpset() addsimps [@{thm zdiff_def}, @{thm zadd_zmult_distrib}]) 1); 
88 
by (simp_tac (simpset() addsimps @{thms zcompare_rls}) 1); 

89 
by (simp_tac (simpset() addsimps @{thms zadd_ac}) 1); 

23146  90 
qed "le_add_iff2"; 
91 

92 

93 
structure Int_Numeral_Simprocs = 

94 
struct 

95 

96 
(*Utilities*) 

97 

26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
24893
diff
changeset

98 
val integ_of_const = Const (@{const_name "Bin.integ_of"}, iT > iT); 
23146  99 

100 
fun mk_numeral n = integ_of_const $ NumeralSyntax.mk_bin n; 

101 

102 
(*Decodes a binary INTEGER*) 

26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
24893
diff
changeset

103 
fun dest_numeral (Const(@{const_name "Bin.integ_of"}, _) $ w) = 
23146  104 
(NumeralSyntax.dest_bin w 
105 
handle Match => raise TERM("Int_Numeral_Simprocs.dest_numeral:1", [w])) 

106 
 dest_numeral t = raise TERM("Int_Numeral_Simprocs.dest_numeral:2", [t]); 

107 

108 
fun find_first_numeral past (t::terms) = 

109 
((dest_numeral t, rev past @ terms) 

110 
handle TERM _ => find_first_numeral (t::past) terms) 

111 
 find_first_numeral past [] = raise TERM("find_first_numeral", []); 

112 

113 
val zero = mk_numeral 0; 

26059  114 
val mk_plus = FOLogic.mk_binop @{const_name "zadd"}; 
23146  115 

116 
val iT = Ind_Syntax.iT; 

117 

26059  118 
val zminus_const = Const (@{const_name "zminus"}, iT > iT); 
23146  119 

120 
(*Thus mk_sum[t] yields t+#0; longer sums don't have a trailing zero*) 

121 
fun mk_sum [] = zero 

122 
 mk_sum [t,u] = mk_plus (t, u) 

123 
 mk_sum (t :: ts) = mk_plus (t, mk_sum ts); 

124 

125 
(*this version ALWAYS includes a trailing zero*) 

126 
fun long_mk_sum [] = zero 

127 
 long_mk_sum (t :: ts) = mk_plus (t, mk_sum ts); 

128 

26059  129 
val dest_plus = FOLogic.dest_bin @{const_name "zadd"} iT; 
23146  130 

131 
(*decompose additions AND subtractions as a sum*) 

26059  132 
fun dest_summing (pos, Const (@{const_name "zadd"}, _) $ t $ u, ts) = 
23146  133 
dest_summing (pos, t, dest_summing (pos, u, ts)) 
26059  134 
 dest_summing (pos, Const (@{const_name "zdiff"}, _) $ t $ u, ts) = 
23146  135 
dest_summing (pos, t, dest_summing (not pos, u, ts)) 
136 
 dest_summing (pos, t, ts) = 

137 
if pos then t::ts else zminus_const$t :: ts; 

138 

139 
fun dest_sum t = dest_summing (true, t, []); 

140 

26059  141 
val mk_diff = FOLogic.mk_binop @{const_name "zdiff"}; 
142 
val dest_diff = FOLogic.dest_bin @{const_name "zdiff"} iT; 

23146  143 

144 
val one = mk_numeral 1; 

26059  145 
val mk_times = FOLogic.mk_binop @{const_name "zmult"}; 
23146  146 

147 
fun mk_prod [] = one 

148 
 mk_prod [t] = t 

149 
 mk_prod (t :: ts) = if t = one then mk_prod ts 

150 
else mk_times (t, mk_prod ts); 

151 

26059  152 
val dest_times = FOLogic.dest_bin @{const_name "zmult"} iT; 
23146  153 

154 
fun dest_prod t = 

155 
let val (t,u) = dest_times t 

156 
in dest_prod t @ dest_prod u end 

157 
handle TERM _ => [t]; 

158 

159 
(*DON'T do the obvious simplifications; that would create special cases*) 

160 
fun mk_coeff (k, t) = mk_times (mk_numeral k, t); 

161 

162 
(*Express t as a product of (possibly) a numeral with other sorted terms*) 

26059  163 
fun dest_coeff sign (Const (@{const_name "zminus"}, _) $ t) = dest_coeff (~sign) t 
23146  164 
 dest_coeff sign t = 
165 
let val ts = sort Term.term_ord (dest_prod t) 

166 
val (n, ts') = find_first_numeral [] ts 

167 
handle TERM _ => (1, ts) 

168 
in (sign*n, mk_prod ts') end; 

169 

170 
(*Find first coefficientterm THAT MATCHES u*) 

171 
fun find_first_coeff past u [] = raise TERM("find_first_coeff", []) 

172 
 find_first_coeff past u (t::terms) = 

173 
let val (n,u') = dest_coeff 1 t 

174 
in if u aconv u' then (n, rev past @ terms) 

175 
else find_first_coeff (t::past) u terms 

176 
end 

177 
handle TERM _ => find_first_coeff (t::past) u terms; 

178 

179 

180 
(*Simplify #1*n and n*#1 to n*) 

24893  181 
val add_0s = [@{thm zadd_0_intify}, @{thm zadd_0_right_intify}]; 
23146  182 

24893  183 
val mult_1s = [@{thm zmult_1_intify}, @{thm zmult_1_right_intify}, 
184 
@{thm zmult_minus1}, @{thm zmult_minus1_right}]; 

23146  185 

24893  186 
val tc_rules = [@{thm integ_of_type}, @{thm intify_in_int}, 
187 
@{thm int_of_type}, @{thm zadd_type}, @{thm zdiff_type}, @{thm zmult_type}] @ 

188 
@{thms bin.intros}; 

189 
val intifys = [@{thm intify_ident}, @{thm zadd_intify1}, @{thm zadd_intify2}, 

190 
@{thm zdiff_intify1}, @{thm zdiff_intify2}, @{thm zmult_intify1}, @{thm zmult_intify2}, 

191 
@{thm zless_intify1}, @{thm zless_intify2}, @{thm zle_intify1}, @{thm zle_intify2}]; 

23146  192 

193 
(*To perform binary arithmetic*) 

24893  194 
val bin_simps = [@{thm add_integ_of_left}] @ @{thms bin_arith_simps} @ @{thms bin_rel_simps}; 
23146  195 

196 
(*To evaluate binary negations of coefficients*) 

24893  197 
val zminus_simps = @{thms NCons_simps} @ 
198 
[@{thm integ_of_minus} RS sym, 

199 
@{thm bin_minus_1}, @{thm bin_minus_0}, @{thm bin_minus_Pls}, @{thm bin_minus_Min}, 

200 
@{thm bin_pred_1}, @{thm bin_pred_0}, @{thm bin_pred_Pls}, @{thm bin_pred_Min}]; 

23146  201 

202 
(*To let us treat subtraction as addition*) 

24893  203 
val diff_simps = [@{thm zdiff_def}, @{thm zminus_zadd_distrib}, @{thm zminus_zminus}]; 
23146  204 

205 
(*push the unary minus down:  x * y = x *  y *) 

206 
val int_minus_mult_eq_1_to_2 = 

24893  207 
[@{thm zmult_zminus}, @{thm zmult_zminus_right} RS sym] MRS trans > standard; 
23146  208 

209 
(*to extract again any uncancelled minuses*) 

210 
val int_minus_from_mult_simps = 

24893  211 
[@{thm zminus_zminus}, @{thm zmult_zminus}, @{thm zmult_zminus_right}]; 
23146  212 

213 
(*combine unary minus with numeric literals, however nested within a product*) 

214 
val int_mult_minus_simps = 

24893  215 
[@{thm zmult_assoc}, @{thm zmult_zminus} RS sym, int_minus_mult_eq_1_to_2]; 
23146  216 

217 
fun prep_simproc (name, pats, proc) = 

218 
Simplifier.simproc (the_context ()) name pats proc; 

219 

220 
structure CancelNumeralsCommon = 

221 
struct 

222 
val mk_sum = (fn T:typ => mk_sum) 

223 
val dest_sum = dest_sum 

224 
val mk_coeff = mk_coeff 

225 
val dest_coeff = dest_coeff 1 

226 
val find_first_coeff = find_first_coeff [] 

227 
fun trans_tac _ = ArithData.gen_trans_tac iff_trans 

228 

24893  229 
val norm_ss1 = ZF_ss addsimps add_0s @ mult_1s @ diff_simps @ zminus_simps @ @{thms zadd_ac} 
23146  230 
val norm_ss2 = ZF_ss addsimps bin_simps @ int_mult_minus_simps @ intifys 
24893  231 
val norm_ss3 = ZF_ss addsimps int_minus_from_mult_simps @ @{thms zadd_ac} @ @{thms zmult_ac} @ tc_rules @ intifys 
23146  232 
fun norm_tac ss = 
233 
ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_ss1)) 

234 
THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_ss2)) 

235 
THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_ss3)) 

236 

237 
val numeral_simp_ss = ZF_ss addsimps add_0s @ bin_simps @ tc_rules @ intifys 

238 
fun numeral_simp_tac ss = 

239 
ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss)) 

240 
THEN ALLGOALS (SIMPSET' (fn simpset => asm_simp_tac (Simplifier.inherit_context ss simpset))) 

241 
val simplify_meta_eq = ArithData.simplify_meta_eq (add_0s @ mult_1s) 

242 
end; 

243 

244 

245 
structure EqCancelNumerals = CancelNumeralsFun 

246 
(open CancelNumeralsCommon 

247 
val prove_conv = ArithData.prove_conv "inteq_cancel_numerals" 

248 
val mk_bal = FOLogic.mk_eq 

249 
val dest_bal = FOLogic.dest_eq 

250 
val bal_add1 = eq_add_iff1 RS iff_trans 

251 
val bal_add2 = eq_add_iff2 RS iff_trans 

252 
); 

253 

254 
structure LessCancelNumerals = CancelNumeralsFun 

255 
(open CancelNumeralsCommon 

256 
val prove_conv = ArithData.prove_conv "intless_cancel_numerals" 

26059  257 
val mk_bal = FOLogic.mk_binrel @{const_name "zless"} 
258 
val dest_bal = FOLogic.dest_bin @{const_name "zless"} iT 

23146  259 
val bal_add1 = less_add_iff1 RS iff_trans 
260 
val bal_add2 = less_add_iff2 RS iff_trans 

261 
); 

262 

263 
structure LeCancelNumerals = CancelNumeralsFun 

264 
(open CancelNumeralsCommon 

265 
val prove_conv = ArithData.prove_conv "intle_cancel_numerals" 

26059  266 
val mk_bal = FOLogic.mk_binrel @{const_name "zle"} 
267 
val dest_bal = FOLogic.dest_bin @{const_name "zle"} iT 

23146  268 
val bal_add1 = le_add_iff1 RS iff_trans 
269 
val bal_add2 = le_add_iff2 RS iff_trans 

270 
); 

271 

272 
val cancel_numerals = 

273 
map prep_simproc 

274 
[("inteq_cancel_numerals", 

275 
["l $+ m = n", "l = m $+ n", 

276 
"l $ m = n", "l = m $ n", 

277 
"l $* m = n", "l = m $* n"], 

278 
K EqCancelNumerals.proc), 

279 
("intless_cancel_numerals", 

280 
["l $+ m $< n", "l $< m $+ n", 

281 
"l $ m $< n", "l $< m $ n", 

282 
"l $* m $< n", "l $< m $* n"], 

283 
K LessCancelNumerals.proc), 

284 
("intle_cancel_numerals", 

285 
["l $+ m $<= n", "l $<= m $+ n", 

286 
"l $ m $<= n", "l $<= m $ n", 

287 
"l $* m $<= n", "l $<= m $* n"], 

288 
K LeCancelNumerals.proc)]; 

289 

290 

291 
(*version without the hyps argument*) 

292 
fun prove_conv_nohyps name tacs sg = ArithData.prove_conv name tacs sg []; 

293 

294 
structure CombineNumeralsData = 

295 
struct 

24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
23146
diff
changeset

296 
type coeff = int 
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
23146
diff
changeset

297 
val iszero = (fn x => x = 0) 
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
23146
diff
changeset

298 
val add = op + 
23146  299 
val mk_sum = (fn T:typ => long_mk_sum) (*to work for #2*x $+ #3*x *) 
300 
val dest_sum = dest_sum 

301 
val mk_coeff = mk_coeff 

302 
val dest_coeff = dest_coeff 1 

303 
val left_distrib = left_zadd_zmult_distrib RS trans 

304 
val prove_conv = prove_conv_nohyps "int_combine_numerals" 

305 
fun trans_tac _ = ArithData.gen_trans_tac trans 

306 

24893  307 
val norm_ss1 = ZF_ss addsimps add_0s @ mult_1s @ diff_simps @ zminus_simps @ @{thms zadd_ac} @ intifys 
23146  308 
val norm_ss2 = ZF_ss addsimps bin_simps @ int_mult_minus_simps @ intifys 
24893  309 
val norm_ss3 = ZF_ss addsimps int_minus_from_mult_simps @ @{thms zadd_ac} @ @{thms zmult_ac} @ tc_rules @ intifys 
23146  310 
fun norm_tac ss = 
311 
ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_ss1)) 

312 
THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_ss2)) 

313 
THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_ss3)) 

314 

315 
val numeral_simp_ss = ZF_ss addsimps add_0s @ bin_simps @ tc_rules @ intifys 

316 
fun numeral_simp_tac ss = 

317 
ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss)) 

318 
val simplify_meta_eq = ArithData.simplify_meta_eq (add_0s @ mult_1s) 

319 
end; 

320 

321 
structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData); 

322 

323 
val combine_numerals = 

324 
prep_simproc ("int_combine_numerals", ["i $+ j", "i $ j"], K CombineNumerals.proc); 

325 

326 

327 

328 
(** Constant folding for integer multiplication **) 

329 

330 
(*The trick is to regard products as sums, e.g. #3 $* x $* #4 as 

331 
the "sum" of #3, x, #4; the literals are then multiplied*) 

332 

333 

334 
structure CombineNumeralsProdData = 

335 
struct 

24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
23146
diff
changeset

336 
type coeff = int 
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
23146
diff
changeset

337 
val iszero = (fn x => x = 0) 
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
23146
diff
changeset

338 
val add = op * 
23146  339 
val mk_sum = (fn T:typ => mk_prod) 
340 
val dest_sum = dest_prod 

341 
fun mk_coeff(k,t) = if t=one then mk_numeral k 

342 
else raise TERM("mk_coeff", []) 

343 
fun dest_coeff t = (dest_numeral t, one) (*We ONLY want pure numerals.*) 

24893  344 
val left_distrib = @{thm zmult_assoc} RS sym RS trans 
23146  345 
val prove_conv = prove_conv_nohyps "int_combine_numerals_prod" 
346 
fun trans_tac _ = ArithData.gen_trans_tac trans 

347 

348 

349 

350 
val norm_ss1 = ZF_ss addsimps mult_1s @ diff_simps @ zminus_simps 

24893  351 
val norm_ss2 = ZF_ss addsimps [@{thm zmult_zminus_right} RS sym] @ 
352 
bin_simps @ @{thms zmult_ac} @ tc_rules @ intifys 

23146  353 
fun norm_tac ss = 
354 
ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_ss1)) 

355 
THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_ss2)) 

356 

357 
val numeral_simp_ss = ZF_ss addsimps bin_simps @ tc_rules @ intifys 

358 
fun numeral_simp_tac ss = 

359 
ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss)) 

360 
val simplify_meta_eq = ArithData.simplify_meta_eq (mult_1s); 

361 
end; 

362 

363 

364 
structure CombineNumeralsProd = CombineNumeralsFun(CombineNumeralsProdData); 

365 

366 
val combine_numerals_prod = 

367 
prep_simproc ("int_combine_numerals_prod", ["i $* j"], K CombineNumeralsProd.proc); 

368 

369 
end; 

370 

371 

372 
Addsimprocs Int_Numeral_Simprocs.cancel_numerals; 

373 
Addsimprocs [Int_Numeral_Simprocs.combine_numerals, 

374 
Int_Numeral_Simprocs.combine_numerals_prod]; 

375 

376 

377 
(*examples:*) 

378 
(* 

379 
print_depth 22; 

380 
set timing; 

381 
set trace_simp; 

382 
fun test s = (Goal s; by (Asm_simp_tac 1)); 

383 
val sg = #sign (rep_thm (topthm())); 

384 
val t = FOLogic.dest_Trueprop (Logic.strip_assums_concl(getgoal 1)); 

385 
val (t,_) = FOLogic.dest_eq t; 

386 

387 
(*combine_numerals_prod (products of separate literals) *) 

388 
test "#5 $* x $* #3 = y"; 

389 

390 
test "y2 $+ ?x42 = y $+ y2"; 

391 

392 
test "oo : int ==> l $+ (l $+ #2) $+ oo = oo"; 

393 

394 
test "#9$*x $+ y = x$*#23 $+ z"; 

395 
test "y $+ x = x $+ z"; 

396 

397 
test "x : int ==> x $+ y $+ z = x $+ z"; 

398 
test "x : int ==> y $+ (z $+ x) = z $+ x"; 

399 
test "z : int ==> x $+ y $+ z = (z $+ y) $+ (x $+ w)"; 

400 
test "z : int ==> x$*y $+ z = (z $+ y) $+ (y$*x $+ w)"; 

401 

402 
test "#3 $* x $+ y $<= x $* #2 $+ z"; 

403 
test "y $+ x $<= x $+ z"; 

404 
test "x $+ y $+ z $<= x $+ z"; 

405 

406 
test "y $+ (z $+ x) $< z $+ x"; 

407 
test "x $+ y $+ z $< (z $+ y) $+ (x $+ w)"; 

408 
test "x$*y $+ z $< (z $+ y) $+ (y$*x $+ w)"; 

409 

410 
test "l $+ #2 $+ #2 $+ #2 $+ (l $+ #2) $+ (oo $+ #2) = uu"; 

411 
test "u : int ==> #2 $* u = u"; 

412 
test "(i $+ j $+ #12 $+ k) $ #15 = y"; 

413 
test "(i $+ j $+ #12 $+ k) $ #5 = y"; 

414 

415 
test "y $ b $< b"; 

416 
test "y $ (#3 $* b $+ c) $< b $ #2 $* c"; 

417 

418 
test "(#2 $* x $ (u $* v) $+ y) $ v $* #3 $* u = w"; 

419 
test "(#2 $* x $* u $* v $+ (u $* v) $* #4 $+ y) $ v $* u $* #4 = w"; 

420 
test "(#2 $* x $* u $* v $+ (u $* v) $* #4 $+ y) $ v $* u = w"; 

421 
test "u $* v $ (x $* u $* v $+ (u $* v) $* #4 $+ y) = w"; 

422 

423 
test "(i $+ j $+ #12 $+ k) = u $+ #15 $+ y"; 

424 
test "(i $+ j $* #2 $+ #12 $+ k) = j $+ #5 $+ y"; 

425 

426 
test "#2 $* y $+ #3 $* z $+ #6 $* w $+ #2 $* y $+ #3 $* z $+ #2 $* u = #2 $* y' $+ #3 $* z' $+ #6 $* w' $+ #2 $* y' $+ #3 $* z' $+ u $+ vv"; 

427 

428 
test "a $+ $(b$+c) $+ b = d"; 

429 
test "a $+ $(b$+c) $ b = d"; 

430 

431 
(*negative numerals*) 

432 
test "(i $+ j $+ #2 $+ k) $ (u $+ #5 $+ y) = zz"; 

433 
test "(i $+ j $+ #3 $+ k) $< u $+ #5 $+ y"; 

434 
test "(i $+ j $+ #3 $+ k) $< u $+ #6 $+ y"; 

435 
test "(i $+ j $+ #12 $+ k) $ #15 = y"; 

436 
test "(i $+ j $+ #12 $+ k) $ #15 = y"; 

437 
test "(i $+ j $+ #12 $+ k) $ #15 = y"; 

438 

439 
(*Multiplying separated numerals*) 

440 
Goal "#6 $* ($# x $* #2) = uu"; 

441 
Goal "#4 $* ($# x $* $# x) $* (#2 $* $# x) = uu"; 

442 
*) 

443 