proposition: Lemma k_step_iter k p a1 b1 a2 b2 : (k <= a1 \/ a1 = a2) -> (k <= b1 \/ b1 = b2) -> steps k (p, (a1, b1)) = Some (p, (a2, b2)) -> let ca := if Nat.eq_dec a1 a2 then 0 else 1 in let cb := if Nat.eq_dec b1 b2 then 0 else 1 in forall i n a b, i <= n -> steps (i*k) (p, (a1+ca*(a+n*a1),b1+cb*(b+n*b1))) = Some (p, (a1+ca*(a+(n-i)*a1+i*a2),b1+cb*(b+(n-i)*b1+i*b2))).
proof: Proof. move=> Ha Hb Hk ca cb. elim. { move=> ????. congr (Some (_, (_, _))); lia. } move=> i IH [|n] a b; first by lia. move=> /(iffRL (Nat.succ_le_mono _ _)) /IH {}IH. rewrite /= steps_plus'. have := IH (a2+a) (b2+b). congr eq; first last. { congr (Some (_, (_, _))); lia. } have -> : steps (i * k) (p, (a1 + ca * (a2 + a + n * a1), b1 + cb * (b2 + b + n * b1))) = obind (steps (i * k)) (Some (p, (a1 + ca * (a2 + a + n * a1), b1 + cb * (b2 + b + n * b1)))) by done. congr obind. rewrite /ca /cb. move: (Nat.eq_dec a1 a2) (Nat.eq_dec b1 b2) => [?|?] [?|?] /=. - rewrite ?Nat.add_0_r Hk. congr (Some (_, (_, _))); lia. - rewrite shift_steps_b; first lia. rewrite ?Nat.add_0_r Hk. congr (Some (_, (_, _))); lia. - rewrite shift_steps_a; first lia. rewrite ?Nat.add_0_r Hk. congr (Some (_, (_, _))); lia. - rewrite shift_steps_a; first lia. rewrite shift_steps_b; first lia. rewrite ?Nat.add_0_r Hk. congr (Some (_, (_, _))); lia. Qed.
imports: List ListDec PeanoNat Lia Relation_Operators Operators_Properties Permutation Undecidability.MinskyMachines.MM2 Undecidability.MinskyMachines.Util.MM2_facts ssreflect ssrbool ssrfun