proposition: Lemma move_sb_left' {p n x y} : p < state_bound -> ((x, y) = (1, 3) \/ (x, y) = (3, 2)) -> multi_step srs ([(x, None)] ++ repeat sb n ++ [(y, Some p)]) ([(x, Some p)] ++ repeat sb n ++ [(y, None)]).
proof: Proof. move=> ? /= Hxy. case: n. - apply /rt_step /stepI_nil. move: Hxy => [] [-> ->]; by eauto with in_srs_db nocore. - move=> n. apply: (rt_trans (y := [(x, None)] ++ (repeat sb n) ++ [sb' p] ++ [(y, None)])). + rewrite (ltac:(lia) : S n = n + 1) repeat_app -?app_assoc. do ? apply: multi_step_applI. apply /rt_step /stepI_nil. move: Hxy => [] [_ ->]; by eauto with in_srs_db nocore. + rewrite ?app_assoc. apply: multi_step_apprI. apply: (rt_trans (y := [(x, None)] ++ [sb' p] ++ (repeat sb n))). * rewrite -?app_assoc. apply: multi_step_applI. by apply: move_sb_left. * apply /rt_step /stepI_nil. move: Hxy => [] [-> _]; by eauto with in_srs_db nocore. Qed.
imports: List Relation_Operators Operators_Properties PeanoNat Lia ssreflect ssrbool ssrfun