then (andM_l 1) (andM_l 2).
delta_r.
then down_r at_r.
then (copy 1) (then (lunfold_l 1) (then (dagger_l 1)
  (then (wall_l1 1 (w\w) 1) (at_l 1)))).
imp_l 1 (2::4::nil).
then (orA_r1) (then (orA_r2) (then (andM_r (1::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))).
andA_r.
andM_r (2::3::nil).
then (andM_r (2::nil)) init.
then orA_r1 init.
then delta_r (then down_r at_r).
then (copy 5) (then (lunfold_l 1) (then (dagger_l 1)
  (then (wall_l1 1 (w\ (w + 2)) 1) (at_l 1)))).
imp_l 1 (3::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) (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 + 3)) 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) (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))).
andM_r (2::3::nil).
then (andM_r (2::nil)) init.
then orA_r1 init.