Hi Hamed, Yes, the side-condition
n < dimindex (:α) is redundant. I’ve updated this theorem accordingly. To get a theorem with no side-conditions we can introduce a MOD: wordsTheory.n2w_DIV |> Q.SPEC `a MOD dimword(:'a)` |> SIMP_RULE (srw_ss()) [wordsTheory.n2w_mod] |> GEN_ALL val it = |- ∀a n. n2w (a MOD dimword (:α) DIV 2 ** n) = n2w a ⋙ n: thm It would also have been possible to get to this theorem using word_lsr_n2w as the starting point. Regards, Anthony On 4 Mar 2013, at 19:48, hamed nemati <[email protected]> wrote: > 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 can > do 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 ------------------------------------------------------------------------------ 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
