proposition: Lemma C_interp_or_spec : forall rho c, C_interp_or rho c = C.interp rho (to_list c).
proof: Proof. intros rho c; unfold C_interp_or; case_eq (C.interp rho (to_list c)). unfold C.interp; rewrite List.existsb_exists; intros [x [H1 H2]]; destruct (In_to_list _ _ H1) as [i [H3 H4]]; subst x; apply (afold_left_orb_true i); rewrite ?length_amap,?get_amap;auto. unfold C.interp; intro H; apply afold_left_orb_false; rewrite length_amap; intros i H1; rewrite get_amap; case_eq (Lit.interp rho (c .[ i])); auto; intro Heq; assert (H2: exists x, List.In x (to_list c) /\ Lit.interp rho x = true). exists (c.[i]); split; auto; apply to_list_In; auto. rewrite <- List.existsb_exists in H2; rewrite H2 in H; auto. Qed.
imports: Bool Int63 PArray Misc State SMT_terms Syntactic Arithmetic Operators Assumptions Cnf Euf Lia BVList Bva_checker Array_checker