proposition: Fact stack_enc_S s : { k | stack_enc s = S k }.
proof: Proof. induction s as [ | [] s (k & Hk) ]. + exists 0; auto. + exists (2*stack_enc s); auto. + exists (S (2*k)); simpl; lia. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils list_bool pos vec subcode sss) Undecidability.MinskyMachines.MMA(mma_defs mma_utils)