proposition: Lemma to_SR2ab : multi_step srs (repeat sz (1+(d - 1))) (repeat so (1+(d - 1))).
proof: Proof. Proof using Hc0c'0 Hc'0. have H'y := simulate_mm_halting Hc0c'0 Hc'0. apply: rt_trans; last by eassumption. apply: rt_trans; first by apply: (multi_step_enc_c0). move: (Hc0c'0) => /(@clos_rt_rtn1 mm2_state). elim. { by apply: rt_refl. } move=> > /simulate_mm_step IH /(@clos_rtn1_rt mm2_state) /IH. move=> *. by apply: rt_trans; eassumption. Qed.
imports: List Relation_Operators Operators_Properties PeanoNat Lia ssreflect ssrbool ssrfun