Require Import PeanoNat Lia Relation_Operators Operators_Properties List.
Import ListNotations.

Require Import ssreflect ssrfun ssrbool.

Require Import Undecidability.StackMachines.SSM.

From Undecidability.StackMachines.Util Require Import Facts.

Set Default Proof Using "Type".
Set Default Goal Selector "!".

Definition width : config := '(A, B, _) length A + length B.

Lemma stack_eq_dec (A B: stack) : {A = B} + {A B}.
Proof. by do 2 (decide equality). Qed.


Section CSSM.

Context {M : ssm}.
Variable confluent_M : confluent M.
Arguments confluent_M {X }.

Lemma reachable_app {x x': state} {A B A' B' C D: stack} :
  reachable M (A, B, x) (A', B', x') reachable M (AC, BD, x) (A'C, B'D, x').
Proof.
  move HX: (A, B, x) X. move HX': (A', B', x') X'.
  move H. elim: H C D x x' A B A' B' HX HX'; clear.
  - move X X'. case; clear.
    + move > H >. case . case .
      apply: rt_step. by apply: step_l.
    + move > H >. case . case .
      apply: rt_step. by apply: step_r.
  - move > . case .
    by apply: rt_refl.
  - move X [[A' B'] x'] Z ? IHXY ? IHYZ *.
    apply: rt_trans; [by apply: IHXY | by apply: IHYZ].
Qed.


Definition equiv (X Y: config) := (Z: config), reachable M X Z reachable M Y Z.

Lemma equiv_refl {X: config} : equiv X X.
Proof. exists X. constructor; by apply: rt_refl. Qed.

Lemma equiv_sym {X Y: config} : equiv X Y equiv Y X.
Proof. constructor; move [Z [? ?]]; exists Z; by constructor. Qed.

Lemma equiv_trans {X Y Z: config} : equiv X Y equiv Y Z equiv X Z.
Proof using confluent_M.
  move [ [? ]] [ [ ?]].
  have [ [? ?]] := (confluent_M ).
  exists . constructor; apply: rt_trans; by eassumption.
Qed.


Lemma equiv_app {x x': state} {A B A' B' C D: stack} : equiv (A, B, x) (A', B', x')
  equiv (AC, BD, x) (A'C, B'D, x').
Proof.
  move [[[A'' B''] x''] [? ?]].
  exists (A''C, B''D, x''). constructor; by apply: reachable_app.
Qed.


Corollary equiv_appR {x x': state} {A B A' B': stack} {b: bool} : equiv (A, B, x) (A', B', x')
  equiv (A, B [b], x) (A', B' [b], x').
Proof. move /(equiv_app (C := []) (D := [b])). by rewrite ? app_nil_r. Qed.

Corollary equiv_appL {x x': state} {A B A' B': stack} {a: bool} : equiv (A, B, x) (A', B', x')
  equiv (A[a], B, x) (A'[a], B', x').
Proof. move /(equiv_app (C := [a]) (D := [])). by rewrite ? app_nil_r. Qed.

Fixpoint enum_stacks (n: ) : list stack :=
  if n is S n then (map (cons true) (enum_stacks n)) (map (cons false) (enum_stacks n)) else [[]].

Lemma enum_stacksP {A: stack} : In A (enum_stacks (length A)).
Proof.
  elim: A /=; first by left.
  move a A IH. rewrite in_app_iff ? in_map_iff.
  case: a; [left | right]; exists A; by constructor.
Qed.


Fixpoint enum_states (M': ssm) : list state :=
  match M' with
  | [] []
  | (x, y, _, _, _) :: M' x :: y :: enum_states M'
  end.

Lemma enum_statesP {x y: state} {a b: symbol} {d: dir} : In (x, y, a, b, d) M
  In x (enum_states M) In y (enum_states M).
Proof.
  elim: M x y a b d /=; clear; first done.
  move i M IH >. case.
  - move . constructor; [by left | by right; left].
  - move /IH [? ?]. move: i [[[[? ?] ?] ?] ?]. constructor; right; by right.
Qed.


Definition get_state : config state :=
   '(_, _, x) x.

Lemma enum_states_step {X Y: config} : step M X Y
  In (get_state X) (enum_states M) In (get_state Y) (enum_states M).
Proof.
  case > /enum_statesP [? ?]; by constructor.
Qed.


Lemma enum_states_reachable {X Y: config} : reachable M X Y
  X = Y (In (get_state X) (enum_states M) In (get_state Y) (enum_states M)).
Proof.
  elim.
  - move ? ? /enum_states_step ?. by right.
  - move ?. by left.
  - move > _ + _. case.
    + move . case; [move ; by left | move ?; by right].
    + move [? ?]. case; [move | move [? ?]]; by right.
Qed.


Definition enum_configs (lA lB: ) : list config :=
  list_prod (list_prod (enum_stacks lA) (enum_stacks lB)) (enum_states M).

Lemma enum_configsP (x: state) (A B: stack) : In x (enum_states M)
  In (A, B, x) (enum_configs (length A) (length B)).
Proof.
  move Hx. rewrite /enum_configs ? in_prod_iff.
  have ? := enum_stacksP. by (constructor; first by constructor).
Qed.


Definition space (X: config) : list config :=
  X :: flat_map ( i enum_configs i (width X - i)) (seq 0 (width X + 1)).

Lemma reachable_width {X Y: config} : reachable M X Y width X = width Y.
Proof.
  elim; clear.
  - move X Y. case *; rewrite /width /length; by .
  - done.
  - move *. by .
Qed.


Lemma spaceP {X Y: config} : In (get_state X) (enum_states M) width X = width Y In X (space Y).
Proof.
  rewrite /space. case: X [[A B] x]. move HX . right.
  apply /in_flat_map. exists (length A). constructor /=.
  { apply /in_seq. by . }
  have : (length A + length B - length A = length B) by .
  by apply: enum_configsP.
Qed.


Lemma spaceP0 {X Y: config} : reachable M X Y In Y (space X).
Proof.
  move /copy [/enum_states_reachable + /reachable_width]. case.
  - move _. by left.
  - move [_ /spaceP] + ?. by apply.
Qed.


Lemma space_equivP {X Y: config} : equiv X Y In Y (space X).
Proof.
  move [Z] /copy [[/reachable_width + /reachable_width]] /spaceP HY.
  move [/enum_states_reachable + /enum_states_reachable]. case.
  - move . case.
    + move . by left.
    + move [? ?]. by apply: HY.
  - move [? ?]. case.
    + move ?. subst Z. by apply: HY.
    + move [? ?]. by apply: HY.
Qed.


Definition get_left : config stack :=
   '(A, _, _) A.

Definition get_right : config stack :=
   '(_, B, _) B.

Lemma step_dec (X Y: config) : decidable (step M X Y).
Proof.
  case: (Exists_dec ( '(x, y, a, b, d)
    (get_state X, get_state Y, if d then get_left X else b :: get_left X, if d then b :: get_right X else get_right X) =
    (x, y, if d then a :: get_left Y else get_left Y, if d then get_right Y else a :: get_right Y)) M).
  - move [[[[x y] a] b] d]. do 4 (decide equality).
  - move H. left. move: H. rewrite Exists_exists.
    move [[[[[x y] a] b] d]]. case: d.
    + move [?]. move: X Y [[A ?] ?] [[? B] ?] /=. case: A; case: B //=.
      move >. case *. subst.
      by apply: step_l.
    + move [?]. move: X Y [[? B] ?] [[A ?] ?] /=. case: A; case: B //=.
      move >. case *. subst.
      by apply: step_r.
  - move H. right. move HXY. apply: H. rewrite Exists_exists. case: HXY.
    + move x y a b A B H. exists (x, y, a, b, true) /=. by constructor.
    + move x y a b A B H. exists (x, y, b, a, false) /=. by constructor.
Qed.


Inductive reachable_n : config config Prop :=
  | rn_refl n X : reachable_n n X X
  | rn_step n X Y Z: reachable_n n X Y step M Y Z reachable_n (1+n) X Z.

Lemma reachable_0E {X Y} : reachable_n 0 X Y X = Y.
Proof.
  move Hn: (0) n HXY. case: HXY Hn; first done. by .
Qed.


Lemma reachable_SnE {n X Z} : reachable_n (1+n) X Z
  X = Z ( Y, reachable_n n X Y step M Y Z).
Proof.
  move Hn': (1+n) n' HXY. case: HXY Hn'.
  - move *. by left.
  - move {}n' *. right. have : n = n' by . by firstorder done.
Qed.


Lemma reachable_to_reachable_n {X Y} : reachable M X Y n, reachable_n n X Y.
Proof.
  move /(@clos_rt_rtn1 config). elim.
  - exists 0. by apply: rn_refl.
  - move > ? _ [n ?]. exists (1+n). apply: rn_step; by eassumption.
Qed.


Lemma reachable_n_to_reachable {n X Y} : reachable_n n X Y reachable M X Y.
Proof.
  elim.
  - move *. by apply: rt_refl.
  - move *. apply: rt_trans; first by eassumption.
    by apply: rt_step.
Qed.


Lemma reachable_n_monotone {X Y m n} : m n reachable_n m X Y reachable_n n X Y.
Proof.
  elim: n m X Y.
  { move m > ?. have : m = 0 by . move /reachable_0E . by apply: rn_refl. }
  move n IH [|m] > ?.
  { move /reachable_0E . by apply: rn_refl. }
  move /reachable_SnE. case.
  - move . by apply: rn_refl.
  - move [Z [? ?]]. apply: rn_step; last by eassumption.
    apply: IH; last by eassumption. by .
Qed.


Lemma reachable_n_dec (n: ) (X Y: config) : decidable (reachable_n n X Y).
Proof.
  elim: n X Y.
  { move X Y. have : {X = Y} + {X Y} by do 4 (decide equality). case.
    - move . left. by apply: rn_refl.
    - move ?. right. by move /reachable_0E. }
  move n IH X Y.
  have : {X = Y} + {X Y} by do 4 (decide equality). case.
  { move . left. by apply: rn_refl. }
  move ?.
  case: (Exists_dec ( Z reachable_n n X Z step M Z Y) (space X)).
  - move Z. have := IH X Z. have := step_dec Z Y. by firstorder done.
  - move + /ltac:(left). rewrite Exists_exists. move [?] [?] [?] ?.
    apply: rn_step; by eassumption.
  - move H. right. move /reachable_SnE. case; first done.
    move [Z [? ?]]. apply: H. rewrite Exists_exists. exists Z.
    constructor; last by constructor.
    apply: spaceP0. apply: reachable_n_to_reachable. by eassumption.
Qed.


Lemma reachable_n_bounded {X Y: config} {n: } {L: list config} :
  ( Z, reachable_n n X Z In Z L) reachable_n n X Y
  reachable_n (length L) X Y.
Proof.
  elim /(measure_ind id): n L X Y. case.
  { move /= *. apply: reachable_n_monotone; last by eassumption. by . }
  move n IH L X Y HL. case: (reachable_n_dec n X Y) HXY.
  { move _. apply: (IH n ltac:()); last by eassumption.
    move ? ?. apply: HL. apply: reachable_n_monotone; last by eassumption. by . }
  move . have := HL _ . move /(@in_split config) [ [ ?]]. subst L.
  move: /reachable_SnE. case.
  { move . by apply: rn_refl. }
  move [Z [HXZ HZY]]. rewrite ?app_length /length -?/(length _).
  have : (length + S (length )) = 1 + length ( ) by rewrite app_length; .
  apply: rn_step; last by eassumption.
  apply: (IH n ltac:()); last by eassumption.
  move Z' HXZ'. have HYZ' : Y Z' by move ?; subst.
  move: HXZ' HYZ' /reachable_n_monotone /(_ (1+n) ltac:()) /HL.
  rewrite ?in_app_iff /In -?/(In _ _). clear. by firstorder done.
Qed.


Lemma reachable_dec (X Y: config) : decidable (reachable M X Y).
Proof.
  have := reachable_n_dec (length (space X)) X Y. case HXY; [left | right].
  - apply: reachable_n_to_reachable. by eassumption.
  - move /reachable_to_reachable_n [n ]. apply: HXY. apply: reachable_n_bounded; last by eassumption.
    move *. apply: spaceP0. apply: reachable_n_to_reachable. by eassumption.
Qed.


Lemma equiv_dec (X Y: config) : decidable (equiv X Y).
Proof.
  case: (Exists_dec ( Z reachable M X Z reachable M Y Z) (space X)).
  - move Z. case: (reachable_dec X Z) ?; case: (reachable_dec Y Z) ?; by firstorder done.
  - move + /ltac:(left). rewrite Exists_exists. move [Z [? ?]].
    eexists. by eassumption.
  - move + /ltac:(right) + [Z [? ?]]. apply. rewrite Exists_exists.
    exists Z. constructor; [by apply: spaceP0 | by constructor].
Qed.


Definition narrow (X: config) := (x: state) (A: stack), equiv X (A, [], x).

Lemma narrow_dec (X: config) : decidable (narrow X).
Proof.
  case: (Exists_dec ( Y get_right Y = [] equiv X Y) (space X)).
  - move [[A + ] y]. case; first last.
    { move >. right. by move [+]. }
    case: (equiv_dec X (A, [], y)).
    + move ?. by left.
    + move ?. right. by move [_].
  - move + /ltac:(left). rewrite Exists_exists. move [[[A B] y] [_]] /= [] ?.
    by exists y, A.
  - move + /ltac:(right) + [y [A HX]]. rewrite Exists_exists. apply.
    exists (A, [], y). constructor; last done.
    by apply: space_equivP.
Qed.


Lemma narrow_appL {x: state} {A B: stack} {a: bool} : narrow (A, B, x) narrow (A [a], B, x).
Proof.
  move [y [A']].
  move /(equiv_app (C := [a]) (D := [])). rewrite ? app_nil_r ?.
  do 2 eexists. by eassumption.
Qed.


Lemma remove_rendundant_suffixL {x: state} {A B: stack} {a: symbol} {Y: config}: reachable M (A[a], B, x) Y
  ( (x': state) (B': stack), reachable M (A[a], B, x) ([], B', x'))
  ( (C: stack), get_left Y = C [a] reachable M (A, B, x) (C, get_right Y, get_state Y)).
Proof.
  move HX: (A [a], B, x) X H. elim: H x A B a HX.
  - move ? ?. case.
    + move x y a b. case.
      * move B ? > _. left. exists y, (b::B). apply: rt_step. by apply: step_l.
      * move a' A B ? >.
        have [A'' [a'' ]] := (@exists_last _ (a' :: A) ltac:(done)).
        case. rewrite app_comm_cons. move /(@app_inj_tail symbol). case ? ? ? ?. subst.
        right. exists A''. constructor; first done.
        apply: rt_step. by apply: step_l.
    + move > ? >. case . right. eexists. constructor.
      * rewrite app_comm_cons. by reflexivity.
      * apply: rt_step. by apply: step_r.
  - move > . right. eexists. constructor; first by reflexivity.
    by apply: rt_refl.
  - move {}X {}[[A' B'] x'] Z. move _ _ x A B a ?. subst.
    case: ( x A B a ltac:(done)).
    { move ?. by left. }
    move /= [C' [? Hxx']]. subst.
    case: ( x' C' B' a ltac:(done)).
    + move [x'' [B'' ?]]. left.
      exists x'', B''. apply: rt_trans; last by eassumption.
      have : (B = B []) by rewrite app_nil_r.
      have : (B' = B' []) by rewrite app_nil_r.
      by apply: reachable_app.
    + move [C'' [? ?]]. right. exists C''. constructor; first done.
      apply: rt_trans; by eassumption.
Qed.


Lemma remove_rendundant_suffixR {x: state} {A B: stack} {b: symbol} {Y: config} : reachable M (A, B[b], x) Y
  ( (x': state) (A': stack), reachable M (A, B[b], x) (A', [], x'))
  ( (D: stack), get_right Y = D [b] reachable M (A, B, x) (get_left Y, D, get_state Y)).
Proof.
  move HX: (A, B [b], x) X H. elim: H x A B b HX.
  - move ? ?. case.
    + move > ? >. case . right. eexists. constructor.
      * rewrite app_comm_cons. by reflexivity.
      * apply: rt_step. by apply: step_l.
    + move x y a b A. case.
      * move ? > _. left. exists y, (a::A). apply: rt_step. by apply: step_r.
      * move b' B ? >.
        have [B'' [b'' ]] := (@exists_last _ (b' :: B) ltac:(done)).
        case ?. rewrite app_comm_cons. move /(@app_inj_tail symbol). case ? ? ?. subst.
        right. exists B''. constructor; first done.
        apply: rt_step. by apply: step_r.
  - move > . right. eexists. constructor; first by reflexivity.
    by apply: rt_refl.
  - move {}X {}[[A' B'] x'] Z. move _ _ x A B b ?. subst.
    case: ( x A B b ltac:(done)).
    { move ?. by left. }
    move /= [D' [? Hxx']]. subst.
    case: ( x' A' D' b ltac:(done)).
    + move [x'' [A'' ?]]. left.
      exists x'', A''. apply: rt_trans; last by eassumption.
      have : (A = A []) by rewrite app_nil_r.
      have : (A' = A' []) by rewrite app_nil_r.
      by apply: reachable_app.
    + move [D'' [? ?]]. right. exists D''. constructor; first done.
      apply: rt_trans; by eassumption.
Qed.


Lemma bounded_stack_difference {n: } {x y: state} {A B C D: stack} : bounded M n reachable M (A, B, x) (C, D, y)
  length B length D + n length D length B + n.
Proof.
  move /(_ (A, B, x)) [L [ ]]. move /reachable_to_reachable_n [m].
  move /(reachable_n_bounded (L := L)). apply: unnest.
  { move *. apply: . apply: reachable_n_to_reachable. by eassumption. }
  move /reachable_n_monotone /(_ n ltac:()). clear m L.
  elim: n x y A B C D.
  { move > /reachable_0E [] *. subst. by . }
  move n IH x y A B C D /reachable_SnE. case.
  { move [] *. subst. by . }
  move [[[C' D'] z]] [/IH] {}IH.
  move HZ: (C', D', z) Z. move HY: (C, D, y) Y HZY.
  case: HZY HZ HY.
  - move > _ [] ? ? ? [] ? ? ?. subst. move: IH. rewrite /length -?/(length _). by .
  - move > _ [] ? ? ? [] ? ? ?. subst. move: IH. rewrite /length -?/(length _). by .
Qed.


Definition bounded' (n: ) : Prop := (c: config) (x y: state) (A B: stack),
  reachable M (A, [], x) c reachable M ([], B, y) c length B n.

Lemma length_flat_map_le {X: Type} {f g: list X} {l1 l2: } :
  ( i, length (f i) length (g i))
  length (flat_map f (seq 0 )) length (flat_map g (seq 0 )).
Proof.
  move: (X in (seq X)) i. move + Hfg. elim: i.
  {move /= *. by . }
  move IH i ?. have : ( = S ( - 1)) by .
  move /=. rewrite ? app_length.
  have := (IH ( - 1) (S i) ltac:()).
  have := (Hfg i). by .
Qed.


Lemma length_enum_stacks {l: } : length (enum_stacks l) = Nat.pow 2 l.
Proof.
  elim: l; first done.
  move l /=. rewrite app_length ? map_length. move . by .
Qed.


Lemma length_enum_configs {lA lB} : length (enum_configs lA lB) = length (enum_stacks lA) * length (enum_stacks lB) * length (enum_states M).
Proof. by rewrite /enum_configs ? prod_length. Qed.

Lemma space_length {X Y: config} :
  width X width Y length (space X) length (space Y).
Proof.
  rewrite /space /=. move: (width X) . move: (width Y) . clear.
  move H. apply: le_n_S.
  apply: length_flat_map_le; first by .
  move i. rewrite ? length_enum_configs ? length_enum_stacks.
  have ?: 2 ^ ( - i) 2 ^ ( - i).
  { apply: Nat.pow_le_mono_r; by . }
  suff : 2 ^ i * 2 ^ ( - i) 2 ^ i * 2 ^ ( - i) by nia.
  by nia.
Qed.


Theorem reachable_suffixes (X: config) :
  ( A x y B, reachable M X (A, [], x) reachable M X ([], B, y))
  ( AX a, get_left X = AX [a] Y, reachable M X Y AY, get_left Y = AY [a]
    reachable M (AX, get_right X, get_state X) (AY, get_right Y, get_state Y))
  ( BX b, get_right X = BX [b] Y, reachable M X Y BY, get_right Y = BY [b]
    reachable M (get_left X, BX, get_state X) (get_left Y, BY, get_state Y)).
Proof.
  case: (Exists_dec ( Y get_right Y = [] reachable M X Y) (space X)).
  { move [[A +] x]. case; first last.
    - move >. right. by move [? ?].
    - case: (reachable_dec X (A, [], x)); first last.
      + move >. right. by move [? ?].
      + move ?. by left. }
  1: case: (Exists_dec ( Y get_left Y = [] reachable M X Y) (space X)).
  { move [[+ B] x]. case; first last.
    - move >. right. by move [? ?].
    - case: (reachable_dec X ([], B, x)); first last.
      + move >. right. by move [? ?].
      + move ?. by left. }
  all: rewrite ?Exists_exists.
  - move [[[ ] ]] + [[[ ] ]] /= [[_ [? ?]]] [_ [? ?]]. subst.
    left. do 4 eexists. constructor; by eassumption.
  - move HX _. right. left. case: (stack_eq_dec (get_left X) []).
    { move ?. exfalso. apply: HX. exists X. constructor; first by left.
      constructor; first done. apply: rt_refl. }
    move /exists_last [A [a HAa]]. exists A, a. constructor; first done.
    move Y. move: X HX HAa [[AX BX] xX] HX /= HAa. subst.
    case /remove_rendundant_suffixL; last done.
    move [x' [B' ?]]. exfalso. apply: HX. exists ([], B', x').
    constructor; first by apply: spaceP0.
    by constructor.
  - move HX. right. right. case: (stack_eq_dec (get_right X) []).
    { move ?. exfalso. apply: HX. exists X. constructor; first by left.
      constructor; first done. apply: rt_refl. }
    move /exists_last [B [b HBb]]. exists B, b. constructor; first done.
    move Y. move: X HX HBb [[AX BX] xX] HX /= HBb. subst.
    case /remove_rendundant_suffixR; last done.
    move [x' [A' ?]]. exfalso. apply: HX. exists (A', [], x').
    constructor; first by apply: spaceP0.
    by constructor.
Qed.


Lemma bounded_of_bounded' {n: }: bounded' n (m: ), bounded M m.
Proof using confluent_M.
  move Hn.
  pose W := (repeat false n, repeat false n, 0) : config.
  exists (length (space W)). elim /(measure_ind width).
  move X IH. case: (reachable_suffixes X); last case.
  - move [?] [?] [?] [?] [+ /copy] /confluent_M H [/H{H}] [Y].
    move [/Hn] H /H{H} ? /reachable_width HwX. move /= in HwX.
    exists (space X). constructor.
    + by move ? /spaceP0.
    + apply: space_length /=. rewrite repeat_length. by .
  - move: X IH [[A B] x] IH. move [AX] [a] [HA HX]. move /= in HA. subst.
    case: (IH (AX, B, x)).
    { move /=. rewrite app_length /length. by . }
    move L [ ]. exists (map ( '(A, B, x) (A [a], B, x)) L).
    constructor; last by rewrite map_length.
    move [[A' y] B'] /HX [AY] /= [] / ?. rewrite in_map_iff.
    eexists. by constructor; last by eassumption.
  - move: X IH [[A B] x] IH. move [BX] [b] [HB HX]. move /= in HB. subst.
    case: (IH (A, BX, x)).
    { move /=. rewrite app_length /length. by . }
    move L [ ]. exists (map ( '(A, B, x) (A, B [b], x)) L).
    constructor; last by rewrite map_length.
    move [[A' y] B'] /HX [BY] /= [] / ?. rewrite in_map_iff.
    eexists. by constructor; last by eassumption.
Qed.


Lemma bounded_to_bounded' {n: }: bounded M n (m: ), bounded' m.
Proof.
  move Hn. exists (n+n). rewrite /bounded'.
  move [[A' B'] z] x y A B /(bounded_stack_difference Hn) + /(bounded_stack_difference Hn) /=.
  by .
Qed.


Lemma extend_bounded' {n: } {X: config} : bounded' n narrow X length (get_right X) n.
Proof using confluent_M.
  move: X [[A B] x] Hn. elim /(measure_ind (@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 . }
  move /exists_last [A'' [a' HA']]. subst A'. rename A'' into A'.
  move: Z Hx [[A'' B''] z] /copy [/remove_rendundant_suffixL]. case.
  { move [x' [B']] /copy [/reachable_width] /= HB Hy.
    have [Y [ ]] := (confluent_M ).
    move: Hy /(@rt_trans config). move H /H{H}.
    move /Hn H /H{H}. by . }
  move /= [A''' [? Hx]]. subst A''. rename A''' into A''.
  move _ /copy [/remove_rendundant_suffixL]. case.
  { move [x' [B']]. move /copy [/reachable_width] /=.
    rewrite app_length /= ?. move /Hn.
    move /(_ _ _ ltac:(apply: rt_refl)) ?.
    move: Hx /reachable_width + /reachable_width /=.
    rewrite ?app_length /=. by . }
  move [A''']. move [/(@app_inj_tail symbol) [? ?]]. subst.
  move ? _. apply: (IH A).
  - rewrite app_length /length. by .
  - do 3 eexists. constructor; by eassumption.
Qed.


Theorem boundedP : ( n, bounded M n) ( m, bounded' m).
Proof using confluent_M.
  constructor.
  - move [?]. by apply /bounded_to_bounded'.
  - move [?]. by apply /bounded_of_bounded'.
Qed.


Lemma narrow_equiv {X Y: config} : equiv X Y narrow X narrow Y.
Proof using confluent_M.
  move /equiv_sym HXY [x [A HX]]. exists x, A.
  apply: (equiv_trans); by eassumption.
Qed.


End CSSM.