proposition: Lemma extend_bounded' {n: nat} {X: config} : bounded' n -> narrow X -> length (get_right X) <= n.
proof: Proof. Proof using confluent_M. move: X => [[A B] x] Hn. elim /(Nat.measure_induction _ (@length symbol)) : A => A IH. case: (stack_eq_dec A []). { move=> -> [y [A']] [Z [+ ?]]. move /Hn. apply. by eassumption. } move /exists_last => [A' [a HA]]. subst A. rename A' into A. move=> [y [A']] [Z [Hx]]. case: (stack_eq_dec A' []). { move=> ->. move: Hx => /reachable_width + /reachable_width => <- /=. by lia. } move /exists_last => [A'' [a' HA']]. subst A'. rename A'' into A'. move: Z Hx => [[A'' B''] z] /[dup] [/remove_rendundant_suffixL]. case. { move=> [x' [B']] /[dup] [/reachable_width] /= HB Hx1 Hx2 Hy. have [Y [HY1 HY2]] := (confluent_M Hx1 Hx2). move: Hy HY2 HY1 => /(@rt_trans config). move=> H /H{H}. move /Hn => H /H{H}. by lia. } move=> /= [A''' [? Hx]]. subst A''. rename A''' into A''. move=> _ /[dup] [/remove_rendundant_suffixL]. case. { move=> [x' [B']]. move=> /[dup] [/reachable_width] /=. rewrite app_length => /= ?. move /Hn. move /(_ _ _ ltac:(apply: rt_refl)) => ?. move: Hx => /reachable_width + /reachable_width => /=. rewrite ?app_length => /=. by lia. } move=> [A''']. move=> [/(@app_inj_tail symbol) [? ?]]. subst. move=> ? _. apply: (IH A). - rewrite app_length /length. by lia. - do 3 eexists. constructor; by eassumption. Qed.
imports: PeanoNat Lia Relation_Operators Operators_Properties List ssreflect ssrfun ssrbool Undecidability.StackMachines.SSM