fact: Definition mm_no_self_loops (Q : nat * list (mm_instr (pos n))) := forall i x, ~ (i,DEC x i::nil) <sc Q.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils pos vec subcode sss) Undecidability.MinskyMachines.MM(mm_defs)