proposition: Lemma iter_cm_step {C N: nat} : bound_reachable_n C N -> forall l r n, let p := (Nat.iter n (CM1.step P) cm_start) in CM.value p <= G + C -> reachable_n (n * (step_time C N)) ([§1] ++ l, [§0] ++ [§1] ++ (§0^(CM.value p - 1)) ++ r, '#?0) ([§1] ++ l, §0^(CM.value p) ++ [§1] ++ r, '#?(CM.state p)).
proof: Proof. Proof using capped_P. move=> HN l r n. elim: n l r => [l r _ _ | n] /=; first by apply: reach_refl. have := CM_facts.run_value_monotone P cm_start n. set p := (Nat.iter n (CM1.step P) cm_start) => Hp IH l r ?. rewrite /cm_start /= in Hp. have ? : CM.value p <= CM.value (CM1.step P p) by apply: CM_facts.step_value_monotone. have := IH l (§0^(CM.value (CM1.step P p) - CM.value p) ++ r) ltac:(lia). apply: (reachable_n_trans' (step_time C N)); [by lia | by rewrite ?app_norm; do 6 f_equal; lia |]. by have := do_cm_step HN l r p ltac:(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