proposition: Lemma κ_mod2 {a b c: nat} : κ a b c mod 2 = if a is 0 then 1 else 0.
proof: Proof. rewrite /κ. rewrite [(_ * 5^_) mod 2]mul_mod. rewrite [(_ * 3^_) mod 2]mul_mod. rewrite pow_3_mod_2 pow_5_mod_2. move: a => [|a]; first done. have -> : 2 ^ S a = 2 * 2 ^ a by move=> /=; lia. by rewrite [(2 * _) mod 2]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