proposition: Lemma steps'E k x y : steps' k x = Some y -> exists n m, value1 y = value1 x + n /\ value2 y = value2 x + m /\ forall a b, (a > 0 -> value1 x > 0) -> (b > 0 -> value2 x > 0) -> steps' k (index x, (a, b)) = Some (index y, (a + n, b + m)).
proof: Proof. elim: k x y. { move=> x y [<-]. exists 0, 0. do 2 (split; first by lia). move=> a b ?? /=. by rewrite ?Nat.add_0_r. } move=> k IH x y /=. case Hx': (steps' k x) => [x'|]; last done. move: Hx' => /IH [n] [m] [Hax'] [Hbx'] {}IH /=. rewrite /(step' x'). move: (index x') IH => [|xp] IH; [done|]. case Hi: (nth_error M xp) => [i|]; last done. move: i Hi => []. - move=> Hi [<-] /=. exists (1 + n), m. split; first by lia. split; first by lia. move=> a b Ha Hb. rewrite IH; [done|done|]. rewrite /= /step' /= Hi. congr Some. congr pair. congr pair; lia. - move=> Hi [<-] /=. exists n, (1 + m). split; first by lia. split; first by lia. move=> a b Ha Hb. rewrite IH; [done|done|]. rewrite /= /step' /= Hi. congr Some. congr pair. congr pair; lia. - move=> q Hi. case H'ax': (value1 x') => [|ax']; last done. move=> [<-] /=. exists 0, m. split; first by lia. split; first by lia. move=> a b ??. rewrite IH; [done|done|]. rewrite /step' /= Hi. have ->: a + n = 0 by lia. congr Some. congr pair. congr pair; lia. - move=> q Hi. case H'bx': (value2 x') => [|bx']; last done. move=> [<-] /=. exists n, 0. split; first by lia. split; first by lia. move=> a b ??. rewrite IH; [done|done|]. rewrite /step' /= Hi. have ->: b + m = 0 by lia. congr Some. congr pair. congr pair; lia. Qed.
imports: List PeanoNat Lia Relation_Operators Operators_Properties Transitive_Closure Undecidability.MinskyMachines.MM2 Undecidability.MinskyMachines.Util.MM2_facts ssreflect ssrbool ssrfun