proposition: Lemma list_symbol_shape (l: list Symbol) : (exists n, l = §0^n) \/ (exists n l', l = §0^n ++ [§1] ++ l').
proof: Proof. elim: l; first by (left; exists 0). move=> [|] l +; last by (right; by exists 0, l). by move=> [[n ->] | [n] [l' ->]]; [left | right]; exists (1+n); [| exists l']. Qed.
imports: Relation_Operators Operators_Properties Lia PeanoNat List Undecidability.StackMachines.Reductions.CM1_HALT_to_SMNdl_UB.SMX_facts Undecidability.StackMachines.Util(Nat_facts List_facts) ssreflect ssrbool ssrfun