proposition: Lemma mm2_step_parallel {P x y} x' : mm2_step P x y -> (index x = index x' /\ (value1 x > 0 <-> value1 x' > 0) /\ (value2 x > 0 <-> value2 x' > 0)) -> exists y', mm2_step P x' y' /\ index y = index y' /\ value1 x + value1 y' = value1 x' + value1 y /\ value2 x + value2 y' = value2 x' + value2 y.
proof: Proof. move=> [?] [+ Hxy]. move: x' => [i' [a' b']]. case: Hxy => [i a b|i a b|i j a b|i j a b|i j b|i j a] /= Hi [<- ?]. - eexists. split; [eexists; split; [eassumption|constructor]|cbn; lia]. - eexists. split; [eexists; split; [eassumption|constructor]|cbn; lia]. - have ->: a' = S (Nat.pred a') by lia. eexists. split; [eexists; split; [eassumption|constructor]|cbn; lia]. - have ->: b' = S (Nat.pred b') by lia. eexists. split; [eexists; split; [eassumption|constructor]|cbn; lia]. - have ->: a' = 0 by lia. eexists. split; [eexists; split; [eassumption|constructor]|cbn; lia]. - have ->: b' = 0 by lia. eexists. split; [eexists; split; [eassumption|constructor]|cbn; lia]. Qed.
imports: List PeanoNat Lia Relation_Operators Operators_Properties Wellfounded.Transitive_Closure Undecidability.MinskyMachines.MM2 ssreflect ssrbool ssrfun