fact: Definition redirect_inc_trans (c : Config) (s1 s2 : Site) (q : queue Message) := mkconfig (st c) (rt c) (Post_message Message dec (change_queue (queue Message) (bm c) s1 owner q) s1 s2).
imports: abstract_machine