val int2bv_lognot: #n: pos -> #x: uint_t n -> #z: bv_t n -> squash (bvnot #n (int2bv #n x) == z)
  -> Lemma (int2bv #n (lognot #n x) == z)
let int2bv_lognot #n #x #y pf =
  inverse_vec_lemma #n (bvnot #n (int2bv x))
val int2bv_lognot: #n: pos -> #x: uint_t n -> #z: bv_t n -> squash (bvnot #n (int2bv #n x) == z)
  -> Lemma (int2bv #n (lognot #n x) == z)
let int2bv_lognot #n #x #y pf =
inverse_vec_lemma #n (bvnot #n (int2bv x))
FStar.BV.fst.checked
prims.fst.checked FStar.UInt.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.BitVector.fst.checked
FStar.BV.fst
Prims.pos FStar.UInt.uint_t FStar.BV.bv_t Prims.squash Prims.eq2 FStar.BV.bvnot FStar.BV.int2bv FStar.BV.inverse_vec_lemma Prims.unit
(*
   Copyright 2008-2018 Microsoft Research

   Licensed under the Apache License, Version 2.0 (the "License");
   you may not use this file except in compliance with the License.
   You may obtain a copy of the License at

       http://www.apache.org/licenses/LICENSE-2.0

   Unless required by applicable law or agreed to in writing, software
   distributed under the License is distributed on an "AS IS" BASIS,
   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
   See the License for the specific language governing permissions and
   limitations under the License.
*)
module FStar.BV

module U = FStar.UInt
module B = FStar.BitVector
module S = FStar.Seq

let bv_t (n : nat) = B.bv_t n

let bv_uext #n #i a =
  Seq.append (Seq.create i false) a

let int2bv = U.to_vec
let bv2int = U.from_vec

let int2bv_lemma_1 = U.to_vec_lemma_1
let int2bv_lemma_2 = U.to_vec_lemma_2
let inverse_vec_lemma = U.inverse_vec_lemma
let inverse_num_lemma = U.inverse_num_lemma

let list2bv #n l = S.seq_of_list l
let bv2list #n s = S.seq_to_list s
let list2bv_bij #n a = S.lemma_list_seq_bij a
let bv2list_bij #n a = S.lemma_seq_list_bij a

let bvand = B.logand_vec
let int2bv_logand #n #x #y #z pf =
  inverse_vec_lemma #n (bvand #n (int2bv #n x) (int2bv #n y))

let bvxor = B.logxor_vec
let int2bv_logxor #n #x #y #z pf =
  inverse_vec_lemma #n (bvxor #n (int2bv x) (int2bv y))

let bvor = B.logor_vec
let int2bv_logor #n #x #y #z pf =
  inverse_vec_lemma #n (bvor #n (int2bv x) (int2bv y))

let bvnot = B.lognot_vec
val int2bv_lognot: #n: pos -> #x: uint_t n -> #z: bv_t n -> squash (bvnot #n (int2bv #n x) == z)
  -> Lemma (int2bv #n (lognot #n x) == z)
pf: Prims.squash (FStar.BV.bvnot (FStar.BV.int2bv x) == z)
  -> FStar.Pervasives.Lemma (ensures FStar.BV.int2bv (FStar.UInt.lognot x) == z)