proposition: Fact mma_loop_loop v : (i,mma_loop) // (i,v) -+> (i,v).
proof: Proof. apply mma_jump_progress; auto. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils list_bool gcd pos vec subcode sss) Undecidability.MinskyMachines.MMA(mma_defs)