| 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 | (569 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 | (36 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 | (10 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 | (19 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 | (239 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 | (58 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 | (6 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 | (21 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 | (12 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 | (23 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 | (3 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 | (130 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 | (12 entries) |
Global Index
A
Allfv [module, in PCF2.pcf_2]allfv_tm_dec [lemma, in PCF2.pcf_2_system]
Allfv.allfvImpl_tm [definition, in PCF2.pcf_2]
Allfv.allfvRenL_tm [definition, in PCF2.pcf_2]
Allfv.allfvRenR_tm [definition, in PCF2.pcf_2]
Allfv.allfvTriv_tm [definition, in PCF2.pcf_2]
Allfv.allfv_tm [definition, in PCF2.pcf_2]
Allfv.upAllfvImpl_tm_tm [lemma, in PCF2.pcf_2]
Allfv.upAllfvRenL_tm_tm [lemma, in PCF2.pcf_2]
Allfv.upAllfvRenR_tm_tm [lemma, in PCF2.pcf_2]
Allfv.upAllfvTriv_tm_tm [lemma, in PCF2.pcf_2]
Allfv.upAllfv_tm_tm [lemma, in PCF2.pcf_2]
ap [definition, in PCF2.unscoped]
ap [definition, in PCF2.core]
apc [definition, in PCF2.unscoped]
apc [definition, in PCF2.core]
AppL [constructor, in PCF2.pcf_2_system]
apply_args_steps_list' [lemma, in PCF2.SATIS]
apply_args_steps_list [lemma, in PCF2.SATIS]
apply_args_steps_body [lemma, in PCF2.SATIS]
apply_args_typed [lemma, in PCF2.SATIS]
apply_args_cons [lemma, in PCF2.SATIS]
apply_args_app [lemma, in PCF2.SATIS]
apply_args [definition, in PCF2.SATIS]
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.SATIS]
B
basefun_var_applied_typed [lemma, in PCF2.SATIS]base_context_le_base [lemma, in PCF2.SR_SATIS_forward]
base_fun_applied_typed [lemma, in PCF2.SATIS]
base_context_rev [lemma, in PCF2.SATIS]
base_context_rev' [lemma, in PCF2.SATIS]
base_context_some_base [lemma, in PCF2.SATIS]
base_context [definition, in PCF2.SATIS]
base_fun [definition, in PCF2.SATIS]
base_preord_ff_le [lemma, in PCF2.contextual_equivalence]
base_preord_tt_le [lemma, in PCF2.contextual_equivalence]
base_preord_le_bot [lemma, in PCF2.contextual_equivalence]
Beta [constructor, in PCF2.pcf_2_system]
bool_eq_dec [lemma, in PCF2.preliminaries]
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_closed [definition, in PCF2.CE]
CE_undecidable [lemma, in PCF2.undecidability]
CE_closed_undecidable [lemma, in PCF2.undecidability]
church_rosser [axiom, in PCF2.pcf_2_system]
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.core_axioms]
cod_comp [definition, in PCF2.core_axioms]
cod_ext [definition, in PCF2.core_axioms]
cod_id [definition, in PCF2.core_axioms]
cod_map [definition, in PCF2.core_axioms]
CombineNotations [module, in PCF2.unscoped]
_ >> _ (fscope) [notation, in PCF2.unscoped]
_ .: _ (subst_scope) [notation, in PCF2.unscoped]
concat [definition, in PCF2.pcf_2_contexts]
context [definition, in PCF2.pcf_2_system]
contextual_equivalence [library]
cont_pre_order_imp_cont_equiv [lemma, in PCF2.contextual_equivalence]
cont_equiv [definition, in PCF2.contextual_equivalence]
Core [module, in PCF2.pcf_2]
core [library]
core_axioms [library]
Core.app [constructor, in PCF2.pcf_2]
Core.Base [constructor, in PCF2.pcf_2]
Core.bot [constructor, in PCF2.pcf_2]
Core.compRenRen_tm [definition, in PCF2.pcf_2]
Core.compRenSubst_tm [definition, in PCF2.pcf_2]
Core.compSubstRen_tm [definition, in PCF2.pcf_2]
Core.compSubstSubst_tm [definition, in PCF2.pcf_2]
Core.congr_Fun [lemma, in PCF2.pcf_2]
Core.congr_Base [lemma, in PCF2.pcf_2]
Core.congr_lam [lemma, in PCF2.pcf_2]
Core.congr_app [lemma, in PCF2.pcf_2]
Core.congr_trny [lemma, in PCF2.pcf_2]
Core.congr_bot [lemma, in PCF2.pcf_2]
Core.congr_ff [lemma, in PCF2.pcf_2]
Core.congr_tt [lemma, in PCF2.pcf_2]
Core.extRen_tm [definition, in PCF2.pcf_2]
Core.ext_tm [definition, in PCF2.pcf_2]
Core.ff [constructor, in PCF2.pcf_2]
Core.Fun [constructor, in PCF2.pcf_2]
Core.idSubst_tm [definition, in PCF2.pcf_2]
Core.instId'_tm_pointwise [lemma, in PCF2.pcf_2]
Core.instId'_tm [lemma, in PCF2.pcf_2]
Core.lam [constructor, in PCF2.pcf_2]
Core.renRen_tm [lemma, in PCF2.pcf_2]
Core.renRen'_tm_pointwise [lemma, in PCF2.pcf_2]
Core.renSubst_tm_pointwise [lemma, in PCF2.pcf_2]
Core.renSubst_tm [lemma, in PCF2.pcf_2]
Core.ren_tm_morphism2 [instance, in PCF2.pcf_2]
Core.ren_tm_morphism [instance, in PCF2.pcf_2]
Core.Ren_tm [instance, in PCF2.pcf_2]
Core.ren_tm [definition, in PCF2.pcf_2]
Core.rinstId'_tm_pointwise [lemma, in PCF2.pcf_2]
Core.rinstId'_tm [lemma, in PCF2.pcf_2]
Core.rinstInst_up_tm_tm [lemma, in PCF2.pcf_2]
Core.rinstInst'_tm_pointwise [lemma, in PCF2.pcf_2]
Core.rinstInst'_tm [lemma, in PCF2.pcf_2]
Core.rinst_inst_tm [definition, in PCF2.pcf_2]
Core.substRen_tm_pointwise [lemma, in PCF2.pcf_2]
Core.substRen_tm [lemma, in PCF2.pcf_2]
Core.substSubst_tm_pointwise [lemma, in PCF2.pcf_2]
Core.substSubst_tm [lemma, in PCF2.pcf_2]
Core.subst_tm_morphism2 [instance, in PCF2.pcf_2]
Core.subst_tm_morphism [instance, in PCF2.pcf_2]
Core.Subst_tm [instance, in PCF2.pcf_2]
Core.subst_tm [definition, in PCF2.pcf_2]
Core.tm [inductive, in PCF2.pcf_2]
Core.tm_sind [definition, in PCF2.pcf_2]
Core.tm_rec [definition, in PCF2.pcf_2]
Core.tm_ind [definition, in PCF2.pcf_2]
Core.tm_rect [definition, in PCF2.pcf_2]
Core.trny [constructor, in PCF2.pcf_2]
Core.tt [constructor, in PCF2.pcf_2]
Core.ty [inductive, in PCF2.pcf_2]
Core.ty_sind [definition, in PCF2.pcf_2]
Core.ty_rec [definition, in PCF2.pcf_2]
Core.ty_ind [definition, in PCF2.pcf_2]
Core.ty_rect [definition, in PCF2.pcf_2]
Core.upExtRen_tm_tm [lemma, in PCF2.pcf_2]
Core.upExt_tm_tm [lemma, in PCF2.pcf_2]
Core.upId_tm_tm [lemma, in PCF2.pcf_2]
Core.upRen_tm_tm [lemma, in PCF2.pcf_2]
Core.Up_tm_tm [instance, in PCF2.pcf_2]
Core.up_tm [projection, in PCF2.pcf_2]
Core.Up_tm [record, in PCF2.pcf_2]
Core.up_tm [constructor, in PCF2.pcf_2]
Core.Up_tm [inductive, in PCF2.pcf_2]
Core.up_subst_subst_tm_tm [lemma, in PCF2.pcf_2]
Core.up_subst_ren_tm_tm [lemma, in PCF2.pcf_2]
Core.up_ren_subst_tm_tm [lemma, in PCF2.pcf_2]
Core.up_ren_ren_tm_tm [lemma, in PCF2.pcf_2]
Core.up_tm_tm [lemma, in PCF2.pcf_2]
Core.VarInstance_tm [instance, in PCF2.pcf_2]
Core.varLRen'_tm_pointwise [lemma, in PCF2.pcf_2]
Core.varLRen'_tm [lemma, in PCF2.pcf_2]
Core.varL'_tm_pointwise [lemma, in PCF2.pcf_2]
Core.varL'_tm [lemma, in PCF2.pcf_2]
Core.var_tm [constructor, in PCF2.pcf_2]
[ _ ] (fscope) [notation, in PCF2.pcf_2]
⟨ _ ⟩ (fscope) [notation, in PCF2.pcf_2]
_ __tm (subst_scope) [notation, in PCF2.pcf_2]
_ __tm (subst_scope) [notation, in PCF2.pcf_2]
var (subst_scope) [notation, in PCF2.pcf_2]
_ ⟨ _ ⟩ (subst_scope) [notation, in PCF2.pcf_2]
↑__tm (subst_scope) [notation, in PCF2.pcf_2]
↑__tm (subst_scope) [notation, in PCF2.pcf_2]
_ [ _ ] (subst_scope) [notation, in PCF2.pcf_2]
co_SR_reduces_CE_closed [lemma, in PCF2.undecidability]
co_RPS_CE [library]
ctxt_concat_fill [lemma, in PCF2.pcf_2_contexts]
ctxt_concat_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]
E
embed [definition, in PCF2.pcf_2_system]enc_typed [lemma, in PCF2.SATIS]
equiv_empty_imp_equiv_nonempty [lemma, in PCF2.contextual_equivalence]
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.contextual_equivalence]
eval_step [lemma, in PCF2.pcf_2_system]
Extra [module, in PCF2.pcf_2]
F
Fext [module, in PCF2.pcf_2]Fext.instId_tm [lemma, in PCF2.pcf_2]
Fext.renRen'_tm [lemma, in PCF2.pcf_2]
Fext.renSubst'_tm [lemma, in PCF2.pcf_2]
Fext.rinstId_tm [lemma, in PCF2.pcf_2]
Fext.rinstInst_tm [lemma, in PCF2.pcf_2]
Fext.substRen'_tm [lemma, in PCF2.pcf_2]
Fext.substSubst'_tm [lemma, in PCF2.pcf_2]
Fext.varLRen_tm [lemma, in PCF2.pcf_2]
Fext.varL_tm [lemma, in PCF2.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]
funcomp [definition, in PCF2.core]
funcomp_charact [lemma, in PCF2.pcf_2_system]
funcomp_morphism2 [instance, in PCF2.core]
funcomp_morphism [instance, in PCF2.core]
funcomp_assoc [lemma, in PCF2.core]
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_rev_to_context [lemma, in PCF2.SATIS]
fun_rule_encoding [definition, in PCF2.SATIS]
fv_subst [lemma, in PCF2.pcf_2_system]
G
G [definition, in PCF2.co_RPS_CE]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.unscoped]ids [projection, in PCF2.unscoped]
ids [constructor, in PCF2.unscoped]
idsRen [instance, in PCF2.unscoped]
IfB [constructor, in PCF2.pcf_2_system]
IfF [constructor, in PCF2.pcf_2_system]
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]
interface [module, in PCF2.pcf_2]
iq_sys_wf_cons_char [lemma, in PCF2.PS]
iq_sys_val_cons_char [lemma, in PCF2.PS]
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_proper [instance, in PCF2.pcf_2_system]
lam_args_subst [lemma, in PCF2.SATIS_PS]
lam_list_to_type' [lemma, in PCF2.SATIS]
lam_list_to_type [lemma, in PCF2.SATIS]
lam_T_split [lemma, in PCF2.SATIS]
lam_T_shift_subst [lemma, in PCF2.SATIS]
lam_T [definition, in PCF2.SATIS]
lam_subst_typed [lemma, in PCF2.contextual_equivalence]
lam_subst_step [lemma, in PCF2.contextual_equivalence]
lam_subst_concat [lemma, in PCF2.contextual_equivalence]
lam_subst [definition, in PCF2.contextual_equivalence]
leb_le_false [lemma, in PCF2.preliminaries]
leb_le_true [lemma, in PCF2.preliminaries]
length_base_context [lemma, in PCF2.SATIS]
length_var_seq [lemma, in PCF2.SATIS]
list_eq [lemma, in PCF2.preliminaries]
list_eq_dec [lemma, in PCF2.preliminaries]
list_val_exist [lemma, in PCF2.SATIS_PS]
list_to_fun_app' [lemma, in PCF2.SATIS]
list_to_fun [definition, in PCF2.SATIS]
list_comp [definition, in PCF2.core]
list_id [definition, in PCF2.core]
list_ext [definition, in PCF2.core]
Loaders_word_enc [axiom, in PCF2.undecidability]
ltb_lt_false [lemma, in PCF2.preliminaries]
ltb_lt_true [lemma, in PCF2.preliminaries]
M
make_rule_types_length [lemma, in PCF2.SATIS]make_rule_types [definition, in PCF2.SATIS]
N
nat_ord_dec [lemma, in PCF2.preliminaries]norm_comp [constructor, in PCF2.contextual_equivalence]
norm_bot_min [constructor, in PCF2.contextual_equivalence]
O
obs_preord_empty_imp_obs_preord_closed [lemma, in PCF2.contextual_equivalence]obs_equiv_trans [lemma, in PCF2.contextual_equivalence]
obs_equiv_refl [lemma, in PCF2.contextual_equivalence]
obs_equiv_rewrite_right [lemma, in PCF2.contextual_equivalence]
obs_equiv_rewrite_left [lemma, in PCF2.contextual_equivalence]
obs_preord_PreOrder [instance, in PCF2.contextual_equivalence]
obs_equiv_obs_preord [instance, in PCF2.contextual_equivalence]
obs_preord_rest [definition, in PCF2.contextual_equivalence]
obs_equiv_imp_cont_equiv [lemma, in PCF2.contextual_equivalence]
obs_equiv_imp_cont_pre_order [lemma, in PCF2.contextual_equivalence]
obs_equiv_base_eval_same [lemma, in PCF2.contextual_equivalence]
obs_equiv_context [lemma, in PCF2.contextual_equivalence]
obs_preord_context [lemma, in PCF2.contextual_equivalence]
obs_preord_base_refl [lemma, in PCF2.contextual_equivalence]
obs_preord_base_bot [lemma, in PCF2.contextual_equivalence]
obs_preord_incl_steps' [lemma, in PCF2.contextual_equivalence]
obs_preord_incl_step' [lemma, in PCF2.contextual_equivalence]
obs_preord_closed_incl_step' [lemma, in PCF2.contextual_equivalence]
obs_preord_incl_steps [lemma, in PCF2.contextual_equivalence]
obs_preord_incl_step [lemma, in PCF2.contextual_equivalence]
obs_preord_closed_incl_step [lemma, in PCF2.contextual_equivalence]
obs_preord_fun_char [lemma, in PCF2.contextual_equivalence]
obs_preord_closed_fun_char [lemma, in PCF2.contextual_equivalence]
obs_preord_trans [lemma, in PCF2.contextual_equivalence]
obs_preord_closed_trans [lemma, in PCF2.contextual_equivalence]
obs_preord_refl [lemma, in PCF2.contextual_equivalence]
obs_preord_closed_refl [lemma, in PCF2.contextual_equivalence]
obs_preord_closed_steps [lemma, in PCF2.contextual_equivalence]
obs_equiv [definition, in PCF2.contextual_equivalence]
obs_preord [definition, in PCF2.contextual_equivalence]
obs_preord_closed [definition, in PCF2.contextual_equivalence]
obs_preord_base_sind [definition, in PCF2.contextual_equivalence]
obs_preord_base_ind [definition, in PCF2.contextual_equivalence]
obs_preord_base [inductive, in PCF2.contextual_equivalence]
option_comp [definition, in PCF2.core]
option_ext [definition, in PCF2.core]
option_id [definition, in PCF2.core]
option_map [definition, in PCF2.core]
P
pair_eq_dec [lemma, in PCF2.preliminaries]pcf_2_system [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.core]
preliminaries [library]
pre_order_imp_obs_preord [lemma, in PCF2.contextual_equivalence]
pre_order_imp_obs_preord_closed [lemma, in PCF2.contextual_equivalence]
pre_order [definition, in PCF2.contextual_equivalence]
prod_comp [definition, in PCF2.core]
prod_ext [definition, in PCF2.core]
prod_id [definition, in PCF2.core]
prod_map [definition, in PCF2.core]
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 [definition, in PCF2.PS]
PS_RPS [library]
R
reduces_SR_SATIS_forward [lemma, in PCF2.SR_SATIS_forward]reduces_SATIS_PS [lemma, in PCF2.SATIS_PS]
reduces_CE_closed_CE [lemma, in PCF2.CE]
reduces_co_RPS_CE_closed [lemma, in PCF2.co_RPS_CE]
reduces_PS_RPS [lemma, in PCF2.PS_RPS]
reduces_SR_SATIS [lemma, in PCF2.undecidability]
reduces_SR_SATIS_backward [axiom, in PCF2.undecidability]
RenNotations [module, in PCF2.unscoped]
⟨ _ ; _ ⟩ (fscope) [notation, in PCF2.unscoped]
⟨ _ ⟩ (fscope) [notation, in PCF2.unscoped]
_ ⟨ _ ; _ ; _ ; _ ; _ ⟩ (subst_scope) [notation, in PCF2.unscoped]
_ ⟨ _ ; _ ; _ ; _ ⟩ (subst_scope) [notation, in PCF2.unscoped]
_ ⟨ _ ; _ ; _ ⟩ (subst_scope) [notation, in PCF2.unscoped]
_ ⟨ _ ; _ ⟩ (subst_scope) [notation, in PCF2.unscoped]
_ ⟨ _ ⟩ (subst_scope) [notation, in PCF2.unscoped]
ren_shift_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]
ren1 [projection, in PCF2.unscoped]
Ren1 [record, in PCF2.unscoped]
ren1 [constructor, in PCF2.unscoped]
Ren1 [inductive, in PCF2.unscoped]
ren2 [projection, in PCF2.unscoped]
Ren2 [record, in PCF2.unscoped]
ren2 [constructor, in PCF2.unscoped]
Ren2 [inductive, in PCF2.unscoped]
ren3 [projection, in PCF2.unscoped]
Ren3 [record, in PCF2.unscoped]
ren3 [constructor, in PCF2.unscoped]
Ren3 [inductive, in PCF2.unscoped]
ren4 [projection, in PCF2.unscoped]
Ren4 [record, in PCF2.unscoped]
ren4 [constructor, in PCF2.unscoped]
Ren4 [inductive, in PCF2.unscoped]
ren5 [projection, in PCF2.unscoped]
Ren5 [record, in PCF2.unscoped]
ren5 [constructor, in PCF2.unscoped]
Ren5 [inductive, in PCF2.unscoped]
restrict_sys [lemma, in PCF2.PS_RPS]
rest_PCF [definition, in PCF2.contextual_equivalence]
res_ineq_sys_val_cons_char [lemma, in PCF2.RPS]
rev_nth_error2 [lemma, in PCF2.preliminaries]
rev_nth_error1 [lemma, in PCF2.preliminaries]
rew [inductive, in PCF2.SR]
rewB [constructor, in PCF2.SR]
rewR [constructor, in PCF2.SR]
rewrite_in_evaluates [instance, in PCF2.contextual_equivalence]
rewrite_in_obs_preord_base [instance, in PCF2.contextual_equivalence]
rewS [constructor, in PCF2.SR]
rewt [inductive, in PCF2.SR]
rewt_sind [definition, in PCF2.SR]
rewt_ind [definition, in PCF2.SR]
rew_sind [definition, in PCF2.SR]
rew_ind [definition, in PCF2.SR]
riq_sys_wf_cons_char [lemma, in PCF2.RPS]
RPS [definition, in PCF2.RPS]
RPS [library]
rps_system_well_formed [definition, in PCF2.RPS]
rps_system_solvable [definition, in PCF2.RPS]
rps_system [definition, in PCF2.RPS]
RuleNotation [module, in PCF2.SR]
_ / _ [notation, in PCF2.SR]
rules_eq_decidable [lemma, in PCF2.preliminaries]
rule_enc_word_enc_closed' [lemma, in PCF2.SATIS]
rule_enc_word_enc_closed [lemma, in PCF2.SATIS]
rule_enc_equiv [lemma, in PCF2.SATIS]
rule_some [lemma, in PCF2.SATIS]
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_PS [library]
scons [definition, in PCF2.unscoped]
scons_morphism2 [instance, in PCF2.unscoped]
scons_morphism [instance, in PCF2.unscoped]
scons_comp' [lemma, in PCF2.unscoped]
scons_eta_id' [lemma, in PCF2.unscoped]
scons_eta' [lemma, in PCF2.unscoped]
scons_comp [lemma, in PCF2.unscoped_axioms]
scons_eta [lemma, in PCF2.unscoped_axioms]
scons_eta_id [lemma, in PCF2.unscoped_axioms]
shift [definition, in PCF2.unscoped]
shifted_subst_char [lemma, in PCF2.pcf_2_system]
shifted_subst [definition, in PCF2.pcf_2_system]
solves_rps_system [definition, in PCF2.RPS]
solves_ps_system [definition, in PCF2.PS]
SR [definition, in PCF2.SR]
SR [library]
SRS [abbreviation, in PCF2.SR]
SR_undec [axiom, in PCF2.undecidability]
SR_SATIS_forward [library]
step [inductive, in PCF2.pcf_2_system]
steps [definition, in PCF2.pcf_2_system]
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_preord_backward [lemma, in PCF2.contextual_equivalence]
steps_preserve_obs_preord [lemma, in PCF2.contextual_equivalence]
steps_equiv [lemma, in PCF2.contextual_equivalence]
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.SR]
string [abbreviation, in PCF2.SR]
strong_obs_preord_imp_obs_preord [lemma, in PCF2.contextual_equivalence]
strong_obs_preord_refl [lemma, in PCF2.contextual_equivalence]
strong_obs_preord_steps [lemma, in PCF2.contextual_equivalence]
strong_obs_preord [definition, in PCF2.contextual_equivalence]
SubstNotations [module, in PCF2.unscoped]
_ [ _ ; _ ] (subst_scope) [notation, in PCF2.unscoped]
_ [ _ ] (subst_scope) [notation, in PCF2.unscoped]
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_apply_args [lemma, in PCF2.SATIS]
subst_equiv [lemma, in PCF2.contextual_equivalence]
subst_rel_nil [lemma, in PCF2.contextual_equivalence]
subst_rel [definition, in PCF2.contextual_equivalence]
subst1 [projection, in PCF2.unscoped]
Subst1 [record, in PCF2.unscoped]
subst1 [constructor, in PCF2.unscoped]
Subst1 [inductive, in PCF2.unscoped]
subst2 [projection, in PCF2.unscoped]
Subst2 [record, in PCF2.unscoped]
subst2 [constructor, in PCF2.unscoped]
Subst2 [inductive, in PCF2.unscoped]
subst3 [projection, in PCF2.unscoped]
Subst3 [record, in PCF2.unscoped]
subst3 [constructor, in PCF2.unscoped]
Subst3 [inductive, in PCF2.unscoped]
subst4 [projection, in PCF2.unscoped]
Subst4 [record, in PCF2.unscoped]
subst4 [constructor, in PCF2.unscoped]
Subst4 [inductive, in PCF2.unscoped]
subst5 [projection, in PCF2.unscoped]
Subst5 [record, in PCF2.unscoped]
subst5 [constructor, in PCF2.unscoped]
Subst5 [inductive, in PCF2.unscoped]
swap [definition, in PCF2.SR]
T
T [definition, in PCF2.SATIS]trny_typed [constructor, in PCF2.pcf_2_system]
TSR [definition, in PCF2.SR]
tt_typed [constructor, in PCF2.pcf_2_system]
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.SR_SATIS_forward]
t_subst_char [lemma, in PCF2.SATIS_PS]
t_subst_map_var_rules' [lemma, in PCF2.SATIS]
t_subst_map_var_rules [lemma, in PCF2.SATIS]
t_subst_map_var_id' [lemma, in PCF2.SATIS]
t_subst_map_var_id [lemma, in PCF2.SATIS]
t_subst_well_typed [lemma, in PCF2.SATIS]
T_list_to_fun [lemma, in PCF2.SATIS]
t_subst [definition, in PCF2.SATIS]
U
undecidability [library]unscoped [library]
UnscopedNotations [module, in PCF2.unscoped]
↑ (subst_scope) [notation, in PCF2.unscoped]
_ .. (subst_scope) [notation, in PCF2.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.unscoped]
up_ren_ren [lemma, in PCF2.unscoped]
up_ren [definition, in PCF2.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.unscoped]
Var [inductive, in PCF2.unscoped]
var_typed [constructor, in PCF2.pcf_2_system]
var_seq_map_nth [lemma, in PCF2.SATIS]
var_seq_nth [lemma, in PCF2.SATIS]
var_seq_split [lemma, in PCF2.SATIS]
var_seq [definition, in PCF2.SATIS]
var_zero [definition, in PCF2.unscoped]
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.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]
_ ⊢ _ ≡c _ : _ [notation, in PCF2.contextual_equivalence]
_ ⊢ _ ≡ _ : _ [notation, in PCF2.contextual_equivalence]
_ ≤b _ [notation, in PCF2.contextual_equivalence]
_ ≤c _ : _ [notation, in PCF2.contextual_equivalence]
_ ⊢ _ ≤ _ : _ [notation, in PCF2.contextual_equivalence]
list_map [notation, in PCF2.core]
Notation Index
C
_ >> _ (fscope) [in PCF2.unscoped]_ .: _ (subst_scope) [in PCF2.unscoped]
[ _ ] (fscope) [in PCF2.pcf_2]
⟨ _ ⟩ (fscope) [in PCF2.pcf_2]
_ __tm (subst_scope) [in PCF2.pcf_2]
_ __tm (subst_scope) [in PCF2.pcf_2]
var (subst_scope) [in PCF2.pcf_2]
_ ⟨ _ ⟩ (subst_scope) [in PCF2.pcf_2]
↑__tm (subst_scope) [in PCF2.pcf_2]
↑__tm (subst_scope) [in PCF2.pcf_2]
_ [ _ ] (subst_scope) [in PCF2.pcf_2]
R
⟨ _ ; _ ⟩ (fscope) [in PCF2.unscoped]⟨ _ ⟩ (fscope) [in PCF2.unscoped]
_ ⟨ _ ; _ ; _ ; _ ; _ ⟩ (subst_scope) [in PCF2.unscoped]
_ ⟨ _ ; _ ; _ ; _ ⟩ (subst_scope) [in PCF2.unscoped]
_ ⟨ _ ; _ ; _ ⟩ (subst_scope) [in PCF2.unscoped]
_ ⟨ _ ; _ ⟩ (subst_scope) [in PCF2.unscoped]
_ ⟨ _ ⟩ (subst_scope) [in PCF2.unscoped]
_ / _ [in PCF2.SR]
S
_ [ _ ; _ ] (subst_scope) [in PCF2.unscoped]_ [ _ ] (subst_scope) [in PCF2.unscoped]
U
↑ (subst_scope) [in PCF2.unscoped]_ .. (subst_scope) [in PCF2.unscoped]
other
_ [ _ , _ ] : _ , _ [in PCF2.pcf_2_contexts]_ ⊢ _ [ _ ] [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]
_ ⊢ _ ≡c _ : _ [in PCF2.contextual_equivalence]
_ ⊢ _ ≡ _ : _ [in PCF2.contextual_equivalence]
_ ≤b _ [in PCF2.contextual_equivalence]
_ ≤c _ : _ [in PCF2.contextual_equivalence]
_ ⊢ _ ≤ _ : _ [in PCF2.contextual_equivalence]
list_map [in PCF2.core]
Module Index
A
Allfv [in PCF2.pcf_2]C
CombineNotations [in PCF2.unscoped]Core [in PCF2.pcf_2]
E
Extra [in PCF2.pcf_2]F
Fext [in PCF2.pcf_2]I
interface [in PCF2.pcf_2]R
RenNotations [in PCF2.unscoped]RuleNotation [in PCF2.SR]
S
SubstNotations [in PCF2.unscoped]U
UnscopedNotations [in PCF2.unscoped]Library Index
C
CEcontextual_equivalence
core
core_axioms
co_RPS_CE
P
pcf_2_systempcf_2_contexts
pcf_2
preliminaries
PS
PS_RPS
R
RPSS
SATISSATIS_PS
SR
SR_SATIS_forward
U
undecidabilityunscoped
unscoped_axioms
Lemma Index
A
allfv_tm_dec [in PCF2.pcf_2_system]Allfv.upAllfvImpl_tm_tm [in PCF2.pcf_2]
Allfv.upAllfvRenL_tm_tm [in PCF2.pcf_2]
Allfv.upAllfvRenR_tm_tm [in PCF2.pcf_2]
Allfv.upAllfvTriv_tm_tm [in PCF2.pcf_2]
Allfv.upAllfv_tm_tm [in PCF2.pcf_2]
apply_args_steps_list' [in PCF2.SATIS]
apply_args_steps_list [in PCF2.SATIS]
apply_args_steps_body [in PCF2.SATIS]
apply_args_typed [in PCF2.SATIS]
apply_args_cons [in PCF2.SATIS]
apply_args_app [in PCF2.SATIS]
app_right [in PCF2.pcf_2_system]
app_left [in PCF2.pcf_2_system]
arith_technical [in PCF2.SATIS]
B
basefun_var_applied_typed [in PCF2.SATIS]base_context_le_base [in PCF2.SR_SATIS_forward]
base_fun_applied_typed [in PCF2.SATIS]
base_context_rev [in PCF2.SATIS]
base_context_rev' [in PCF2.SATIS]
base_context_some_base [in PCF2.SATIS]
base_preord_ff_le [in PCF2.contextual_equivalence]
base_preord_tt_le [in PCF2.contextual_equivalence]
base_preord_le_bot [in PCF2.contextual_equivalence]
bool_eq_dec [in PCF2.preliminaries]
bval_steps_char [in PCF2.pcf_2_system]
C
CE_undecidable [in PCF2.undecidability]CE_closed_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]
cont_pre_order_imp_cont_equiv [in PCF2.contextual_equivalence]
Core.congr_Fun [in PCF2.pcf_2]
Core.congr_Base [in PCF2.pcf_2]
Core.congr_lam [in PCF2.pcf_2]
Core.congr_app [in PCF2.pcf_2]
Core.congr_trny [in PCF2.pcf_2]
Core.congr_bot [in PCF2.pcf_2]
Core.congr_ff [in PCF2.pcf_2]
Core.congr_tt [in PCF2.pcf_2]
Core.instId'_tm_pointwise [in PCF2.pcf_2]
Core.instId'_tm [in PCF2.pcf_2]
Core.renRen_tm [in PCF2.pcf_2]
Core.renRen'_tm_pointwise [in PCF2.pcf_2]
Core.renSubst_tm_pointwise [in PCF2.pcf_2]
Core.renSubst_tm [in PCF2.pcf_2]
Core.rinstId'_tm_pointwise [in PCF2.pcf_2]
Core.rinstId'_tm [in PCF2.pcf_2]
Core.rinstInst_up_tm_tm [in PCF2.pcf_2]
Core.rinstInst'_tm_pointwise [in PCF2.pcf_2]
Core.rinstInst'_tm [in PCF2.pcf_2]
Core.substRen_tm_pointwise [in PCF2.pcf_2]
Core.substRen_tm [in PCF2.pcf_2]
Core.substSubst_tm_pointwise [in PCF2.pcf_2]
Core.substSubst_tm [in PCF2.pcf_2]
Core.upExtRen_tm_tm [in PCF2.pcf_2]
Core.upExt_tm_tm [in PCF2.pcf_2]
Core.upId_tm_tm [in PCF2.pcf_2]
Core.upRen_tm_tm [in PCF2.pcf_2]
Core.up_subst_subst_tm_tm [in PCF2.pcf_2]
Core.up_subst_ren_tm_tm [in PCF2.pcf_2]
Core.up_ren_subst_tm_tm [in PCF2.pcf_2]
Core.up_ren_ren_tm_tm [in PCF2.pcf_2]
Core.up_tm_tm [in PCF2.pcf_2]
Core.varLRen'_tm_pointwise [in PCF2.pcf_2]
Core.varLRen'_tm [in PCF2.pcf_2]
Core.varL'_tm_pointwise [in PCF2.pcf_2]
Core.varL'_tm [in PCF2.pcf_2]
co_SR_reduces_CE_closed [in PCF2.undecidability]
ctxt_concat_fill [in PCF2.pcf_2_contexts]
ctxt_concat_typed [in PCF2.pcf_2_contexts]
E
enc_typed [in PCF2.SATIS]equiv_empty_imp_equiv_nonempty [in PCF2.contextual_equivalence]
evaluates_to_same [in PCF2.pcf_2_system]
evaluates_to_final [in PCF2.contextual_equivalence]
eval_step [in PCF2.pcf_2_system]
F
Fext.instId_tm [in PCF2.pcf_2]Fext.renRen'_tm [in PCF2.pcf_2]
Fext.renSubst'_tm [in PCF2.pcf_2]
Fext.rinstId_tm [in PCF2.pcf_2]
Fext.rinstInst_tm [in PCF2.pcf_2]
Fext.substRen'_tm [in PCF2.pcf_2]
Fext.substSubst'_tm [in PCF2.pcf_2]
Fext.varLRen_tm [in PCF2.pcf_2]
Fext.varL_tm [in PCF2.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.core]
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]
fun_rev_to_context [in PCF2.SATIS]
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]
iq_sys_wf_cons_char [in PCF2.PS]
iq_sys_val_cons_char [in PCF2.PS]
iter_succ_l [in PCF2.preliminaries]
iter_succ_r [in PCF2.preliminaries]
iter_ren_closed [in PCF2.pcf_2_system]
L
lam_args_subst [in PCF2.SATIS_PS]lam_list_to_type' [in PCF2.SATIS]
lam_list_to_type [in PCF2.SATIS]
lam_T_split [in PCF2.SATIS]
lam_T_shift_subst [in PCF2.SATIS]
lam_subst_typed [in PCF2.contextual_equivalence]
lam_subst_step [in PCF2.contextual_equivalence]
lam_subst_concat [in PCF2.contextual_equivalence]
leb_le_false [in PCF2.preliminaries]
leb_le_true [in PCF2.preliminaries]
length_base_context [in PCF2.SATIS]
length_var_seq [in PCF2.SATIS]
list_eq [in PCF2.preliminaries]
list_eq_dec [in PCF2.preliminaries]
list_val_exist [in PCF2.SATIS_PS]
list_to_fun_app' [in PCF2.SATIS]
ltb_lt_false [in PCF2.preliminaries]
ltb_lt_true [in PCF2.preliminaries]
M
make_rule_types_length [in PCF2.SATIS]N
nat_ord_dec [in PCF2.preliminaries]O
obs_preord_empty_imp_obs_preord_closed [in PCF2.contextual_equivalence]obs_equiv_trans [in PCF2.contextual_equivalence]
obs_equiv_refl [in PCF2.contextual_equivalence]
obs_equiv_rewrite_right [in PCF2.contextual_equivalence]
obs_equiv_rewrite_left [in PCF2.contextual_equivalence]
obs_equiv_imp_cont_equiv [in PCF2.contextual_equivalence]
obs_equiv_imp_cont_pre_order [in PCF2.contextual_equivalence]
obs_equiv_base_eval_same [in PCF2.contextual_equivalence]
obs_equiv_context [in PCF2.contextual_equivalence]
obs_preord_context [in PCF2.contextual_equivalence]
obs_preord_base_refl [in PCF2.contextual_equivalence]
obs_preord_base_bot [in PCF2.contextual_equivalence]
obs_preord_incl_steps' [in PCF2.contextual_equivalence]
obs_preord_incl_step' [in PCF2.contextual_equivalence]
obs_preord_closed_incl_step' [in PCF2.contextual_equivalence]
obs_preord_incl_steps [in PCF2.contextual_equivalence]
obs_preord_incl_step [in PCF2.contextual_equivalence]
obs_preord_closed_incl_step [in PCF2.contextual_equivalence]
obs_preord_fun_char [in PCF2.contextual_equivalence]
obs_preord_closed_fun_char [in PCF2.contextual_equivalence]
obs_preord_trans [in PCF2.contextual_equivalence]
obs_preord_closed_trans [in PCF2.contextual_equivalence]
obs_preord_refl [in PCF2.contextual_equivalence]
obs_preord_closed_refl [in PCF2.contextual_equivalence]
obs_preord_closed_steps [in PCF2.contextual_equivalence]
P
pair_eq_dec [in PCF2.preliminaries]pointwise_forall [in PCF2.core]
pre_order_imp_obs_preord [in PCF2.contextual_equivalence]
pre_order_imp_obs_preord_closed [in PCF2.contextual_equivalence]
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_SATIS_PS [in PCF2.SATIS_PS]
reduces_CE_closed_CE [in PCF2.CE]
reduces_co_RPS_CE_closed [in PCF2.co_RPS_CE]
reduces_PS_RPS [in PCF2.PS_RPS]
reduces_SR_SATIS [in PCF2.undecidability]
ren_shift_typed [in PCF2.SR_SATIS_forward]
ren_subst [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]
rev_nth_error2 [in PCF2.preliminaries]
rev_nth_error1 [in PCF2.preliminaries]
riq_sys_wf_cons_char [in PCF2.RPS]
rules_eq_decidable [in PCF2.preliminaries]
rule_enc_word_enc_closed' [in PCF2.SATIS]
rule_enc_word_enc_closed [in PCF2.SATIS]
rule_enc_equiv [in PCF2.SATIS]
rule_some [in PCF2.SATIS]
S
satisfies_rule_enc_ind [in PCF2.SATIS_PS]scons_comp' [in PCF2.unscoped]
scons_eta_id' [in PCF2.unscoped]
scons_eta' [in PCF2.unscoped]
scons_comp [in PCF2.unscoped_axioms]
scons_eta [in PCF2.unscoped_axioms]
scons_eta_id [in PCF2.unscoped_axioms]
shifted_subst_char [in PCF2.pcf_2_system]
steps_n1 [in PCF2.pcf_2_system]
steps_1n [in PCF2.pcf_2_system]
steps_preserve_obs_preord_backward [in PCF2.contextual_equivalence]
steps_preserve_obs_preord [in PCF2.contextual_equivalence]
steps_equiv [in PCF2.contextual_equivalence]
step_eval [in PCF2.pcf_2_system]
strong_obs_preord_imp_obs_preord [in PCF2.contextual_equivalence]
strong_obs_preord_refl [in PCF2.contextual_equivalence]
strong_obs_preord_steps [in PCF2.contextual_equivalence]
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_apply_args [in PCF2.SATIS]
subst_equiv [in PCF2.contextual_equivalence]
subst_rel_nil [in PCF2.contextual_equivalence]
T
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.SR_SATIS_forward]
t_subst_char [in PCF2.SATIS_PS]
t_subst_map_var_rules' [in PCF2.SATIS]
t_subst_map_var_rules [in PCF2.SATIS]
t_subst_map_var_id' [in PCF2.SATIS]
t_subst_map_var_id [in PCF2.SATIS]
t_subst_well_typed [in PCF2.SATIS]
T_list_to_fun [in PCF2.SATIS]
U
up_tm_tm_iter2 [in PCF2.pcf_2_system]up_tm_tm_iter1 [in PCF2.pcf_2_system]
up_ren_ren [in PCF2.unscoped]
V
val_list_closed [in PCF2.pcf_2_system]val_no_step [in PCF2.pcf_2_system]
var_seq_map_nth [in PCF2.SATIS]
var_seq_nth [in PCF2.SATIS]
var_seq_split [in PCF2.SATIS]
W
well_formed_forall [in PCF2.PS_RPS]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.pcf_2]Core.Base [in PCF2.pcf_2]
Core.bot [in PCF2.pcf_2]
Core.ff [in PCF2.pcf_2]
Core.Fun [in PCF2.pcf_2]
Core.lam [in PCF2.pcf_2]
Core.trny [in PCF2.pcf_2]
Core.tt [in PCF2.pcf_2]
Core.up_tm [in PCF2.pcf_2]
Core.var_tm [in PCF2.pcf_2]
F
ff_typed [in PCF2.pcf_2_system]fun_typed [in PCF2.pcf_2_system]
I
ids [in PCF2.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.contextual_equivalence]norm_bot_min [in PCF2.contextual_equivalence]
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.unscoped]ren2 [in PCF2.unscoped]
ren3 [in PCF2.unscoped]
ren4 [in PCF2.unscoped]
ren5 [in PCF2.unscoped]
rewB [in PCF2.SR]
rewR [in PCF2.SR]
rewS [in PCF2.SR]
S
subst1 [in PCF2.unscoped]subst2 [in PCF2.unscoped]
subst3 [in PCF2.unscoped]
subst4 [in PCF2.unscoped]
subst5 [in PCF2.unscoped]
T
trny_typed [in PCF2.pcf_2_system]tt_typed [in PCF2.pcf_2_system]
V
var_typed [in PCF2.pcf_2_system]Axiom Index
C
church_rosser [in PCF2.pcf_2_system]L
Loaders_word_enc [in PCF2.undecidability]R
reduces_SR_SATIS_backward [in PCF2.undecidability]rule_enc_exist [in PCF2.SATIS]
S
SR_undec [in PCF2.undecidability]W
weak_normalisation_comp [in PCF2.pcf_2_system]Inductive Index
C
Core.tm [in PCF2.pcf_2]Core.ty [in PCF2.pcf_2]
Core.Up_tm [in PCF2.pcf_2]
ctxt_typed [in PCF2.pcf_2_contexts]
O
obs_preord_base [in PCF2.contextual_equivalence]P
pctxt [in PCF2.pcf_2_contexts]R
Ren1 [in PCF2.unscoped]Ren2 [in PCF2.unscoped]
Ren3 [in PCF2.unscoped]
Ren4 [in PCF2.unscoped]
Ren5 [in PCF2.unscoped]
rew [in PCF2.SR]
rewt [in PCF2.SR]
S
step [in PCF2.pcf_2_system]Subst1 [in PCF2.unscoped]
Subst2 [in PCF2.unscoped]
Subst3 [in PCF2.unscoped]
Subst4 [in PCF2.unscoped]
Subst5 [in PCF2.unscoped]
T
typed [in PCF2.pcf_2_system]V
Var [in PCF2.unscoped]Projection Index
C
Core.up_tm [in PCF2.pcf_2]I
ids [in PCF2.unscoped]R
ren1 [in PCF2.unscoped]ren2 [in PCF2.unscoped]
ren3 [in PCF2.unscoped]
ren4 [in PCF2.unscoped]
ren5 [in PCF2.unscoped]
S
subst1 [in PCF2.unscoped]subst2 [in PCF2.unscoped]
subst3 [in PCF2.unscoped]
subst4 [in PCF2.unscoped]
subst5 [in PCF2.unscoped]
Instance Index
A
app_proper [in PCF2.pcf_2_system]C
Core.ren_tm_morphism2 [in PCF2.pcf_2]Core.ren_tm_morphism [in PCF2.pcf_2]
Core.Ren_tm [in PCF2.pcf_2]
Core.subst_tm_morphism2 [in PCF2.pcf_2]
Core.subst_tm_morphism [in PCF2.pcf_2]
Core.Subst_tm [in PCF2.pcf_2]
Core.Up_tm_tm [in PCF2.pcf_2]
Core.VarInstance_tm [in PCF2.pcf_2]
E
evaluates_steps [in PCF2.pcf_2_system]F
funcomp_morphism2 [in PCF2.core]funcomp_morphism [in PCF2.core]
I
idsRen [in PCF2.unscoped]if_proper [in PCF2.pcf_2_system]
L
lam_proper [in PCF2.pcf_2_system]O
obs_preord_PreOrder [in PCF2.contextual_equivalence]obs_equiv_obs_preord [in PCF2.contextual_equivalence]
R
rewrite_in_evaluates [in PCF2.contextual_equivalence]rewrite_in_obs_preord_base [in PCF2.contextual_equivalence]
S
scons_morphism2 [in PCF2.unscoped]scons_morphism [in PCF2.unscoped]
steps_PreOrder [in PCF2.pcf_2_system]
step_steps [in PCF2.pcf_2_system]
Abbreviation Index
S
SRS [in PCF2.SR]str [in PCF2.SR]
string [in PCF2.SR]
Definition Index
A
Allfv.allfvImpl_tm [in PCF2.pcf_2]Allfv.allfvRenL_tm [in PCF2.pcf_2]
Allfv.allfvRenR_tm [in PCF2.pcf_2]
Allfv.allfvTriv_tm [in PCF2.pcf_2]
Allfv.allfv_tm [in PCF2.pcf_2]
ap [in PCF2.unscoped]
ap [in PCF2.core]
apc [in PCF2.unscoped]
apc [in PCF2.core]
apply_args [in PCF2.SATIS]
B
base_context [in PCF2.SATIS]base_fun [in PCF2.SATIS]
C
CE [in PCF2.CE]CE_closed [in PCF2.CE]
closed [in PCF2.pcf_2_system]
cod [in PCF2.core_axioms]
cod_comp [in PCF2.core_axioms]
cod_ext [in PCF2.core_axioms]
cod_id [in PCF2.core_axioms]
cod_map [in PCF2.core_axioms]
concat [in PCF2.pcf_2_contexts]
context [in PCF2.pcf_2_system]
cont_equiv [in PCF2.contextual_equivalence]
Core.compRenRen_tm [in PCF2.pcf_2]
Core.compRenSubst_tm [in PCF2.pcf_2]
Core.compSubstRen_tm [in PCF2.pcf_2]
Core.compSubstSubst_tm [in PCF2.pcf_2]
Core.extRen_tm [in PCF2.pcf_2]
Core.ext_tm [in PCF2.pcf_2]
Core.idSubst_tm [in PCF2.pcf_2]
Core.ren_tm [in PCF2.pcf_2]
Core.rinst_inst_tm [in PCF2.pcf_2]
Core.subst_tm [in PCF2.pcf_2]
Core.tm_sind [in PCF2.pcf_2]
Core.tm_rec [in PCF2.pcf_2]
Core.tm_ind [in PCF2.pcf_2]
Core.tm_rect [in PCF2.pcf_2]
Core.ty_sind [in PCF2.pcf_2]
Core.ty_rec [in PCF2.pcf_2]
Core.ty_ind [in PCF2.pcf_2]
Core.ty_rect [in PCF2.pcf_2]
ctxt_typed_sind [in PCF2.pcf_2_contexts]
ctxt_typed_ind [in PCF2.pcf_2_contexts]
E
embed [in PCF2.pcf_2_system]eq_dec [in PCF2.preliminaries]
evaluates_to_base [in PCF2.pcf_2_system]
F
fill [in PCF2.pcf_2_contexts]funcomp [in PCF2.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.unscoped]is_bval [in PCF2.pcf_2_system]
L
lam_T [in PCF2.SATIS]lam_subst [in PCF2.contextual_equivalence]
list_to_fun [in PCF2.SATIS]
list_comp [in PCF2.core]
list_id [in PCF2.core]
list_ext [in PCF2.core]
M
make_rule_types [in PCF2.SATIS]O
obs_preord_rest [in PCF2.contextual_equivalence]obs_equiv [in PCF2.contextual_equivalence]
obs_preord [in PCF2.contextual_equivalence]
obs_preord_closed [in PCF2.contextual_equivalence]
obs_preord_base_sind [in PCF2.contextual_equivalence]
obs_preord_base_ind [in PCF2.contextual_equivalence]
option_comp [in PCF2.core]
option_ext [in PCF2.core]
option_id [in PCF2.core]
option_map [in PCF2.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]
pre_order [in PCF2.contextual_equivalence]
prod_comp [in PCF2.core]
prod_ext [in PCF2.core]
prod_id [in PCF2.core]
prod_map [in PCF2.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]
ps_system [in PCF2.PS]
R
ren_shift [in PCF2.SR_SATIS_forward]rest_PCF [in PCF2.contextual_equivalence]
rewt_sind [in PCF2.SR]
rewt_ind [in PCF2.SR]
rew_sind [in PCF2.SR]
rew_ind [in PCF2.SR]
RPS [in PCF2.RPS]
rps_system_well_formed [in PCF2.RPS]
rps_system_solvable [in PCF2.RPS]
rps_system [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]
scons [in PCF2.unscoped]
shift [in PCF2.unscoped]
shifted_subst [in PCF2.pcf_2_system]
solves_rps_system [in PCF2.RPS]
solves_ps_system [in PCF2.PS]
SR [in PCF2.SR]
steps [in PCF2.pcf_2_system]
step_sind [in PCF2.pcf_2_system]
step_ind [in PCF2.pcf_2_system]
strong_obs_preord [in PCF2.contextual_equivalence]
subst_well_typed [in PCF2.pcf_2_system]
subst_list [in PCF2.SATIS_PS]
subst_rel [in PCF2.contextual_equivalence]
swap [in PCF2.SR]
T
T [in PCF2.SATIS]TSR [in PCF2.SR]
typed_sind [in PCF2.pcf_2_system]
typed_ind [in PCF2.pcf_2_system]
t_subst [in PCF2.SATIS]
U
up_allfv [in PCF2.unscoped]up_ren [in PCF2.unscoped]
V
val_rule_enc [in PCF2.SATIS]val_word_enc [in PCF2.SATIS]
var_seq [in PCF2.SATIS]
var_zero [in PCF2.unscoped]
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.pcf_2]R
Ren1 [in PCF2.unscoped]Ren2 [in PCF2.unscoped]
Ren3 [in PCF2.unscoped]
Ren4 [in PCF2.unscoped]
Ren5 [in PCF2.unscoped]
S
Subst1 [in PCF2.unscoped]Subst2 [in PCF2.unscoped]
Subst3 [in PCF2.unscoped]
Subst4 [in PCF2.unscoped]
Subst5 [in PCF2.unscoped]
V
Var [in PCF2.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 | (569 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 | (36 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 | (10 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 | (19 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 | (239 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 | (58 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 | (6 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 | (21 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 | (12 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 | (23 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 | (3 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 | (130 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 | (12 entries) |
This page has been generated by coqdoc