Hi Hamed, Ideally there shouldn’t be any theorems with redundant side-conditions, so these are worth reporting/fixing, especially if they’re hampering progress. In general, side-conditions will be there because they’re needed.
You may be able to specialise other theorems to eliminate side-conditions, however this can make the resulting theorems less useful. For example: n2w (a MOD dimword (:α) DIV 2 ** n) = ... is a less useful than the conditional rewrite a < dimword(:’a) ==> (n2w (a DIV 2 ** n) = ...) This is because with the latter we can do: > SIMP_CONV (srw_ss()) [n2w_DIV] ``n2w (3 DIV 2 ** n) : word8``; val it = |- n2w (3 DIV 2 ** n) = 3w ⋙ n: thm which isn’t directly possible with the former. Regards, Anthony On 4 Mar 2013, at 22:04, hamed nemati <[email protected]> wrote: > Dear Anthony, > > Thank you very much for your response. Is it a general case and we can do the > same for all the other theorems like the n2w_DIV or no? > > Regards, ------------------------------------------------------------------------------ Everyone hates slow websites. So do we. Make your web apps faster with AppDynamics Download AppDynamics Lite for free today: http://p.sf.net/sfu/appdyn_d2d_feb _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
