proposition: Lemma maybe_goto_1 l r n X Y m : maybe_reachable maybe_goto_1_time (l, §0^m ++ [§1] ++ r, goto n X Y) ([§1] ++ r, §0^m ++ l, basic_state (if m mod (n+1) is 0 then X else Y)).
proof: Proof. Proof using NP_spec. rewrite /maybe_goto_1_time. have := in_dec _ (n, X, Y) gotos. move=> /(_ ltac:(do 4 decide equality)) [| ?]; first last. { apply: terminal_maybe_reachable. by apply: not_in_gotos_terminal. } have [? | ?]: m <= G + CP \/ G + CP < m by lia. { move=> /gotos_igotos => [[i]] /(goto_1 HTP l r) => /(_ m ltac:(lia)) /reachable_n_maybe_reachable. apply: maybe_reachable_mon'; [by lia | done]. } move=> ?. apply: maybe_goto_1_far; 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