Hello all,For Theorems like the following one what is the corresponding theorem
if the guard conditions do not hold, I mean what the n2w_DIV theorem would
like if a or n or both of them are greater that dimword (:α). [n2w_DIV]
Theorem
|- ∀a n.
n < dimindex (:α) ∧ a < dimword (:α) ⇒
(n2w (a DIV 2 ** n) = n2w a ⋙ n)
do we have module to dimword(:'a) of these two numbers? if no what we cando in
such a case? Thanks in advance.
Regards,Hamed Nemati------------------------------------------------------------------------------
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
