proposition: Lemma simulate_mm_step {x y} : mm2_reaches c0 x -> mm2_step mm x y -> multi_step srs (enc_Config x) (enc_Config y).
proof: Proof. move=> /[dup] /(Hab_ub x) H'x Hx Hxy. have Hy : mm2_reaches c0 y. { by apply: rt_trans; [apply Hx|apply rt_step]. } move: Hxy => [instr] [Hinstr H]. have := move_right Hx. have := move_left Hy. case: H H'x Hinstr. - move=> p a b /= ?? H'x H'y. have [-> ->]: S ab_ub - a = (ab_ub - a) + 1 /\ S a = 1 + a by lia. rewrite ?repeat_app -?app_assoc. apply: multi_step_applI. apply /rt_step /stepI_nil. by eauto with in_srs_db nocore. - move=> p a b /= ?? H'x H'y. apply: rt_trans; first by eassumption. apply: rt_trans; last by eassumption. have [-> ->]: S b = b + 1 /\ S ab_ub - b = 1 + (S ab_ub - (b + 1)) by lia. rewrite ?repeat_app -?app_assoc. do 5 apply: multi_step_applI. apply /rt_step /stepI_nil. by eauto with in_srs_db nocore. - move=> p q a b /= ?? H'x H'y. have ->: S ab_ub - a = (ab_ub - a) + 1 by lia. rewrite repeat_app -?app_assoc. apply /multi_step_applI /rt_step /stepI_nil. by eauto with in_srs_db nocore. - move=> p q a b /= ?? H'x H'y. apply: rt_trans; first by eassumption. apply: rt_trans; last by eassumption. have [-> ->] : S b = b + 1 /\ S ab_ub - b = 1 + (S ab_ub - (b + 1)) by lia. rewrite ?repeat_app -?app_assoc. do 5 apply: multi_step_applI. apply /rt_step /stepI_nil. by eauto with in_srs_db nocore. - move=> p a b /= ?? H'x H'y. apply /multi_step_applI /rt_step /stepI_nil. by eauto with in_srs_db nocore. - move=> p a b /= ?? H'x H'y. apply: rt_trans; first by eassumption. apply: rt_trans; last by eassumption. do 3 apply: multi_step_applI. apply /rt_step /stepI_nil. by eauto with in_srs_db nocore. Qed.
imports: List Relation_Operators Operators_Properties PeanoNat Lia ssreflect ssrbool ssrfun