proposition: Lemma init_encodes : exists s, encodes c0 s /\ multi_step srs s (repeat so (1+N)).
proof: Proof. Proof using HN. have [s] : exists s, multi_step srs s (repeat so (1+N)) /\ Forall (fun x => snd x = None) s /\ forall n, nth n s sz = st -> nth (1+n) s sz = sr. { eexists. constructor; [|constructor]; [by eassumption | apply /Forall_repeatI; by tauto |]. move: (1+N) => m n H. exfalso. elim: n m H; first by case. move=> n IH [|m]; [done | by apply: IH]. } move Ht: (repeat so (1+N)) => t [/rt_rt1n Hst] []. elim: Hst Ht; first by move=> ? <- /Forall_cons_iff []. move=> {}s {}t > Hst Ht IH /IH {IH}. case: Hst Ht => u v a b c d /In_srs_stE [|[]]. - move=> [] <- <- <- <- _ IH. move=> /Forall_app [Hu] /Forall_cons_iff [_] /Forall_cons_iff [_ Ht] Huv. apply: IH. + apply /Forall_app. by do ? constructor. + move=> n. have := Huv n. elim: (u) n; first by move=> [|[|n]]. clear. move=> x {}u IH [|n]; last by move/IH. move: (u) => [|? ?]; [by move=> H /H | done]. - move=> [] <- <- <- <- /rt_rt1n Ht _ _ /(_ (1 + length u)). do 2 (rewrite app_nth2; first by lia). rewrite (ltac:(lia) : 1 + length u - length u = 1). rewrite (ltac:(lia) : 1 + (1 + length u) - length u = 2). move=> /(_ ltac:(done)) Hv. eexists. constructor; last by eassumption. move: (v) Hv => [|? v']; first done. move=> /= ->. exists u, v', [sl' 1; sm; sr]. constructor; [done | by constructor]. - move=> H _ _ /Forall_app [_] /Forall_cons_iff [+] /Forall_cons_iff [+] _. by move: a b H => [? [?|]] [? [?|]]. Qed.
imports: List Relation_Operators Operators_Properties PeanoNat Lia ssreflect ssrbool ssrfun