proposition: Lemma valid_spec : forall rho d, valid rho d <-> (forall i : int, i <? length d -> C.interp rho (to_list (d.[i]))).
proof: Proof. unfold valid; intros rho d; split; intro H. intros i Hi; case_eq (C.interp rho (to_list (d .[ i]))); try reflexivity. intro Heq; erewrite afold_left_andb_false in H; rewrite ?length_amap, ?get_amap; try eassumption. rewrite C_interp_or_spec; auto. apply afold_left_andb_true; rewrite length_amap; intros i Hi; rewrite get_amap, C_interp_or_spec by assumption; apply H; auto. Qed.
imports: Bool Int63 PArray Misc State SMT_terms Syntactic Arithmetic Operators Assumptions Cnf Euf Lia BVList Bva_checker Array_checker