fact: Definition check_bbDiseq lres := if negb (Lit.is_pos lres) then match get_form (Lit.blit lres) with | Fatom f => match (get_atom f) with | Abop (BO_eq (Typ.TBV n)) a b => match (get_atom a), (get_atom b) with | (Acop (CO_BV bv1 n1)), (Acop (CO_BV bv2 n2)) => if List_diseqb bv1 bv2 && (N.of_nat (length bv1) =? n)%N && (N.of_nat (length bv2) =? n)%N && (n1 =? n)%N && (n2 =? n)%N then lres::nil else C._true | _, _ => C._true end | _ => C._true end | _ => C._true end else C._true.
imports: Int63 PArray SMT_classes ZArith Misc State SMT_terms BVList Psatz Bool List BoolEq NZParity Nnat BinPos BinNat Pnat Init.Peano ProofIrrelevance