src/ZF/int_arith.ML
author wenzelm
Wed Jun 11 18:02:25 2008 +0200 (2008-06-11)
changeset 27154 026f3db3f5c6
parent 26190 cf51a23c0cd0
child 27237 c94eefffc3a5
permissions -rw-r--r--
OldGoals.inst;
     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 
    14 Addsimps [OldGoals.inst "y" "integ_of(?w)" @{thm zminus_equation},
    15           OldGoals.inst "x" "integ_of(?w)" @{thm equation_zminus}];
    16 
    17 AddIffs [OldGoals.inst "y" "integ_of(?w)" @{thm zminus_zless},
    18          OldGoals.inst "x" "integ_of(?w)" @{thm zless_zminus}];
    19 
    20 AddIffs [OldGoals.inst "y" "integ_of(?w)" @{thm zminus_zle},
    21          OldGoals.inst "x" "integ_of(?w)" @{thm zle_zminus}];
    22 
    23 Addsimps [OldGoals.inst "s" "integ_of(?w)" @{thm Let_def}];
    24 
    25 (*** Simprocs for numeric literals ***)
    26 
    27 (** Combining of literal coefficients in sums of products **)
    28 
    29 Goal "(x $< y) <-> (x$-y $< #0)";
    30 by (simp_tac (simpset() addsimps @{thms zcompare_rls}) 1);
    31 qed "zless_iff_zdiff_zless_0";
    32 
    33 Goal "[| x: int; y: int |] ==> (x = y) <-> (x$-y = #0)";
    34 by (asm_simp_tac (simpset() addsimps @{thms zcompare_rls}) 1);
    35 qed "eq_iff_zdiff_eq_0";
    36 
    37 Goal "(x $<= y) <-> (x$-y $<= #0)";
    38 by (asm_simp_tac (simpset() addsimps @{thms zcompare_rls}) 1);
    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";
    45 by (simp_tac (simpset() addsimps [@{thm zadd_zmult_distrib}]@ @{thms zadd_ac}) 1);
    46 qed "left_zadd_zmult_distrib";
    47 
    48 
    49 (** For cancel_numerals **)
    50 
    51 val rel_iff_rel_0_rls = map (OldGoals.inst "y" "?u$+?v")
    52                           [zless_iff_zdiff_zless_0, eq_iff_zdiff_eq_0,
    53                            zle_iff_zdiff_zle_0] @
    54                         map (OldGoals.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))";
    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);
    62 qed "eq_add_iff1";
    63 
    64 Goal "(i$*u $+ m = j$*u $+ n) <-> (intify(m) = (j$-i)$*u $+ n)";
    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);
    68 qed "eq_add_iff2";
    69 
    70 Goal "(i$*u $+ m $< j$*u $+ n) <-> ((i$-j)$*u $+ m $< n)";
    71 by (asm_simp_tac (simpset() addsimps [@{thm zdiff_def}, @{thm zadd_zmult_distrib}]@
    72                                      @{thms zadd_ac} @ rel_iff_rel_0_rls) 1);
    73 qed "less_add_iff1";
    74 
    75 Goal "(i$*u $+ m $< j$*u $+ n) <-> (m $< (j$-i)$*u $+ n)";
    76 by (asm_simp_tac (simpset() addsimps [@{thm zdiff_def}, @{thm zadd_zmult_distrib}]@
    77                                      @{thms zadd_ac} @ rel_iff_rel_0_rls) 1);
    78 qed "less_add_iff2";
    79 
    80 Goal "(i$*u $+ m $<= j$*u $+ n) <-> ((i$-j)$*u $+ m $<= n)";
    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);
    84 qed "le_add_iff1";
    85 
    86 Goal "(i$*u $+ m $<= j$*u $+ n) <-> (m $<= (j$-i)$*u $+ n)";
    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);
    90 qed "le_add_iff2";
    91 
    92 
    93 structure Int_Numeral_Simprocs =
    94 struct
    95 
    96 (*Utilities*)
    97 
    98 val integ_of_const = Const (@{const_name "Bin.integ_of"}, @{typ "i => i"});
    99 
   100 fun mk_numeral n = integ_of_const $ NumeralSyntax.mk_bin n;
   101 
   102 (*Decodes a binary INTEGER*)
   103 fun dest_numeral (Const(@{const_name "Bin.integ_of"}, _) $ w) =
   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;
   114 val mk_plus = FOLogic.mk_binop @{const_name "zadd"};
   115 
   116 val zminus_const = Const (@{const_name "zminus"}, @{typ "i => i"});
   117 
   118 (*Thus mk_sum[t] yields t+#0; longer sums don't have a trailing zero*)
   119 fun mk_sum []        = zero
   120   | mk_sum [t,u]     = mk_plus (t, u)
   121   | mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
   122 
   123 (*this version ALWAYS includes a trailing zero*)
   124 fun long_mk_sum []        = zero
   125   | long_mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
   126 
   127 val dest_plus = FOLogic.dest_bin @{const_name "zadd"} @{typ i};
   128 
   129 (*decompose additions AND subtractions as a sum*)
   130 fun dest_summing (pos, Const (@{const_name "zadd"}, _) $ t $ u, ts) =
   131         dest_summing (pos, t, dest_summing (pos, u, ts))
   132   | dest_summing (pos, Const (@{const_name "zdiff"}, _) $ t $ u, ts) =
   133         dest_summing (pos, t, dest_summing (not pos, u, ts))
   134   | dest_summing (pos, t, ts) =
   135         if pos then t::ts else zminus_const$t :: ts;
   136 
   137 fun dest_sum t = dest_summing (true, t, []);
   138 
   139 val mk_diff = FOLogic.mk_binop @{const_name "zdiff"};
   140 val dest_diff = FOLogic.dest_bin @{const_name "zdiff"} @{typ i};
   141 
   142 val one = mk_numeral 1;
   143 val mk_times = FOLogic.mk_binop @{const_name "zmult"};
   144 
   145 fun mk_prod [] = one
   146   | mk_prod [t] = t
   147   | mk_prod (t :: ts) = if t = one then mk_prod ts
   148                         else mk_times (t, mk_prod ts);
   149 
   150 val dest_times = FOLogic.dest_bin @{const_name "zmult"} @{typ i};
   151 
   152 fun dest_prod t =
   153       let val (t,u) = dest_times t
   154       in  dest_prod t @ dest_prod u  end
   155       handle TERM _ => [t];
   156 
   157 (*DON'T do the obvious simplifications; that would create special cases*)
   158 fun mk_coeff (k, t) = mk_times (mk_numeral k, t);
   159 
   160 (*Express t as a product of (possibly) a numeral with other sorted terms*)
   161 fun dest_coeff sign (Const (@{const_name "zminus"}, _) $ t) = dest_coeff (~sign) t
   162   | dest_coeff sign t =
   163     let val ts = sort Term.term_ord (dest_prod t)
   164         val (n, ts') = find_first_numeral [] ts
   165                           handle TERM _ => (1, ts)
   166     in (sign*n, mk_prod ts') end;
   167 
   168 (*Find first coefficient-term THAT MATCHES u*)
   169 fun find_first_coeff past u [] = raise TERM("find_first_coeff", [])
   170   | find_first_coeff past u (t::terms) =
   171         let val (n,u') = dest_coeff 1 t
   172         in  if u aconv u' then (n, rev past @ terms)
   173                           else find_first_coeff (t::past) u terms
   174         end
   175         handle TERM _ => find_first_coeff (t::past) u terms;
   176 
   177 
   178 (*Simplify #1*n and n*#1 to n*)
   179 val add_0s = [@{thm zadd_0_intify}, @{thm zadd_0_right_intify}];
   180 
   181 val mult_1s = [@{thm zmult_1_intify}, @{thm zmult_1_right_intify},
   182                @{thm zmult_minus1}, @{thm zmult_minus1_right}];
   183 
   184 val tc_rules = [@{thm integ_of_type}, @{thm intify_in_int},
   185                 @{thm int_of_type}, @{thm zadd_type}, @{thm zdiff_type}, @{thm zmult_type}] @ 
   186                @{thms bin.intros};
   187 val intifys = [@{thm intify_ident}, @{thm zadd_intify1}, @{thm zadd_intify2},
   188                @{thm zdiff_intify1}, @{thm zdiff_intify2}, @{thm zmult_intify1}, @{thm zmult_intify2},
   189                @{thm zless_intify1}, @{thm zless_intify2}, @{thm zle_intify1}, @{thm zle_intify2}];
   190 
   191 (*To perform binary arithmetic*)
   192 val bin_simps = [@{thm add_integ_of_left}] @ @{thms bin_arith_simps} @ @{thms bin_rel_simps};
   193 
   194 (*To evaluate binary negations of coefficients*)
   195 val zminus_simps = @{thms NCons_simps} @
   196                    [@{thm integ_of_minus} RS sym,
   197                     @{thm bin_minus_1}, @{thm bin_minus_0}, @{thm bin_minus_Pls}, @{thm bin_minus_Min},
   198                     @{thm bin_pred_1}, @{thm bin_pred_0}, @{thm bin_pred_Pls}, @{thm bin_pred_Min}];
   199 
   200 (*To let us treat subtraction as addition*)
   201 val diff_simps = [@{thm zdiff_def}, @{thm zminus_zadd_distrib}, @{thm zminus_zminus}];
   202 
   203 (*push the unary minus down: - x * y = x * - y *)
   204 val int_minus_mult_eq_1_to_2 =
   205     [@{thm zmult_zminus}, @{thm zmult_zminus_right} RS sym] MRS trans |> standard;
   206 
   207 (*to extract again any uncancelled minuses*)
   208 val int_minus_from_mult_simps =
   209     [@{thm zminus_zminus}, @{thm zmult_zminus}, @{thm zmult_zminus_right}];
   210 
   211 (*combine unary minus with numeric literals, however nested within a product*)
   212 val int_mult_minus_simps =
   213     [@{thm zmult_assoc}, @{thm zmult_zminus} RS sym, int_minus_mult_eq_1_to_2];
   214 
   215 fun prep_simproc (name, pats, proc) =
   216   Simplifier.simproc (the_context ()) name pats proc;
   217 
   218 structure CancelNumeralsCommon =
   219   struct
   220   val mk_sum            = (fn T:typ => mk_sum)
   221   val dest_sum          = dest_sum
   222   val mk_coeff          = mk_coeff
   223   val dest_coeff        = dest_coeff 1
   224   val find_first_coeff  = find_first_coeff []
   225   fun trans_tac _       = ArithData.gen_trans_tac iff_trans
   226 
   227   val norm_ss1 = ZF_ss addsimps add_0s @ mult_1s @ diff_simps @ zminus_simps @ @{thms zadd_ac}
   228   val norm_ss2 = ZF_ss addsimps bin_simps @ int_mult_minus_simps @ intifys
   229   val norm_ss3 = ZF_ss addsimps int_minus_from_mult_simps @ @{thms zadd_ac} @ @{thms zmult_ac} @ tc_rules @ intifys
   230   fun norm_tac ss =
   231     ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_ss1))
   232     THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_ss2))
   233     THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_ss3))
   234 
   235   val numeral_simp_ss = ZF_ss addsimps add_0s @ bin_simps @ tc_rules @ intifys
   236   fun numeral_simp_tac ss =
   237     ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
   238     THEN ALLGOALS (SIMPSET' (fn simpset => asm_simp_tac (Simplifier.inherit_context ss simpset)))
   239   val simplify_meta_eq  = ArithData.simplify_meta_eq (add_0s @ mult_1s)
   240   end;
   241 
   242 
   243 structure EqCancelNumerals = CancelNumeralsFun
   244  (open CancelNumeralsCommon
   245   val prove_conv = ArithData.prove_conv "inteq_cancel_numerals"
   246   val mk_bal   = FOLogic.mk_eq
   247   val dest_bal = FOLogic.dest_eq
   248   val bal_add1 = eq_add_iff1 RS iff_trans
   249   val bal_add2 = eq_add_iff2 RS iff_trans
   250 );
   251 
   252 structure LessCancelNumerals = CancelNumeralsFun
   253  (open CancelNumeralsCommon
   254   val prove_conv = ArithData.prove_conv "intless_cancel_numerals"
   255   val mk_bal   = FOLogic.mk_binrel @{const_name "zless"}
   256   val dest_bal = FOLogic.dest_bin @{const_name "zless"} @{typ i}
   257   val bal_add1 = less_add_iff1 RS iff_trans
   258   val bal_add2 = less_add_iff2 RS iff_trans
   259 );
   260 
   261 structure LeCancelNumerals = CancelNumeralsFun
   262  (open CancelNumeralsCommon
   263   val prove_conv = ArithData.prove_conv "intle_cancel_numerals"
   264   val mk_bal   = FOLogic.mk_binrel @{const_name "zle"}
   265   val dest_bal = FOLogic.dest_bin @{const_name "zle"} @{typ i}
   266   val bal_add1 = le_add_iff1 RS iff_trans
   267   val bal_add2 = le_add_iff2 RS iff_trans
   268 );
   269 
   270 val cancel_numerals =
   271   map prep_simproc
   272    [("inteq_cancel_numerals",
   273      ["l $+ m = n", "l = m $+ n",
   274       "l $- m = n", "l = m $- n",
   275       "l $* m = n", "l = m $* n"],
   276      K EqCancelNumerals.proc),
   277     ("intless_cancel_numerals",
   278      ["l $+ m $< n", "l $< m $+ n",
   279       "l $- m $< n", "l $< m $- n",
   280       "l $* m $< n", "l $< m $* n"],
   281      K LessCancelNumerals.proc),
   282     ("intle_cancel_numerals",
   283      ["l $+ m $<= n", "l $<= m $+ n",
   284       "l $- m $<= n", "l $<= m $- n",
   285       "l $* m $<= n", "l $<= m $* n"],
   286      K LeCancelNumerals.proc)];
   287 
   288 
   289 (*version without the hyps argument*)
   290 fun prove_conv_nohyps name tacs sg = ArithData.prove_conv name tacs sg [];
   291 
   292 structure CombineNumeralsData =
   293   struct
   294   type coeff            = int
   295   val iszero            = (fn x => x = 0)
   296   val add               = op + 
   297   val mk_sum            = (fn T:typ => long_mk_sum) (*to work for #2*x $+ #3*x *)
   298   val dest_sum          = dest_sum
   299   val mk_coeff          = mk_coeff
   300   val dest_coeff        = dest_coeff 1
   301   val left_distrib      = left_zadd_zmult_distrib RS trans
   302   val prove_conv        = prove_conv_nohyps "int_combine_numerals"
   303   fun trans_tac _       = ArithData.gen_trans_tac trans
   304 
   305   val norm_ss1 = ZF_ss addsimps add_0s @ mult_1s @ diff_simps @ zminus_simps @ @{thms zadd_ac} @ intifys
   306   val norm_ss2 = ZF_ss addsimps bin_simps @ int_mult_minus_simps @ intifys
   307   val norm_ss3 = ZF_ss addsimps int_minus_from_mult_simps @ @{thms zadd_ac} @ @{thms zmult_ac} @ tc_rules @ intifys
   308   fun norm_tac ss =
   309     ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_ss1))
   310     THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_ss2))
   311     THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_ss3))
   312 
   313   val numeral_simp_ss = ZF_ss addsimps add_0s @ bin_simps @ tc_rules @ intifys
   314   fun numeral_simp_tac ss =
   315     ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
   316   val simplify_meta_eq  = ArithData.simplify_meta_eq (add_0s @ mult_1s)
   317   end;
   318 
   319 structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData);
   320 
   321 val combine_numerals =
   322   prep_simproc ("int_combine_numerals", ["i $+ j", "i $- j"], K CombineNumerals.proc);
   323 
   324 
   325 
   326 (** Constant folding for integer multiplication **)
   327 
   328 (*The trick is to regard products as sums, e.g. #3 $* x $* #4 as
   329   the "sum" of #3, x, #4; the literals are then multiplied*)
   330 
   331 
   332 structure CombineNumeralsProdData =
   333   struct
   334   type coeff            = int
   335   val iszero            = (fn x => x = 0)
   336   val add               = op *
   337   val mk_sum            = (fn T:typ => mk_prod)
   338   val dest_sum          = dest_prod
   339   fun mk_coeff(k,t) = if t=one then mk_numeral k
   340                       else raise TERM("mk_coeff", [])
   341   fun dest_coeff t = (dest_numeral t, one)  (*We ONLY want pure numerals.*)
   342   val left_distrib      = @{thm zmult_assoc} RS sym RS trans
   343   val prove_conv        = prove_conv_nohyps "int_combine_numerals_prod"
   344   fun trans_tac _       = ArithData.gen_trans_tac trans
   345 
   346 
   347 
   348 val norm_ss1 = ZF_ss addsimps mult_1s @ diff_simps @ zminus_simps
   349   val norm_ss2 = ZF_ss addsimps [@{thm zmult_zminus_right} RS sym] @
   350     bin_simps @ @{thms zmult_ac} @ tc_rules @ intifys
   351   fun norm_tac ss =
   352     ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_ss1))
   353     THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_ss2))
   354 
   355   val numeral_simp_ss = ZF_ss addsimps bin_simps @ tc_rules @ intifys
   356   fun numeral_simp_tac ss =
   357     ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
   358   val simplify_meta_eq  = ArithData.simplify_meta_eq (mult_1s);
   359   end;
   360 
   361 
   362 structure CombineNumeralsProd = CombineNumeralsFun(CombineNumeralsProdData);
   363 
   364 val combine_numerals_prod =
   365   prep_simproc ("int_combine_numerals_prod", ["i $* j"], K CombineNumeralsProd.proc);
   366 
   367 end;
   368 
   369 
   370 Addsimprocs Int_Numeral_Simprocs.cancel_numerals;
   371 Addsimprocs [Int_Numeral_Simprocs.combine_numerals,
   372              Int_Numeral_Simprocs.combine_numerals_prod];
   373 
   374 
   375 (*examples:*)
   376 (*
   377 print_depth 22;
   378 set timing;
   379 set trace_simp;
   380 fun test s = (Goal s; by (Asm_simp_tac 1));
   381 val sg = #sign (rep_thm (topthm()));
   382 val t = FOLogic.dest_Trueprop (Logic.strip_assums_concl(getgoal 1));
   383 val (t,_) = FOLogic.dest_eq t;
   384 
   385 (*combine_numerals_prod (products of separate literals) *)
   386 test "#5 $* x $* #3 = y";
   387 
   388 test "y2 $+ ?x42 = y $+ y2";
   389 
   390 test "oo : int ==> l $+ (l $+ #2) $+ oo = oo";
   391 
   392 test "#9$*x $+ y = x$*#23 $+ z";
   393 test "y $+ x = x $+ z";
   394 
   395 test "x : int ==> x $+ y $+ z = x $+ z";
   396 test "x : int ==> y $+ (z $+ x) = z $+ x";
   397 test "z : int ==> x $+ y $+ z = (z $+ y) $+ (x $+ w)";
   398 test "z : int ==> x$*y $+ z = (z $+ y) $+ (y$*x $+ w)";
   399 
   400 test "#-3 $* x $+ y $<= x $* #2 $+ z";
   401 test "y $+ x $<= x $+ z";
   402 test "x $+ y $+ z $<= x $+ z";
   403 
   404 test "y $+ (z $+ x) $< z $+ x";
   405 test "x $+ y $+ z $< (z $+ y) $+ (x $+ w)";
   406 test "x$*y $+ z $< (z $+ y) $+ (y$*x $+ w)";
   407 
   408 test "l $+ #2 $+ #2 $+ #2 $+ (l $+ #2) $+ (oo $+ #2) = uu";
   409 test "u : int ==> #2 $* u = u";
   410 test "(i $+ j $+ #12 $+ k) $- #15 = y";
   411 test "(i $+ j $+ #12 $+ k) $- #5 = y";
   412 
   413 test "y $- b $< b";
   414 test "y $- (#3 $* b $+ c) $< b $- #2 $* c";
   415 
   416 test "(#2 $* x $- (u $* v) $+ y) $- v $* #3 $* u = w";
   417 test "(#2 $* x $* u $* v $+ (u $* v) $* #4 $+ y) $- v $* u $* #4 = w";
   418 test "(#2 $* x $* u $* v $+ (u $* v) $* #4 $+ y) $- v $* u = w";
   419 test "u $* v $- (x $* u $* v $+ (u $* v) $* #4 $+ y) = w";
   420 
   421 test "(i $+ j $+ #12 $+ k) = u $+ #15 $+ y";
   422 test "(i $+ j $* #2 $+ #12 $+ k) = j $+ #5 $+ y";
   423 
   424 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";
   425 
   426 test "a $+ $-(b$+c) $+ b = d";
   427 test "a $+ $-(b$+c) $- b = d";
   428 
   429 (*negative numerals*)
   430 test "(i $+ j $+ #-2 $+ k) $- (u $+ #5 $+ y) = zz";
   431 test "(i $+ j $+ #-3 $+ k) $< u $+ #5 $+ y";
   432 test "(i $+ j $+ #3 $+ k) $< u $+ #-6 $+ y";
   433 test "(i $+ j $+ #-12 $+ k) $- #15 = y";
   434 test "(i $+ j $+ #12 $+ k) $- #-15 = y";
   435 test "(i $+ j $+ #-12 $+ k) $- #-15 = y";
   436 
   437 (*Multiplying separated numerals*)
   438 Goal "#6 $* ($# x $* #2) =  uu";
   439 Goal "#4 $* ($# x $* $# x) $* (#2 $* $# x) =  uu";
   440 *)
   441