proposition: Lemma flatten_and_correct : forall args, List.fold_right (fun l res => andb res (interp_lit l)) true (flatten_and args) = afold_left _ true andb (amap interp_lit args).
proof: Proof. intros;rewrite afold_left_spec;auto;unfold flatten_and. change true with (List.fold_right (fun (l : int) (res : bool) => res && interp_lit l) true nil) at 2. rewrite !foldi_to_list, to_list_amap. generalize (@nil int);induction (to_list args);simpl;trivial. intros l0;rewrite IHl. clear IHl;f_equal; unfold flatten_op_lit. clear l;revert a l0;apply foldi_ind;simpl;trivial. apply leb_0. intros i cont _ Hlt Hrec a l;unfold flatten_op_body. case_eq (get_and a);intros;trivial. rewrite get_and_correct with (1:= H);simpl. rewrite afold_left_spec; auto; rewrite !foldi_to_list. rewrite <- !fold_left_rev_right, to_list_amap, <- map_rev. clear H a;revert l;induction (List.rev (to_list a0));simpl. intros l;rewrite andb_true_r;trivial. intros;rewrite Hrec, IHl, andb_assoc;trivial. Qed.
imports: List PArray Bool Int63 ZMicromega ZArith Misc State SMT_terms BVList