proposition: Lemma move_sb_right' {p n x y} : p < state_bound -> ((x, y) = (1, 3) \/ (x, y) = (3, 2)) -> multi_step srs ([(x, Some p)] ++ repeat sb n ++ [(y, None)]) ([(x, None)] ++ repeat sb n ++ [(y, Some p)]).
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)] ++ [sb' p] ++ (repeat sb n) ++ [(y, None)])). + have ->: repeat sb (S n) = [sb] ++ repeat sb n by done. rewrite /= -?app_assoc. apply /rt_step /stepI_nil. move: Hxy => [] [-> _]; by eauto with in_srs_db nocore. + rewrite -?app_assoc. apply: multi_step_applI. apply: (rt_trans (y := (repeat sb n) ++ [sb' p] ++ [(y, None)])). * rewrite ?app_assoc. apply: multi_step_apprI. by apply: move_sb_right. * have ->: S n = n + 1 by lia. rewrite repeat_app -?app_assoc. apply /multi_step_applI /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