Library Asm.Bitvector.Bitwise

Bitwise operations





Require Import Bool Bvector.




Require Import Asm.Util.ArithUtil.

Require Import Asm.Util.Mod.

Require Import Asm.Util.Tactics.




Require Import Asm.Bitvector.Convert.

Require Import Asm.Bitvector.Defs.

Require Import Asm.Bitvector.Tactics.

NOT





Lemma bnot_btn : forall len (v : Bvector len),

  eqMod (pow2 len) (bvec_to_nat (bnot v)) (pow2 len - bvec_to_nat v - 1).




Lemma bnot_btn_double : forall len (v : Bvector len),

  bnot (bnot v) = v.




Hint Resolve bnot_btn : asm.

Index

This page has been generated by coqdoc