proposition: Theorem length_preserving_M {s t X s' t' Y b} : In ((s, t, X), (s', t', Y), b) M -> length (s ++ t) = length (s' ++ t') /\ 1 <= length (s ++ t).
proof: Proof. Proof using capped_P. move /(transition _ [] []). rewrite ?app_norm. move: b => [|] /stepE [] > + [] *; move=> [] *; subst; rewrite ?app_length ?repeat_length ?/G /=. all: try by lia. all: have := in_igotos_lt ltac:(eassumption); have ? := igotos_capped ltac:(eassumption); by lia. Qed.
imports: Relation_Operators Operators_Properties Lia PeanoNat List Undecidability.StackMachines.Reductions.CM1_HALT_to_SMNdl_UB.SMX_facts Undecidability.StackMachines.Util(Nat_facts List_facts) ssreflect ssrbool ssrfun