proposition: Lemma steps_values_bound k x y : steps k x = Some y -> value1 y + value2 y <= k + value1 x + value2 x /\ value1 x + value2 x <= k + value1 y + value2 y /\ value1 x <= k + value1 y /\ value1 y <= k + value1 x /\ value2 x <= k + value2 y /\ value2 y <= k + value2 x.
proof: Proof. elim: k x. { move=> ? [<-]. lia. } move=> k IH x. rewrite (steps_plus' (k := 1) (k' := k)). case Hxz: (steps 1 x) => [z|]; last done. move=> /IH. move: Hxz => /step_values_bound. lia. Qed.
imports: List ListDec PeanoNat Lia Relation_Operators Operators_Properties Permutation Undecidability.MinskyMachines.MM2 Undecidability.MinskyMachines.Util.MM2_facts ssreflect ssrbool ssrfun