Revision 109cbb72b58c68e6f8ab6290ad3f8c96aa62f4a5 authored by Dominique Larchey-Wendling on 11 April 2020, 19:44:16 UTC, committed by Dominique Larchey-Wendling on 11 April 2020, 19:44:16 UTC
This reverts commit 1991a25ab6b82f256292db63ce90100454f212c7.
1 parent 1991a25
DIO_MUREC.v
(**************************************************************)
(* Copyright Dominique Larchey-Wendling [*] *)
(* *)
(* [*] Affiliation LORIA -- CNRS *)
(**************************************************************)
(* This file is distributed under the terms of the *)
(* CeCILL v2 FREE SOFTWARE LICENSE AGREEMENT *)
(**************************************************************)
Require Import List.
From Undecidability.ILL Require Import Definitions.
From Undecidability.Shared.Libs.DLW.Utils
Require Import utils_tac utils_nat.
From Undecidability.Shared.Libs.DLW.Vec
Require Import pos vec.
From Undecidability.H10
Require Import Dio.dio_single H10.
From Undecidability.MuRec
Require Import recalg ra_dio_poly.
Section H10_MUREC_HALTING.
Let f : H10_PROBLEM -> MUREC_PROBLEM.
Proof.
intros (n & p & q).
exact (ra_dio_poly_find p q).
Defined.
Theorem H10_MUREC_HALTING : H10 ⪯ MUREC_HALTING.
Proof.
exists f.
intros (n & p & q); simpl; unfold MUREC_HALTING.
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.
End H10_MUREC_HALTING.
Check H10_MUREC_HALTING.
Print Assumptions H10_MUREC_HALTING.
![swh spinner](/static/img/swh-spinner.gif)
Computing file changes ...