proposition: Fact mma_jump_progress i v w : w = v -> (i,JUMPₐ) // (i,v) -+> (j,w).
proof: Proof. intros ->. unfold mma_jump. mma sss INC with x. mma sss DEC S with x j (v#>x); rew vec. mma sss stop. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils list_bool gcd pos vec subcode sss) Undecidability.MinskyMachines.MMA(mma_defs)