proposition: Lemma length_preservingP {M l r x l' r' y} : length_preserving M -> reachable M (l, r, x) (l', r', y) -> (l, r, x) = (l', r', y) \/ (length (l ++ r) = length (l' ++ r') /\ 1 <= length (l ++ r)).
proof: Proof. move=> HM /reachable_to_reachable_n [n]. elim: n l r x l' r' y. { move=> > /reachable_0E => ?. by left. } move=> n IH l r x l' r' y /reachable_SnE [? | [Z] []]; first by left. move HX: (l, r, x) => X HXZ. case: HXZ HX. move=> > /HM []. rewrite ?app_length. move=> ? ? [] ? ? ?. subst. move /IH. case. - move=> [] *. subst. rewrite ?app_length. right. by lia. - rewrite ?app_length. move=> [] ? ?. right. by lia. Qed.
imports: Arith Lia Relation_Operators Operators_Properties List Undecidability.StackMachines.Util(Nat_facts List_facts) Undecidability.StackMachines.SMN ssreflect ssrbool ssrfun