then imp_r (then (orA_l 1) (andM_l 1)). orA_r2. then (copy 12) (then (dagger_l 1) (then (wall_l1 1 (w\w) 1) (at_l 1))). orA_l 1. andM_r (1::3::nil). then orA_r2 (then (andM_r (1::nil)) init). then orA_r1 init. andM_r (1::3::nil). then orA_r1 (then orA_r2 (then (andM_r (1::nil)) init)). then orA_r1 init. then (copy 12) (then (dagger_l 1) (then (wall_l1 1 (w\w) 1) (at_l 1))). orA_l 1. orA_r2. andM_r (1::3::nil). then orA_r1 (then orA_r1 (then (andM_r (1::nil)) init)). then orA_r2 init. orA_r1. andA_r. andM_r (1::3::nil). then (andM_r (1::nil)) init. then orA_r2 init. then (copy 6) (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 (andM_r (1::nil)) init. then step_r (then down_r at_r). andM_l 1. then (down_l 2) (then (bang_l 2) (then (copy 1) (andA_l2 1))). imp_l 1 (3::nil). then at_r init. then (step_l 2) (then (down_l 2) (then (at_l 2) (andM_l 2))). at_l 1. andM_r (1::3::nil). then orA_r2 (then (andM_r (1::nil)) init). then orA_r2 init.