Lines Matching refs:sg
249 \\ REV (sg `~(n2mw (n DIV dimword (:'a)) = ([]:'a word list))`)
341 \\ REV (sg `m DIV dimword (:'a) <= n DIV dimword (:'a)`) THEN1 METIS_TAC []
491 \\ REV (sg `(n + n' + b2n c) DIV dimword (:'a) = 1`)
1024 (REV (sg `mw2n (SNOC x xs) < mw2n (SNOC z zs)`) THEN1 DECIDE_TAC
2177 REV (sg `mw_cmp [u3; u2; u1] (mw_mul_by_single q [v2; v1]) = SOME T`)
2187 REV (sg `w2n u1 * dimword(:'a) * dimword(:'a) + w2n u2 * dimword(:'a) + w2n u3 < w2n q * (w2n v1 * dimword(:'a) + w2n v2)`)
2384 sg `w2n q3 = mw2n (REVERSE us) DIV mw2n (REVERSE ys)`
2515 sg `w2n q3 = mw2n (REVERSE us) DIV mw2n (REVERSE ys)`
2814 (sg `mw_mul_by_single d (mw_fix ys) <> []`
3436 \\ sg `w2n (m << 1) = 2 * w2n m` \\ fs []
3451 \\ sg `2 * n + 1 < 2 * (2 ** k * 2 ** p) /\
3455 \\ sg `w2n (m << 1 + 1w) = 2 * w2n m + 1` \\ fs []
3461 \\ sg `mw2n q = mw2n is - mw2n ns DIV 2` \\ fs []