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