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