Require Export SMat_most_f_byz.
Require Export SMtactics3.


Section SMsame_states.

  Local Open Scope eo.
  Local Open Scope proc.

  Context { dtc   : DTimeContext }.
  Context { dtime : @TimeConstraint dtc }.

  Context { sm_context       : SMcontext }.
  Context { sm_auth          : SMauth }.
  Context { sm_initial_keys  : SMinitial_keys }.

  Lemma SM_replicas_never_stop :
    forall i (x : SMstate) m t, exists s, fst (sm_update (SMreplicaSM i) x m t) = Some s.
  Proof.
    introv.
    unfold SMreplicaSM; simpl.
    unfold SMupdate; destruct m; simpl in *; ginv; tcsp; eauto.

    { unfold SMhandler_initial; smash_sm; eauto. }
    { unfold SMhandler_alarm; smash_sm; eauto. }
    { unfold SMhandler_lieutenant; smash_sm; eauto. }
  Qed.
  Hint Resolve SM_replicas_never_stop : sm.

End SMsame_states.


Hint Resolve SM_replicas_never_stop : sm.
