Require Import List.
Import ListNotations.
Require Import Undecidability.CFG.CFP.
Require Import Undecidability.CFG.CFG.
Require Undecidability.CFG.Reductions.CFPP_to_CFP.
Require Import Undecidability.Synthetic.Definitions.
Theorem reduction :
CFPI ⪯ CFI.
Proof.
exists (fun '(R1, R2, a) => (CFPP_to_CFP.G R1 a, CFPP_to_CFP.G R2 a)). intros [[R1 R2] a].
intuition; cbn in *.
- destruct H as (A1 & A2 & HR1 & HR2 & HA1 & HA2 & H).
exists (sigma a A1). split; eapply CFPP_to_CFP.reduction_full; eauto.
- destruct H as (x & HR1 & HR2).
eapply CFPP_to_CFP.reduction_full in HR1 as (A1 & HR1 & HA1 & H1).
eapply CFPP_to_CFP.reduction_full in HR2 as (A2 & HR2 & HA2 & H2).
exists A1, A2. subst; eauto.
Qed.
Import ListNotations.
Require Import Undecidability.CFG.CFP.
Require Import Undecidability.CFG.CFG.
Require Undecidability.CFG.Reductions.CFPP_to_CFP.
Require Import Undecidability.Synthetic.Definitions.
Theorem reduction :
CFPI ⪯ CFI.
Proof.
exists (fun '(R1, R2, a) => (CFPP_to_CFP.G R1 a, CFPP_to_CFP.G R2 a)). intros [[R1 R2] a].
intuition; cbn in *.
- destruct H as (A1 & A2 & HR1 & HR2 & HA1 & HA2 & H).
exists (sigma a A1). split; eapply CFPP_to_CFP.reduction_full; eauto.
- destruct H as (x & HR1 & HR2).
eapply CFPP_to_CFP.reduction_full in HR1 as (A1 & HR1 & HA1 & H1).
eapply CFPP_to_CFP.reduction_full in HR2 as (A2 & HR2 & HA2 & H2).
exists A1, A2. subst; eauto.
Qed.