proposition: Lemma valid_check_ImmBuildDef : forall cid, C.valid rho (check_ImmBuildDef cid).
proof: Proof. unfold check_ImmBuildDef,C.valid;intros cid. generalize (Hs cid);unfold C.valid. destruct (S.get s cid) as [ | l [ | _l _c]];auto using C.interp_true. simpl;unfold Lit.interp, Var.interp; rewrite !rho_interp; destruct (t_form.[Lit.blit l]);auto using C.interp_true; case_eq (Lit.is_pos l);intros Heq;auto using C.interp_true;simpl; tauto_check. - rewrite afold_left_and, C.Cinterp_neg, orb_false_r;trivial. - rewrite afold_left_or, orb_false_r;trivial. - case_eq (PArray.length a =? 0); auto using C.interp_true. intro Hl. now rewrite orb_false_r, (afold_right_impb (Lit.interp_neg _) Hl). - case_eq (PArray.length a =? 0); auto using C.interp_true. Qed.
imports: PArray List Bool ZArith Psatz Misc State SMT_terms BVList