proposition: Theorem boundedness : (exists NM, bounded M NM) <-> (exists NM', bounded M' NM').
proof: Proof. Proof using derivable. constructor. - move=> [NM] HM. exists NM => x. have [Lx [HLx ?]]:= HM x. exists Lx. constructor; last done. by move=> ? /simulation /HLx. - move=> [NM'] HM'. exists NM' => 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