proposition: Lemma prop_lit2: forall bsres, Lit.is_pos bsres = false -> Lit.interp (interp_state_var (fun a0 : int => interp_bool t_i (t_interp .[ a0])) interp_form_hatom_bv t_form) bsres = negb (Form.interp (fun a0 : int => interp_bool t_i (t_interp .[ a0])) interp_form_hatom_bv t_form (t_form .[ Lit.blit bsres])).
proof: Proof. intros. rewrite <- rho_interp. simpl. unfold Lit.interp, Var.interp. rewrite H. simpl. 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