| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (837 entries) |
| Notation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (40 entries) |
| Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (14 entries) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (17 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (36 entries) |
| Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (61 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (345 entries) |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (5 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (23 entries) |
| Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (20 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (6 entries) |
| Instance Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (48 entries) |
| Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (11 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (195 entries) |
| Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (16 entries) |
Global Index
A
Allfv [module, in PCF2.Autosubst.pcf_2]allfv_tm_dec [lemma, in PCF2.pcf_2_system]
Allfv.allfvImpl_tm [definition, in PCF2.Autosubst.pcf_2]
Allfv.allfvRenL_tm [definition, in PCF2.Autosubst.pcf_2]
Allfv.allfvRenR_tm [definition, in PCF2.Autosubst.pcf_2]
Allfv.allfvTriv_tm [definition, in PCF2.Autosubst.pcf_2]
Allfv.allfv_tm [definition, in PCF2.Autosubst.pcf_2]
Allfv.upAllfvImpl_tm_tm [lemma, in PCF2.Autosubst.pcf_2]
Allfv.upAllfvRenL_tm_tm [lemma, in PCF2.Autosubst.pcf_2]
Allfv.upAllfvRenR_tm_tm [lemma, in PCF2.Autosubst.pcf_2]
Allfv.upAllfvTriv_tm_tm [lemma, in PCF2.Autosubst.pcf_2]
Allfv.upAllfv_tm_tm [lemma, in PCF2.Autosubst.pcf_2]
all_fins [definition, in PCF2.external.Synthetic.EnumerabilityFacts]
and_dec [instance, in PCF2.external.Shared.Dec]
ap [definition, in PCF2.Autosubst.core]
ap [definition, in PCF2.Autosubst.unscoped]
apc [definition, in PCF2.Autosubst.core]
apc [definition, in PCF2.Autosubst.unscoped]
AppL [constructor, in PCF2.pcf_2_system]
apply_args_steps_list' [lemma, in PCF2.pcf_2_utils]
apply_args_steps_list [lemma, in PCF2.pcf_2_utils]
apply_args_steps_body [lemma, in PCF2.pcf_2_utils]
apply_args_typed [lemma, in PCF2.pcf_2_utils]
apply_args_cons [lemma, in PCF2.pcf_2_utils]
apply_args_app [lemma, in PCF2.pcf_2_utils]
apply_args [definition, in PCF2.pcf_2_utils]
AppR [constructor, in PCF2.pcf_2_system]
app_proper [instance, in PCF2.pcf_2_system]
app_right [lemma, in PCF2.pcf_2_system]
app_left [lemma, in PCF2.pcf_2_system]
app_typed [constructor, in PCF2.pcf_2_system]
arith_technical' [lemma, in PCF2.preliminaries]
arith_technical [lemma, in PCF2.preliminaries]
B
basefun_var_applied_typed [lemma, in PCF2.pcf_2_utils]base_fun_applied_typed [lemma, in PCF2.pcf_2_utils]
base_context_rev [lemma, in PCF2.pcf_2_utils]
base_context_rev' [lemma, in PCF2.pcf_2_utils]
base_context_le_base [lemma, in PCF2.pcf_2_utils]
base_context_some_base [lemma, in PCF2.pcf_2_utils]
base_context [definition, in PCF2.pcf_2_utils]
base_fun [definition, in PCF2.pcf_2_utils]
base_eval [lemma, in PCF2.pcf_2_system]
base_preord_ff_le'' [lemma, in PCF2.CE_facts]
base_preord_ff_le' [lemma, in PCF2.CE_facts]
base_preord_ff_le [lemma, in PCF2.CE_facts]
base_preord_tt_le'' [lemma, in PCF2.CE_facts]
base_preord_tt_le' [lemma, in PCF2.CE_facts]
base_preord_tt_le [lemma, in PCF2.CE_facts]
base_preord_le_bot [lemma, in PCF2.CE_facts]
Beta [constructor, in PCF2.pcf_2_system]
bool_eq_dec [lemma, in PCF2.preliminaries]
bool_eq_dec [instance, in PCF2.external.Shared.Dec]
bool_enum [definition, in PCF2.external.Synthetic.EnumerabilityFacts]
bot_typed [constructor, in PCF2.pcf_2_system]
bval_steps_char [lemma, in PCF2.pcf_2_system]
C
CE [definition, in PCF2.CE]CE [library]
CE_open [definition, in PCF2.CE]
CE_open_undecidable [lemma, in PCF2.undecidability]
CE_undecidable [lemma, in PCF2.undecidability]
CE_facts [library]
church_rosser [axiom, in PCF2.pcf_2_system]
class [projection, in PCF2.external.Shared.FinTypesDef]
closed [definition, in PCF2.pcf_2_system]
closed_ren [lemma, in PCF2.pcf_2_system]
closed_subst [lemma, in PCF2.pcf_2_system]
closed_dec [lemma, in PCF2.pcf_2_system]
cod [definition, in PCF2.Autosubst.core_axioms]
cod_comp [definition, in PCF2.Autosubst.core_axioms]
cod_ext [definition, in PCF2.Autosubst.core_axioms]
cod_id [definition, in PCF2.Autosubst.core_axioms]
cod_map [definition, in PCF2.Autosubst.core_axioms]
CombineNotations [module, in PCF2.Autosubst.unscoped]
_ >> _ (fscope) [notation, in PCF2.Autosubst.unscoped]
_ .: _ (subst_scope) [notation, in PCF2.Autosubst.unscoped]
comp [definition, in PCF2.pcf_2_contexts]
complement [definition, in PCF2.external.Synthetic.Definitions]
complement_SBTM_HALT_undec [lemma, in PCF2.external.TM.SBTM_undec]
config_enumeration [lemma, in PCF2.external.TM.SBTM_HALT_enum]
context [definition, in PCF2.pcf_2_system]
context_existence [lemma, in PCF2.SR_SATIS_forward]
cont_equiv [definition, in PCF2.CE]
cont_equiv_Equiv [instance, in PCF2.CE_facts]
cont_equiv_rest [definition, in PCF2.CE_facts]
cont_equiv_obs_equiv_agree [lemma, in PCF2.CE_facts]
cont_equiv_imp_obs_equiv [lemma, in PCF2.CE_facts]
cont_pre_order_imp_cont_equiv [lemma, in PCF2.CE_facts]
cont_preorder [definition, in PCF2.CE_facts]
Core [module, in PCF2.Autosubst.pcf_2]
core [library]
core_axioms [library]
Core.app [constructor, in PCF2.Autosubst.pcf_2]
Core.Base [constructor, in PCF2.Autosubst.pcf_2]
Core.bot [constructor, in PCF2.Autosubst.pcf_2]
Core.compRenRen_tm [definition, in PCF2.Autosubst.pcf_2]
Core.compRenSubst_tm [definition, in PCF2.Autosubst.pcf_2]
Core.compSubstRen_tm [definition, in PCF2.Autosubst.pcf_2]
Core.compSubstSubst_tm [definition, in PCF2.Autosubst.pcf_2]
Core.congr_Fun [lemma, in PCF2.Autosubst.pcf_2]
Core.congr_Base [lemma, in PCF2.Autosubst.pcf_2]
Core.congr_lam [lemma, in PCF2.Autosubst.pcf_2]
Core.congr_app [lemma, in PCF2.Autosubst.pcf_2]
Core.congr_trny [lemma, in PCF2.Autosubst.pcf_2]
Core.congr_bot [lemma, in PCF2.Autosubst.pcf_2]
Core.congr_ff [lemma, in PCF2.Autosubst.pcf_2]
Core.congr_tt [lemma, in PCF2.Autosubst.pcf_2]
Core.extRen_tm [definition, in PCF2.Autosubst.pcf_2]
Core.ext_tm [definition, in PCF2.Autosubst.pcf_2]
Core.ff [constructor, in PCF2.Autosubst.pcf_2]
Core.Fun [constructor, in PCF2.Autosubst.pcf_2]
Core.idSubst_tm [definition, in PCF2.Autosubst.pcf_2]
Core.instId'_tm_pointwise [lemma, in PCF2.Autosubst.pcf_2]
Core.instId'_tm [lemma, in PCF2.Autosubst.pcf_2]
Core.lam [constructor, in PCF2.Autosubst.pcf_2]
Core.renRen_tm [lemma, in PCF2.Autosubst.pcf_2]
Core.renRen'_tm_pointwise [lemma, in PCF2.Autosubst.pcf_2]
Core.renSubst_tm_pointwise [lemma, in PCF2.Autosubst.pcf_2]
Core.renSubst_tm [lemma, in PCF2.Autosubst.pcf_2]
Core.ren_tm_morphism2 [instance, in PCF2.Autosubst.pcf_2]
Core.ren_tm_morphism [instance, in PCF2.Autosubst.pcf_2]
Core.Ren_tm [instance, in PCF2.Autosubst.pcf_2]
Core.ren_tm [definition, in PCF2.Autosubst.pcf_2]
Core.rinstId'_tm_pointwise [lemma, in PCF2.Autosubst.pcf_2]
Core.rinstId'_tm [lemma, in PCF2.Autosubst.pcf_2]
Core.rinstInst_up_tm_tm [lemma, in PCF2.Autosubst.pcf_2]
Core.rinstInst'_tm_pointwise [lemma, in PCF2.Autosubst.pcf_2]
Core.rinstInst'_tm [lemma, in PCF2.Autosubst.pcf_2]
Core.rinst_inst_tm [definition, in PCF2.Autosubst.pcf_2]
Core.substRen_tm_pointwise [lemma, in PCF2.Autosubst.pcf_2]
Core.substRen_tm [lemma, in PCF2.Autosubst.pcf_2]
Core.substSubst_tm_pointwise [lemma, in PCF2.Autosubst.pcf_2]
Core.substSubst_tm [lemma, in PCF2.Autosubst.pcf_2]
Core.subst_tm_morphism2 [instance, in PCF2.Autosubst.pcf_2]
Core.subst_tm_morphism [instance, in PCF2.Autosubst.pcf_2]
Core.Subst_tm [instance, in PCF2.Autosubst.pcf_2]
Core.subst_tm [definition, in PCF2.Autosubst.pcf_2]
Core.tm [inductive, in PCF2.Autosubst.pcf_2]
Core.tm_sind [definition, in PCF2.Autosubst.pcf_2]
Core.tm_rec [definition, in PCF2.Autosubst.pcf_2]
Core.tm_ind [definition, in PCF2.Autosubst.pcf_2]
Core.tm_rect [definition, in PCF2.Autosubst.pcf_2]
Core.trny [constructor, in PCF2.Autosubst.pcf_2]
Core.tt [constructor, in PCF2.Autosubst.pcf_2]
Core.ty [inductive, in PCF2.Autosubst.pcf_2]
Core.ty_sind [definition, in PCF2.Autosubst.pcf_2]
Core.ty_rec [definition, in PCF2.Autosubst.pcf_2]
Core.ty_ind [definition, in PCF2.Autosubst.pcf_2]
Core.ty_rect [definition, in PCF2.Autosubst.pcf_2]
Core.upExtRen_tm_tm [lemma, in PCF2.Autosubst.pcf_2]
Core.upExt_tm_tm [lemma, in PCF2.Autosubst.pcf_2]
Core.upId_tm_tm [lemma, in PCF2.Autosubst.pcf_2]
Core.upRen_tm_tm [lemma, in PCF2.Autosubst.pcf_2]
Core.Up_tm_tm [instance, in PCF2.Autosubst.pcf_2]
Core.up_tm [projection, in PCF2.Autosubst.pcf_2]
Core.Up_tm [record, in PCF2.Autosubst.pcf_2]
Core.up_tm [constructor, in PCF2.Autosubst.pcf_2]
Core.Up_tm [inductive, in PCF2.Autosubst.pcf_2]
Core.up_subst_subst_tm_tm [lemma, in PCF2.Autosubst.pcf_2]
Core.up_subst_ren_tm_tm [lemma, in PCF2.Autosubst.pcf_2]
Core.up_ren_subst_tm_tm [lemma, in PCF2.Autosubst.pcf_2]
Core.up_ren_ren_tm_tm [lemma, in PCF2.Autosubst.pcf_2]
Core.up_tm_tm [lemma, in PCF2.Autosubst.pcf_2]
Core.VarInstance_tm [instance, in PCF2.Autosubst.pcf_2]
Core.varLRen'_tm_pointwise [lemma, in PCF2.Autosubst.pcf_2]
Core.varLRen'_tm [lemma, in PCF2.Autosubst.pcf_2]
Core.varL'_tm_pointwise [lemma, in PCF2.Autosubst.pcf_2]
Core.varL'_tm [lemma, in PCF2.Autosubst.pcf_2]
Core.var_tm [constructor, in PCF2.Autosubst.pcf_2]
[ _ ] (fscope) [notation, in PCF2.Autosubst.pcf_2]
⟨ _ ⟩ (fscope) [notation, in PCF2.Autosubst.pcf_2]
_ __tm (subst_scope) [notation, in PCF2.Autosubst.pcf_2]
_ __tm (subst_scope) [notation, in PCF2.Autosubst.pcf_2]
var (subst_scope) [notation, in PCF2.Autosubst.pcf_2]
_ ⟨ _ ⟩ (subst_scope) [notation, in PCF2.Autosubst.pcf_2]
↑__tm (subst_scope) [notation, in PCF2.Autosubst.pcf_2]
↑__tm (subst_scope) [notation, in PCF2.Autosubst.pcf_2]
_ [ _ ] (subst_scope) [notation, in PCF2.Autosubst.pcf_2]
count [definition, in PCF2.external.Shared.FinTypesDef]
co_SR_reduces_CE [lemma, in PCF2.undecidability]
co_RPS_CE [library]
ctxt_comp_fill [lemma, in PCF2.pcf_2_contexts]
ctxt_comp_typed [lemma, in PCF2.pcf_2_contexts]
ctxt_typed_sind [definition, in PCF2.pcf_2_contexts]
ctxt_typed_ind [definition, in PCF2.pcf_2_contexts]
ctxt_typed [inductive, in PCF2.pcf_2_contexts]
cumul [abbreviation, in PCF2.external.Synthetic.ListEnumerabilityFacts]
cumulative [definition, in PCF2.external.Synthetic.ListEnumerabilityFacts]
cumul_spec [lemma, in PCF2.external.Synthetic.ListEnumerabilityFacts]
cumul_spec__T [lemma, in PCF2.external.Synthetic.ListEnumerabilityFacts]
cumul_In [lemma, in PCF2.external.Synthetic.ListEnumerabilityFacts]
cum_ge' [lemma, in PCF2.external.Synthetic.ListEnumerabilityFacts]
cum_ge [lemma, in PCF2.external.Synthetic.ListEnumerabilityFacts]
D
Dec [definition, in PCF2.external.Shared.Dec]dec [definition, in PCF2.external.Shared.Dec]
Dec [definition, in PCF2.external.Shared.EqDecDef]
dec [definition, in PCF2.external.Shared.EqDecDef]
Dec [library]
DecidabilityFacts [library]
decidable [definition, in PCF2.external.Synthetic.Definitions]
decidable_iff' [lemma, in PCF2.external.Synthetic.DecidabilityFacts]
decidable_iff [lemma, in PCF2.external.Synthetic.DecidabilityFacts]
decidable_complement_semi_decidable [lemma, in PCF2.external.Synthetic.SemiDecidabilityFacts]
decidable_semi_decidable [lemma, in PCF2.external.Synthetic.SemiDecidabilityFacts]
decider [definition, in PCF2.external.Synthetic.Definitions]
dec_red [lemma, in PCF2.external.Synthetic.ReducibilityFacts]
Dec_auto [lemma, in PCF2.external.Shared.Dec]
dec_count_enum' [lemma, in PCF2.external.Synthetic.EnumerabilityFacts]
dec_count_enum [lemma, in PCF2.external.Synthetic.EnumerabilityFacts]
dec_disj [lemma, in PCF2.external.Synthetic.DecidabilityFacts]
dec_conj [lemma, in PCF2.external.Synthetic.DecidabilityFacts]
dec_compl' [lemma, in PCF2.external.Synthetic.DecidabilityFacts]
dec_compl [lemma, in PCF2.external.Synthetic.DecidabilityFacts]
dec_decidable' [lemma, in PCF2.external.Synthetic.DecidabilityFacts]
dec2bool [definition, in PCF2.external.Shared.EqDecDef]
Definitions [library]
derived_satis_ineq [lemma, in PCF2.SR_SATIS_forward]
diff [definition, in PCF2.preliminaries]
diff1 [lemma, in PCF2.preliminaries]
diff2 [lemma, in PCF2.preliminaries]
direction [inductive, in PCF2.external.TM.SBTM]
direction_sind [definition, in PCF2.external.TM.SBTM]
direction_rec [definition, in PCF2.external.TM.SBTM]
direction_ind [definition, in PCF2.external.TM.SBTM]
direction_rect [definition, in PCF2.external.TM.SBTM]
direction_enumeration [lemma, in PCF2.external.TM.SBTM_HALT_enum]
discrete [definition, in PCF2.external.Synthetic.DecidabilityFacts]
discrete_list [lemma, in PCF2.external.Synthetic.DecidabilityFacts]
discrete_option [lemma, in PCF2.external.Synthetic.DecidabilityFacts]
discrete_sum [lemma, in PCF2.external.Synthetic.DecidabilityFacts]
discrete_prod [lemma, in PCF2.external.Synthetic.DecidabilityFacts]
discrete_nat [lemma, in PCF2.external.Synthetic.DecidabilityFacts]
discrete_bool [lemma, in PCF2.external.Synthetic.DecidabilityFacts]
discrete_iff [lemma, in PCF2.external.Synthetic.DecidabilityFacts]
E
el_T [definition, in PCF2.external.Synthetic.ListEnumerabilityFacts]embed [definition, in PCF2.pcf_2_system]
Empty_set_eq_dec [instance, in PCF2.external.Shared.Dec]
enc_typed [lemma, in PCF2.SATIS_facts]
enum [projection, in PCF2.external.Shared.FinTypesDef]
EnumerabilityFacts [library]
enumerable [definition, in PCF2.external.Synthetic.Definitions]
enumerable_enumerable_T [lemma, in PCF2.external.Synthetic.EnumerabilityFacts]
enumerable__T [definition, in PCF2.external.Synthetic.EnumerabilityFacts]
enumerable_semi_decidable [lemma, in PCF2.external.Synthetic.EnumerabilityFacts]
enumerable_enum [lemma, in PCF2.external.Synthetic.ListEnumerabilityFacts]
enumerable_list [lemma, in PCF2.external.Synthetic.ListEnumerabilityFacts]
enumerable__T_list_enumerable [lemma, in PCF2.external.Synthetic.ListEnumerabilityFacts]
enumerable_list_enumerable [lemma, in PCF2.external.Synthetic.ListEnumerabilityFacts]
enumerator [definition, in PCF2.external.Synthetic.Definitions]
enumerator_enumerable [lemma, in PCF2.external.Synthetic.EnumerabilityFacts]
enumerator__T_Vector [lemma, in PCF2.external.Synthetic.EnumerabilityFacts]
enumerator__T_Fin [lemma, in PCF2.external.Synthetic.EnumerabilityFacts]
enumerator__T_finType [lemma, in PCF2.external.Synthetic.EnumerabilityFacts]
enumerator__T_sigT2 [lemma, in PCF2.external.Synthetic.EnumerabilityFacts]
enumerator__T_sigT [lemma, in PCF2.external.Synthetic.EnumerabilityFacts]
enumerator__T_option [lemma, in PCF2.external.Synthetic.EnumerabilityFacts]
enumerator__T_sum [lemma, in PCF2.external.Synthetic.EnumerabilityFacts]
enumerator__T_prod [lemma, in PCF2.external.Synthetic.EnumerabilityFacts]
enumerator__T_bool [lemma, in PCF2.external.Synthetic.EnumerabilityFacts]
enumerator__T_unit [lemma, in PCF2.external.Synthetic.EnumerabilityFacts]
enumerator__T_nat [lemma, in PCF2.external.Synthetic.EnumerabilityFacts]
enumerator__T [abbreviation, in PCF2.external.Synthetic.EnumerabilityFacts]
enumerator__T' [definition, in PCF2.external.Synthetic.EnumerabilityFacts]
enumerator__T_of_list [instance, in PCF2.external.Synthetic.ListEnumerabilityFacts]
enumerator__T_to_list [instance, in PCF2.external.Synthetic.ListEnumerabilityFacts]
enumerator__T_list [lemma, in PCF2.external.Synthetic.ListEnumerabilityFacts]
enumerator_list_enumerator.e [variable, in PCF2.external.Synthetic.ListEnumerabilityFacts]
enumerator_list_enumerator.T [variable, in PCF2.external.Synthetic.ListEnumerabilityFacts]
enumerator_list_enumerator.X [variable, in PCF2.external.Synthetic.ListEnumerabilityFacts]
enumerator_list_enumerator [section, in PCF2.external.Synthetic.ListEnumerabilityFacts]
enumerator_to_list_enumerator [lemma, in PCF2.external.Synthetic.ListEnumerabilityFacts]
enumerator_list_enumerator.T [variable, in PCF2.external.Synthetic.ListEnumerabilityFacts]
enumerator_list_enumerator.e [variable, in PCF2.external.Synthetic.ListEnumerabilityFacts]
enumerator_list_enumerator.p [variable, in PCF2.external.Synthetic.ListEnumerabilityFacts]
enumerator_list_enumerator.X [variable, in PCF2.external.Synthetic.ListEnumerabilityFacts]
enumerator_list_enumerator [section, in PCF2.external.Synthetic.ListEnumerabilityFacts]
enum_ok [projection, in PCF2.external.Shared.FinTypesDef]
enum_enumT [lemma, in PCF2.external.Synthetic.ListEnumerabilityFacts]
EqDecDef [library]
eqType [record, in PCF2.external.Shared.EqDecDef]
eqType_CS [definition, in PCF2.external.Shared.EqDecDef]
eqType_dec [projection, in PCF2.external.Shared.EqDecDef]
eqType_X [projection, in PCF2.external.Shared.EqDecDef]
equiv_empty_imp_equiv_nonempty [lemma, in PCF2.CE_facts]
eq_dec [definition, in PCF2.preliminaries]
evaluates_to_same [lemma, in PCF2.pcf_2_system]
evaluates_steps [instance, in PCF2.pcf_2_system]
evaluates_to_base [definition, in PCF2.pcf_2_system]
evaluates_to_final [lemma, in PCF2.CE_facts]
eval_step [lemma, in PCF2.pcf_2_system]
Extra [module, in PCF2.Autosubst.pcf_2]
F
False_eq_dec [instance, in PCF2.external.Shared.Dec]False_dec [instance, in PCF2.external.Shared.Dec]
Fext [module, in PCF2.Autosubst.pcf_2]
Fext.instId_tm [lemma, in PCF2.Autosubst.pcf_2]
Fext.renRen'_tm [lemma, in PCF2.Autosubst.pcf_2]
Fext.renSubst'_tm [lemma, in PCF2.Autosubst.pcf_2]
Fext.rinstId_tm [lemma, in PCF2.Autosubst.pcf_2]
Fext.rinstInst_tm [lemma, in PCF2.Autosubst.pcf_2]
Fext.substRen'_tm [lemma, in PCF2.Autosubst.pcf_2]
Fext.substSubst'_tm [lemma, in PCF2.Autosubst.pcf_2]
Fext.varLRen_tm [lemma, in PCF2.Autosubst.pcf_2]
Fext.varL_tm [lemma, in PCF2.Autosubst.pcf_2]
ff_typed [constructor, in PCF2.pcf_2_system]
fill [definition, in PCF2.pcf_2_contexts]
fill_step [lemma, in PCF2.pcf_2_contexts]
fill_type [lemma, in PCF2.pcf_2_contexts]
finType [record, in PCF2.external.Shared.FinTypesDef]
finTypeC [record, in PCF2.external.Shared.FinTypesDef]
FinTypesDef [library]
finType_CS [definition, in PCF2.external.Shared.FinTypesDef]
finType_enum [definition, in PCF2.external.Synthetic.EnumerabilityFacts]
Fin_enum [definition, in PCF2.external.Synthetic.EnumerabilityFacts]
funcomp [definition, in PCF2.Autosubst.core]
funcomp_charact [lemma, in PCF2.pcf_2_system]
funcomp_morphism2 [instance, in PCF2.Autosubst.core]
funcomp_morphism [instance, in PCF2.Autosubst.core]
funcomp_assoc [lemma, in PCF2.Autosubst.core]
fun_rev_to_context [lemma, in PCF2.pcf_2_utils]
fun_typed [constructor, in PCF2.pcf_2_system]
fun_rule_enc_rev [lemma, in PCF2.SATIS_PS]
fun_rule_encoding_many_exist [lemma, in PCF2.SATIS_PS]
fun_rule_enc_exist [lemma, in PCF2.SATIS_PS]
fun_rule_encoding_many [definition, in PCF2.SATIS_PS]
fun_rule_encoding [definition, in PCF2.SATIS]
fv_subst [lemma, in PCF2.pcf_2_system]
G
G [definition, in PCF2.co_RPS_CE]go_right [constructor, in PCF2.external.TM.SBTM]
go_left [constructor, in PCF2.external.TM.SBTM]
G_charact' [lemma, in PCF2.co_RPS_CE]
G_solves [lemma, in PCF2.co_RPS_CE]
G_subst [lemma, in PCF2.co_RPS_CE]
G_steps [lemma, in PCF2.co_RPS_CE]
G_typed [lemma, in PCF2.co_RPS_CE]
I
id [definition, in PCF2.Autosubst.unscoped]ids [projection, in PCF2.Autosubst.unscoped]
ids [constructor, in PCF2.Autosubst.unscoped]
idsRen [instance, in PCF2.Autosubst.unscoped]
IfB [constructor, in PCF2.pcf_2_system]
IfF [constructor, in PCF2.pcf_2_system]
iff_dec [instance, in PCF2.external.Shared.Dec]
IfT [constructor, in PCF2.pcf_2_system]
if_proper [instance, in PCF2.pcf_2_system]
if_trm2 [lemma, in PCF2.pcf_2_system]
if_trm1 [lemma, in PCF2.pcf_2_system]
if_cond [lemma, in PCF2.pcf_2_system]
If_nested [constructor, in PCF2.pcf_2_system]
If1 [constructor, in PCF2.pcf_2_system]
If2 [constructor, in PCF2.pcf_2_system]
If3 [constructor, in PCF2.pcf_2_system]
impl_dec [instance, in PCF2.external.Shared.Dec]
ineq_subst [lemma, in PCF2.CE_facts]
ineq_ren [lemma, in PCF2.CE_facts]
inf_to_enumerator [instance, in PCF2.external.Synthetic.ListEnumerabilityFacts]
inf_list_enumerable__T [definition, in PCF2.external.Synthetic.ListEnumerabilityFacts]
interface [module, in PCF2.Autosubst.pcf_2]
In_cumul [lemma, in PCF2.external.Synthetic.ListEnumerabilityFacts]
iq_sys_wf_cons_char [lemma, in PCF2.PS_facts]
iq_sys_val_cons_char [lemma, in PCF2.PS_facts]
is_bval [definition, in PCF2.pcf_2_system]
iter_succ_l [lemma, in PCF2.preliminaries]
iter_succ_r [lemma, in PCF2.preliminaries]
iter_ren_closed [lemma, in PCF2.pcf_2_system]
L
Lam [constructor, in PCF2.pcf_2_system]lam_list_to_type' [lemma, in PCF2.pcf_2_utils]
lam_list_to_type [lemma, in PCF2.pcf_2_utils]
lam_T_split [lemma, in PCF2.pcf_2_utils]
lam_T_shift_subst [lemma, in PCF2.pcf_2_utils]
lam_T [definition, in PCF2.pcf_2_utils]
lam_proper [instance, in PCF2.pcf_2_system]
lam_args_subst [lemma, in PCF2.SATIS_PS]
lam_subst_typed [lemma, in PCF2.CE_facts]
lam_subst_step [lemma, in PCF2.CE_facts]
lam_subst_concat [lemma, in PCF2.CE_facts]
lam_subst [definition, in PCF2.CE_facts]
leb_le_false [lemma, in PCF2.preliminaries]
leb_le_true [lemma, in PCF2.preliminaries]
length_base_context [lemma, in PCF2.pcf_2_utils]
length_var_seq [lemma, in PCF2.pcf_2_utils]
ListEnumerabilityFacts [library]
list_eq [lemma, in PCF2.preliminaries]
list_eq_dec [lemma, in PCF2.preliminaries]
list_to_fun_app' [lemma, in PCF2.pcf_2_utils]
list_to_fun [definition, in PCF2.pcf_2_utils]
list_eq_dec [instance, in PCF2.external.Shared.Dec]
list_val_exist [lemma, in PCF2.SATIS_PS]
list_comp [definition, in PCF2.Autosubst.core]
list_id [definition, in PCF2.Autosubst.core]
list_ext [definition, in PCF2.Autosubst.core]
list_enumerator_to_cumul [lemma, in PCF2.external.Synthetic.ListEnumerabilityFacts]
list_enumerable__T_enumerable [lemma, in PCF2.external.Synthetic.ListEnumerabilityFacts]
list_enumerable_enumerable [lemma, in PCF2.external.Synthetic.ListEnumerabilityFacts]
list_enumerator_enumerator [lemma, in PCF2.external.Synthetic.ListEnumerabilityFacts]
list_enumerator_to_enumerator [lemma, in PCF2.external.Synthetic.ListEnumerabilityFacts]
list_enumerable__T [definition, in PCF2.external.Synthetic.ListEnumerabilityFacts]
list_enumerator__T [abbreviation, in PCF2.external.Synthetic.ListEnumerabilityFacts]
list_enumerator__T' [definition, in PCF2.external.Synthetic.ListEnumerabilityFacts]
list_enumerable [definition, in PCF2.external.Synthetic.ListEnumerabilityFacts]
list_enumerator [definition, in PCF2.external.Synthetic.ListEnumerabilityFacts]
list_in_dec [instance, in PCF2.external.Synthetic.ListEnumerabilityFacts]
ltb_lt_false [lemma, in PCF2.preliminaries]
ltb_lt_true [lemma, in PCF2.preliminaries]
L_T [definition, in PCF2.external.Synthetic.ListEnumerabilityFacts]
L_list_cumulative [lemma, in PCF2.external.Synthetic.ListEnumerabilityFacts]
L_list [definition, in PCF2.external.Synthetic.ListEnumerabilityFacts]
L_list_def.L [variable, in PCF2.external.Synthetic.ListEnumerabilityFacts]
L_list_def [section, in PCF2.external.Synthetic.ListEnumerabilityFacts]
M
make_rule_types_length [lemma, in PCF2.SATIS_facts]make_rule_types [definition, in PCF2.SATIS]
mv [definition, in PCF2.external.TM.SBTM]
N
nat_ord_dec [lemma, in PCF2.preliminaries]nat_eq_dec [instance, in PCF2.external.Shared.Dec]
nat_enum [definition, in PCF2.external.Synthetic.EnumerabilityFacts]
norm_comp [constructor, in PCF2.CE]
norm_bot_min [constructor, in PCF2.CE]
not_dec [instance, in PCF2.external.Shared.Dec]
num_states [projection, in PCF2.external.TM.SBTM]
O
obind [definition, in PCF2.external.TM.SBTM]obs_equiv [definition, in PCF2.CE]
obs_preorder [definition, in PCF2.CE]
obs_preorder_closed [definition, in PCF2.CE]
obs_preorder_base_sind [definition, in PCF2.CE]
obs_preorder_base_ind [definition, in PCF2.CE]
obs_preorder_base [inductive, in PCF2.CE]
obs_preorder_empty_imp_obs_preorder_closed [lemma, in PCF2.CE_facts]
obs_equiv_Equiv [instance, in PCF2.CE_facts]
obs_equiv_rest [definition, in PCF2.CE_facts]
obs_equiv_trans [lemma, in PCF2.CE_facts]
obs_equiv_refl [lemma, in PCF2.CE_facts]
obs_equiv_rewrite_right [lemma, in PCF2.CE_facts]
obs_equiv_rewrite_left [lemma, in PCF2.CE_facts]
obs_preorder_PreOrder [instance, in PCF2.CE_facts]
obs_preorder_rest [definition, in PCF2.CE_facts]
obs_equiv_obs_preorder [instance, in PCF2.CE_facts]
obs_equiv_imp_cont_equiv [lemma, in PCF2.CE_facts]
obs_equiv_imp_cont_pre_order [lemma, in PCF2.CE_facts]
obs_equiv_base_eval_same [lemma, in PCF2.CE_facts]
obs_equiv_context [lemma, in PCF2.CE_facts]
obs_preorder_context [lemma, in PCF2.CE_facts]
obs_preorder_base_refl [lemma, in PCF2.CE_facts]
obs_preorder_base_bot [lemma, in PCF2.CE_facts]
obs_preorder_incl_steps' [lemma, in PCF2.CE_facts]
obs_preorder_incl_step' [lemma, in PCF2.CE_facts]
obs_preorder_closed_incl_step' [lemma, in PCF2.CE_facts]
obs_preorder_incl_steps [lemma, in PCF2.CE_facts]
obs_preorder_incl_step [lemma, in PCF2.CE_facts]
obs_preorder_closed_incl_step [lemma, in PCF2.CE_facts]
obs_preorder_fun_char [lemma, in PCF2.CE_facts]
obs_preorder_closed_fun_char [lemma, in PCF2.CE_facts]
obs_preorder_trans [lemma, in PCF2.CE_facts]
obs_preorder_closed_trans [lemma, in PCF2.CE_facts]
obs_preorder_refl [lemma, in PCF2.CE_facts]
obs_preorder_closed_refl [lemma, in PCF2.CE_facts]
obs_preorder_closed_steps [lemma, in PCF2.CE_facts]
option_eq_dec [instance, in PCF2.external.Shared.Dec]
option_enum [definition, in PCF2.external.Synthetic.EnumerabilityFacts]
option_comp [definition, in PCF2.Autosubst.core]
option_ext [definition, in PCF2.Autosubst.core]
option_id [definition, in PCF2.Autosubst.core]
option_map [definition, in PCF2.Autosubst.core]
or_dec [instance, in PCF2.external.Shared.Dec]
P
pair_eq_dec [lemma, in PCF2.preliminaries]pcf_2_system [library]
pcf_2_utils [library]
pcf_2_contexts [library]
pcf_2 [library]
pctxt [inductive, in PCF2.pcf_2_contexts]
pctxtAppL [constructor, in PCF2.pcf_2_contexts]
pctxtAppR [constructor, in PCF2.pcf_2_contexts]
pctxtHole [constructor, in PCF2.pcf_2_contexts]
pctxtLam [constructor, in PCF2.pcf_2_contexts]
pctxtTrny1 [constructor, in PCF2.pcf_2_contexts]
pctxtTrny2 [constructor, in PCF2.pcf_2_contexts]
pctxtTrny3 [constructor, in PCF2.pcf_2_contexts]
pctxt_typed_AppR [constructor, in PCF2.pcf_2_contexts]
pctxt_typed_AppL [constructor, in PCF2.pcf_2_contexts]
pctxt_typed_Lam [constructor, in PCF2.pcf_2_contexts]
pctxt_typed_Trnry3 [constructor, in PCF2.pcf_2_contexts]
pctxt_typed_Trnry2 [constructor, in PCF2.pcf_2_contexts]
pctxt_typed_Trnry1 [constructor, in PCF2.pcf_2_contexts]
pctxt_typed_Hole [constructor, in PCF2.pcf_2_contexts]
pctxt_sind [definition, in PCF2.pcf_2_contexts]
pctxt_rec [definition, in PCF2.pcf_2_contexts]
pctxt_ind [definition, in PCF2.pcf_2_contexts]
pctxt_rect [definition, in PCF2.pcf_2_contexts]
pointwise_forall [lemma, in PCF2.Autosubst.core]
preliminaries [library]
pre_order_imp_obs_preorder [lemma, in PCF2.CE_facts]
pre_order_imp_obs_preorder_closed [lemma, in PCF2.CE_facts]
prod_eq_dec [instance, in PCF2.external.Shared.Dec]
prod_enum [definition, in PCF2.external.Synthetic.EnumerabilityFacts]
prod_comp [definition, in PCF2.Autosubst.core]
prod_ext [definition, in PCF2.Autosubst.core]
prod_id [definition, in PCF2.Autosubst.core]
prod_map [definition, in PCF2.Autosubst.core]
Properties [section, in PCF2.external.Synthetic.ReducibilityFacts]
Properties.P [variable, in PCF2.external.Synthetic.ReducibilityFacts]
Properties.Q [variable, in PCF2.external.Synthetic.ReducibilityFacts]
Properties.R [variable, in PCF2.external.Synthetic.ReducibilityFacts]
Properties.X [variable, in PCF2.external.Synthetic.ReducibilityFacts]
Properties.Y [variable, in PCF2.external.Synthetic.ReducibilityFacts]
Properties.Z [variable, in PCF2.external.Synthetic.ReducibilityFacts]
Proper_decidable [instance, in PCF2.external.Synthetic.DecidabilityFacts]
Proper_decides [instance, in PCF2.external.Synthetic.DecidabilityFacts]
PS [definition, in PCF2.PS]
PS [library]
ps_system_type_list_to_fun_rev [lemma, in PCF2.SATIS_PS]
ps_system_char_SATIS [lemma, in PCF2.SATIS_PS]
ps_system_char_enc_exist [lemma, in PCF2.SATIS_PS]
ps_system_char_enc [definition, in PCF2.SATIS_PS]
ps_system_type [definition, in PCF2.SATIS_PS]
ps_system_char_bool_exist [lemma, in PCF2.SATIS_PS]
ps_system_char_bool [definition, in PCF2.SATIS_PS]
ps_system_well_formed [definition, in PCF2.PS]
ps_system_solvable [definition, in PCF2.PS]
ps_system [abbreviation, in PCF2.PS]
PS_RPS [library]
PS_facts [library]
R
reduces [definition, in PCF2.external.Synthetic.Definitions]reduces_SR_SATIS_forward [lemma, in PCF2.SR_SATIS_forward]
reduces_complement [lemma, in PCF2.external.Synthetic.ReducibilityFacts]
reduces_dependent [lemma, in PCF2.external.Synthetic.ReducibilityFacts]
reduces_transitive [lemma, in PCF2.external.Synthetic.ReducibilityFacts]
reduces_reflexive [lemma, in PCF2.external.Synthetic.ReducibilityFacts]
reduces_co_SATIS_co_PS [lemma, in PCF2.SATIS_PS]
reduces_SATIS_PS [lemma, in PCF2.SATIS_PS]
reduces_co_RPS_CE_closed [lemma, in PCF2.co_RPS_CE]
reduces_co_PS_co_RPS [lemma, in PCF2.PS_RPS]
reduces_PS_RPS [lemma, in PCF2.PS_RPS]
reduces_CE_CE_open [lemma, in PCF2.undecidability]
reduces_co_SR_co_SATIS [lemma, in PCF2.undecidability]
reduces_SR_SATIS [lemma, in PCF2.undecidability]
ReducibilityFacts [library]
reduction [definition, in PCF2.external.Synthetic.Definitions]
ReductionChainNotations [module, in PCF2.external.Synthetic.ReducibilityFacts]
red_comp [lemma, in PCF2.external.Synthetic.ReducibilityFacts]
reflects [definition, in PCF2.external.Synthetic.Definitions]
reflects_prv [lemma, in PCF2.external.Synthetic.DecidabilityFacts]
reflects_disj [lemma, in PCF2.external.Synthetic.DecidabilityFacts]
reflects_conj [lemma, in PCF2.external.Synthetic.DecidabilityFacts]
reflects_not [lemma, in PCF2.external.Synthetic.DecidabilityFacts]
RenNotations [module, in PCF2.Autosubst.unscoped]
⟨ _ ; _ ⟩ (fscope) [notation, in PCF2.Autosubst.unscoped]
⟨ _ ⟩ (fscope) [notation, in PCF2.Autosubst.unscoped]
_ ⟨ _ ; _ ; _ ; _ ; _ ⟩ (subst_scope) [notation, in PCF2.Autosubst.unscoped]
_ ⟨ _ ; _ ; _ ; _ ⟩ (subst_scope) [notation, in PCF2.Autosubst.unscoped]
_ ⟨ _ ; _ ; _ ⟩ (subst_scope) [notation, in PCF2.Autosubst.unscoped]
_ ⟨ _ ; _ ⟩ (subst_scope) [notation, in PCF2.Autosubst.unscoped]
_ ⟨ _ ⟩ (subst_scope) [notation, in PCF2.Autosubst.unscoped]
ren_apply_args [lemma, in PCF2.pcf_2_utils]
ren_var [lemma, in PCF2.SR_SATIS_forward]
ren_shift_shifted_t_subst_char [lemma, in PCF2.SR_SATIS_forward]
ren_shift_typed [lemma, in PCF2.SR_SATIS_forward]
ren_shift_well_typed' [lemma, in PCF2.SR_SATIS_forward]
ren_shift_well_typed [lemma, in PCF2.SR_SATIS_forward]
ren_shift [definition, in PCF2.SR_SATIS_forward]
ren_subst [lemma, in PCF2.pcf_2_system]
ren_preserves [lemma, in PCF2.pcf_2_system]
ren_preserves' [lemma, in PCF2.pcf_2_system]
ren_well_typed [definition, in PCF2.pcf_2_system]
ren1 [projection, in PCF2.Autosubst.unscoped]
Ren1 [record, in PCF2.Autosubst.unscoped]
ren1 [constructor, in PCF2.Autosubst.unscoped]
Ren1 [inductive, in PCF2.Autosubst.unscoped]
ren2 [projection, in PCF2.Autosubst.unscoped]
Ren2 [record, in PCF2.Autosubst.unscoped]
ren2 [constructor, in PCF2.Autosubst.unscoped]
Ren2 [inductive, in PCF2.Autosubst.unscoped]
ren3 [projection, in PCF2.Autosubst.unscoped]
Ren3 [record, in PCF2.Autosubst.unscoped]
ren3 [constructor, in PCF2.Autosubst.unscoped]
Ren3 [inductive, in PCF2.Autosubst.unscoped]
ren4 [projection, in PCF2.Autosubst.unscoped]
Ren4 [record, in PCF2.Autosubst.unscoped]
ren4 [constructor, in PCF2.Autosubst.unscoped]
Ren4 [inductive, in PCF2.Autosubst.unscoped]
ren5 [projection, in PCF2.Autosubst.unscoped]
Ren5 [record, in PCF2.Autosubst.unscoped]
ren5 [constructor, in PCF2.Autosubst.unscoped]
Ren5 [inductive, in PCF2.Autosubst.unscoped]
restrict_sys [lemma, in PCF2.PS_RPS]
rest_PCF [definition, in PCF2.CE_facts]
res_ineq_sys_val_cons_char [lemma, in PCF2.RPS_facts]
rev_nth_error2 [lemma, in PCF2.preliminaries]
rev_nth_error1 [lemma, in PCF2.preliminaries]
rew [inductive, in PCF2.external.SR]
rewB [constructor, in PCF2.external.SR]
rewR [constructor, in PCF2.external.SR]
rewrite_in_evaluates [instance, in PCF2.CE_facts]
rewrite_in_obs_preorder_base [instance, in PCF2.CE_facts]
rewS [constructor, in PCF2.external.SR]
rewt [inductive, in PCF2.external.SR]
rewt_sind [definition, in PCF2.external.SR]
rewt_ind [definition, in PCF2.external.SR]
rew_sind [definition, in PCF2.external.SR]
rew_ind [definition, in PCF2.external.SR]
riq_sys_wf_cons_char [lemma, in PCF2.RPS_facts]
RoseTree [module, in PCF2.external.Synthetic.EnumerabilityFacts]
RoseTree.Auxiliary [section, in PCF2.external.Synthetic.EnumerabilityFacts]
RoseTree.Auxiliary.of_nat' [variable, in PCF2.external.Synthetic.EnumerabilityFacts]
RoseTree.Auxiliary.to_nat' [variable, in PCF2.external.Synthetic.EnumerabilityFacts]
RoseTree.cancel_to_of [lemma, in PCF2.external.Synthetic.EnumerabilityFacts]
RoseTree.cancel_of_to [lemma, in PCF2.external.Synthetic.EnumerabilityFacts]
RoseTree.mk [constructor, in PCF2.external.Synthetic.EnumerabilityFacts]
RoseTree.of_nat [definition, in PCF2.external.Synthetic.EnumerabilityFacts]
RoseTree.t [inductive, in PCF2.external.Synthetic.EnumerabilityFacts]
RoseTree.to_enumerable_T [lemma, in PCF2.external.Synthetic.EnumerabilityFacts]
RoseTree.to_enumerator__T [lemma, in PCF2.external.Synthetic.EnumerabilityFacts]
RoseTree.to_nat [definition, in PCF2.external.Synthetic.EnumerabilityFacts]
RoseTree.t_sind [definition, in PCF2.external.Synthetic.EnumerabilityFacts]
RoseTree.t_rec [definition, in PCF2.external.Synthetic.EnumerabilityFacts]
RoseTree.t_ind [definition, in PCF2.external.Synthetic.EnumerabilityFacts]
RoseTree.t_rect [definition, in PCF2.external.Synthetic.EnumerabilityFacts]
RPS [definition, in PCF2.RPS]
RPS [library]
rps_system_well_formed [definition, in PCF2.RPS]
rps_system_solvable [definition, in PCF2.RPS]
rps_system [abbreviation, in PCF2.RPS]
RPS_facts [library]
RuleNotation [module, in PCF2.external.SR]
_ / _ [notation, in PCF2.external.SR]
rules_eq_decidable [lemma, in PCF2.preliminaries]
rule_enc_word_enc_closed' [lemma, in PCF2.SATIS_facts]
rule_enc_word_enc_closed [lemma, in PCF2.SATIS_facts]
rule_enc_equiv [lemma, in PCF2.SATIS_facts]
rule_some [lemma, in PCF2.SATIS_facts]
rule_fun [definition, in PCF2.SATIS]
rule_enc_exist [axiom, in PCF2.SATIS]
rule_encoding [definition, in PCF2.SATIS]
rule_ineq [definition, in PCF2.SATIS]
rule_type [definition, in PCF2.SATIS]
S
SATIS [definition, in PCF2.SATIS]SATIS [library]
satisfies [definition, in PCF2.SATIS]
satisfies_rule_enc_ind [lemma, in PCF2.SATIS_PS]
SATIS_facts [library]
SATIS_PS [library]
SBTM [record, in PCF2.external.TM.SBTM]
SBTM [library]
SBTMNotations [module, in PCF2.external.TM.SBTM]
SBTMNotations.config [abbreviation, in PCF2.external.TM.SBTM]
SBTMNotations.state [abbreviation, in PCF2.external.TM.SBTM]
SBTMNotations.tape [abbreviation, in PCF2.external.TM.SBTM]
SBTM_HALT_undec [lemma, in PCF2.external.TM.SBTM_undec]
SBTM_HALT [definition, in PCF2.external.TM.SBTM]
SBTM_HALT_enumerator_spec [lemma, in PCF2.external.TM.SBTM_HALT_enum]
SBTM_HALT_enumerator [definition, in PCF2.external.TM.SBTM_HALT_enum]
SBTM_HALT_enumeration [lemma, in PCF2.external.TM.SBTM_HALT_enum]
SBTM_HALT_INSTANCE_enumeration [lemma, in PCF2.external.TM.SBTM_HALT_enum]
SBTM_enumeration [lemma, in PCF2.external.TM.SBTM_HALT_enum]
SBTM_of_sigT [definition, in PCF2.external.TM.SBTM_HALT_enum]
SBTM_to_sigT [definition, in PCF2.external.TM.SBTM_HALT_enum]
SBTM_HALT_semi_decision [lemma, in PCF2.external.TM.SBTM_HALT_enum]
SBTM_undec [library]
SBTM_HALT_enum [library]
scons [definition, in PCF2.Autosubst.unscoped]
scons_comp [lemma, in PCF2.Autosubst.unscoped_axioms]
scons_eta [lemma, in PCF2.Autosubst.unscoped_axioms]
scons_eta_id [lemma, in PCF2.Autosubst.unscoped_axioms]
scons_morphism2 [instance, in PCF2.Autosubst.unscoped]
scons_morphism [instance, in PCF2.Autosubst.unscoped]
scons_comp' [lemma, in PCF2.Autosubst.unscoped]
scons_eta_id' [lemma, in PCF2.Autosubst.unscoped]
scons_eta' [lemma, in PCF2.Autosubst.unscoped]
SemiDecidabilityFacts [library]
semi_decidable [definition, in PCF2.external.Synthetic.Definitions]
semi_decider [definition, in PCF2.external.Synthetic.Definitions]
semi_decidable_enumerable [lemma, in PCF2.external.Synthetic.EnumerabilityFacts]
semi_decider_enumerator [lemma, in PCF2.external.Synthetic.EnumerabilityFacts]
shift [definition, in PCF2.Autosubst.unscoped]
shifted_subst_char [lemma, in PCF2.pcf_2_system]
shifted_subst [definition, in PCF2.pcf_2_system]
shift_t_subst_well_typed [lemma, in PCF2.SR_SATIS_forward]
sigT_enum [definition, in PCF2.external.Synthetic.EnumerabilityFacts]
sigT2_enum [definition, in PCF2.external.Synthetic.EnumerabilityFacts]
solves_rps_system [definition, in PCF2.RPS]
solves_ps_system [definition, in PCF2.PS]
SR [definition, in PCF2.external.SR]
SR [library]
SRS [abbreviation, in PCF2.external.SR]
SR_undec [axiom, in PCF2.undecidability]
SR_SATIS_equiv [axiom, in PCF2.undecidability]
SR_SATIS_forward [library]
step [inductive, in PCF2.pcf_2_system]
step [definition, in PCF2.external.TM.SBTM]
steps [definition, in PCF2.pcf_2_system]
steps [definition, in PCF2.external.TM.SBTM]
steps_n1 [lemma, in PCF2.pcf_2_system]
steps_1n [lemma, in PCF2.pcf_2_system]
steps_PreOrder [instance, in PCF2.pcf_2_system]
steps_preserve_obs_preorder_backward [lemma, in PCF2.CE_facts]
steps_preserve_obs_preorder [lemma, in PCF2.CE_facts]
steps_equiv [lemma, in PCF2.CE_facts]
step_eval [lemma, in PCF2.pcf_2_system]
step_steps [instance, in PCF2.pcf_2_system]
step_sind [definition, in PCF2.pcf_2_system]
step_ind [definition, in PCF2.pcf_2_system]
str [abbreviation, in PCF2.external.SR]
string [abbreviation, in PCF2.external.SR]
strong_obs_preorder_imp_obs_preorder [lemma, in PCF2.CE_facts]
strong_obs_preorder_refl [lemma, in PCF2.CE_facts]
strong_obs_preorder_steps [lemma, in PCF2.CE_facts]
strong_obs_preorder [definition, in PCF2.CE_facts]
SubstNotations [module, in PCF2.Autosubst.unscoped]
_ [ _ ; _ ] (subst_scope) [notation, in PCF2.Autosubst.unscoped]
_ [ _ ] (subst_scope) [notation, in PCF2.Autosubst.unscoped]
subst_apply_args [lemma, in PCF2.pcf_2_utils]
subst_map_closed_list [lemma, in PCF2.pcf_2_system]
subst_well_typed_singleton [lemma, in PCF2.pcf_2_system]
subst_well_typed_nil_nil [lemma, in PCF2.pcf_2_system]
subst_closes [lemma, in PCF2.pcf_2_system]
subst_preserves_step [lemma, in PCF2.pcf_2_system]
subst_shift [lemma, in PCF2.pcf_2_system]
subst_concat [lemma, in PCF2.pcf_2_system]
subst_charact [lemma, in PCF2.pcf_2_system]
subst_charact_typed [lemma, in PCF2.pcf_2_system]
subst_preserves [lemma, in PCF2.pcf_2_system]
subst_well_typed [definition, in PCF2.pcf_2_system]
subst_bool_var [lemma, in PCF2.SATIS_PS]
subst_nil_ids [lemma, in PCF2.SATIS_PS]
subst_list_shift [lemma, in PCF2.SATIS_PS]
subst_list_subst [lemma, in PCF2.SATIS_PS]
subst_list_subst' [lemma, in PCF2.SATIS_PS]
subst_list_last [lemma, in PCF2.SATIS_PS]
subst_list [definition, in PCF2.SATIS_PS]
subst_equiv [lemma, in PCF2.CE_facts]
subst_rel_nil [lemma, in PCF2.CE_facts]
subst_rel [definition, in PCF2.CE_facts]
subst1 [projection, in PCF2.Autosubst.unscoped]
Subst1 [record, in PCF2.Autosubst.unscoped]
subst1 [constructor, in PCF2.Autosubst.unscoped]
Subst1 [inductive, in PCF2.Autosubst.unscoped]
subst2 [projection, in PCF2.Autosubst.unscoped]
Subst2 [record, in PCF2.Autosubst.unscoped]
subst2 [constructor, in PCF2.Autosubst.unscoped]
Subst2 [inductive, in PCF2.Autosubst.unscoped]
subst3 [projection, in PCF2.Autosubst.unscoped]
Subst3 [record, in PCF2.Autosubst.unscoped]
subst3 [constructor, in PCF2.Autosubst.unscoped]
Subst3 [inductive, in PCF2.Autosubst.unscoped]
subst4 [projection, in PCF2.Autosubst.unscoped]
Subst4 [record, in PCF2.Autosubst.unscoped]
subst4 [constructor, in PCF2.Autosubst.unscoped]
Subst4 [inductive, in PCF2.Autosubst.unscoped]
subst5 [projection, in PCF2.Autosubst.unscoped]
Subst5 [record, in PCF2.Autosubst.unscoped]
subst5 [constructor, in PCF2.Autosubst.unscoped]
Subst5 [inductive, in PCF2.Autosubst.unscoped]
sum_eq_dec [instance, in PCF2.external.Shared.Dec]
sum_enum [definition, in PCF2.external.Synthetic.EnumerabilityFacts]
swap [definition, in PCF2.external.SR]
T
T [definition, in PCF2.SATIS]to_cumul_spec [lemma, in PCF2.external.Synthetic.ListEnumerabilityFacts]
to_cumul_cumulative [lemma, in PCF2.external.Synthetic.ListEnumerabilityFacts]
to_cumul [definition, in PCF2.external.Synthetic.ListEnumerabilityFacts]
trans [projection, in PCF2.external.TM.SBTM]
trans' [definition, in PCF2.external.TM.SBTM]
trny_typed [constructor, in PCF2.pcf_2_system]
True_eq_dec [instance, in PCF2.external.Shared.Dec]
True_dec [instance, in PCF2.external.Shared.Dec]
TSR [definition, in PCF2.external.SR]
tt_typed [constructor, in PCF2.pcf_2_system]
type [projection, in PCF2.external.Shared.FinTypesDef]
typed [inductive, in PCF2.pcf_2_system]
typed_empty_closed [lemma, in PCF2.pcf_2_system]
typed_free_var [lemma, in PCF2.pcf_2_system]
typed_sind [definition, in PCF2.pcf_2_system]
typed_ind [definition, in PCF2.pcf_2_system]
type_preservation [lemma, in PCF2.pcf_2_system]
type_preservation_step [lemma, in PCF2.pcf_2_system]
type_weakening [lemma, in PCF2.pcf_2_system]
t_subst_rule [lemma, in PCF2.SR_SATIS_forward]
t_subst_map_var_id'' [lemma, in PCF2.SR_SATIS_forward]
t_subst_initial [lemma, in PCF2.SATIS_facts]
t_subst_map_var_rules' [lemma, in PCF2.SATIS_facts]
t_subst_map_var_rules [lemma, in PCF2.SATIS_facts]
t_subst_map_var_id' [lemma, in PCF2.SATIS_facts]
t_subst_map_var_id [lemma, in PCF2.SATIS_facts]
t_subst_well_typed [lemma, in PCF2.SATIS_facts]
T_list_to_fun [lemma, in PCF2.SATIS_facts]
t_subst_char [lemma, in PCF2.SATIS_PS]
t_subst [definition, in PCF2.SATIS]
U
undecidability [section, in PCF2.undecidability]undecidability [library]
Undecidability [library]
undecidabilityNotations [module, in PCF2.external.Synthetic.Undecidability]
undecidability_to_complement [lemma, in PCF2.external.Synthetic.Undecidability]
undecidability_from_complement [lemma, in PCF2.external.Synthetic.Undecidability]
undecidability_from_reducibility [lemma, in PCF2.external.Synthetic.Undecidability]
undecidability.Loaders_word_enc [variable, in PCF2.undecidability]
undecidable [definition, in PCF2.external.Synthetic.Undecidability]
unit_eq_dec [instance, in PCF2.external.Shared.Dec]
unit_enum [definition, in PCF2.external.Synthetic.EnumerabilityFacts]
unscoped [library]
UnscopedNotations [module, in PCF2.Autosubst.unscoped]
↑ (subst_scope) [notation, in PCF2.Autosubst.unscoped]
_ .. (subst_scope) [notation, in PCF2.Autosubst.unscoped]
unscoped_axioms [library]
up_tm_tm_iter2 [lemma, in PCF2.pcf_2_system]
up_tm_tm_iter1 [lemma, in PCF2.pcf_2_system]
up_allfv [definition, in PCF2.Autosubst.unscoped]
up_ren_ren [lemma, in PCF2.Autosubst.unscoped]
up_ren [definition, in PCF2.Autosubst.unscoped]
V
val_list_closed [lemma, in PCF2.pcf_2_system]val_no_step [lemma, in PCF2.pcf_2_system]
val_rule_enc [definition, in PCF2.SATIS]
val_word_enc [definition, in PCF2.SATIS]
Var [record, in PCF2.Autosubst.unscoped]
Var [inductive, in PCF2.Autosubst.unscoped]
var_seq_map_nth [lemma, in PCF2.pcf_2_utils]
var_seq_nth [lemma, in PCF2.pcf_2_utils]
var_seq_split [lemma, in PCF2.pcf_2_utils]
var_seq [definition, in PCF2.pcf_2_utils]
var_typed [constructor, in PCF2.pcf_2_system]
var_zero [definition, in PCF2.Autosubst.unscoped]
Vector_enum [definition, in PCF2.external.Synthetic.EnumerabilityFacts]
W
weak_normalisation_comp [axiom, in PCF2.pcf_2_system]well_formed_forall [lemma, in PCF2.PS_RPS]
wf_rps_system [definition, in PCF2.RPS]
wf_ps_system [definition, in PCF2.PS]
word_encoding [definition, in PCF2.SATIS]
other
_ [ _ , _ ] : _ , _ [notation, in PCF2.pcf_2_contexts]_ ⪯ _ [notation, in PCF2.external.Synthetic.Definitions]
_ ⊢ _ [ _ ] [notation, in PCF2.pcf_2_system]
_ ⇓ _ [notation, in PCF2.pcf_2_system]
_ ≻* _ [notation, in PCF2.pcf_2_system]
_ ⊢ _ : _ [notation, in PCF2.pcf_2_system]
_ ≻ _ [notation, in PCF2.pcf_2_system]
_ ⟶ _ [notation, in PCF2.pcf_2_system]
_ ⊢ _ ≡ _ : _ [notation, in PCF2.CE]
_ ⊢ _ ≤ _ : _ [notation, in PCF2.CE]
_ ≤c _ : _ [notation, in PCF2.CE]
_ ≤b _ [notation, in PCF2.CE]
_ ⊢ _ ≡c _ : _ [notation, in PCF2.CE]
eq_dec _ [notation, in PCF2.external.Shared.Dec]
eq_dec _ [notation, in PCF2.external.Shared.EqDecDef]
if! _ is _ then _ else _ [notation, in PCF2.external.Synthetic.EnumerabilityFacts]
list_map [notation, in PCF2.Autosubst.core]
Notation Index
C
_ >> _ (fscope) [in PCF2.Autosubst.unscoped]_ .: _ (subst_scope) [in PCF2.Autosubst.unscoped]
[ _ ] (fscope) [in PCF2.Autosubst.pcf_2]
⟨ _ ⟩ (fscope) [in PCF2.Autosubst.pcf_2]
_ __tm (subst_scope) [in PCF2.Autosubst.pcf_2]
_ __tm (subst_scope) [in PCF2.Autosubst.pcf_2]
var (subst_scope) [in PCF2.Autosubst.pcf_2]
_ ⟨ _ ⟩ (subst_scope) [in PCF2.Autosubst.pcf_2]
↑__tm (subst_scope) [in PCF2.Autosubst.pcf_2]
↑__tm (subst_scope) [in PCF2.Autosubst.pcf_2]
_ [ _ ] (subst_scope) [in PCF2.Autosubst.pcf_2]
R
⟨ _ ; _ ⟩ (fscope) [in PCF2.Autosubst.unscoped]⟨ _ ⟩ (fscope) [in PCF2.Autosubst.unscoped]
_ ⟨ _ ; _ ; _ ; _ ; _ ⟩ (subst_scope) [in PCF2.Autosubst.unscoped]
_ ⟨ _ ; _ ; _ ; _ ⟩ (subst_scope) [in PCF2.Autosubst.unscoped]
_ ⟨ _ ; _ ; _ ⟩ (subst_scope) [in PCF2.Autosubst.unscoped]
_ ⟨ _ ; _ ⟩ (subst_scope) [in PCF2.Autosubst.unscoped]
_ ⟨ _ ⟩ (subst_scope) [in PCF2.Autosubst.unscoped]
_ / _ [in PCF2.external.SR]
S
_ [ _ ; _ ] (subst_scope) [in PCF2.Autosubst.unscoped]_ [ _ ] (subst_scope) [in PCF2.Autosubst.unscoped]
U
↑ (subst_scope) [in PCF2.Autosubst.unscoped]_ .. (subst_scope) [in PCF2.Autosubst.unscoped]
other
_ [ _ , _ ] : _ , _ [in PCF2.pcf_2_contexts]_ ⪯ _ [in PCF2.external.Synthetic.Definitions]
_ ⊢ _ [ _ ] [in PCF2.pcf_2_system]
_ ⇓ _ [in PCF2.pcf_2_system]
_ ≻* _ [in PCF2.pcf_2_system]
_ ⊢ _ : _ [in PCF2.pcf_2_system]
_ ≻ _ [in PCF2.pcf_2_system]
_ ⟶ _ [in PCF2.pcf_2_system]
_ ⊢ _ ≡ _ : _ [in PCF2.CE]
_ ⊢ _ ≤ _ : _ [in PCF2.CE]
_ ≤c _ : _ [in PCF2.CE]
_ ≤b _ [in PCF2.CE]
_ ⊢ _ ≡c _ : _ [in PCF2.CE]
eq_dec _ [in PCF2.external.Shared.Dec]
eq_dec _ [in PCF2.external.Shared.EqDecDef]
if! _ is _ then _ else _ [in PCF2.external.Synthetic.EnumerabilityFacts]
list_map [in PCF2.Autosubst.core]
Module Index
A
Allfv [in PCF2.Autosubst.pcf_2]C
CombineNotations [in PCF2.Autosubst.unscoped]Core [in PCF2.Autosubst.pcf_2]
E
Extra [in PCF2.Autosubst.pcf_2]F
Fext [in PCF2.Autosubst.pcf_2]I
interface [in PCF2.Autosubst.pcf_2]R
ReductionChainNotations [in PCF2.external.Synthetic.ReducibilityFacts]RenNotations [in PCF2.Autosubst.unscoped]
RoseTree [in PCF2.external.Synthetic.EnumerabilityFacts]
RuleNotation [in PCF2.external.SR]
S
SBTMNotations [in PCF2.external.TM.SBTM]SubstNotations [in PCF2.Autosubst.unscoped]
U
undecidabilityNotations [in PCF2.external.Synthetic.Undecidability]UnscopedNotations [in PCF2.Autosubst.unscoped]
Variable Index
E
enumerator_list_enumerator.e [in PCF2.external.Synthetic.ListEnumerabilityFacts]enumerator_list_enumerator.T [in PCF2.external.Synthetic.ListEnumerabilityFacts]
enumerator_list_enumerator.X [in PCF2.external.Synthetic.ListEnumerabilityFacts]
enumerator_list_enumerator.T [in PCF2.external.Synthetic.ListEnumerabilityFacts]
enumerator_list_enumerator.e [in PCF2.external.Synthetic.ListEnumerabilityFacts]
enumerator_list_enumerator.p [in PCF2.external.Synthetic.ListEnumerabilityFacts]
enumerator_list_enumerator.X [in PCF2.external.Synthetic.ListEnumerabilityFacts]
L
L_list_def.L [in PCF2.external.Synthetic.ListEnumerabilityFacts]P
Properties.P [in PCF2.external.Synthetic.ReducibilityFacts]Properties.Q [in PCF2.external.Synthetic.ReducibilityFacts]
Properties.R [in PCF2.external.Synthetic.ReducibilityFacts]
Properties.X [in PCF2.external.Synthetic.ReducibilityFacts]
Properties.Y [in PCF2.external.Synthetic.ReducibilityFacts]
Properties.Z [in PCF2.external.Synthetic.ReducibilityFacts]
R
RoseTree.Auxiliary.of_nat' [in PCF2.external.Synthetic.EnumerabilityFacts]RoseTree.Auxiliary.to_nat' [in PCF2.external.Synthetic.EnumerabilityFacts]
U
undecidability.Loaders_word_enc [in PCF2.undecidability]Library Index
C
CECE_facts
core
core_axioms
co_RPS_CE
D
DecDecidabilityFacts
Definitions
E
EnumerabilityFactsEqDecDef
F
FinTypesDefL
ListEnumerabilityFactsP
pcf_2_systempcf_2_utils
pcf_2_contexts
pcf_2
preliminaries
PS
PS_RPS
PS_facts
R
ReducibilityFactsRPS
RPS_facts
S
SATISSATIS_facts
SATIS_PS
SBTM
SBTM_undec
SBTM_HALT_enum
SemiDecidabilityFacts
SR
SR_SATIS_forward
U
undecidabilityUndecidability
unscoped
unscoped_axioms
Constructor Index
A
AppL [in PCF2.pcf_2_system]AppR [in PCF2.pcf_2_system]
app_typed [in PCF2.pcf_2_system]
B
Beta [in PCF2.pcf_2_system]bot_typed [in PCF2.pcf_2_system]
C
Core.app [in PCF2.Autosubst.pcf_2]Core.Base [in PCF2.Autosubst.pcf_2]
Core.bot [in PCF2.Autosubst.pcf_2]
Core.ff [in PCF2.Autosubst.pcf_2]
Core.Fun [in PCF2.Autosubst.pcf_2]
Core.lam [in PCF2.Autosubst.pcf_2]
Core.trny [in PCF2.Autosubst.pcf_2]
Core.tt [in PCF2.Autosubst.pcf_2]
Core.up_tm [in PCF2.Autosubst.pcf_2]
Core.var_tm [in PCF2.Autosubst.pcf_2]
F
ff_typed [in PCF2.pcf_2_system]fun_typed [in PCF2.pcf_2_system]
G
go_right [in PCF2.external.TM.SBTM]go_left [in PCF2.external.TM.SBTM]
I
ids [in PCF2.Autosubst.unscoped]IfB [in PCF2.pcf_2_system]
IfF [in PCF2.pcf_2_system]
IfT [in PCF2.pcf_2_system]
If_nested [in PCF2.pcf_2_system]
If1 [in PCF2.pcf_2_system]
If2 [in PCF2.pcf_2_system]
If3 [in PCF2.pcf_2_system]
L
Lam [in PCF2.pcf_2_system]N
norm_comp [in PCF2.CE]norm_bot_min [in PCF2.CE]
P
pctxtAppL [in PCF2.pcf_2_contexts]pctxtAppR [in PCF2.pcf_2_contexts]
pctxtHole [in PCF2.pcf_2_contexts]
pctxtLam [in PCF2.pcf_2_contexts]
pctxtTrny1 [in PCF2.pcf_2_contexts]
pctxtTrny2 [in PCF2.pcf_2_contexts]
pctxtTrny3 [in PCF2.pcf_2_contexts]
pctxt_typed_AppR [in PCF2.pcf_2_contexts]
pctxt_typed_AppL [in PCF2.pcf_2_contexts]
pctxt_typed_Lam [in PCF2.pcf_2_contexts]
pctxt_typed_Trnry3 [in PCF2.pcf_2_contexts]
pctxt_typed_Trnry2 [in PCF2.pcf_2_contexts]
pctxt_typed_Trnry1 [in PCF2.pcf_2_contexts]
pctxt_typed_Hole [in PCF2.pcf_2_contexts]
R
ren1 [in PCF2.Autosubst.unscoped]ren2 [in PCF2.Autosubst.unscoped]
ren3 [in PCF2.Autosubst.unscoped]
ren4 [in PCF2.Autosubst.unscoped]
ren5 [in PCF2.Autosubst.unscoped]
rewB [in PCF2.external.SR]
rewR [in PCF2.external.SR]
rewS [in PCF2.external.SR]
RoseTree.mk [in PCF2.external.Synthetic.EnumerabilityFacts]
S
subst1 [in PCF2.Autosubst.unscoped]subst2 [in PCF2.Autosubst.unscoped]
subst3 [in PCF2.Autosubst.unscoped]
subst4 [in PCF2.Autosubst.unscoped]
subst5 [in PCF2.Autosubst.unscoped]
T
trny_typed [in PCF2.pcf_2_system]tt_typed [in PCF2.pcf_2_system]
V
var_typed [in PCF2.pcf_2_system]Lemma Index
A
allfv_tm_dec [in PCF2.pcf_2_system]Allfv.upAllfvImpl_tm_tm [in PCF2.Autosubst.pcf_2]
Allfv.upAllfvRenL_tm_tm [in PCF2.Autosubst.pcf_2]
Allfv.upAllfvRenR_tm_tm [in PCF2.Autosubst.pcf_2]
Allfv.upAllfvTriv_tm_tm [in PCF2.Autosubst.pcf_2]
Allfv.upAllfv_tm_tm [in PCF2.Autosubst.pcf_2]
apply_args_steps_list' [in PCF2.pcf_2_utils]
apply_args_steps_list [in PCF2.pcf_2_utils]
apply_args_steps_body [in PCF2.pcf_2_utils]
apply_args_typed [in PCF2.pcf_2_utils]
apply_args_cons [in PCF2.pcf_2_utils]
apply_args_app [in PCF2.pcf_2_utils]
app_right [in PCF2.pcf_2_system]
app_left [in PCF2.pcf_2_system]
arith_technical' [in PCF2.preliminaries]
arith_technical [in PCF2.preliminaries]
B
basefun_var_applied_typed [in PCF2.pcf_2_utils]base_fun_applied_typed [in PCF2.pcf_2_utils]
base_context_rev [in PCF2.pcf_2_utils]
base_context_rev' [in PCF2.pcf_2_utils]
base_context_le_base [in PCF2.pcf_2_utils]
base_context_some_base [in PCF2.pcf_2_utils]
base_eval [in PCF2.pcf_2_system]
base_preord_ff_le'' [in PCF2.CE_facts]
base_preord_ff_le' [in PCF2.CE_facts]
base_preord_ff_le [in PCF2.CE_facts]
base_preord_tt_le'' [in PCF2.CE_facts]
base_preord_tt_le' [in PCF2.CE_facts]
base_preord_tt_le [in PCF2.CE_facts]
base_preord_le_bot [in PCF2.CE_facts]
bool_eq_dec [in PCF2.preliminaries]
bval_steps_char [in PCF2.pcf_2_system]
C
CE_open_undecidable [in PCF2.undecidability]CE_undecidable [in PCF2.undecidability]
closed_ren [in PCF2.pcf_2_system]
closed_subst [in PCF2.pcf_2_system]
closed_dec [in PCF2.pcf_2_system]
complement_SBTM_HALT_undec [in PCF2.external.TM.SBTM_undec]
config_enumeration [in PCF2.external.TM.SBTM_HALT_enum]
context_existence [in PCF2.SR_SATIS_forward]
cont_equiv_obs_equiv_agree [in PCF2.CE_facts]
cont_equiv_imp_obs_equiv [in PCF2.CE_facts]
cont_pre_order_imp_cont_equiv [in PCF2.CE_facts]
Core.congr_Fun [in PCF2.Autosubst.pcf_2]
Core.congr_Base [in PCF2.Autosubst.pcf_2]
Core.congr_lam [in PCF2.Autosubst.pcf_2]
Core.congr_app [in PCF2.Autosubst.pcf_2]
Core.congr_trny [in PCF2.Autosubst.pcf_2]
Core.congr_bot [in PCF2.Autosubst.pcf_2]
Core.congr_ff [in PCF2.Autosubst.pcf_2]
Core.congr_tt [in PCF2.Autosubst.pcf_2]
Core.instId'_tm_pointwise [in PCF2.Autosubst.pcf_2]
Core.instId'_tm [in PCF2.Autosubst.pcf_2]
Core.renRen_tm [in PCF2.Autosubst.pcf_2]
Core.renRen'_tm_pointwise [in PCF2.Autosubst.pcf_2]
Core.renSubst_tm_pointwise [in PCF2.Autosubst.pcf_2]
Core.renSubst_tm [in PCF2.Autosubst.pcf_2]
Core.rinstId'_tm_pointwise [in PCF2.Autosubst.pcf_2]
Core.rinstId'_tm [in PCF2.Autosubst.pcf_2]
Core.rinstInst_up_tm_tm [in PCF2.Autosubst.pcf_2]
Core.rinstInst'_tm_pointwise [in PCF2.Autosubst.pcf_2]
Core.rinstInst'_tm [in PCF2.Autosubst.pcf_2]
Core.substRen_tm_pointwise [in PCF2.Autosubst.pcf_2]
Core.substRen_tm [in PCF2.Autosubst.pcf_2]
Core.substSubst_tm_pointwise [in PCF2.Autosubst.pcf_2]
Core.substSubst_tm [in PCF2.Autosubst.pcf_2]
Core.upExtRen_tm_tm [in PCF2.Autosubst.pcf_2]
Core.upExt_tm_tm [in PCF2.Autosubst.pcf_2]
Core.upId_tm_tm [in PCF2.Autosubst.pcf_2]
Core.upRen_tm_tm [in PCF2.Autosubst.pcf_2]
Core.up_subst_subst_tm_tm [in PCF2.Autosubst.pcf_2]
Core.up_subst_ren_tm_tm [in PCF2.Autosubst.pcf_2]
Core.up_ren_subst_tm_tm [in PCF2.Autosubst.pcf_2]
Core.up_ren_ren_tm_tm [in PCF2.Autosubst.pcf_2]
Core.up_tm_tm [in PCF2.Autosubst.pcf_2]
Core.varLRen'_tm_pointwise [in PCF2.Autosubst.pcf_2]
Core.varLRen'_tm [in PCF2.Autosubst.pcf_2]
Core.varL'_tm_pointwise [in PCF2.Autosubst.pcf_2]
Core.varL'_tm [in PCF2.Autosubst.pcf_2]
co_SR_reduces_CE [in PCF2.undecidability]
ctxt_comp_fill [in PCF2.pcf_2_contexts]
ctxt_comp_typed [in PCF2.pcf_2_contexts]
cumul_spec [in PCF2.external.Synthetic.ListEnumerabilityFacts]
cumul_spec__T [in PCF2.external.Synthetic.ListEnumerabilityFacts]
cumul_In [in PCF2.external.Synthetic.ListEnumerabilityFacts]
cum_ge' [in PCF2.external.Synthetic.ListEnumerabilityFacts]
cum_ge [in PCF2.external.Synthetic.ListEnumerabilityFacts]
D
decidable_iff' [in PCF2.external.Synthetic.DecidabilityFacts]decidable_iff [in PCF2.external.Synthetic.DecidabilityFacts]
decidable_complement_semi_decidable [in PCF2.external.Synthetic.SemiDecidabilityFacts]
decidable_semi_decidable [in PCF2.external.Synthetic.SemiDecidabilityFacts]
dec_red [in PCF2.external.Synthetic.ReducibilityFacts]
Dec_auto [in PCF2.external.Shared.Dec]
dec_count_enum' [in PCF2.external.Synthetic.EnumerabilityFacts]
dec_count_enum [in PCF2.external.Synthetic.EnumerabilityFacts]
dec_disj [in PCF2.external.Synthetic.DecidabilityFacts]
dec_conj [in PCF2.external.Synthetic.DecidabilityFacts]
dec_compl' [in PCF2.external.Synthetic.DecidabilityFacts]
dec_compl [in PCF2.external.Synthetic.DecidabilityFacts]
dec_decidable' [in PCF2.external.Synthetic.DecidabilityFacts]
derived_satis_ineq [in PCF2.SR_SATIS_forward]
diff1 [in PCF2.preliminaries]
diff2 [in PCF2.preliminaries]
direction_enumeration [in PCF2.external.TM.SBTM_HALT_enum]
discrete_list [in PCF2.external.Synthetic.DecidabilityFacts]
discrete_option [in PCF2.external.Synthetic.DecidabilityFacts]
discrete_sum [in PCF2.external.Synthetic.DecidabilityFacts]
discrete_prod [in PCF2.external.Synthetic.DecidabilityFacts]
discrete_nat [in PCF2.external.Synthetic.DecidabilityFacts]
discrete_bool [in PCF2.external.Synthetic.DecidabilityFacts]
discrete_iff [in PCF2.external.Synthetic.DecidabilityFacts]
E
enc_typed [in PCF2.SATIS_facts]enumerable_enumerable_T [in PCF2.external.Synthetic.EnumerabilityFacts]
enumerable_semi_decidable [in PCF2.external.Synthetic.EnumerabilityFacts]
enumerable_enum [in PCF2.external.Synthetic.ListEnumerabilityFacts]
enumerable_list [in PCF2.external.Synthetic.ListEnumerabilityFacts]
enumerable__T_list_enumerable [in PCF2.external.Synthetic.ListEnumerabilityFacts]
enumerable_list_enumerable [in PCF2.external.Synthetic.ListEnumerabilityFacts]
enumerator_enumerable [in PCF2.external.Synthetic.EnumerabilityFacts]
enumerator__T_Vector [in PCF2.external.Synthetic.EnumerabilityFacts]
enumerator__T_Fin [in PCF2.external.Synthetic.EnumerabilityFacts]
enumerator__T_finType [in PCF2.external.Synthetic.EnumerabilityFacts]
enumerator__T_sigT2 [in PCF2.external.Synthetic.EnumerabilityFacts]
enumerator__T_sigT [in PCF2.external.Synthetic.EnumerabilityFacts]
enumerator__T_option [in PCF2.external.Synthetic.EnumerabilityFacts]
enumerator__T_sum [in PCF2.external.Synthetic.EnumerabilityFacts]
enumerator__T_prod [in PCF2.external.Synthetic.EnumerabilityFacts]
enumerator__T_bool [in PCF2.external.Synthetic.EnumerabilityFacts]
enumerator__T_unit [in PCF2.external.Synthetic.EnumerabilityFacts]
enumerator__T_nat [in PCF2.external.Synthetic.EnumerabilityFacts]
enumerator__T_list [in PCF2.external.Synthetic.ListEnumerabilityFacts]
enumerator_to_list_enumerator [in PCF2.external.Synthetic.ListEnumerabilityFacts]
enum_enumT [in PCF2.external.Synthetic.ListEnumerabilityFacts]
equiv_empty_imp_equiv_nonempty [in PCF2.CE_facts]
evaluates_to_same [in PCF2.pcf_2_system]
evaluates_to_final [in PCF2.CE_facts]
eval_step [in PCF2.pcf_2_system]
F
Fext.instId_tm [in PCF2.Autosubst.pcf_2]Fext.renRen'_tm [in PCF2.Autosubst.pcf_2]
Fext.renSubst'_tm [in PCF2.Autosubst.pcf_2]
Fext.rinstId_tm [in PCF2.Autosubst.pcf_2]
Fext.rinstInst_tm [in PCF2.Autosubst.pcf_2]
Fext.substRen'_tm [in PCF2.Autosubst.pcf_2]
Fext.substSubst'_tm [in PCF2.Autosubst.pcf_2]
Fext.varLRen_tm [in PCF2.Autosubst.pcf_2]
Fext.varL_tm [in PCF2.Autosubst.pcf_2]
fill_step [in PCF2.pcf_2_contexts]
fill_type [in PCF2.pcf_2_contexts]
funcomp_charact [in PCF2.pcf_2_system]
funcomp_assoc [in PCF2.Autosubst.core]
fun_rev_to_context [in PCF2.pcf_2_utils]
fun_rule_enc_rev [in PCF2.SATIS_PS]
fun_rule_encoding_many_exist [in PCF2.SATIS_PS]
fun_rule_enc_exist [in PCF2.SATIS_PS]
fv_subst [in PCF2.pcf_2_system]
G
G_charact' [in PCF2.co_RPS_CE]G_solves [in PCF2.co_RPS_CE]
G_subst [in PCF2.co_RPS_CE]
G_steps [in PCF2.co_RPS_CE]
G_typed [in PCF2.co_RPS_CE]
I
if_trm2 [in PCF2.pcf_2_system]if_trm1 [in PCF2.pcf_2_system]
if_cond [in PCF2.pcf_2_system]
ineq_subst [in PCF2.CE_facts]
ineq_ren [in PCF2.CE_facts]
In_cumul [in PCF2.external.Synthetic.ListEnumerabilityFacts]
iq_sys_wf_cons_char [in PCF2.PS_facts]
iq_sys_val_cons_char [in PCF2.PS_facts]
iter_succ_l [in PCF2.preliminaries]
iter_succ_r [in PCF2.preliminaries]
iter_ren_closed [in PCF2.pcf_2_system]
L
lam_list_to_type' [in PCF2.pcf_2_utils]lam_list_to_type [in PCF2.pcf_2_utils]
lam_T_split [in PCF2.pcf_2_utils]
lam_T_shift_subst [in PCF2.pcf_2_utils]
lam_args_subst [in PCF2.SATIS_PS]
lam_subst_typed [in PCF2.CE_facts]
lam_subst_step [in PCF2.CE_facts]
lam_subst_concat [in PCF2.CE_facts]
leb_le_false [in PCF2.preliminaries]
leb_le_true [in PCF2.preliminaries]
length_base_context [in PCF2.pcf_2_utils]
length_var_seq [in PCF2.pcf_2_utils]
list_eq [in PCF2.preliminaries]
list_eq_dec [in PCF2.preliminaries]
list_to_fun_app' [in PCF2.pcf_2_utils]
list_val_exist [in PCF2.SATIS_PS]
list_enumerator_to_cumul [in PCF2.external.Synthetic.ListEnumerabilityFacts]
list_enumerable__T_enumerable [in PCF2.external.Synthetic.ListEnumerabilityFacts]
list_enumerable_enumerable [in PCF2.external.Synthetic.ListEnumerabilityFacts]
list_enumerator_enumerator [in PCF2.external.Synthetic.ListEnumerabilityFacts]
list_enumerator_to_enumerator [in PCF2.external.Synthetic.ListEnumerabilityFacts]
ltb_lt_false [in PCF2.preliminaries]
ltb_lt_true [in PCF2.preliminaries]
L_list_cumulative [in PCF2.external.Synthetic.ListEnumerabilityFacts]
M
make_rule_types_length [in PCF2.SATIS_facts]N
nat_ord_dec [in PCF2.preliminaries]O
obs_preorder_empty_imp_obs_preorder_closed [in PCF2.CE_facts]obs_equiv_trans [in PCF2.CE_facts]
obs_equiv_refl [in PCF2.CE_facts]
obs_equiv_rewrite_right [in PCF2.CE_facts]
obs_equiv_rewrite_left [in PCF2.CE_facts]
obs_equiv_imp_cont_equiv [in PCF2.CE_facts]
obs_equiv_imp_cont_pre_order [in PCF2.CE_facts]
obs_equiv_base_eval_same [in PCF2.CE_facts]
obs_equiv_context [in PCF2.CE_facts]
obs_preorder_context [in PCF2.CE_facts]
obs_preorder_base_refl [in PCF2.CE_facts]
obs_preorder_base_bot [in PCF2.CE_facts]
obs_preorder_incl_steps' [in PCF2.CE_facts]
obs_preorder_incl_step' [in PCF2.CE_facts]
obs_preorder_closed_incl_step' [in PCF2.CE_facts]
obs_preorder_incl_steps [in PCF2.CE_facts]
obs_preorder_incl_step [in PCF2.CE_facts]
obs_preorder_closed_incl_step [in PCF2.CE_facts]
obs_preorder_fun_char [in PCF2.CE_facts]
obs_preorder_closed_fun_char [in PCF2.CE_facts]
obs_preorder_trans [in PCF2.CE_facts]
obs_preorder_closed_trans [in PCF2.CE_facts]
obs_preorder_refl [in PCF2.CE_facts]
obs_preorder_closed_refl [in PCF2.CE_facts]
obs_preorder_closed_steps [in PCF2.CE_facts]
P
pair_eq_dec [in PCF2.preliminaries]pointwise_forall [in PCF2.Autosubst.core]
pre_order_imp_obs_preorder [in PCF2.CE_facts]
pre_order_imp_obs_preorder_closed [in PCF2.CE_facts]
ps_system_type_list_to_fun_rev [in PCF2.SATIS_PS]
ps_system_char_SATIS [in PCF2.SATIS_PS]
ps_system_char_enc_exist [in PCF2.SATIS_PS]
ps_system_char_bool_exist [in PCF2.SATIS_PS]
R
reduces_SR_SATIS_forward [in PCF2.SR_SATIS_forward]reduces_complement [in PCF2.external.Synthetic.ReducibilityFacts]
reduces_dependent [in PCF2.external.Synthetic.ReducibilityFacts]
reduces_transitive [in PCF2.external.Synthetic.ReducibilityFacts]
reduces_reflexive [in PCF2.external.Synthetic.ReducibilityFacts]
reduces_co_SATIS_co_PS [in PCF2.SATIS_PS]
reduces_SATIS_PS [in PCF2.SATIS_PS]
reduces_co_RPS_CE_closed [in PCF2.co_RPS_CE]
reduces_co_PS_co_RPS [in PCF2.PS_RPS]
reduces_PS_RPS [in PCF2.PS_RPS]
reduces_CE_CE_open [in PCF2.undecidability]
reduces_co_SR_co_SATIS [in PCF2.undecidability]
reduces_SR_SATIS [in PCF2.undecidability]
red_comp [in PCF2.external.Synthetic.ReducibilityFacts]
reflects_prv [in PCF2.external.Synthetic.DecidabilityFacts]
reflects_disj [in PCF2.external.Synthetic.DecidabilityFacts]
reflects_conj [in PCF2.external.Synthetic.DecidabilityFacts]
reflects_not [in PCF2.external.Synthetic.DecidabilityFacts]
ren_apply_args [in PCF2.pcf_2_utils]
ren_var [in PCF2.SR_SATIS_forward]
ren_shift_shifted_t_subst_char [in PCF2.SR_SATIS_forward]
ren_shift_typed [in PCF2.SR_SATIS_forward]
ren_shift_well_typed' [in PCF2.SR_SATIS_forward]
ren_shift_well_typed [in PCF2.SR_SATIS_forward]
ren_subst [in PCF2.pcf_2_system]
ren_preserves [in PCF2.pcf_2_system]
ren_preserves' [in PCF2.pcf_2_system]
restrict_sys [in PCF2.PS_RPS]
res_ineq_sys_val_cons_char [in PCF2.RPS_facts]
rev_nth_error2 [in PCF2.preliminaries]
rev_nth_error1 [in PCF2.preliminaries]
riq_sys_wf_cons_char [in PCF2.RPS_facts]
RoseTree.cancel_to_of [in PCF2.external.Synthetic.EnumerabilityFacts]
RoseTree.cancel_of_to [in PCF2.external.Synthetic.EnumerabilityFacts]
RoseTree.to_enumerable_T [in PCF2.external.Synthetic.EnumerabilityFacts]
RoseTree.to_enumerator__T [in PCF2.external.Synthetic.EnumerabilityFacts]
rules_eq_decidable [in PCF2.preliminaries]
rule_enc_word_enc_closed' [in PCF2.SATIS_facts]
rule_enc_word_enc_closed [in PCF2.SATIS_facts]
rule_enc_equiv [in PCF2.SATIS_facts]
rule_some [in PCF2.SATIS_facts]
S
satisfies_rule_enc_ind [in PCF2.SATIS_PS]SBTM_HALT_undec [in PCF2.external.TM.SBTM_undec]
SBTM_HALT_enumerator_spec [in PCF2.external.TM.SBTM_HALT_enum]
SBTM_HALT_enumeration [in PCF2.external.TM.SBTM_HALT_enum]
SBTM_HALT_INSTANCE_enumeration [in PCF2.external.TM.SBTM_HALT_enum]
SBTM_enumeration [in PCF2.external.TM.SBTM_HALT_enum]
SBTM_HALT_semi_decision [in PCF2.external.TM.SBTM_HALT_enum]
scons_comp [in PCF2.Autosubst.unscoped_axioms]
scons_eta [in PCF2.Autosubst.unscoped_axioms]
scons_eta_id [in PCF2.Autosubst.unscoped_axioms]
scons_comp' [in PCF2.Autosubst.unscoped]
scons_eta_id' [in PCF2.Autosubst.unscoped]
scons_eta' [in PCF2.Autosubst.unscoped]
semi_decidable_enumerable [in PCF2.external.Synthetic.EnumerabilityFacts]
semi_decider_enumerator [in PCF2.external.Synthetic.EnumerabilityFacts]
shifted_subst_char [in PCF2.pcf_2_system]
shift_t_subst_well_typed [in PCF2.SR_SATIS_forward]
steps_n1 [in PCF2.pcf_2_system]
steps_1n [in PCF2.pcf_2_system]
steps_preserve_obs_preorder_backward [in PCF2.CE_facts]
steps_preserve_obs_preorder [in PCF2.CE_facts]
steps_equiv [in PCF2.CE_facts]
step_eval [in PCF2.pcf_2_system]
strong_obs_preorder_imp_obs_preorder [in PCF2.CE_facts]
strong_obs_preorder_refl [in PCF2.CE_facts]
strong_obs_preorder_steps [in PCF2.CE_facts]
subst_apply_args [in PCF2.pcf_2_utils]
subst_map_closed_list [in PCF2.pcf_2_system]
subst_well_typed_singleton [in PCF2.pcf_2_system]
subst_well_typed_nil_nil [in PCF2.pcf_2_system]
subst_closes [in PCF2.pcf_2_system]
subst_preserves_step [in PCF2.pcf_2_system]
subst_shift [in PCF2.pcf_2_system]
subst_concat [in PCF2.pcf_2_system]
subst_charact [in PCF2.pcf_2_system]
subst_charact_typed [in PCF2.pcf_2_system]
subst_preserves [in PCF2.pcf_2_system]
subst_bool_var [in PCF2.SATIS_PS]
subst_nil_ids [in PCF2.SATIS_PS]
subst_list_shift [in PCF2.SATIS_PS]
subst_list_subst [in PCF2.SATIS_PS]
subst_list_subst' [in PCF2.SATIS_PS]
subst_list_last [in PCF2.SATIS_PS]
subst_equiv [in PCF2.CE_facts]
subst_rel_nil [in PCF2.CE_facts]
T
to_cumul_spec [in PCF2.external.Synthetic.ListEnumerabilityFacts]to_cumul_cumulative [in PCF2.external.Synthetic.ListEnumerabilityFacts]
typed_empty_closed [in PCF2.pcf_2_system]
typed_free_var [in PCF2.pcf_2_system]
type_preservation [in PCF2.pcf_2_system]
type_preservation_step [in PCF2.pcf_2_system]
type_weakening [in PCF2.pcf_2_system]
t_subst_rule [in PCF2.SR_SATIS_forward]
t_subst_map_var_id'' [in PCF2.SR_SATIS_forward]
t_subst_initial [in PCF2.SATIS_facts]
t_subst_map_var_rules' [in PCF2.SATIS_facts]
t_subst_map_var_rules [in PCF2.SATIS_facts]
t_subst_map_var_id' [in PCF2.SATIS_facts]
t_subst_map_var_id [in PCF2.SATIS_facts]
t_subst_well_typed [in PCF2.SATIS_facts]
T_list_to_fun [in PCF2.SATIS_facts]
t_subst_char [in PCF2.SATIS_PS]
U
undecidability_to_complement [in PCF2.external.Synthetic.Undecidability]undecidability_from_complement [in PCF2.external.Synthetic.Undecidability]
undecidability_from_reducibility [in PCF2.external.Synthetic.Undecidability]
up_tm_tm_iter2 [in PCF2.pcf_2_system]
up_tm_tm_iter1 [in PCF2.pcf_2_system]
up_ren_ren [in PCF2.Autosubst.unscoped]
V
val_list_closed [in PCF2.pcf_2_system]val_no_step [in PCF2.pcf_2_system]
var_seq_map_nth [in PCF2.pcf_2_utils]
var_seq_nth [in PCF2.pcf_2_utils]
var_seq_split [in PCF2.pcf_2_utils]
W
well_formed_forall [in PCF2.PS_RPS]Axiom Index
C
church_rosser [in PCF2.pcf_2_system]R
rule_enc_exist [in PCF2.SATIS]S
SR_undec [in PCF2.undecidability]SR_SATIS_equiv [in PCF2.undecidability]
W
weak_normalisation_comp [in PCF2.pcf_2_system]Inductive Index
C
Core.tm [in PCF2.Autosubst.pcf_2]Core.ty [in PCF2.Autosubst.pcf_2]
Core.Up_tm [in PCF2.Autosubst.pcf_2]
ctxt_typed [in PCF2.pcf_2_contexts]
D
direction [in PCF2.external.TM.SBTM]O
obs_preorder_base [in PCF2.CE]P
pctxt [in PCF2.pcf_2_contexts]R
Ren1 [in PCF2.Autosubst.unscoped]Ren2 [in PCF2.Autosubst.unscoped]
Ren3 [in PCF2.Autosubst.unscoped]
Ren4 [in PCF2.Autosubst.unscoped]
Ren5 [in PCF2.Autosubst.unscoped]
rew [in PCF2.external.SR]
rewt [in PCF2.external.SR]
RoseTree.t [in PCF2.external.Synthetic.EnumerabilityFacts]
S
step [in PCF2.pcf_2_system]Subst1 [in PCF2.Autosubst.unscoped]
Subst2 [in PCF2.Autosubst.unscoped]
Subst3 [in PCF2.Autosubst.unscoped]
Subst4 [in PCF2.Autosubst.unscoped]
Subst5 [in PCF2.Autosubst.unscoped]
T
typed [in PCF2.pcf_2_system]V
Var [in PCF2.Autosubst.unscoped]Projection Index
C
class [in PCF2.external.Shared.FinTypesDef]Core.up_tm [in PCF2.Autosubst.pcf_2]
E
enum [in PCF2.external.Shared.FinTypesDef]enum_ok [in PCF2.external.Shared.FinTypesDef]
eqType_dec [in PCF2.external.Shared.EqDecDef]
eqType_X [in PCF2.external.Shared.EqDecDef]
I
ids [in PCF2.Autosubst.unscoped]N
num_states [in PCF2.external.TM.SBTM]R
ren1 [in PCF2.Autosubst.unscoped]ren2 [in PCF2.Autosubst.unscoped]
ren3 [in PCF2.Autosubst.unscoped]
ren4 [in PCF2.Autosubst.unscoped]
ren5 [in PCF2.Autosubst.unscoped]
S
subst1 [in PCF2.Autosubst.unscoped]subst2 [in PCF2.Autosubst.unscoped]
subst3 [in PCF2.Autosubst.unscoped]
subst4 [in PCF2.Autosubst.unscoped]
subst5 [in PCF2.Autosubst.unscoped]
T
trans [in PCF2.external.TM.SBTM]type [in PCF2.external.Shared.FinTypesDef]
Section Index
E
enumerator_list_enumerator [in PCF2.external.Synthetic.ListEnumerabilityFacts]enumerator_list_enumerator [in PCF2.external.Synthetic.ListEnumerabilityFacts]
L
L_list_def [in PCF2.external.Synthetic.ListEnumerabilityFacts]P
Properties [in PCF2.external.Synthetic.ReducibilityFacts]R
RoseTree.Auxiliary [in PCF2.external.Synthetic.EnumerabilityFacts]U
undecidability [in PCF2.undecidability]Instance Index
A
and_dec [in PCF2.external.Shared.Dec]app_proper [in PCF2.pcf_2_system]
B
bool_eq_dec [in PCF2.external.Shared.Dec]C
cont_equiv_Equiv [in PCF2.CE_facts]Core.ren_tm_morphism2 [in PCF2.Autosubst.pcf_2]
Core.ren_tm_morphism [in PCF2.Autosubst.pcf_2]
Core.Ren_tm [in PCF2.Autosubst.pcf_2]
Core.subst_tm_morphism2 [in PCF2.Autosubst.pcf_2]
Core.subst_tm_morphism [in PCF2.Autosubst.pcf_2]
Core.Subst_tm [in PCF2.Autosubst.pcf_2]
Core.Up_tm_tm [in PCF2.Autosubst.pcf_2]
Core.VarInstance_tm [in PCF2.Autosubst.pcf_2]
E
Empty_set_eq_dec [in PCF2.external.Shared.Dec]enumerator__T_of_list [in PCF2.external.Synthetic.ListEnumerabilityFacts]
enumerator__T_to_list [in PCF2.external.Synthetic.ListEnumerabilityFacts]
evaluates_steps [in PCF2.pcf_2_system]
F
False_eq_dec [in PCF2.external.Shared.Dec]False_dec [in PCF2.external.Shared.Dec]
funcomp_morphism2 [in PCF2.Autosubst.core]
funcomp_morphism [in PCF2.Autosubst.core]
I
idsRen [in PCF2.Autosubst.unscoped]iff_dec [in PCF2.external.Shared.Dec]
if_proper [in PCF2.pcf_2_system]
impl_dec [in PCF2.external.Shared.Dec]
inf_to_enumerator [in PCF2.external.Synthetic.ListEnumerabilityFacts]
L
lam_proper [in PCF2.pcf_2_system]list_eq_dec [in PCF2.external.Shared.Dec]
list_in_dec [in PCF2.external.Synthetic.ListEnumerabilityFacts]
N
nat_eq_dec [in PCF2.external.Shared.Dec]not_dec [in PCF2.external.Shared.Dec]
O
obs_equiv_Equiv [in PCF2.CE_facts]obs_preorder_PreOrder [in PCF2.CE_facts]
obs_equiv_obs_preorder [in PCF2.CE_facts]
option_eq_dec [in PCF2.external.Shared.Dec]
or_dec [in PCF2.external.Shared.Dec]
P
prod_eq_dec [in PCF2.external.Shared.Dec]Proper_decidable [in PCF2.external.Synthetic.DecidabilityFacts]
Proper_decides [in PCF2.external.Synthetic.DecidabilityFacts]
R
rewrite_in_evaluates [in PCF2.CE_facts]rewrite_in_obs_preorder_base [in PCF2.CE_facts]
S
scons_morphism2 [in PCF2.Autosubst.unscoped]scons_morphism [in PCF2.Autosubst.unscoped]
steps_PreOrder [in PCF2.pcf_2_system]
step_steps [in PCF2.pcf_2_system]
sum_eq_dec [in PCF2.external.Shared.Dec]
T
True_eq_dec [in PCF2.external.Shared.Dec]True_dec [in PCF2.external.Shared.Dec]
U
unit_eq_dec [in PCF2.external.Shared.Dec]Abbreviation Index
C
cumul [in PCF2.external.Synthetic.ListEnumerabilityFacts]E
enumerator__T [in PCF2.external.Synthetic.EnumerabilityFacts]L
list_enumerator__T [in PCF2.external.Synthetic.ListEnumerabilityFacts]P
ps_system [in PCF2.PS]R
rps_system [in PCF2.RPS]S
SBTMNotations.config [in PCF2.external.TM.SBTM]SBTMNotations.state [in PCF2.external.TM.SBTM]
SBTMNotations.tape [in PCF2.external.TM.SBTM]
SRS [in PCF2.external.SR]
str [in PCF2.external.SR]
string [in PCF2.external.SR]
Definition Index
A
Allfv.allfvImpl_tm [in PCF2.Autosubst.pcf_2]Allfv.allfvRenL_tm [in PCF2.Autosubst.pcf_2]
Allfv.allfvRenR_tm [in PCF2.Autosubst.pcf_2]
Allfv.allfvTriv_tm [in PCF2.Autosubst.pcf_2]
Allfv.allfv_tm [in PCF2.Autosubst.pcf_2]
all_fins [in PCF2.external.Synthetic.EnumerabilityFacts]
ap [in PCF2.Autosubst.core]
ap [in PCF2.Autosubst.unscoped]
apc [in PCF2.Autosubst.core]
apc [in PCF2.Autosubst.unscoped]
apply_args [in PCF2.pcf_2_utils]
B
base_context [in PCF2.pcf_2_utils]base_fun [in PCF2.pcf_2_utils]
bool_enum [in PCF2.external.Synthetic.EnumerabilityFacts]
C
CE [in PCF2.CE]CE_open [in PCF2.CE]
closed [in PCF2.pcf_2_system]
cod [in PCF2.Autosubst.core_axioms]
cod_comp [in PCF2.Autosubst.core_axioms]
cod_ext [in PCF2.Autosubst.core_axioms]
cod_id [in PCF2.Autosubst.core_axioms]
cod_map [in PCF2.Autosubst.core_axioms]
comp [in PCF2.pcf_2_contexts]
complement [in PCF2.external.Synthetic.Definitions]
context [in PCF2.pcf_2_system]
cont_equiv [in PCF2.CE]
cont_equiv_rest [in PCF2.CE_facts]
cont_preorder [in PCF2.CE_facts]
Core.compRenRen_tm [in PCF2.Autosubst.pcf_2]
Core.compRenSubst_tm [in PCF2.Autosubst.pcf_2]
Core.compSubstRen_tm [in PCF2.Autosubst.pcf_2]
Core.compSubstSubst_tm [in PCF2.Autosubst.pcf_2]
Core.extRen_tm [in PCF2.Autosubst.pcf_2]
Core.ext_tm [in PCF2.Autosubst.pcf_2]
Core.idSubst_tm [in PCF2.Autosubst.pcf_2]
Core.ren_tm [in PCF2.Autosubst.pcf_2]
Core.rinst_inst_tm [in PCF2.Autosubst.pcf_2]
Core.subst_tm [in PCF2.Autosubst.pcf_2]
Core.tm_sind [in PCF2.Autosubst.pcf_2]
Core.tm_rec [in PCF2.Autosubst.pcf_2]
Core.tm_ind [in PCF2.Autosubst.pcf_2]
Core.tm_rect [in PCF2.Autosubst.pcf_2]
Core.ty_sind [in PCF2.Autosubst.pcf_2]
Core.ty_rec [in PCF2.Autosubst.pcf_2]
Core.ty_ind [in PCF2.Autosubst.pcf_2]
Core.ty_rect [in PCF2.Autosubst.pcf_2]
count [in PCF2.external.Shared.FinTypesDef]
ctxt_typed_sind [in PCF2.pcf_2_contexts]
ctxt_typed_ind [in PCF2.pcf_2_contexts]
cumulative [in PCF2.external.Synthetic.ListEnumerabilityFacts]
D
Dec [in PCF2.external.Shared.Dec]dec [in PCF2.external.Shared.Dec]
Dec [in PCF2.external.Shared.EqDecDef]
dec [in PCF2.external.Shared.EqDecDef]
decidable [in PCF2.external.Synthetic.Definitions]
decider [in PCF2.external.Synthetic.Definitions]
dec2bool [in PCF2.external.Shared.EqDecDef]
diff [in PCF2.preliminaries]
direction_sind [in PCF2.external.TM.SBTM]
direction_rec [in PCF2.external.TM.SBTM]
direction_ind [in PCF2.external.TM.SBTM]
direction_rect [in PCF2.external.TM.SBTM]
discrete [in PCF2.external.Synthetic.DecidabilityFacts]
E
el_T [in PCF2.external.Synthetic.ListEnumerabilityFacts]embed [in PCF2.pcf_2_system]
enumerable [in PCF2.external.Synthetic.Definitions]
enumerable__T [in PCF2.external.Synthetic.EnumerabilityFacts]
enumerator [in PCF2.external.Synthetic.Definitions]
enumerator__T' [in PCF2.external.Synthetic.EnumerabilityFacts]
eqType_CS [in PCF2.external.Shared.EqDecDef]
eq_dec [in PCF2.preliminaries]
evaluates_to_base [in PCF2.pcf_2_system]
F
fill [in PCF2.pcf_2_contexts]finType_CS [in PCF2.external.Shared.FinTypesDef]
finType_enum [in PCF2.external.Synthetic.EnumerabilityFacts]
Fin_enum [in PCF2.external.Synthetic.EnumerabilityFacts]
funcomp [in PCF2.Autosubst.core]
fun_rule_encoding_many [in PCF2.SATIS_PS]
fun_rule_encoding [in PCF2.SATIS]
G
G [in PCF2.co_RPS_CE]I
id [in PCF2.Autosubst.unscoped]inf_list_enumerable__T [in PCF2.external.Synthetic.ListEnumerabilityFacts]
is_bval [in PCF2.pcf_2_system]
L
lam_T [in PCF2.pcf_2_utils]lam_subst [in PCF2.CE_facts]
list_to_fun [in PCF2.pcf_2_utils]
list_comp [in PCF2.Autosubst.core]
list_id [in PCF2.Autosubst.core]
list_ext [in PCF2.Autosubst.core]
list_enumerable__T [in PCF2.external.Synthetic.ListEnumerabilityFacts]
list_enumerator__T' [in PCF2.external.Synthetic.ListEnumerabilityFacts]
list_enumerable [in PCF2.external.Synthetic.ListEnumerabilityFacts]
list_enumerator [in PCF2.external.Synthetic.ListEnumerabilityFacts]
L_T [in PCF2.external.Synthetic.ListEnumerabilityFacts]
L_list [in PCF2.external.Synthetic.ListEnumerabilityFacts]
M
make_rule_types [in PCF2.SATIS]mv [in PCF2.external.TM.SBTM]
N
nat_enum [in PCF2.external.Synthetic.EnumerabilityFacts]O
obind [in PCF2.external.TM.SBTM]obs_equiv [in PCF2.CE]
obs_preorder [in PCF2.CE]
obs_preorder_closed [in PCF2.CE]
obs_preorder_base_sind [in PCF2.CE]
obs_preorder_base_ind [in PCF2.CE]
obs_equiv_rest [in PCF2.CE_facts]
obs_preorder_rest [in PCF2.CE_facts]
option_enum [in PCF2.external.Synthetic.EnumerabilityFacts]
option_comp [in PCF2.Autosubst.core]
option_ext [in PCF2.Autosubst.core]
option_id [in PCF2.Autosubst.core]
option_map [in PCF2.Autosubst.core]
P
pctxt_sind [in PCF2.pcf_2_contexts]pctxt_rec [in PCF2.pcf_2_contexts]
pctxt_ind [in PCF2.pcf_2_contexts]
pctxt_rect [in PCF2.pcf_2_contexts]
prod_enum [in PCF2.external.Synthetic.EnumerabilityFacts]
prod_comp [in PCF2.Autosubst.core]
prod_ext [in PCF2.Autosubst.core]
prod_id [in PCF2.Autosubst.core]
prod_map [in PCF2.Autosubst.core]
PS [in PCF2.PS]
ps_system_char_enc [in PCF2.SATIS_PS]
ps_system_type [in PCF2.SATIS_PS]
ps_system_char_bool [in PCF2.SATIS_PS]
ps_system_well_formed [in PCF2.PS]
ps_system_solvable [in PCF2.PS]
R
reduces [in PCF2.external.Synthetic.Definitions]reduction [in PCF2.external.Synthetic.Definitions]
reflects [in PCF2.external.Synthetic.Definitions]
ren_shift [in PCF2.SR_SATIS_forward]
ren_well_typed [in PCF2.pcf_2_system]
rest_PCF [in PCF2.CE_facts]
rewt_sind [in PCF2.external.SR]
rewt_ind [in PCF2.external.SR]
rew_sind [in PCF2.external.SR]
rew_ind [in PCF2.external.SR]
RoseTree.of_nat [in PCF2.external.Synthetic.EnumerabilityFacts]
RoseTree.to_nat [in PCF2.external.Synthetic.EnumerabilityFacts]
RoseTree.t_sind [in PCF2.external.Synthetic.EnumerabilityFacts]
RoseTree.t_rec [in PCF2.external.Synthetic.EnumerabilityFacts]
RoseTree.t_ind [in PCF2.external.Synthetic.EnumerabilityFacts]
RoseTree.t_rect [in PCF2.external.Synthetic.EnumerabilityFacts]
RPS [in PCF2.RPS]
rps_system_well_formed [in PCF2.RPS]
rps_system_solvable [in PCF2.RPS]
rule_fun [in PCF2.SATIS]
rule_encoding [in PCF2.SATIS]
rule_ineq [in PCF2.SATIS]
rule_type [in PCF2.SATIS]
S
SATIS [in PCF2.SATIS]satisfies [in PCF2.SATIS]
SBTM_HALT [in PCF2.external.TM.SBTM]
SBTM_HALT_enumerator [in PCF2.external.TM.SBTM_HALT_enum]
SBTM_of_sigT [in PCF2.external.TM.SBTM_HALT_enum]
SBTM_to_sigT [in PCF2.external.TM.SBTM_HALT_enum]
scons [in PCF2.Autosubst.unscoped]
semi_decidable [in PCF2.external.Synthetic.Definitions]
semi_decider [in PCF2.external.Synthetic.Definitions]
shift [in PCF2.Autosubst.unscoped]
shifted_subst [in PCF2.pcf_2_system]
sigT_enum [in PCF2.external.Synthetic.EnumerabilityFacts]
sigT2_enum [in PCF2.external.Synthetic.EnumerabilityFacts]
solves_rps_system [in PCF2.RPS]
solves_ps_system [in PCF2.PS]
SR [in PCF2.external.SR]
step [in PCF2.external.TM.SBTM]
steps [in PCF2.pcf_2_system]
steps [in PCF2.external.TM.SBTM]
step_sind [in PCF2.pcf_2_system]
step_ind [in PCF2.pcf_2_system]
strong_obs_preorder [in PCF2.CE_facts]
subst_well_typed [in PCF2.pcf_2_system]
subst_list [in PCF2.SATIS_PS]
subst_rel [in PCF2.CE_facts]
sum_enum [in PCF2.external.Synthetic.EnumerabilityFacts]
swap [in PCF2.external.SR]
T
T [in PCF2.SATIS]to_cumul [in PCF2.external.Synthetic.ListEnumerabilityFacts]
trans' [in PCF2.external.TM.SBTM]
TSR [in PCF2.external.SR]
typed_sind [in PCF2.pcf_2_system]
typed_ind [in PCF2.pcf_2_system]
t_subst [in PCF2.SATIS]
U
undecidable [in PCF2.external.Synthetic.Undecidability]unit_enum [in PCF2.external.Synthetic.EnumerabilityFacts]
up_allfv [in PCF2.Autosubst.unscoped]
up_ren [in PCF2.Autosubst.unscoped]
V
val_rule_enc [in PCF2.SATIS]val_word_enc [in PCF2.SATIS]
var_seq [in PCF2.pcf_2_utils]
var_zero [in PCF2.Autosubst.unscoped]
Vector_enum [in PCF2.external.Synthetic.EnumerabilityFacts]
W
wf_rps_system [in PCF2.RPS]wf_ps_system [in PCF2.PS]
word_encoding [in PCF2.SATIS]
Record Index
C
Core.Up_tm [in PCF2.Autosubst.pcf_2]E
eqType [in PCF2.external.Shared.EqDecDef]F
finType [in PCF2.external.Shared.FinTypesDef]finTypeC [in PCF2.external.Shared.FinTypesDef]
R
Ren1 [in PCF2.Autosubst.unscoped]Ren2 [in PCF2.Autosubst.unscoped]
Ren3 [in PCF2.Autosubst.unscoped]
Ren4 [in PCF2.Autosubst.unscoped]
Ren5 [in PCF2.Autosubst.unscoped]
S
SBTM [in PCF2.external.TM.SBTM]Subst1 [in PCF2.Autosubst.unscoped]
Subst2 [in PCF2.Autosubst.unscoped]
Subst3 [in PCF2.Autosubst.unscoped]
Subst4 [in PCF2.Autosubst.unscoped]
Subst5 [in PCF2.Autosubst.unscoped]
V
Var [in PCF2.Autosubst.unscoped]| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (837 entries) |
| Notation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (40 entries) |
| Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (14 entries) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (17 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (36 entries) |
| Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (61 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (345 entries) |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (5 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (23 entries) |
| Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (20 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (6 entries) |
| Instance Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (48 entries) |
| Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (11 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (195 entries) |
| Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (16 entries) |