proposition: Lemma first_step {M} (op : Instruction) (v w: list Symbol) {n X Z} : 1 <= n -> In op M -> let '((r, s, x), (r', s', y), b) := op in X = (r ++ v, s ++ w, x) -> reachable_n M (n-1) (if b is true then (s' ++ w, r' ++ v, y) else (r' ++ v, s' ++ w, y)) Z -> reachable_n M n X Z.
proof: Proof. move=> Hn. move: op=> [[[[r s] x] [[r' s'] y]] b]. move /(transition M v w) /reachable_n_step => + ? ?. subst X. by (apply: (reachable_n_trans' (n-1)); first by lia). Qed.
imports: List Lia Relation_Operators Undecidability.StackMachines.Util(Nat_facts List_facts) Undecidability.StackMachines.Reductions.CM1_HALT_to_SMNdl_UB.SMX ssreflect ssrbool ssrfun