fact: Fixpoint check_symopp (bs1 bs2 bsres : list _lit) (bvop: binop) := match bs1, bs2, bsres with | nil, nil, nil => true | b1::bs1, b2::bs2, bres::bsres => if Lit.is_pos bres then let (ires, bvop) := match get_form (Lit.blit bres), bvop with | Fand args, BO_BVand n => ((if PArray.length args =? 2 then let a1 := args.[0] in let a2 := args.[1] in ((a1 =? b1) && (a2 =? b2)) || ((a1 =? b2) && (a2 =? b1)) else false), BO_BVand (n-1)) | For args, BO_BVor n => ((if PArray.length args =? 2 then let a1 := args.[0] in let a2 := args.[1] in ((a1 =? b1) && (a2 =? b2)) || ((a1 =? b2) && (a2 =? b1)) else false), BO_BVor (n-1)) | Fxor a1 a2, BO_BVxor n => (((a1 =? b1) && (a2 =? b2)) || ((a1 =? b2) && (a2 =? b1)), BO_BVxor (n-1)) | Fiff a1 a2, (BO_eq (Typ.TBV n)) => (((a1 =? b1) && (a2 =? b2)) || ((a1 =? b2) && (a2 =? b1)), BO_eq (Typ.TBV n)) | _, _ => (false, bvop) end in if ires then check_symopp bs1 bs2 bsres bvop else false else false | _, _, _ => 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