proposition: Lemma step_checker_correct : forall rho rhobv t_form, Form.check_form t_form -> forall s, S.valid (Form.interp_state_var rho rhobv t_form) s -> forall st : step, S.valid (Form.interp_state_var rho rhobv t_form) (step_checker t_form s st).
proof: Proof. intros rho rhobv t_form Ht s H; destruct (Form.check_form_correct rho rhobv _ Ht) as [[Ht1 Ht2] Ht3]; intros [pos res|pos cid lf|pos|pos|pos l|pos l|pos l i|pos cid|pos cid|pos cid i]; simpl; try apply S.valid_set_clause; auto. apply S.valid_set_resolve; auto. apply valid_check_flatten; auto; try discriminate; intros a1 a2; unfold is_true; rewrite Int63.eqb_spec; intro; subst a1; auto. apply valid_check_True; auto. apply valid_check_False; auto. apply valid_check_BuildDef; auto. apply valid_check_BuildDef2; auto. apply valid_check_BuildProj; auto. apply valid_check_ImmBuildDef; auto. apply valid_check_ImmBuildDef2; auto. apply valid_check_ImmBuildProj; auto. Qed.
imports: Bool Int63 PArray Misc State SMT_terms Syntactic Arithmetic Operators Assumptions Cnf Euf Lia BVList Bva_checker Array_checker