proposition: Lemma shift_steps_a k K p a b : k <= K -> steps k (p, (K + a, b)) = match steps k (p, (K, b)) with | Some (p', (a', b')) => Some (p', (a' + a, b')) | None => None end.
proof: Proof. elim: k K p a b. { done. } move=> k IH [|K] p a b ? /=; [lia|]. case: (mm2_sig_step_dec M (p, (S (K + a), b))) => [[[p1 [a1 b1]]]|]. - move=> /(mm2_step_parallel (p, (S K, b))) /= /(_ ltac:(lia)). move=> [[p2 [a2 b2]]] /= [+] [?] ?. move=> /[dup] /mm2_step_values_bound /= ?. case: (mm2_sig_step_dec M (p, _)) => [[?]|] /=; first last. { by move=> /[apply]. } move=> /mm2_step_det /[apply] ->. subst p1. have [-> ->]: a1 = K + (a1 - K) /\ a2 = K + (a2 - K) by lia. have ->: b2 = b1 by lia. rewrite IH; [lia|]. rewrite IH; [lia|]. case: (steps k (p2, (K, b1))); last done. move=> [? [? ?]] /=. congr (Some (_, (_, _))); lia. - move=> /mm2_stop_index_iff /= ?. case: (mm2_sig_step_dec M (p, (S K, b))) => [[?]|]; last done. move=> [?] [/mm2_instr_at_bounds] /=. lia. Qed.
imports: List ListDec PeanoNat Lia Relation_Operators Operators_Properties Permutation Undecidability.MinskyMachines.MM2 Undecidability.MinskyMachines.Util.MM2_facts ssreflect ssrbool ssrfun