proposition: Lemma maybe_first_goto_1 T l r T' n X Y c Z : T + maybe_goto_1_time <= T' -> maybe_reachable T ([§1] ++ r, §0^c ++ l, basic_state (if c mod (n+1) is 0 then X else Y)) Z -> maybe_reachable T' (l, §0^c ++ [§1] ++ r, goto n X Y) Z.
proof: Proof. Proof using NP_spec. move=> ? ?. have := maybe_goto_1 l r n X Y c. by (apply: (maybe_reachable_trans' T); first by lia). 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