proposition: Fact mma_jump_spec i v : (i,JUMPₐ) // (i,v) ->> (j,v).
proof: Proof. now apply sss_progress_compute, mma_jump_progress. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils list_bool gcd pos vec subcode sss) Undecidability.MinskyMachines.MMA(mma_defs)