proposition: Theorem reduction : SMNdl_UB ⪯ SSM.CSSM_UB.
proof: Proof. exists SMNdl_to_cssm. move=> [M [H1M H2M]]. constructor. - move=> [nMN] /=. set M1 := (construct_basic_SMN M (deterministic_confluent H1M) H2M). move=> HM. have [? [?]] := svalP M1. move /iffLR => /(_ ltac:(by eexists)) => /Argument.boundedness. by apply. - move /Argument.boundedness. set M1 := (construct_basic_SMN M (deterministic_confluent H1M) H2M). have [? [? <-]] := svalP M1. by apply. 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 Undecidability.Synthetic.Definitions