proposition: Theorem H10_MUREC_HALTING : H10 ⪯ Halt_murec.
proof: Proof. unshelve eexists. { intros (n & p & q). exists 0. 2: exact vec_nil. exact (ra_dio_poly_find p q). } intros (n & p & q); simpl; unfold Halt_murec. setoid_rewrite <- ra_bs_correct. rewrite ra_dio_poly_find_spec; unfold dio_single_pred. split. + intros (phi & Hphi); exists (vec_set_pos phi). simpl in Hphi; eq goal Hphi; f_equal; apply dp_eval_ext; auto; try (intros; rewrite vec_pos_set; auto; fail); intros j; analyse pos j. + intros (v & Hw); exists (vec_pos v). eq goal Hw; f_equal; apply dp_eval_ext; auto; intros j; analyse pos j. Qed.
imports: List Undecidability.Synthetic.Definitions Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_nat) Undecidability.Shared.Libs.DLW.Vec(pos vec) Undecidability.H10(Dio.dio_single H10) Undecidability.MuRec.Util(recalg ra_dio_poly ra_sem_eq)