proposition: Lemma move_left {c} : mm2_reaches c0 c -> multi_step srs (enc_Config' c) (enc_Config c).
proof: Proof. move: c => [p [a b]] /[dup] /mm_state_ub ?. move=> /(svalP Hbound (p, (a, b))) ?. apply: multi_step_applI. rewrite ?app_assoc. apply: multi_step_apprI. apply: (rt_trans (y := [sl] ++ (repeat sb a) ++ [sm' p] ++ (repeat sb b) ++ [sr])). - rewrite -?app_assoc. do 2 apply: multi_step_applI. apply: move_sb_left'; by tauto. - rewrite ?app_assoc. do 2 apply: multi_step_apprI. apply: move_sb_left'; by tauto. Qed.
imports: List Relation_Operators Operators_Properties PeanoNat Lia ssreflect ssrbool ssrfun