andM_l 1.
then (copy 3) (then (lunfold_l 1) (then (dagger_l 1)
  (then (wall_l1 1 (w\ (w + 2)) 1) (at_l 1)))).
imp_l 1 (2::3::nil).
then (orA_r2) (then (andM_r (1::nil)) init).
andM_l 1.
then (down_l 2) (bang_l 2).
then (step_l 1) (then (down_l 1) (then (at_l 1) (andM_l 1))).
then (copy 5) (then (lunfold_l 1) (then (dagger_l 1)  (then (wall_l1 1 (w\ (w + 3)) 1) (at_l 1)))).
imp_l 1 (2::3::nil).
then (orA_r1) (then (orA_r2) (then (andM_r (2::nil)) init)).
andM_l 1.
then (down_l 2) (bang_l 2).
then (step_l 1) (then (down_l 1) (then (at_l 1) (andM_l 1))).
then (andM_r (2::nil)) init.