proposition: Lemma check_hatom_correct : wf t_atom -> default t_atom = Acop CO_xH -> forall h1 h2, check_hatom h1 h2 -> interp_hatom t_i t_func t_atom h1 = interp_hatom t_i t_func t_atom h2.
proof: Proof. unfold check_hatom;intros Hwf Hdef. apply foldi_ind;try discriminate. apply leb_0. intros i cont _ _ Hrec h1 h2. unfold is_true; rewrite orb_true_iff; intros [H|H]. rewrite Int63.eqb_spec in H; rewrite H; reflexivity. unfold interp_hatom;rewrite !t_interp_wf;trivial. apply check_atom_aux_correct with cont;trivial. Qed.
imports: List PArray Bool Int63 ZMicromega ZArith Misc State SMT_terms BVList