proposition: Theorem step_1_star_trace_state_correct : forall st st' trace, step_1_star st st' trace -> trace_state_correct trace st st'.
proof: Proof. intros. find_apply_lem_hyp refl_trans_1n_n1_trace. induction H; auto. - unfold trace_state_correct. auto. - unfold trace_state_correct in *. intros. invcs H0. unfold VarDHandler, VarDHandler' in *. vard_unfold. repeat break_match; simpl in *; repeat find_inversion. + destruct (key_eq_dec k0 k). * rewrite inputs_with_key_plus_key; simpl in *; auto. rewrite rev_unit. simpl in *. subst. symmetry; apply Map.add_eq_o. reflexivity. * rewrite inputs_with_key_plus_not_key; simpl in *; eauto. rewrite Map.add_neq_o; auto. + destruct (key_eq_dec k0 k). * rewrite inputs_with_key_plus_key; simpl in *; auto. rewrite rev_unit. simpl in *. subst. eauto. * rewrite inputs_with_key_plus_not_key; simpl in *; eauto. + destruct (key_eq_dec k0 k). * rewrite inputs_with_key_plus_key; simpl in *; auto. rewrite rev_unit. simpl in *. subst. eauto. rewrite Map.remove_eq_o; auto. * rewrite inputs_with_key_plus_not_key; simpl in *; eauto. rewrite Map.remove_neq_o; auto. + destruct (key_eq_dec k0 k). * subst. rewrite inputs_with_key_plus_key; simpl in *; auto. rewrite rev_unit. simpl in *. break_if; [rewrite Map.add_eq_o; auto | idtac]. exfalso. intuition. * rewrite inputs_with_key_plus_not_key; simpl in *; eauto. rewrite Map.add_neq_o; auto. + destruct (key_eq_dec k0 k). * rewrite inputs_with_key_plus_key; simpl in *; auto. rewrite rev_unit. simpl in *. subst. break_if. -- subst. exfalso. intuition. -- simpl in *. apply IHrefl_trans_n1_trace. * rewrite inputs_with_key_plus_not_key; simpl in *; eauto. + destruct (key_eq_dec k0 k). * { subst. rewrite inputs_with_key_plus_key; simpl in *; auto. rewrite rev_unit. simpl in *. break_if; simpl in *. - symmetry. rewrite Map.remove_eq_o; auto. - exfalso. intuition. match goal with | H : _ -> False |- _ => apply H end. find_higher_order_rewrite. auto. } * rewrite inputs_with_key_plus_not_key; simpl in *; eauto. rewrite Map.remove_neq_o; auto. + destruct (key_eq_dec k0 k). * subst. rewrite inputs_with_key_plus_key; simpl in *; auto. rewrite rev_unit. simpl in *. break_if; simpl in *; intuition. exfalso. intuition. match goal with | H : _ -> False |- _ => apply H end. find_higher_order_rewrite. auto. * rewrite inputs_with_key_plus_not_key; simpl in *; eauto. Qed.
imports: Verdi(Verdi) Coq(FMapList String) Verdi(FMapVeryWeak StateMachineHandlerMonad)