proposition: Lemma κ_inj1 {a1 b1 c1 a2 b2 c2: nat} : κ a1 b1 c1 = κ a2 b2 c2 -> a1 = a2.
proof: Proof. elim: a1 a2 b1 b2. { move=> [|a2] >; first done. move /(f_equal (fun x => x mod 2)). by rewrite ?κ_mod2. } move=> a1 IH [|a2] >. { move /(f_equal (fun x => x mod 2)). by rewrite ?κ_mod2. } move /(f_equal (fun x => x * 3 / 2)). rewrite ?κ_32. by move /IH => ->. 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