proposition: Lemma reachable_SnE {M n X Z} : reachable_n M (1+n) X Z -> X = Z \/ (exists Y, step M X Y /\ reachable_n M n Y Z).
proof: Proof. move Hn': (1+n) => n' HXY. case: HXY Hn'; first by (move=> *; left). move=> {}n' *. right. have ->: n = n' by lia. by firstorder done. Qed.
imports: Arith Lia Relation_Operators Operators_Properties List Undecidability.StackMachines.Util(Nat_facts List_facts) Undecidability.StackMachines.SMN ssreflect ssrbool ssrfun