proposition: Lemma check_symopp_bvxor_nl: forall bs1 bs2 bsres N, check_symopp bs1 bs2 bsres (BO_BVxor N) = true -> (List.map (Lit.interp rho) bsres) = (RAWBITVECTOR_LIST.map2 xorb (List.map (Lit.interp rho) bs1) (List.map (Lit.interp rho) bs2)).
proof: Proof. intros. pose proof H. apply check_symopp_bvxor_length in H. destruct H. apply check_symopp_bvxor in H0. easy. easy. easy. Qed.
imports: Int63 PArray SMT_classes ZArith Misc State SMT_terms BVList Psatz Bool List BoolEq NZParity Nnat BinPos BinNat Pnat Init.Peano ProofIrrelevance