proposition: Lemma encode_config_eq_app q ls a rs u v a' q' : encode_config q (ls, a, rs) = u ++ [#a'; encode_state q'] ++ v -> q = q' /\ a = a' /\ u = ⦇ :: rev (map encode_symbol ls) /\ v = (map encode_symbol rs) ++ [⦈].
proof: Proof. move: u => [|c u]. { by case: a'. } move=> /= [<-]. elim /rev_ind: ls u => /=. { move=> [|{}c u]. { move=> [] /encode_symbol_inj ? /Fin.to_nat_inj ? <-. tauto. } move: u => [|c' u]. { by case: (a'). } move=> [] _ _ E. exfalso. have : In (encode_state q') (u ++ # a' :: encode_state q' :: v). { apply /in_app_iff => /=. tauto. } rewrite -E. elim: rs {E}. { by case. } by move=> [] rs IH /= []. } move=> l ls IH u. rewrite map_app rev_unit. move: u => [|{}c u]. - move=> [] _. elim /rev_ind: (ls). + move=> []. by case: (a). + move=> {}c > _. rewrite map_app rev_unit. move=> []. by case: (c). - move=> [<-] /IH [<-] [<-] [[-> ->]]. tauto. Qed.
imports: Undecidability(TM.SBTM TM.Util.SBTM_facts) PeanoNat Lia List ssreflect ssrbool ssrfun