Lines Matching refs:MIN
188 (FCP i. l <= i /\ i <= MIN h ^HB /\ w ' i):'a word`
192 (FCP i. i + l <= MIN h ^HB /\ w ' (i + l)):'a word`
196 (FCP i. l <= MIN h ^HB /\ w ' (MIN (i + l) (MIN h ^HB))):'a word`
1306 (n2w (SLICE (MIN h ^HB) l n)):'a word`,
1311 (n2w (BITS (MIN h ^HB) l n)):'a word`,
1312 FIELD_WORD_TAC \\ Cases_on `i + l <= MIN h ^HB`
1328 n2w (SIGN_EXTEND (MIN (SUC h) (dimindex(:'a)) - l) (dimindex(:'a))
1329 (BITS (MIN h ^HB) l n))`,
1361 `!h t. MIN (MIN h t) (t + l) = MIN h t`,
1367 word_sign_extend (MIN (SUC h) (dimindex(:'a)) - l) ((h -- l) w)`,
1389 `(!m n. MIN m (m + n) = m) /\ !m n. MIN (m + n) m = m`,
1393 `MIN a (MIN b (MIN (c + a) (c + b))) = MIN a b`,
1397 `!x y. x <= y ==> (MIN x y = x)`, RW_TAC arith_ss [MIN_DEF])
1401 w2w ((MIN h (dimindex (:'b) - 1) -- l) w)`,
1540 val lem = Q.prove(`MIN d (l1 + MIN h2 d) = MIN (h2 + l1) d`,
1545 ((MIN h1 (h2 + l1)) -- (l2 + l1)) w`,
1630 (MIN m (MIN (h + n)
1631 (MIN (dimindex(:'c) - 1) (dimindex(:'b) + n - 1))) >< l + n) w`,
1659 simpLib.SIMP_PROVE arith_ss [MIN_DEF] ``l <= h ==> (MIN h l = l)``])
1724 (MIN h (MIN (dimindex(:'b) + l - 1)
1749 (MIN h (MIN (dimindex(:'b) + l - 1)
1906 `!i a b. MIN (LOG2 a) (LOG2 b) < i ==> ~BIT i a \/ ~BIT i b`,
1925 BIT i (BITWISE (SUC (MIN (LOG2 a) (LOG2 b))) op a b))`,
1927 \\ Cases_on `l <= SUC (MIN (LOG2 a) (LOG2 b))`
1929 \\ Cases_on `i < SUC (MIN (LOG2 a) (LOG2 b))`
1932 \\ `MIN (LOG2 a) (LOG2 b) < i` by DECIDE_TAC
1953 `!n m. n2w n && n2w m = n2w (BITWISE (SUC (MIN (LOG2 n) (LOG2 m))) $/\ n m)`,
1980 ~(n2w (BITWISE (SUC (MIN (LOG2 n) (LOG2 m))) $/\ n m))`,
2645 ``0 < m /\ SUC n < m ==> (MIN n (m - 1) = n)``]
2919 Tw << (^WL - MIN n ^WL) || w >>> n
3038 simpLib.SIMP_PROVE arith_ss [MIN_DEF] ``MIN a (a + b) = a``,
3196 ((MIN h (MIN (dimindex(:'b) + l - 1)
3207 ((MIN h (MIN (dimindex(:'b) + l - 1)