proposition: Lemma κ_mod3 {a b c: nat} : κ a b c mod 3 = if b is 0 then (S (locked (κ a b c) mod 3 - 1)) else 0.
proof: Proof. rewrite /κ -lock. rewrite [(_ * 5^_) mod 3]mul_mod. rewrite [(_ * 3^_) mod 3]mul_mod. move: b => [|b]. { by case: (pow_2_mod_3 a); case: (pow_5_mod_3 c); move=> -> ->. } have -> : 3 ^ S b = 3 * 3 ^ b by move=> /=; lia. replace (((3 * 3 ^ b) mod 3)) with 0. - by rewrite Nat.mul_0_r. - by rewrite mul_mod. Qed.
imports: ZArith List PeanoNat Lia Relations.Relation_Operators Relations.Operators_Properties Undecidability.MinskyMachines.MM2 Undecidability.CounterMachines.Util.CM1_facts Undecidability.MinskyMachines.Util.MM2_facts ssreflect ssrbool ssrfun