proposition: Theorem MM_HALTS_ON_ZERO_EILL_PROVABILITY : MM_HALTS_ON_ZERO ⪯ EILL_PROVABILITY.
proof: Proof. exists f. intros (n & P & v); simpl. rewrite <- G_eill_mm; simpl; auto. split. + intros (? & _); auto. + split; simpl; auto. Qed.
imports: List Undecidability.Synthetic.Definitions Undecidability.Shared.Libs.DLW(pos vec sss) Undecidability.MinskyMachines(mm_defs) Undecidability.ILL(ILL EILL eill eill_mm)