fact: Fixpoint stack_enc (s : list bool) : nat := match s with | nil => 1 | One::s => 1+2*stack_enc s | Zero::s => 2*stack_enc s end.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils list_bool pos vec subcode sss) Undecidability.MinskyMachines.MMA(mma_defs mma_utils)