proposition: Lemma left_marker_nth q t n : not (nth_error (encode_config q t) (S n) = Some ⦇).
proof: Proof. move: t => [[ls a] rs] /=. elim /rev_ind: ls n. - move=> [|[|n]] /=; [by case: a|done|]. elim: rs n. { by move=> [|[|?]]. } move=> r rs IH [|n]; first by case: r. by apply: IH. - move=> l ls IH [|n]; rewrite map_app rev_app_distr; first by case: l. by apply: IH. Qed.
imports: Undecidability(TM.SBTM TM.Util.SBTM_facts) Undecidability(StringRewriting.Reductions.SBTM_HALT_to_SR) PeanoNat Lia List ssreflect ssrbool ssrfun