fact: Definition terminal (M: SMN) (X: Config) : Prop := forall (Y: Config), not (step M X Y).
imports: Arith Lia Relation_Operators Operators_Properties List Undecidability.StackMachines.Util(Nat_facts List_facts) Undecidability.StackMachines.SMN ssreflect ssrbool ssrfun