proposition: Theorem boundedness : (exists NM, bounded M NM) <-> (exists NM', bounded M' NM').
proof: Proof. Proof using lp_XY Y_fresh XY_neq. constructor; move=> [? ?]; eexists; [by apply: bounded_M' | by apply: bounded_M]. Qed.
imports: Relation_Operators Operators_Properties List Lia PeanoNat Undecidability.StackMachines.SMN Undecidability.StackMachines.Util(List_facts SMN_facts) ssreflect ssrbool ssrfun