fact: Definition check_bbAdd pos1 pos2 lres := match S.get s pos1, S.get s pos2 with | l1::nil, l2::nil => if (Lit.is_pos l1) && (Lit.is_pos l2) && (Lit.is_pos lres) then match get_form (Lit.blit l1), get_form (Lit.blit l2), get_form (Lit.blit lres) with | FbbT a1 bs1, FbbT a2 bs2, FbbT a bsres => match get_atom a with | Abop (BO_BVadd n) a1' a2' => if (((a1 =? a1') && (a2 =? a2')) || ((a1 =? a2') && (a2 =? a1'))) && (check_add bs1 bs2 bsres (Clit Lit._false)) && (N.of_nat (length bs1) =? n)%N then lres::nil else C._true | _ => C._true end | _, _, _ => C._true end else C._true | _, _ => C._true end.
imports: Int63 PArray SMT_classes ZArith Misc State SMT_terms BVList Psatz Bool List BoolEq NZParity Nnat BinPos BinNat Pnat Init.Peano ProofIrrelevance