proposition: Lemma step_values_bound x y : steps 1 x = Some y -> value1 y + value2 y <= 1 + value1 x + value2 x /\ value1 x + value2 x <= 1 + value1 y + value2 y /\ value1 x <= 1 + value1 y /\ value1 y <= 1 + value1 x /\ value2 x <= 1 + value2 y /\ value2 y <= 1 + value2 x.
proof: Proof. move=> /=. case: (mm2_sig_step_dec M x) => [[?]|]; last done. by move=> /mm2_step_values_bound ? [<-]. Qed.
imports: List ListDec PeanoNat Lia Relation_Operators Operators_Properties Permutation Undecidability.MinskyMachines.MM2 Undecidability.MinskyMachines.Util.MM2_facts ssreflect ssrbool ssrfun