proposition: Lemma bounded_of_bounded' {n: nat}: bounded' n -> exists (m: nat), bounded M m.
proof: Proof. Proof using confluent_M. move=> Hn. pose W := (repeat false n, repeat false n, 0) : config. exists (length (space W)). elim /(Nat.measure_induction _ width). move=> X IH. case: (reachable_suffixes X); last case. - move=> [?] [?] [?] [?] [+ /[dup]] => /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 lia. - 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 lia. } move=> L [HL1 HL2]. exists (map (fun '(A, B, x) => (A ++ [a], B, x)) L). constructor; last by rewrite map_length. move=> [[A' y] B'] /HX [AY] /= [->] /HL1 ?. 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 lia. } move=> L [HL1 HL2]. exists (map (fun '(A, B, x) => (A, B ++ [b], x)) L). constructor; last by rewrite map_length. move=> [[A' y] B'] /HX [BY] /= [->] /HL1 ?. rewrite in_map_iff. eexists. by constructor; last by eassumption. Qed.
imports: PeanoNat Lia Relation_Operators Operators_Properties List ssreflect ssrfun ssrbool Undecidability.StackMachines.SSM