proposition: Lemma mm2_step_values_bound {P x y} : mm2_step P x 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=> [i] [_ []] /=; lia. Qed.
imports: List PeanoNat Lia Relation_Operators Operators_Properties Wellfounded.Transitive_Closure Undecidability.MinskyMachines.MM2 ssreflect ssrbool ssrfun