proposition: Lemma boundedness : (exists NM, bounded M NM) <-> (exists NM', SSM.bounded M' NM').
proof: Proof. Proof using basic_M. constructor. - move=> [NM bounded_M]. exists NM. move=> X. have [L [HL ?]] := bounded_M X. exists L. constructor; last done. by move=> ? /inverse_simulation /= /HL ?. - move=> [NM' bounded_M']. exists NM'. move=> X. have [L [HL ?]] := bounded_M' X. exists L. constructor; last done. by move=> ? /simulation /= /HL ?. Qed.
imports: List Lia Relation_Operators Operators_Properties Undecidability.StackMachines.SMN Undecidability.StackMachines.Util(Nat_facts List_facts SMN_facts) Undecidability.StackMachines.Util.SMN_transform ssreflect ssrbool ssrfun