proposition: Lemma simulate_srs_step {x s t} : step srs s t -> encodes x s -> encodes x t \/ (forall y, mm2_step mm x y -> encodes y t).
proof: Proof. move: x => [p [a b]] [] u v a' b' c' d' H [u'] [v'] [{}t]. rewrite -?/([_] ++ [_] ++ v). move=> [+] [H1t H2t] => /eq2_app_app. have : length t > 1. { move: H1t => /(congr1 (@length _)). rewrite ?map_app ?app_length ?map_length /=. move=> ->. by lia. } move=> Ht /(_ Ht) {Ht}. case; [|case; [|case; [|case]]]. - move=> [u'2 ->]. left. exists (u ++ c' :: d' :: u'2), v', t. constructor; [by rewrite -?app_assoc | done]. - move=> [s2] [?] [? ?]. subst. move: H1t H2t => []. move: H => /srs_specI [|] [] > [] ????; subst; try done; [| |]. + move=> Hi _ H1s2 [<- H2s2]. right. move=> y [?] [/(mm2_instr_at_unique Hi) <-] Hxy. inversion Hxy. subst. eexists u, v', (_ :: _ :: s2). constructor; [done | constructor; by rewrite /= ?H1s2 ?H2s2]. + move=> ? _ _ [<-] _ *. right. move=> y Hxy. exfalso. move: y Hxy. apply /mm2_stop_index_iff => /=. lia. + move=> -> _ _ /= [<-] _. right. move=> y Hxy. exfalso. move: y Hxy. apply /mm2_stop_index_iff => /=. by left. - move=> [s1] [s2] [?] [? ?]. subst. move: H H1t H2t => /srs_specI []. + move=> H + + /ltac:(right). move=> /[dup] [/srs_step_specI] []. * move=> H'. move: H' H => [] ? ? ? ? [] > [] ? ? ? ?; subst; try done; [ | | | ]. ** rewrite app_nil_r /=. move=> Hi [H1] [<-] H2. move=> y [?] [/(mm2_instr_at_unique Hi) <-] Hxy. inversion Hxy. subst. eexists u', v', (_ :: _ :: _). constructor; [done | by rewrite /= H1 H2]. ** rewrite app_nil_r /= ?map_app. move: (a) => [|?]; first done. move=> Hi [] H1 [<-] H2. move=> y [?] [/(mm2_instr_at_unique Hi) <-] Hxy. inversion Hxy. subst. eexists (u' ++ [sz]), v', (_ :: _). rewrite -?app_assoc. constructor; [done | by rewrite /= ?map_app H1 H2]. ** rewrite ?map_app filter_app /= app_nil_r /step. move=> Hi + /(app_inj_tail (y := [])) [H2] [<-]. rewrite ?app_assoc app_nil_r. move=> /app_inj_tail [/app_inj_tail] [H1] _ _. move=> y [?] [/(mm2_instr_at_unique Hi) <-] Hxy. inversion Hxy. subst. eexists u', v', (_ ++ [_; _]). rewrite -?app_assoc. constructor; first done. by rewrite ?map_app filter_app /= H1 H2. ** rewrite [in repeat sb b](ltac:(lia) : b = (b - 1) + 1) repeat_app. rewrite ?map_app ?filter_app ?app_assoc ?app_nil_r /= /step. move=> Hi + /(app_inj_tail (y := [])) [H2] [<-]. move=> /app_inj_tail [/app_inj_tail] [H1] _ _. have -> : b = S (Nat.pred b) by lia. move=> y [?] [/(mm2_instr_at_unique Hi) <-] Hxy. inversion Hxy. subst. eexists u', ([sz] ++ v'), (_ ++ [_]). rewrite (ltac:(lia) : b = 1 + (b - 1)) -?app_assoc /=. constructor; first done. by rewrite ?map_app filter_app /= H1 H2 -?app_assoc. * move: H => + + _ /ltac:(exfalso). move=> [] > [] *; subst; by firstorder done. + move=> + + + /ltac:(left; exists u', v', (s1 ++ c' :: d' :: s2)). move=> /srs_mlr_specE [x] [y] [q] [] [] ? ? ? ? H1t H2t; subst; rewrite -?app_assoc. * constructor; first done. constructor; first by rewrite -H1t ?map_app. move: H2t. by rewrite ?map_app ?filter_app /=. * constructor; first done. constructor; first by rewrite -H1t ?map_app. move: H2t. by rewrite ?map_app ?filter_app /=. - move=> [s1] [?] [? ?]. subst. move: (H1t). rewrite ?map_app ?app_assoc. move=> /app_inj_tail [_]. move: H H1t H2t => /srs_specI [|] [] > [] ? ? ? ?; subst; try done; []. move=> Hi H1s1. rewrite map_app filter_app. move=> /(app_inj_tail (y := [])) [H2s2] [<-] _. right. move=> y [?] [/(mm2_instr_at_unique Hi) <-] Hxy. inversion Hxy. subst. eexists u', v, (s1 ++ [_; _]). rewrite -?app_assoc. constructor; [done | constructor]. * move: H1s1. rewrite ?map_app ?app_assoc. move=> /app_inj_tail [-> _]. by rewrite (ltac:(lia) : S b = b + 1) [repeat _ (b + 1)]repeat_app map_app -?app_assoc. * by rewrite map_app filter_app /= H2s2. - move=> [v'1 ->]. left. exists u', (v'1 ++ c' :: d' :: v), t. constructor; [by rewrite -?app_assoc | done]. Qed.
imports: List Relation_Operators Operators_Properties PeanoNat Lia ssreflect ssrbool ssrfun