proposition: Lemma valid_check_BuildDef : forall l, C.valid rho (check_BuildDef l).
proof: Proof. unfold check_BuildDef,C.valid;intros l. case_eq (t_form.[Lit.blit l]);intros;auto using C.interp_true; case_eq (Lit.is_pos l);intros Heq;auto using C.interp_true;simpl; try (unfold Lit.interp at 1;rewrite Heq;unfold Var.interp; rewrite rho_interp, H;simpl; tauto_check). - rewrite afold_left_and, C.Cinterp_neg;apply orb_negb_r. - rewrite afold_left_or, orb_comm;apply orb_negb_r. - case_eq (PArray.length a =? 0); auto using C.interp_true. intro Hl; simpl. unfold Lit.interp at 1;rewrite Heq;unfold Var.interp; rewrite rho_interp, H;simpl. rewrite (afold_right_impb (Lit.interp_neg _) Hl), orb_comm;try apply orb_negb_r. Qed.
imports: PArray List Bool ZArith Psatz Misc State SMT_terms BVList