(**************************************************************)
(* 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 Arith Bool Lia Relations.
From Undecidability.Problems
Require Import Reduction PCP.
From Undecidability.Shared.Libs.DLW.Utils
Require Import utils_tac utils_list utils_nat finite php.
From Undecidability.Shared.Libs.DLW.Vec
Require Import pos vec.
From Undecidability.Shared.Libs.DLW.Wf
Require Import wf_finite.
From Undecidability.TRAKHTENBROT
Require Import notations bpcp
fo_sig fol_ops fo_terms fo_logic fo_sat fo_sat_dec
decidable enumerable discrete reln_hfs membership
BPCP_SigBPCP Sig_Sig_fin Sig_rem_syms Sig_uniform
Sig_one_rel Sig_rem_cst Sig2_SigSSn1 Sig1_1
Sig_rem_constants Sig_rem_props
red_utils red_enum red_dec red_undec
.
Set Implicit Arguments.
(* 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 Arith Bool Lia Relations.
From Undecidability.Problems
Require Import Reduction PCP.
From Undecidability.Shared.Libs.DLW.Utils
Require Import utils_tac utils_list utils_nat finite php.
From Undecidability.Shared.Libs.DLW.Vec
Require Import pos vec.
From Undecidability.Shared.Libs.DLW.Wf
Require Import wf_finite.
From Undecidability.TRAKHTENBROT
Require Import notations bpcp
fo_sig fol_ops fo_terms fo_logic fo_sat fo_sat_dec
decidable enumerable discrete reln_hfs membership
BPCP_SigBPCP Sig_Sig_fin Sig_rem_syms Sig_uniform
Sig_one_rel Sig_rem_cst Sig2_SigSSn1 Sig1_1
Sig_rem_constants Sig_rem_props
red_utils red_enum red_dec red_undec
.
Set Implicit Arguments.
(* Definition 1 *)
About decidable. Print decidable.
Check decidable_bool_eq.
About opt_enum_t. Print opt_enum_t.
About type_enum_t. Print type_enum_t.
About discrete. Print discrete.
(* Definition 2 *)
About reduces. Print reduces.
(* Fact 3 *)
About reduction_decidable.
About reduction_rec_enum_t.
About reduction_opt_enum_t.
(* Definition 4 *)
About pcp_hand. Print pcp_hand.
About BPCP_problem. Print BPCP_problem.
(* Fact 5, for the reduction for TM halting, you need much more code from the
undec. library and that one is not trivial at all *)
About bpcp_hand_dec.
Print Assumptions bpcp_hand_dec.
About BPCP_BPCP_problem_eq.
About BPCP_BPCP_problem.
(* Definition 6 *)
About finite_t. Print finite_t.
(* Theorem 7 *)
About PHP_rel.
Print Assumptions PHP_rel.
(* Fact 8 *)
About wf_strict_order_finite.
Print Assumptions wf_strict_order_finite.
(* Theorem 9 *)
About decidable_EQUIV_fin_quotient.
Print Assumptions decidable_EQUIV_fin_quotient.
(* Corollary 10 *)
Print bij_t. (* to understand the meaning of the following result *)
About finite_t_discrete_bij_t_pos.
Print Assumptions finite_t_discrete_bij_t_pos.
(* Definition FOL *)
About fo_term. Print fo_term.
Print fo_signature.
Print fol_bop.
Print fol_qop.
About fol_form. Print fol_form.
(* Definition 11 *)
About fo_model. Print fo_model.
About fo_term_sem. Print fo_term_sem.
About fol_sem. Print fol_sem.
(* Fact 12 *)
About fol_sem_dec.
Print Assumptions fol_sem_dec.
(* Definition 13 *)
About fo_form_fin_dec_SAT_in.
Print fo_form_fin_dec_SAT_in.
Print fo_form_fin_dec_SAT.
About fo_form_fin_dec_eq_SAT_in.
Print fo_form_fin_dec_eq_SAT_in.
Print fo_form_fin_dec_eq_SAT.
(* Theorem 14 *)
About BPCP_FIN_DEC_EQ_SAT.
Print Assumptions BPCP_FIN_DEC_EQ_SAT.
(* Lemma 15 *)
About Σbpcp_encode_sound.
(* Lemma 16 *)
About Σbpcp_encode_complete.
(* Definition 17 *)
About fo_form_fin_discr_dec_SAT_in.
Print fo_form_fin_discr_dec_SAT_in.
Print fo_form_fin_discr_dec_SAT.
(* Definition 18 *)
About fo_bisimilar.
Print fo_bisimilar.
(* Theorem 19 *)
Print fo_congruence_upto. (* to understand the meaning of the following result *)
About fo_bisimilar_dec_congr.
Print Assumptions fo_bisimilar_dec_congr.
(* Theorem 20 *)
About fo_form_fin_dec_SAT_discr_equiv.
Check FIN_DEC_SAT_FIN_DISCR_DEC_SAT.
(* Theorem 21 *)
About FIN_DEC_EQ_SAT_FIN_DEC_SAT.
Print Assumptions FIN_DEC_EQ_SAT_FIN_DEC_SAT.
(* Lemma 22 *)
About Sig_discrete_to_pos.
Print Assumptions Sig_discrete_to_pos.
(* Lemma 23 *)
Print Σnosyms.
About FSAT_Σnosyms.
(* Lemma 24 *)
Print Σrel. (* to understand the meaning of the following result *)
About FSAT_REL_BOUNDED_ONE_REL.
Print Assumptions FSAT_REL_BOUNDED_ONE_REL.
(* Fact 25 *)
Print Σunif. (* to understand the meaning of the following result *)
About FSAT_UNIFORM.
Print Σone_rel. (* to understand the meaning of the following result *)
About FSAT_ONE_REL.
Print Σrem_cst. (* to understand the meaning of the following result *)
Check FSAT_NOCST.
(* Lemma 26 *)
About FIN_DISCR_DEC_nSAT_FIN_DEC_2SAT.
Print Assumptions FIN_DISCR_DEC_nSAT_FIN_DEC_2SAT.
(* Theorem 27 *)
About reln_hfs.
Print Assumptions reln_hfs.
(* Theorem 28 *)
About FSAT_REL_nto2.
Print Assumptions FSAT_REL_nto2.
(* Lemma 29 *)
Print Σn1. (* to understand the meaning of the following result *)
About FSAT_REL2_to_FUNnREL1.
Print Assumptions FSAT_REL2_to_FUNnREL1.
(* Fact 30 *)
Print Σrel. (* to understand the meaning of the following results *)
About FSAT_REL_2ton.
About FSAT_RELn_ANY.
Print Σn1. (* to understand the meaning of the following result *)
About FSAT_FUNnREL1_ANY.
(* Lemma 31 *)
About FSAT_in_dec.
Print Assumptions FSAT_in_dec.
(* Lemma 32 *)
About fo_form_fin_discr_dec_SAT_pos.
Print Assumptions fo_form_fin_discr_dec_SAT_pos.
(* Lemma 33 *)
Print Σ11. (* to understand the meaning of the following result *)
About FSAT_MONADIC_DEC.
Print Assumptions FSAT_MONADIC_DEC.
(* Lemma 34 *)
Print Σ11. (* to understand the meaning of the following result *)
About FSAT_MONADIC_11_FSAT_MONADIC_1.
Print Assumptions FSAT_MONADIC_11_FSAT_MONADIC_1.
(* Fact 35 *)
Print Σ11. (* to understand the meaning of the following result *)
About FSAT_FULL_MONADIC_FSAT_11.
Print Assumptions FSAT_FULL_MONADIC_FSAT_11.
About Σrem_constants_correct.
About Σrem_props_correct.
(* Theorem 36 *)
About FSAT_rec_enum_t.
Print Assumptions FSAT_rec_enum_t.
About FSAT_opt_enum_t.
Print Assumptions FSAT_opt_enum_t.
(* Theorem 37 *)
About FULL_MONADIC.
Print Assumptions FULL_MONADIC.
(* Theorem 38 *)
About FULL_TRAKHTENBROT.
Print Assumptions FULL_TRAKHTENBROT.