(check (= 0 (& 10 0)))
(check (= 8 (& 8 10)))
(check (= 10 (| 8 10)))
(check (= 2 (^ 8 10)))
(check (= 8 (<< 1 3)))
(check (= 1 (>> 8 3)))
(check (= 2 (% 8 3)))
(check (= 2 (/ 8 3)))
(check (= -1 (not-i64 0)))

; bitsets
;(function bs-union (i64 i64) i64)
;(rewrite (bs-union a b) (| a b))

;(function bs-inter (i64 i64) i64)
;(rewrite (bs-inter a b) (& a b))

;(function bs-comp (i64) i64)
;(rewrite (bs-comp a) (bvnot a))

; singleton set
;(function bs-sing (i64) i64)
;(rewrite (bs-sing a) (1 << a))

;(function bs-insert (i64 i64) i64)
;(rewrite (bs-insert s x) (| s (1 << a))

;(function bs-diff (i64 i64) i64)
;(rewrite (bs-diff a b) (^ a (bs-inter a b))

;(let bs-empty 0)

;(let bs-subset (i64 i64) bool)
;(rewrite (bs-subset x y) (is-zero (bs-diff x y)))

;(let bs-is-elem (i64 i64) bool)
;(rewrite (bs-is-elem s x) (not (is-zero (bs-inter s (sing x)))))