fact: Fixpoint check_bb (a: int) (bs: list _lit) (i n: nat) := match bs with | nil => Nat.eqb i n | b::bs => if Lit.is_pos b then match get_form (Lit.blit b) with | Fatom a' => match get_atom a' with | Auop (UO_BVbitOf N p) a' => if (a =? a') && (Nat.eqb i p) && (Nat.eqb n (N.to_nat N)) then check_bb a bs (S i) n else false | _ => false end | _ => false end else false end.
imports: Int63 PArray SMT_classes ZArith Misc State SMT_terms BVList Psatz Bool List BoolEq NZParity Nnat BinPos BinNat Pnat Init.Peano ProofIrrelevance