proposition: Theorem mma_loop_spec v : ~ (i,mma_loop) // (i,v) ↓.
proof: Proof. apply sss_progress_non_termination. + apply mma_sss_fun. + apply mma_loop_loop. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils list_bool gcd pos vec subcode sss) Undecidability.MinskyMachines.MMA(mma_defs)