proposition: Theorem FSATd_undec_frag : undecidable FSATd.
proof: Proof. apply (undecidability_from_reducibility (FSATd_undec)). exists translate_form. intros k. split; intros (D & I & rho & (l & Hlist) & Hdisc & Hdec & H). - exists D, (full_tarski_tarski_interp I), rho; repeat split. + now exists l. + easy. + destruct I; apply Hdec. + rewrite <- (full_interp_inverse_1 I) in H. destruct (Hdec FSAT.P) as [fP HfP]. destruct (Hdec FSAT.less) as [fL HfL]. destruct (Hdec FSAT.equiv) as [fE HfE]. unshelve now eapply translate_form_correct in H. intros ff phi rho'. apply Full.general_decider. 1: now exists l. rewrite full_interp_inverse_1. intros ff' [] v ee; cbn; apply DecidabilityFacts.decidable_iff'. 1: now exists fP. 1: now exists fL. now exists fE. - exists D, (tarski_full_tarski_interp I), rho; repeat split. + now exists l. + easy. + destruct I; apply Hdec. + destruct (Hdec FSAT.P) as [fP HfP]. destruct (Hdec FSAT.less) as [fL HfL]. destruct (Hdec FSAT.equiv) as [fE HfE]. unshelve now eapply translate_form_correct. intros ff phi rho'. apply Full.general_decider. 1: now exists l. intros ff' [] v ee; cbn; apply DecidabilityFacts.decidable_iff'; destruct I. 1: now exists fP. 1: now exists fL. now exists fE. Qed.
imports: Undecidability.PCP(PCP_undec) Undecidability.Synthetic(Undecidability ReducibilityFacts DecidabilityFacts) Undecidability.FOL(FSAT Reductions.FSATd_to_FSATdc Reductions.PCPb_to_FSAT)