fact: Definition bsm_instr_compile_length (ii : bsm_instr m) := match ii with | PUSH _ Zero => 7 | PUSH _ One => 8 | POP _ _ _ => 16 end.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils list_bool pos vec subcode sss compiler_correction) Undecidability.StackMachines.BSM(bsm_defs) Undecidability.MinskyMachines.MM(mm_defs mm_utils)