proposition: Lemma first_goto_1 {C N: nat} : bound_reachable_n C N -> forall (T: nat) (l r: list Symbol) T' n X Y c Z, In (n, X, Y) gotos -> (c - G) <= C -> T + goto_time C N <= T' -> reachable_n T ([§1] ++ r, §0^c ++ l, basic_state (if c mod (n+1) is 0 then X else Y)) Z -> reachable_n T' (l, §0^c ++ [§1] ++ r, goto n X Y) Z.
proof: Proof. Proof using capped_P. move=> HN T l r T' > /gotos_igotos [?] /(goto_1 HN l r) H => /H => + ? ?. by apply: (reachable_n_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