fact: Definition weight (M: SMN) : nat := fold_right (fun op w => w + weight_Instruction op) 0 M.
imports: Relation_Operators Operators_Properties List Lia PeanoNat Undecidability.StackMachines.SMN Undecidability.StackMachines.Util(List_facts SMN_facts) ssreflect ssrbool ssrfun