9570
|
1 |
(* Title: ZF/Integ/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 |
(*** Simprocs for numeric literals ***)
|
|
10 |
|
|
11 |
(** Combining of literal coefficients in sums of products **)
|
|
12 |
|
|
13 |
Goal "(x $< y) <-> (x$-y $< #0)";
|
|
14 |
by (simp_tac (simpset() addsimps zcompare_rls) 1);
|
|
15 |
qed "zless_iff_zdiff_zless_0";
|
|
16 |
|
|
17 |
Goal "[| x: int; y: int |] ==> (x = y) <-> (x$-y = #0)";
|
|
18 |
by (asm_simp_tac (simpset() addsimps zcompare_rls) 1);
|
|
19 |
qed "eq_iff_zdiff_eq_0";
|
|
20 |
|
|
21 |
Goal "(x $<= y) <-> (x$-y $<= #0)";
|
|
22 |
by (asm_simp_tac (simpset() addsimps zcompare_rls) 1);
|
|
23 |
qed "zle_iff_zdiff_zle_0";
|
|
24 |
|
|
25 |
|
|
26 |
(** For combine_numerals **)
|
|
27 |
|
|
28 |
Goal "i$*u $+ (j$*u $+ k) = (i$+j)$*u $+ k";
|
|
29 |
by (simp_tac (simpset() addsimps [zadd_zmult_distrib]@zadd_ac) 1);
|
|
30 |
qed "left_zadd_zmult_distrib";
|
|
31 |
|
|
32 |
|
|
33 |
(** For cancel_numerals **)
|
|
34 |
|
|
35 |
val rel_iff_rel_0_rls = map (inst "y" "?u$+?v")
|
|
36 |
[zless_iff_zdiff_zless_0, eq_iff_zdiff_eq_0,
|
|
37 |
zle_iff_zdiff_zle_0] @
|
|
38 |
map (inst "y" "n")
|
|
39 |
[zless_iff_zdiff_zless_0, eq_iff_zdiff_eq_0,
|
|
40 |
zle_iff_zdiff_zle_0];
|
|
41 |
|
|
42 |
Goal "(i$*u $+ m = j$*u $+ n) <-> ((i$-j)$*u $+ m = intify(n))";
|
|
43 |
by (simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]) 1);
|
|
44 |
by (simp_tac (simpset() addsimps zcompare_rls) 1);
|
|
45 |
by (simp_tac (simpset() addsimps zadd_ac) 1);
|
|
46 |
qed "eq_add_iff1";
|
|
47 |
|
|
48 |
Goal "(i$*u $+ m = j$*u $+ n) <-> (intify(m) = (j$-i)$*u $+ n)";
|
|
49 |
by (simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]) 1);
|
|
50 |
by (simp_tac (simpset() addsimps zcompare_rls) 1);
|
|
51 |
by (simp_tac (simpset() addsimps zadd_ac) 1);
|
|
52 |
qed "eq_add_iff2";
|
|
53 |
|
|
54 |
Goal "(i$*u $+ m $< j$*u $+ n) <-> ((i$-j)$*u $+ m $< n)";
|
|
55 |
by (asm_simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]@
|
|
56 |
zadd_ac@rel_iff_rel_0_rls) 1);
|
|
57 |
qed "less_add_iff1";
|
|
58 |
|
|
59 |
Goal "(i$*u $+ m $< j$*u $+ n) <-> (m $< (j$-i)$*u $+ n)";
|
|
60 |
by (asm_simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]@
|
|
61 |
zadd_ac@rel_iff_rel_0_rls) 1);
|
|
62 |
qed "less_add_iff2";
|
|
63 |
|
|
64 |
Goal "(i$*u $+ m $<= j$*u $+ n) <-> ((i$-j)$*u $+ m $<= intify(n))";
|
|
65 |
by (simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]) 1);
|
|
66 |
by (simp_tac (simpset() addsimps zcompare_rls) 1);
|
|
67 |
by (simp_tac (simpset() addsimps zadd_ac) 1);
|
|
68 |
qed "le_add_iff1";
|
|
69 |
|
|
70 |
Goal "(i$*u $+ m $<= j$*u $+ n) <-> (intify(m) $<= (j$-i)$*u $+ n)";
|
|
71 |
by (simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]) 1);
|
|
72 |
by (simp_tac (simpset() addsimps zcompare_rls) 1);
|
|
73 |
by (simp_tac (simpset() addsimps zadd_ac) 1);
|
|
74 |
qed "le_add_iff2";
|
|
75 |
|
|
76 |
|
|
77 |
structure Int_Numeral_Simprocs =
|
|
78 |
struct
|
|
79 |
|
|
80 |
(*Utilities*)
|
|
81 |
|
|
82 |
val integ_of_const = Const ("Bin.integ_of", iT --> iT);
|
|
83 |
|
|
84 |
fun mk_numeral n = integ_of_const $ NumeralSyntax.mk_bin n;
|
|
85 |
|
|
86 |
(*Decodes a binary INTEGER*)
|
|
87 |
fun dest_numeral (Const("Bin.integ_of", _) $ w) =
|
|
88 |
(NumeralSyntax.dest_bin w
|
|
89 |
handle Match => raise TERM("Int_Numeral_Simprocs.dest_numeral:1", [w]))
|
|
90 |
| dest_numeral t = raise TERM("Int_Numeral_Simprocs.dest_numeral:2", [t]);
|
|
91 |
|
|
92 |
fun find_first_numeral past (t::terms) =
|
|
93 |
((dest_numeral t, rev past @ terms)
|
|
94 |
handle TERM _ => find_first_numeral (t::past) terms)
|
|
95 |
| find_first_numeral past [] = raise TERM("find_first_numeral", []);
|
|
96 |
|
|
97 |
val zero = mk_numeral 0;
|
|
98 |
val mk_plus = FOLogic.mk_binop "Int.zadd";
|
|
99 |
|
|
100 |
val iT = Ind_Syntax.iT;
|
|
101 |
|
|
102 |
val zminus_const = Const ("Int.zminus", iT --> iT);
|
|
103 |
|
|
104 |
(*Thus mk_sum[t] yields t+#0; longer sums don't have a trailing zero*)
|
|
105 |
fun mk_sum [] = zero
|
|
106 |
| mk_sum [t,u] = mk_plus (t, u)
|
|
107 |
| mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
|
|
108 |
|
|
109 |
(*this version ALWAYS includes a trailing zero*)
|
|
110 |
fun long_mk_sum [] = zero
|
|
111 |
| long_mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
|
|
112 |
|
|
113 |
val dest_plus = FOLogic.dest_bin "Int.zadd" iT;
|
|
114 |
|
|
115 |
(*decompose additions AND subtractions as a sum*)
|
|
116 |
fun dest_summing (pos, Const ("Int.zadd", _) $ t $ u, ts) =
|
|
117 |
dest_summing (pos, t, dest_summing (pos, u, ts))
|
|
118 |
| dest_summing (pos, Const ("Int.zdiff", _) $ t $ u, ts) =
|
|
119 |
dest_summing (pos, t, dest_summing (not pos, u, ts))
|
|
120 |
| dest_summing (pos, t, ts) =
|
|
121 |
if pos then t::ts else zminus_const$t :: ts;
|
|
122 |
|
|
123 |
fun dest_sum t = dest_summing (true, t, []);
|
|
124 |
|
|
125 |
val mk_diff = FOLogic.mk_binop "Int.zdiff";
|
|
126 |
val dest_diff = FOLogic.dest_bin "Int.zdiff" iT;
|
|
127 |
|
|
128 |
val one = mk_numeral 1;
|
|
129 |
val mk_times = FOLogic.mk_binop "Int.zmult";
|
|
130 |
|
|
131 |
fun mk_prod [] = one
|
|
132 |
| mk_prod [t] = t
|
|
133 |
| mk_prod (t :: ts) = if t = one then mk_prod ts
|
|
134 |
else mk_times (t, mk_prod ts);
|
|
135 |
|
|
136 |
val dest_times = FOLogic.dest_bin "Int.zmult" iT;
|
|
137 |
|
|
138 |
fun dest_prod t =
|
|
139 |
let val (t,u) = dest_times t
|
|
140 |
in dest_prod t @ dest_prod u end
|
|
141 |
handle TERM _ => [t];
|
|
142 |
|
|
143 |
(*DON'T do the obvious simplifications; that would create special cases*)
|
|
144 |
fun mk_coeff (k, t) = mk_times (mk_numeral k, t);
|
|
145 |
|
|
146 |
(*Express t as a product of (possibly) a numeral with other sorted terms*)
|
|
147 |
fun dest_coeff sign (Const ("Int.zminus", _) $ t) = dest_coeff (~sign) t
|
|
148 |
| dest_coeff sign t =
|
|
149 |
let val ts = sort Term.term_ord (dest_prod t)
|
|
150 |
val (n, ts') = find_first_numeral [] ts
|
|
151 |
handle TERM _ => (1, ts)
|
|
152 |
in (sign*n, mk_prod ts') end;
|
|
153 |
|
|
154 |
(*Find first coefficient-term THAT MATCHES u*)
|
|
155 |
fun find_first_coeff past u [] = raise TERM("find_first_coeff", [])
|
|
156 |
| find_first_coeff past u (t::terms) =
|
|
157 |
let val (n,u') = dest_coeff 1 t
|
|
158 |
in if u aconv u' then (n, rev past @ terms)
|
|
159 |
else find_first_coeff (t::past) u terms
|
|
160 |
end
|
|
161 |
handle TERM _ => find_first_coeff (t::past) u terms;
|
|
162 |
|
|
163 |
|
|
164 |
(*Simplify #1*n and n*#1 to n*)
|
|
165 |
val add_0s = [zadd_0_intify, zadd_0_right_intify];
|
|
166 |
|
|
167 |
val mult_1s = [zmult_1_intify, zmult_1_right_intify,
|
|
168 |
zmult_minus1, zmult_minus1_right];
|
|
169 |
|
|
170 |
val tc_rules = [integ_of_type, intify_in_int,
|
|
171 |
zadd_type, zdiff_type, zmult_type] @ bin.intrs;
|
|
172 |
val intifys = [intify_ident, zadd_intify1, zadd_intify2,
|
|
173 |
zdiff_intify1, zdiff_intify2, zmult_intify1, zmult_intify2,
|
|
174 |
zless_intify1, zless_intify2, zle_intify1, zle_intify2];
|
|
175 |
|
|
176 |
(*To perform binary arithmetic*)
|
|
177 |
val bin_simps = [add_integ_of_left] @ bin_arith_simps @ bin_rel_simps;
|
|
178 |
|
|
179 |
(*To evaluate binary negations of coefficients*)
|
|
180 |
val zminus_simps = NCons_simps @
|
|
181 |
[integ_of_minus RS sym,
|
|
182 |
bin_minus_1, bin_minus_0, bin_minus_Pls, bin_minus_Min,
|
|
183 |
bin_pred_1, bin_pred_0, bin_pred_Pls, bin_pred_Min];
|
|
184 |
|
|
185 |
(*To let us treat subtraction as addition*)
|
|
186 |
val diff_simps = [zdiff_def, zminus_zadd_distrib, zminus_zminus];
|
|
187 |
|
|
188 |
fun prep_simproc (name, pats, proc) = Simplifier.mk_simproc name pats proc;
|
|
189 |
fun prep_pat s = Thm.read_cterm (Theory.sign_of (the_context ()))
|
|
190 |
(s, TypeInfer.anyT ["logic"]);
|
|
191 |
val prep_pats = map prep_pat;
|
|
192 |
|
|
193 |
structure CancelNumeralsCommon =
|
|
194 |
struct
|
|
195 |
val mk_sum = mk_sum
|
|
196 |
val dest_sum = dest_sum
|
|
197 |
val mk_coeff = mk_coeff
|
|
198 |
val dest_coeff = dest_coeff 1
|
|
199 |
val find_first_coeff = find_first_coeff []
|
|
200 |
val trans_tac = ArithData.gen_trans_tac iff_trans
|
|
201 |
val norm_tac_ss1 = ZF_ss addsimps add_0s@mult_1s@diff_simps@
|
|
202 |
zminus_simps@zadd_ac
|
|
203 |
val norm_tac_ss2 = ZF_ss addsimps [zmult_zminus_right RS sym]@
|
|
204 |
bin_simps@zadd_ac@zmult_ac@tc_rules@intifys
|
|
205 |
val norm_tac = ALLGOALS (asm_simp_tac norm_tac_ss1)
|
|
206 |
THEN ALLGOALS (asm_simp_tac norm_tac_ss2)
|
|
207 |
val numeral_simp_tac = ALLGOALS (simp_tac (ZF_ss addsimps add_0s@bin_simps@tc_rules@intifys))
|
|
208 |
val simplify_meta_eq = ArithData.simplify_meta_eq (add_0s@mult_1s)
|
|
209 |
end;
|
|
210 |
|
|
211 |
|
|
212 |
structure EqCancelNumerals = CancelNumeralsFun
|
|
213 |
(open CancelNumeralsCommon
|
|
214 |
val prove_conv = ArithData.prove_conv "inteq_cancel_numerals"
|
|
215 |
val mk_bal = FOLogic.mk_eq
|
|
216 |
val dest_bal = FOLogic.dest_bin "op =" iT
|
|
217 |
val bal_add1 = eq_add_iff1 RS iff_trans
|
|
218 |
val bal_add2 = eq_add_iff2 RS iff_trans
|
|
219 |
);
|
|
220 |
|
|
221 |
structure LessCancelNumerals = CancelNumeralsFun
|
|
222 |
(open CancelNumeralsCommon
|
|
223 |
val prove_conv = ArithData.prove_conv "intless_cancel_numerals"
|
|
224 |
val mk_bal = FOLogic.mk_binrel "Int.zless"
|
|
225 |
val dest_bal = FOLogic.dest_bin "Int.zless" iT
|
|
226 |
val bal_add1 = less_add_iff1 RS iff_trans
|
|
227 |
val bal_add2 = less_add_iff2 RS iff_trans
|
|
228 |
);
|
|
229 |
|
|
230 |
structure LeCancelNumerals = CancelNumeralsFun
|
|
231 |
(open CancelNumeralsCommon
|
|
232 |
val prove_conv = ArithData.prove_conv "intle_cancel_numerals"
|
|
233 |
val mk_bal = FOLogic.mk_binrel "Int.zle"
|
|
234 |
val dest_bal = FOLogic.dest_bin "Int.zle" iT
|
|
235 |
val bal_add1 = le_add_iff1 RS iff_trans
|
|
236 |
val bal_add2 = le_add_iff2 RS iff_trans
|
|
237 |
);
|
|
238 |
|
|
239 |
val cancel_numerals =
|
|
240 |
map prep_simproc
|
|
241 |
[("inteq_cancel_numerals",
|
|
242 |
prep_pats ["l $+ m = n", "l = m $+ n",
|
|
243 |
"l $- m = n", "l = m $- n",
|
|
244 |
"l $* m = n", "l = m $* n"],
|
|
245 |
EqCancelNumerals.proc),
|
|
246 |
("intless_cancel_numerals",
|
|
247 |
prep_pats ["l $+ m $< n", "l $< m $+ n",
|
|
248 |
"l $- m $< n", "l $< m $- n",
|
|
249 |
"l $* m $< n", "l $< m $* n"],
|
|
250 |
LessCancelNumerals.proc),
|
|
251 |
("intle_cancel_numerals",
|
|
252 |
prep_pats ["l $+ m $<= n", "l $<= m $+ n",
|
|
253 |
"l $- m $<= n", "l $<= m $- n",
|
|
254 |
"l $* m $<= n", "l $<= m $* n"],
|
|
255 |
LeCancelNumerals.proc)];
|
|
256 |
|
|
257 |
|
|
258 |
(*version without the hyps argument*)
|
|
259 |
fun prove_conv_nohyps name tacs sg = ArithData.prove_conv name tacs sg [];
|
|
260 |
|
|
261 |
structure CombineNumeralsData =
|
|
262 |
struct
|
|
263 |
val add = op + : int*int -> int
|
|
264 |
val mk_sum = long_mk_sum (*to work for e.g. #2*x $+ #3*x *)
|
|
265 |
val dest_sum = dest_sum
|
|
266 |
val mk_coeff = mk_coeff
|
|
267 |
val dest_coeff = dest_coeff 1
|
|
268 |
val left_distrib = left_zadd_zmult_distrib RS trans
|
|
269 |
val prove_conv = prove_conv_nohyps "int_combine_numerals"
|
|
270 |
val trans_tac = ArithData.gen_trans_tac trans
|
|
271 |
val norm_tac_ss1 = ZF_ss addsimps add_0s@mult_1s@diff_simps@
|
|
272 |
zminus_simps@zadd_ac
|
|
273 |
val norm_tac_ss2 = ZF_ss addsimps [zmult_zminus_right RS sym]@
|
|
274 |
bin_simps@zadd_ac@zmult_ac@tc_rules@intifys
|
|
275 |
val norm_tac = ALLGOALS (asm_simp_tac norm_tac_ss1)
|
|
276 |
THEN ALLGOALS (asm_simp_tac norm_tac_ss2)
|
|
277 |
val numeral_simp_tac = ALLGOALS (simp_tac (ZF_ss addsimps add_0s@bin_simps))
|
|
278 |
val simplify_meta_eq = ArithData.simplify_meta_eq (add_0s@mult_1s)
|
|
279 |
end;
|
|
280 |
|
|
281 |
structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData);
|
|
282 |
|
|
283 |
val combine_numerals =
|
|
284 |
prep_simproc ("int_combine_numerals",
|
|
285 |
prep_pats ["i $+ j", "i $- j"],
|
|
286 |
CombineNumerals.proc);
|
|
287 |
|
|
288 |
|
|
289 |
|
|
290 |
(** Constant folding for integer multiplication **)
|
|
291 |
|
|
292 |
(*The trick is to regard products as sums, e.g. #3 $* x $* #4 as
|
|
293 |
the "sum" of #3, x, #4; the literals are then multiplied*)
|
|
294 |
structure CombineNumeralsProdData =
|
|
295 |
struct
|
|
296 |
val add = op * : int*int -> int
|
|
297 |
val mk_sum = mk_prod
|
|
298 |
val dest_sum = dest_prod
|
|
299 |
fun mk_coeff (k, t) = mk_numeral k
|
|
300 |
val dest_coeff = dest_coeff 1
|
|
301 |
val left_distrib = zmult_assoc RS sym RS trans
|
|
302 |
val prove_conv = prove_conv_nohyps "int_combine_numerals_prod"
|
|
303 |
val trans_tac = ArithData.gen_trans_tac trans
|
|
304 |
val norm_tac_ss1 = ZF_ss addsimps mult_1s@diff_simps@zminus_simps
|
|
305 |
val norm_tac_ss2 = ZF_ss addsimps [zmult_zminus_right RS sym]@
|
|
306 |
bin_simps@zmult_ac@tc_rules@intifys
|
|
307 |
val norm_tac = ALLGOALS (asm_simp_tac norm_tac_ss1)
|
|
308 |
THEN ALLGOALS (asm_simp_tac norm_tac_ss2)
|
|
309 |
val numeral_simp_tac = ALLGOALS (simp_tac (ZF_ss addsimps bin_simps))
|
|
310 |
val simplify_meta_eq = ArithData.simplify_meta_eq (mult_1s)
|
|
311 |
end;
|
|
312 |
|
|
313 |
|
|
314 |
structure CombineNumeralsProd = CombineNumeralsFun(CombineNumeralsProdData);
|
|
315 |
|
|
316 |
val combine_numerals_prod =
|
|
317 |
prep_simproc ("int_combine_numerals_prod",
|
|
318 |
prep_pats ["i $* j", "i $* j"],
|
|
319 |
CombineNumeralsProd.proc);
|
|
320 |
|
|
321 |
end;
|
|
322 |
|
|
323 |
|
|
324 |
Addsimprocs Int_Numeral_Simprocs.cancel_numerals;
|
|
325 |
Addsimprocs [Int_Numeral_Simprocs.combine_numerals,
|
|
326 |
Int_Numeral_Simprocs.combine_numerals_prod];
|
|
327 |
|
|
328 |
|
|
329 |
(*examples:*)
|
|
330 |
(*
|
|
331 |
print_depth 22;
|
|
332 |
set timing;
|
|
333 |
set trace_simp;
|
|
334 |
fun test s = (Goal s; by (Asm_simp_tac 1));
|
|
335 |
val sg = #sign (rep_thm (topthm()));
|
|
336 |
val t = FOLogic.dest_Trueprop (Logic.strip_assums_concl(getgoal 1));
|
|
337 |
val (t,_) = FOLogic.dest_eq t;
|
|
338 |
|
|
339 |
(*combine_numerals_prod (products of separate literals) *)
|
|
340 |
test "#5 $* x $* #3 = y";
|
|
341 |
|
|
342 |
test "y2 $+ ?x42 = y $+ y2";
|
|
343 |
|
|
344 |
test "oo : int ==> l $+ (l $+ #2) $+ oo = oo";
|
|
345 |
|
|
346 |
test "#9$*x $+ y = x$*#23 $+ z";
|
|
347 |
test "y $+ x = x $+ z";
|
|
348 |
|
|
349 |
test "x : int ==> x $+ y $+ z = x $+ z";
|
|
350 |
test "x : int ==> y $+ (z $+ x) = z $+ x";
|
|
351 |
test "z : int ==> x $+ y $+ z = (z $+ y) $+ (x $+ w)";
|
|
352 |
test "z : int ==> x$*y $+ z = (z $+ y) $+ (y$*x $+ w)";
|
|
353 |
|
|
354 |
test "#-3 $* x $+ y $<= x $* #2 $+ z";
|
|
355 |
test "y $+ x $<= x $+ z";
|
|
356 |
test "x $+ y $+ z $<= x $+ z";
|
|
357 |
|
|
358 |
test "y $+ (z $+ x) $< z $+ x";
|
|
359 |
test "x $+ y $+ z $< (z $+ y) $+ (x $+ w)";
|
|
360 |
test "x$*y $+ z $< (z $+ y) $+ (y$*x $+ w)";
|
|
361 |
|
|
362 |
test "l $+ #2 $+ #2 $+ #2 $+ (l $+ #2) $+ (oo $+ #2) = uu";
|
|
363 |
test "u : int ==> #2 $* u = u";
|
|
364 |
test "(i $+ j $+ #12 $+ k) $- #15 = y";
|
|
365 |
test "(i $+ j $+ #12 $+ k) $- #5 = y";
|
|
366 |
|
|
367 |
test "y $- b $< b";
|
|
368 |
test "y $- (#3 $* b $+ c) $< b $- #2 $* c";
|
|
369 |
|
|
370 |
test "(#2 $* x $- (u $* v) $+ y) $- v $* #3 $* u = w";
|
|
371 |
test "(#2 $* x $* u $* v $+ (u $* v) $* #4 $+ y) $- v $* u $* #4 = w";
|
|
372 |
test "(#2 $* x $* u $* v $+ (u $* v) $* #4 $+ y) $- v $* u = w";
|
|
373 |
test "u $* v $- (x $* u $* v $+ (u $* v) $* #4 $+ y) = w";
|
|
374 |
|
|
375 |
test "(i $+ j $+ #12 $+ k) = u $+ #15 $+ y";
|
|
376 |
test "(i $+ j $* #2 $+ #12 $+ k) = j $+ #5 $+ y";
|
|
377 |
|
|
378 |
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";
|
|
379 |
|
|
380 |
test "a $+ $-(b$+c) $+ b = d";
|
|
381 |
test "a $+ $-(b$+c) $- b = d";
|
|
382 |
|
|
383 |
(*negative numerals*)
|
|
384 |
test "(i $+ j $+ #-2 $+ k) $- (u $+ #5 $+ y) = zz";
|
|
385 |
test "(i $+ j $+ #-3 $+ k) $< u $+ #5 $+ y";
|
|
386 |
test "(i $+ j $+ #3 $+ k) $< u $+ #-6 $+ y";
|
|
387 |
test "(i $+ j $+ #-12 $+ k) $- #15 = y";
|
|
388 |
test "(i $+ j $+ #12 $+ k) $- #-15 = y";
|
|
389 |
test "(i $+ j $+ #-12 $+ k) $- #-15 = y";
|
|
390 |
*)
|
|
391 |
|