fact: Definition mma_mma0_sim := Q ++ mma_null_all _ (length Q+1) ++ mma_jump 0 pos0.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils pos vec subcode sss compiler_correction) Undecidability.MinskyMachines.MMA(mma_defs mma_utils)