proposition: Lemma boundedness' {n} : bounded M' n <-> bounded M n.
proof: Proof. constructor. - move=> HM' x. have [Lx [HLx ?]]:= HM' x. exists Lx. constructor; last done. by move=> ? /simulation /HLx. - move=> HM x. have [Lx [HLx ?]]:= HM x. exists Lx. constructor; last done. by move=> ? /simulation /HLx. Qed.
imports: Relation_Operators Operators_Properties List Lia PeanoNat Undecidability.StackMachines.SMN Undecidability.StackMachines.Util(List_facts SMN_facts) ssreflect ssrbool ssrfun