repeattac (andM_l 1).
then (copy 1) (then (lunfold_l 1) (then (dagger_l 1)
  (then (wall_l1 1 (w\w) 1) (at_l 1)))).
imp_l 1 (3::4::nil).
then (orA_r1) (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 (copy 3) (then (lunfold_l 1) (then (dagger_l 1)
  (then (wall_l1 1 (w\ (w + 1)) 1) (at_l 1)))).
imp_l 1 (2::4::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_l1 1) (imp_l 1 (3::nil))))).
then at_r init.
at_l 1.
then (step_l 2) (then (down_l 2) (then (at_l 2) (andM_l 2))).
then (copy 7) (then (lunfold_l 1) (then (dagger_l 1)
  (then (wall_l1 1 (w\ (w + 1 + 1)) 1) (at_l 1)))).
imp_l 1 (2::4::nil).
then (orA_r1) (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 (at_l 1) (then (step_l 2) (then (down_l 2) (then (at_l 2) (andM_l 2)))).
then (copy 9) (then (lunfold_l 1) (then (dagger_l 1)
  (then (wall_l1 1 (w\ (w + 1 + 1 + 1)) 1) (at_l 1)))).
imp_l 1 (2::4::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.
at_l 1.
then (step_l 2) (then (down_l 2) (then (at_l 2) (andM_l 2))).
andM_r (1::3::nil).
then (andM_r (1::nil)) init.
init.