proposition: Lemma half_spec n : let '(m, b) := half n in n = (if b then 0 else 1) + m + m.
proof: Proof. elim: n => [|n] /=; [done|case: (half n) => ? []; lia]. Qed.
imports: Undecidability(MinskyMachines.MM MinskyMachines.MMA) Undecidability.Shared.Libs.DLW(Vec.pos Vec.vec Code.sss) PeanoNat List Lia Wf_nat ssreflect ssrbool ssrfun