[Hol-info] Procedure for equations with addition and multiplication

[Alexey G. <ov...@ca...>]

Hi everyone,

Does anyone know if there is a procedure in HOL for proving simple 
statements about equations with addition and multiplication like the 
following one?

(e*bv_c+e*(2*bv_cout+wb_sum)+wbs_sum=bv_cin+e*(bv_c+wb_a+wb_b)+wbs_a+wbs_b) 
==>        (2*e*bv_cout+e*wb_sum+wbs_sum=bv_cin+e*wb_a+e*wb_b+wbs_a+wbs_b)

Unfortunately, PROVE_TAC and RW_TAC arith_ss [] don't do the job.

Best regards,
Alexey Gotsman