imp_r.
repeattac (andM_l 1).
orA_r1.
andA_r.
andM_r (1::2::nil).
orA_r2.
then (andM_r (2::nil)) init.
then orA_r2 init.
then (copy 4) (then (lunfold_l 1) (then (dagger_l 1)
  (then (wall_l1 1 (w\w) 1) (at_l 1)))).
imp_l 1 (2::3::nil).
then (orA_r2) (then (andM_r (2::nil)) init).
andM_l 1.
then (down_l 2) (then (bang_l 2) (then (copy 1)
  (then (andA_l2 1) (imp_l 1 (3::nil))))).
then at_r init.
then (step_l 2) (then (down_l 2) (then (at_l 2) (then (at_l 1) (andM_l 2)))).
then step_r (then down_r at_r).
andM_r (2::3::nil).
then (andM_r (2::nil)) init.
init.