proposition: Lemma goto_1 {C N: nat} : bound_reachable_n C N -> forall l r i n X Y c, In (i, (n, X, Y)) igotos -> (c - G) <= C -> reachable_n (goto_time C N) (l, §0^c ++ [§1] ++ r, goto n X Y) ([§1] ++ r, §0^c ++ l, basic_state (if c mod (n+1) is 0 then X else Y)).
proof: Proof. Proof using capped_P. move=> HN l r i n X Y c Hi HC. suff: reachable_n ((c+1-G)*(N+2)+1) (l, §0^c ++ [§1] ++ r, goto n X Y) ([§1] ++ r, §0^c ++ l, basic_state (if c mod (n+1) is 0 then X else Y)). { apply: reachable_n_mon'; [ by (rewrite /goto_time; nia) | done ]. } elim /(Nat.measure_induction _ id): c l r HC => c IH l r HcC. have [HcG | HcG]: c < G \/ c >= G by lia. { apply: (first_step (goto_spec_1 c (i, (n, X, Y))) l r); [by lia | by auto with M | by rewrite ?app_norm | by apply: reach_refl ]. } apply: (first_step (goto_spec_G (i, (n, X, Y))) l (§0^(c-G) ++ [§1] ++ r)); [ by nia | by auto with M | by rewrite ?app_norm; do 4 f_equal; lia | ]. have := HN (c - G) (§0^i ++ [§1] ++ §0^(G - 2 - i) ++ l) r ltac:(lia). apply: (reachable_n_trans' ((c-G)*(N+2)+2)); [ by nia | by rewrite ?app_norm | ]. apply: (first_step (bound_yes_spec (i, (n, X, Y))) l (§0^(c - G) ++ [§1] ++ r)); [ by nia | by auto with M | by rewrite ?app_norm | ]. have ? : G >= 4 by rewrite /G; lia. have := IH (c - (n+1)) ltac:(lia) (§0^(n+1) ++ l) r ltac:(lia). apply: reachable_n_mon'; first by lia. rewrite ?app_norm. have ? := igotos_capped Hi. do 5 f_equal; [lia ..|]. have Hcn : c - (n + 1) + (n + 1) = c by lia. by rewrite -[in RHS]Hcn add_mod mod_same Nat.add_0_r mod_mod. 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