fact: Definition mm_div2 := DEC src (6+i) :: INC rem :: DEC src (i+6) :: DEC rem (4+i) :: INC quo :: DEC rem i :: nil.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils list_bool pos vec subcode sss) Undecidability.MinskyMachines.MM(mm_defs)