proposition: Lemma simulate_mm_halting {x} : mm2_reaches c0 x -> (forall y, not (mm2_step mm x y)) -> multi_step srs (enc_Config x) (repeat so d).
proof: Proof. move: x => [p [a b]]. move=> /[dup] /Hab_ub /= ?. move=> Hx H'x. apply: (rt_trans (y := (repeat sz (ab_ub - a)) ++ [so] ++ [so] ++ _)). - rewrite (ltac:(lia) : S ab_ub - a = (ab_ub - a) + 1) repeat_app -?app_assoc. apply /multi_step_applI /rt_step /stepI_nil. move: p Hx H'x => [|p]. + move=> *. by eauto with in_srs_db nocore. + move=> /mm_state_ub Hx H'x. have ? : S (length mm) <= (S p) < state_bound. { split; [|done]. suff: not (p < length mm) by lia. move=> /nth_error_Some. case Hinstr: (nth_error mm p) => [instr|]; [|done]. have [y Hxy] := mm2_progress instr (S p, (a, b)). move=> _. apply: (H'x y). exists instr. split; [|done]. move: Hinstr => /(@nth_error_split mm2_instr) [?] [?] [-> <-]. by do 2 eexists. } by eauto with in_srs_db nocore. - apply: (rt_trans (y := (repeat so (ab_ub - a + 1) ++ [so] ++ repeat sb a ++ [sm] ++ repeat sb b ++ [sr] ++ repeat sz (S ab_ub - b)))). + rewrite ?app_assoc. do 6 apply: multi_step_apprI. by apply: multi_step_repeat_solI. + have ->: d = (ab_ub - a + 1) + 1 + a + 1 + b + 1 + (S ab_ub - b) by (rewrite /d; lia). rewrite ?repeat_app -?app_assoc. do 2 apply: multi_step_applI. apply: multi_step_repeat_sorI'; first by left. apply: (rt_trans (y := ([so] ++ [so] ++ repeat sb b ++ [sr] ++ repeat sz (S ab_ub - b)))). * apply /rt_step /stepI_nil. by eauto with in_srs_db nocore. * apply: multi_step_applI. apply: multi_step_repeat_sorI'; first by left. apply: (rt_trans (y := ([so] ++ [so] ++ repeat sz (S ab_ub - b)))). ** apply /rt_step /stepI_nil. by eauto with in_srs_db nocore. ** apply: multi_step_applI. apply: multi_step_repeat_sorI. by right. Qed.
imports: List Relation_Operators Operators_Properties PeanoNat Lia ssreflect ssrbool ssrfun