fact: Definition bblast_bvmult (a b: list _lit) (n: nat) : list carry := let res := and_with_bit a (nth 0 b Lit._false) in match n with | O => res | S O => res | S (S k) => mult_step a b res 1 k end.
imports: Int63 PArray SMT_classes ZArith Misc State SMT_terms BVList Psatz Bool List BoolEq NZParity Nnat BinPos BinNat Pnat Init.Peano ProofIrrelevance