proposition: Theorem reachable_suffixes (X: config) : (exists A x y B, reachable M X (A, [], x) /\ reachable M X ([], B, y)) \/ (exists AX a, get_left X = AX ++ [a] /\ forall Y, reachable M X Y -> exists AY, get_left Y = AY ++ [a] /\ reachable M (AX, get_right X, get_state X) (AY, get_right Y, get_state Y)) \/ (exists BX b, get_right X = BX ++ [b] /\ forall Y, reachable M X Y -> exists BY, get_right Y = BY ++ [b] /\ reachable M (get_left X, BX, get_state X) (get_left Y, BY, get_state Y)).
proof: Proof. case: (Exists_dec (fun 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 (fun 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=> [[[A1 B1] x1]] + [[[A2 B2] x2]] => /= [[_ [? ?]]] [_ [? ?]]. 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.
imports: PeanoNat Lia Relation_Operators Operators_Properties List ssreflect ssrfun ssrbool Undecidability.StackMachines.SSM