proposition: Lemma PB_net_defn' : forall dst src m d os d' ms, PB_net dst src m d = (os, d', ms) -> (os = [] /\ d' = d /\ ms = [] /\ ((dst = Primary /\ exists i, m = BackItUp i) \/ (dst = Backup /\ m = Ack))) \/ (dst = Primary /\ m = Ack /\ ( (queue d = [] /\ os = [] /\ ms = [] /\ d' = d) \/ (exists h t, queue d = h :: t /\ queue d' = t /\ ((t = [] /\ ms = []) \/ (exists y ys, t = y :: ys /\ ms = [(Backup, BackItUp y)])) /\ let (us, st') := handler h (state d) in os = [RequestResponse h us] /\ state d' = st'))) \/ (dst = Backup /\ ms = [(Primary, Ack)] /\ queue d' = queue d /\ os = [] /\ (exists i, m = BackItUp i /\ state d' = snd (handler i (state d)))).
proof: Proof. Proof using. unfold PB_net. intros. pb_unfold. repeat (first [break_let | break_match]); repeat find_inversion; auto; simpl. - left. intuition. left. eauto. - right. left. intuition. - right. left. intuition. right. eexists. eexists. intuition eauto. find_rewrite. auto. - right. left. intuition. right. eexists. eexists. intuition eauto. find_rewrite. auto. - right. right. intuition. eauto. - left. intuition. Qed.
imports: Verdi(Verdi HandlerMonad)