proposition: Lemma multi_step_enc_c0 : multi_step srs (repeat sz d) (enc_Config c0).
proof: Proof. Proof using. apply: (rt_trans (y := (repeat sz (1 + ab_ub)) ++ [sz] ++ [st] ++ [sr] ++ (repeat sz (1 + ab_ub)))). - have ->: d = 1 + ab_ub + 1 + 1 + 1 + 1 + ab_ub by (rewrite /d; lia). rewrite ?repeat_app -?app_assoc. do ? apply: multi_step_applI. apply /rt_step /stepI_nil. by eauto with in_srs_db nocore. - apply /multi_step_applI /rt_step /stepI_nil. by eauto with in_srs_db nocore. Qed.
imports: List Relation_Operators Operators_Properties PeanoNat Lia ssreflect ssrbool ssrfun