Require Import Arith ZArith List.

From Undecidability.Shared.Libs.DLW
  Require Import utils_tac pos vec sss.

From Undecidability.Synthetic Require Import Undecidability.

Require Import Undecidability.TM.TM.

From Undecidability.PCP
  Require Import PCP PCP_undec HaltTM_1_to_PCPb.

From Undecidability.MinskyMachines
  Require Import MM PCPb_to_MM MUREC_MM.

From Undecidability.FRACTRAN
  Require Import FRACTRAN FRACTRAN_undec MM_FRACTRAN.

From Undecidability.H10
  Require Import H10 FRACTRAN_DIO H10_undec H10Z H10Z_undec.

From Undecidability.H10.Dio
  Require Import dio_logic dio_elem dio_single.

From Undecidability.MuRec
  Require Import recalg H10_to_MUREC_HALTING.

Import ReductionChainNotations UndecidabilityNotations.

Set Implicit Arguments.

Local Infix "∈" := In (at level 70).



About "⪯".
Print reduction.
Print reduces.


Print HaltTM.
Print HaltsTM.
Print eval.


Print dPCPb.
Print dPCP.
Print stack.
Print card.
Print derivable.


Print mm_instr.
Print MM_PROBLEM.
Print mm_sss.
Print sss_output.
Print sss_terminates.
Print MM_HALTING.


Print FRACTRAN_PROBLEM.
Print fractran_step. Print fractran_steps.
Print fractran_compute.
Print fractran_stop.
Print fractran_terminates. Print FRACTRAN_HALTING.


Print dio_op.
Print dio_formula.
Print de_op_sem.
Print df_op_sem.
Print df_pred.
Print DIO_LOGIC_SAT.


Print dio_op.
Print dio_elem_expr.
Print dio_constraint.
Print DIO_ELEM_PROBLEM.
Print de_op_sem.
Print dee_eval.
Print dc_eval.
Print DIO_ELEM_SAT.


Print dio_polynomial.
Print dio_single.
Print DIO_SINGLE_PROBLEM.
Print dp_eval.
Print dio_single_pred.
Print DIO_SINGLE_SAT.


Print dio_polynomial.
Print pos. Print Fin.t.
Print H10_PROBLEM. Print dp_eval.
Print dio_single_pred.
Print H10.


Print recalg. Print ra_rel. Print MUREC_PROBLEM.
Print MUREC_HALTING.


Theorem Hilberts_Tenth_entire_chain :
  ⎩ HaltTM 1 ⪯ₘ
    dPCPb ⪯ₘ
    MM_HALTING ⪯ₘ
    FRACTRAN_HALTING ⪯ₘ
    DIO_LOGIC_SAT ⪯ₘ
    DIO_ELEM_SAT ⪯ₘ
    DIO_SINGLE_SAT ⪯ₘ
    H10 ⪯ₘ
    MUREC_HALTING ⪯ₘ
    MM_HALTING ⎭.
Proof.
  msplit 8.
  + apply reduces_transitive with (1 := HaltTM_1_to_PCPb).
    exists id; exact PCPb_iff_dPCPb.PCPb_iff_dPCPb.
  + apply reduces_transitive with (2 := PCPb_MM_HALTING).
    exists id; intro; symmetry; apply PCPb_iff_dPCPb.PCPb_iff_dPCPb.
  + apply MM_FRACTRAN_HALTING.
  + apply FRACTRAN_HALTING_DIO_LOGIC_SAT.
  + apply DIO_LOGIC_ELEM_SAT.
  + apply DIO_ELEM_SINGLE_SAT.
  + apply DIO_SINGLE_SAT_H10.
  + apply H10_MUREC_HALTING.
  + apply MUREC_MM_HALTING.
Qed.

Check Hilberts_Tenth_entire_chain.
Print Assumptions Hilberts_Tenth_entire_chain.

Theorem Hilberts_Tenth_from_PCP : dPCPb ⪯ H10.
Proof.
  do 6 (eapply reduces_transitive; [ apply Hilberts_Tenth_entire_chain | ]).
  apply reduces_reflexive.
Qed.


Print H10Z.dio_polynomial.
Print H10Z_PROBLEM. Print H10Z.dp_eval.
Print H10Z.

Check H10_H10Z.
Print Assumptions H10_H10Z.