| 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 | (430 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 | (16 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 | (14 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 | (12 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 | (155 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 | (39 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) |
| 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 | (13 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 | (11 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 | (15 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 | (138 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 | (5 entries) |
Global Index
B
blank [constructor, in PCPUndecidability.Halt_MPCP]C
class [projection, in PCPUndecidability.Prelim]concat_map_snd_copy [lemma, in PCPUndecidability.SR_MPCP]
concat_map_fst_copy [lemma, in PCPUndecidability.SR_MPCP]
concat_pcp_lsig_snd [lemma, in PCPUndecidability.MPCP_PCP]
concat_pcp_lsig_fst [lemma, in PCPUndecidability.MPCP_PCP]
concat_del_dominos_snd [lemma, in PCPUndecidability.MPCP_PCP]
concat_del_dominos_fst [lemma, in PCPUndecidability.MPCP_PCP]
concat_hash_right [lemma, in PCPUndecidability.MPCP_PCP]
concat_hash_left [lemma, in PCPUndecidability.MPCP_PCP]
conf [definition, in PCPUndecidability.Halt_MPCP]
conf [definition, in PCPUndecidability.Halt_SR]
copy_string_el [lemma, in PCPUndecidability.SR_MPCP]
copy_string [definition, in PCPUndecidability.SR_MPCP]
count [definition, in PCPUndecidability.Prelim]
countIn [lemma, in PCPUndecidability.Prelim]
countSplit [lemma, in PCPUndecidability.Prelim]
cstate [projection, in PCPUndecidability.Single_TM]
ctape [projection, in PCPUndecidability.Single_TM]
current [definition, in PCPUndecidability.Single_TM]
D
Dec [definition, in PCPUndecidability.Prelim]dec [definition, in PCPUndecidability.Prelim]
dec2bool [definition, in PCPUndecidability.Prelim]
delete_fin [lemma, in PCPUndecidability.Halt_SR]
delete_list_left [lemma, in PCPUndecidability.Halt_SR]
delete_list_right [lemma, in PCPUndecidability.Halt_SR]
deletion_dominoes [lemma, in PCPUndecidability.Halt_MPCP]
deletion_dominoes_left [lemma, in PCPUndecidability.Halt_MPCP]
deletion_dominoes_right [lemma, in PCPUndecidability.Halt_MPCP]
delRules [definition, in PCPUndecidability.Halt_SR]
del_empty_dominos [definition, in PCPUndecidability.MPCP_PCP]
del_rule_fin_el [lemma, in PCPUndecidability.Halt_SR]
del_rule_l_el [lemma, in PCPUndecidability.Halt_SR]
del_rule_r_el [lemma, in PCPUndecidability.Halt_SR]
del_rules_fin [definition, in PCPUndecidability.Halt_SR]
del_rules_r [definition, in PCPUndecidability.Halt_SR]
del_rules_l [definition, in PCPUndecidability.Halt_SR]
diff_constructors_count_zero [lemma, in PCPUndecidability.Prelim]
dollar [constructor, in PCPUndecidability.SR_MPCP]
dollar [constructor, in PCPUndecidability.MPCP_PCP]
dollar [constructor, in PCPUndecidability.Halt_MPCP]
dollar [constructor, in PCPUndecidability.RSR_PCP]
dollar [constructor, in PCPUndecidability.Halt_SR]
domino [definition, in PCPUndecidability.Halt_MPCP]
Drules [definition, in PCPUndecidability.Halt_SR]
E
elem [definition, in PCPUndecidability.Prelim]elem_spec [lemma, in PCPUndecidability.Prelim]
enum [projection, in PCPUndecidability.Prelim]
enum_ok [projection, in PCPUndecidability.Prelim]
# [notation, in PCPUndecidability.SR_RSR]
epsilon_srs.esig [variable, in PCPUndecidability.SR_RSR]
epsilon_srs [section, in PCPUndecidability.SR_RSR]
eqType [record, in PCPUndecidability.Prelim]
EqType [constructor, in PCPUndecidability.Prelim]
eqType_CS [definition, in PCPUndecidability.Prelim]
eqType_dec [projection, in PCPUndecidability.Prelim]
eqType_X [projection, in PCPUndecidability.Prelim]
eq_dec_sig [instance, in PCPUndecidability.SR_RSR]
eq_dec_psig [instance, in PCPUndecidability.Halt_MPCP]
eq_dec_states [instance, in PCPUndecidability.Halt_MPCP]
eq_dec_sig [instance, in PCPUndecidability.Halt_MPCP]
eq_dec_conf [instance, in PCPUndecidability.Single_TM]
eq_dec_tape [instance, in PCPUndecidability.Single_TM]
eq_dec_sig [instance, in PCPUndecidability.Single_TM]
eq_dec_rsig [instance, in PCPUndecidability.Halt_SR]
eq_dec_rsig' [instance, in PCPUndecidability.Halt_SR]
eq_dec_states [instance, in PCPUndecidability.Halt_SR]
esig_list_pair_sig [definition, in PCPUndecidability.SR_RSR]
esig_sig [definition, in PCPUndecidability.SR_RSR]
F
fcard [definition, in PCPUndecidability.SR_MPCP]finType [record, in PCPUndecidability.Prelim]
FinType [constructor, in PCPUndecidability.Prelim]
finTypeC [record, in PCPUndecidability.Prelim]
FinTypeC [constructor, in PCPUndecidability.Prelim]
finType_CS [definition, in PCPUndecidability.Prelim]
FinType_sig [definition, in PCPUndecidability.SR_RSR]
finType_rsig [instance, in PCPUndecidability.Halt_SR]
finType_rsig' [instance, in PCPUndecidability.Halt_SR]
fin_rewrite_nil [lemma, in PCPUndecidability.Halt_SR]
firstD [definition, in PCPUndecidability.RSR_PCP]
fix_X.X [variable, in PCPUndecidability.Prelim]
fix_X [section, in PCPUndecidability.Prelim]
$ [notation, in PCPUndecidability.Halt_MPCP]
# [notation, in PCPUndecidability.Halt_MPCP]
Fix_TM.T [variable, in PCPUndecidability.Halt_MPCP]
Fix_TM.sig [variable, in PCPUndecidability.Halt_MPCP]
_ nel _ [notation, in PCPUndecidability.Halt_MPCP]
Fix_TM [section, in PCPUndecidability.Halt_MPCP]
Fix_Sigma.sig [variable, in PCPUndecidability.Single_TM]
Fix_Sigma [section, in PCPUndecidability.Single_TM]
Fix_TM.abstract_epsilon.fin [variable, in PCPUndecidability.Halt_SR]
Fix_TM.abstract_epsilon.gam [variable, in PCPUndecidability.Halt_SR]
Fix_TM.abstract_epsilon [section, in PCPUndecidability.Halt_SR]
$ [notation, in PCPUndecidability.Halt_SR]
# [notation, in PCPUndecidability.Halt_SR]
Fix_TM.T [variable, in PCPUndecidability.Halt_SR]
Fix_TM.sig [variable, in PCPUndecidability.Halt_SR]
Fix_TM [section, in PCPUndecidability.Halt_SR]
G
get_mpcp_solution [definition, in PCPUndecidability.MPCP_PCP]get_type_5_element [lemma, in PCPUndecidability.Halt_MPCP]
get_type_2_sig [definition, in PCPUndecidability.Halt_MPCP]
get_type_5_final [definition, in PCPUndecidability.Halt_MPCP]
get_type_4_blank_r [definition, in PCPUndecidability.Halt_MPCP]
get_type_4_blank_l [definition, in PCPUndecidability.Halt_MPCP]
get_type_4_sig_r [definition, in PCPUndecidability.Halt_MPCP]
get_type_4_sig_l [definition, in PCPUndecidability.Halt_MPCP]
get_rule_fin [definition, in PCPUndecidability.Halt_SR]
get_rule_r [definition, in PCPUndecidability.Halt_SR]
get_rule_l [definition, in PCPUndecidability.Halt_SR]
get_rules_el_TMrules [lemma, in PCPUndecidability.Halt_SR]
get_rules [definition, in PCPUndecidability.Halt_SR]
get_rules_right [definition, in PCPUndecidability.Halt_SR]
get_rules_left [definition, in PCPUndecidability.Halt_SR]
H
Halt [definition, in PCPUndecidability.Single_TM]halt [projection, in PCPUndecidability.Single_TM]
HaltD [definition, in PCPUndecidability.Single_TM]
HaltD' [definition, in PCPUndecidability.Single_TM]
halting [lemma, in PCPUndecidability.Halt_SR]
halting_states_false [lemma, in PCPUndecidability.Halt_MPCP]
halting_states [definition, in PCPUndecidability.Halt_MPCP]
halting_states [definition, in PCPUndecidability.Halt_SR]
Halt_SR_MPCP_PCP_reduction [lemma, in PCPUndecidability.PCP_undecidability]
Halt_SR_RSR_PCP_reduction [lemma, in PCPUndecidability.PCP_undecidability]
Halt_MPCP_PCP_reduction [lemma, in PCPUndecidability.PCP_undecidability]
halt_iff_rewriting [lemma, in PCPUndecidability.Halt_SR]
Halt_SR [library]
Halt_MPCP [library]
hash [constructor, in PCPUndecidability.SR_MPCP]
hash [constructor, in PCPUndecidability.SR_RSR]
hash [constructor, in PCPUndecidability.MPCP_PCP]
hash [constructor, in PCPUndecidability.Halt_MPCP]
hash [constructor, in PCPUndecidability.RSR_PCP]
hash [constructor, in PCPUndecidability.Halt_SR]
hash_right_inj [lemma, in PCPUndecidability.SR_RSR]
hash_hash_right [lemma, in PCPUndecidability.SR_RSR]
hash_left [definition, in PCPUndecidability.SR_RSR]
hash_right [definition, in PCPUndecidability.SR_RSR]
hash_trans_left_inv [lemma, in PCPUndecidability.MPCP_PCP]
hash_trans_right_inv [lemma, in PCPUndecidability.MPCP_PCP]
hash_hash_left [lemma, in PCPUndecidability.MPCP_PCP]
hash_hash_right [lemma, in PCPUndecidability.MPCP_PCP]
hash_equal_hash [lemma, in PCPUndecidability.MPCP_PCP]
hash_list [definition, in PCPUndecidability.MPCP_PCP]
hash_left [definition, in PCPUndecidability.MPCP_PCP]
hash_right [definition, in PCPUndecidability.MPCP_PCP]
hash_y_nil [lemma, in PCPUndecidability.RSR_PCP]
hd_modified_pcp [lemma, in PCPUndecidability.MPCP_PCP]
I
incl_nil [lemma, in PCPUndecidability.Prelim]inductive_count [lemma, in PCPUndecidability.Prelim]
initc [definition, in PCPUndecidability.Single_TM]
Injective [definition, in PCPUndecidability.Prelim]
inj_sigma [lemma, in PCPUndecidability.SR_MPCP]
in_count_app [lemma, in PCPUndecidability.Prelim]
in_concat_iff [lemma, in PCPUndecidability.Prelim]
in_sing [lemma, in PCPUndecidability.Prelim]
L
L [constructor, in PCPUndecidability.Single_TM]lastD [definition, in PCPUndecidability.RSR_PCP]
lastD_equal_symbols [lemma, in PCPUndecidability.RSR_PCP]
lastD_false [lemma, in PCPUndecidability.RSR_PCP]
last_app_eq [lemma, in PCPUndecidability.Prelim]
lcard [definition, in PCPUndecidability.SR_MPCP]
Left [constructor, in PCPUndecidability.RSR_PCP]
left [definition, in PCPUndecidability.Single_TM]
leftof [constructor, in PCPUndecidability.Single_TM]
leftof_domino_config_element [lemma, in PCPUndecidability.Halt_MPCP]
left_some [definition, in PCPUndecidability.Halt_MPCP]
left_none_some [definition, in PCPUndecidability.Halt_MPCP]
left_none_none [definition, in PCPUndecidability.Halt_MPCP]
left_right_in_dominos [lemma, in PCPUndecidability.RSR_PCP]
list_eq_dec [instance, in PCPUndecidability.Prelim]
loop [definition, in PCPUndecidability.Single_TM]
loopM [definition, in PCPUndecidability.Single_TM]
loop_step_not [lemma, in PCPUndecidability.Single_TM]
lsig_lsig' [definition, in PCPUndecidability.MPCP_PCP]
M
make_domino_config_not_nil [lemma, in PCPUndecidability.Halt_MPCP]make_domino_config_element [lemma, in PCPUndecidability.Halt_MPCP]
make_domino_config [definition, in PCPUndecidability.Halt_MPCP]
make_midtape_domino_config [definition, in PCPUndecidability.Halt_MPCP]
make_rightof_domino_config [definition, in PCPUndecidability.Halt_MPCP]
make_niltape_domino_config [definition, in PCPUndecidability.Halt_MPCP]
make_leftof_domino_config [definition, in PCPUndecidability.Halt_MPCP]
map_inj [lemma, in PCPUndecidability.Prelim]
map_LR_in_dominos [lemma, in PCPUndecidability.RSR_PCP]
map_RL_in_dominos [lemma, in PCPUndecidability.RSR_PCP]
map_symb_sigma [lemma, in PCPUndecidability.Halt_SR]
mconfig [record, in PCPUndecidability.Single_TM]
mconfig_pconfig [definition, in PCPUndecidability.Halt_MPCP]
midtape [constructor, in PCPUndecidability.Single_TM]
midtape_domino_config_element [lemma, in PCPUndecidability.Halt_MPCP]
midtape_state [lemma, in PCPUndecidability.Halt_SR]
mkdomino_snd [lemma, in PCPUndecidability.Halt_MPCP]
mkdomino_fst [lemma, in PCPUndecidability.Halt_MPCP]
mk_mconfig [constructor, in PCPUndecidability.Single_TM]
mk_tape [definition, in PCPUndecidability.Single_TM]
mk_srconf_not_nil [lemma, in PCPUndecidability.Halt_SR]
mk_srconf_inj [lemma, in PCPUndecidability.Halt_SR]
mk_srconf [definition, in PCPUndecidability.Halt_SR]
move [inductive, in PCPUndecidability.Single_TM]
move_hash [lemma, in PCPUndecidability.SR_RSR]
move_finC [instance, in PCPUndecidability.Single_TM]
move_eq_dec [instance, in PCPUndecidability.Single_TM]
MPCP [definition, in PCPUndecidability.PCP]
mpcp [definition, in PCPUndecidability.PCP]
MPCPD [definition, in PCPUndecidability.PCP]
mpcp_solution_then_sr [lemma, in PCPUndecidability.SR_MPCP]
mpcp_rewriting [lemma, in PCPUndecidability.SR_MPCP]
mpcp_solution_subset [lemma, in PCPUndecidability.MPCP_PCP]
mpcp_pcp [lemma, in PCPUndecidability.MPCP_PCP]
mpcp_to_pcp_instance [definition, in PCPUndecidability.MPCP_PCP]
mpcp_to_pcp [definition, in PCPUndecidability.MPCP_PCP]
$ [notation, in PCPUndecidability.MPCP_PCP]
# [notation, in PCPUndecidability.MPCP_PCP]
MPCP_PCP_Reduction.sig' [variable, in PCPUndecidability.MPCP_PCP]
MPCP_PCP_Reduction [section, in PCPUndecidability.MPCP_PCP]
MPCP_solution_TM_Halt [lemma, in PCPUndecidability.Halt_MPCP]
MPCP_instance [definition, in PCPUndecidability.Halt_MPCP]
MPCP_PCP [library]
N
N [constructor, in PCPUndecidability.Single_TM]next_cards_solution_list [lemma, in PCPUndecidability.Halt_MPCP]
next_cards_midtape [lemma, in PCPUndecidability.Halt_MPCP]
next_cards_rightof [lemma, in PCPUndecidability.Halt_MPCP]
next_sigma_dominoes_right [lemma, in PCPUndecidability.Halt_MPCP]
next_cards_leftof [lemma, in PCPUndecidability.Halt_MPCP]
next_sigma_dominoes_left [lemma, in PCPUndecidability.Halt_MPCP]
next_cards_niltape [lemma, in PCPUndecidability.Halt_MPCP]
next_rules_right [lemma, in PCPUndecidability.RSR_PCP]
next_rules_left [lemma, in PCPUndecidability.RSR_PCP]
next_rules_left' [lemma, in PCPUndecidability.RSR_PCP]
niltape [constructor, in PCPUndecidability.Single_TM]
niltape_domino_config_element [lemma, in PCPUndecidability.Halt_MPCP]
notInZero [lemma, in PCPUndecidability.Prelim]
not_halting [lemma, in PCPUndecidability.Halt_MPCP]
not_halting_states [definition, in PCPUndecidability.Halt_MPCP]
not_halting [lemma, in PCPUndecidability.Halt_SR]
not_halting_states [definition, in PCPUndecidability.Halt_SR]
no_nil_in_R [lemma, in PCPUndecidability.SR_RSR]
P
PCP [definition, in PCPUndecidability.PCP]pcp [definition, in PCPUndecidability.PCP]
PCP [library]
PCPD [definition, in PCPUndecidability.PCP]
PCP_undecidability [lemma, in PCPUndecidability.PCP_undecidability]
pcp_dominos [definition, in PCPUndecidability.SR_MPCP]
pcp_mpcp [lemma, in PCPUndecidability.MPCP_PCP]
pcp_mpcp_solution [lemma, in PCPUndecidability.MPCP_PCP]
pcp_rewriting [lemma, in PCPUndecidability.RSR_PCP]
pcp_first_rule [lemma, in PCPUndecidability.RSR_PCP]
pcp_dominos [definition, in PCPUndecidability.RSR_PCP]
pcp_rules_right [definition, in PCPUndecidability.RSR_PCP]
pcp_rules_left [definition, in PCPUndecidability.RSR_PCP]
pcp_dominos' [definition, in PCPUndecidability.RSR_PCP]
pcp_solution [definition, in PCPUndecidability.PCP]
pcp_definition.X [variable, in PCPUndecidability.PCP]
pcp_definition [section, in PCPUndecidability.PCP]
PCP_undecidability [library]
Prelim [library]
psig [inductive, in PCPUndecidability.SR_MPCP]
psig [inductive, in PCPUndecidability.Halt_MPCP]
psig [inductive, in PCPUndecidability.RSR_PCP]
psig' [inductive, in PCPUndecidability.RSR_PCP]
R
R [constructor, in PCPUndecidability.Single_TM]Reach [definition, in PCPUndecidability.Single_TM]
reach [inductive, in PCPUndecidability.Single_TM]
reachI [constructor, in PCPUndecidability.Single_TM]
reachS [constructor, in PCPUndecidability.Single_TM]
reach_rewrite_nil [lemma, in PCPUndecidability.Halt_SR]
reach_rewrite [lemma, in PCPUndecidability.Halt_SR]
red [definition, in PCPUndecidability.Reductions]
Reductions [library]
reduction_sr_mpcp [lemma, in PCPUndecidability.SR_MPCP]
reduction_f [definition, in PCPUndecidability.SR_MPCP]
reduction_sr_restricted_sr [lemma, in PCPUndecidability.SR_RSR]
reduction_mpcp_pcp [lemma, in PCPUndecidability.MPCP_PCP]
reduction_halt_mpcp [lemma, in PCPUndecidability.Halt_MPCP]
reduction_restricted_sr_pcp [lemma, in PCPUndecidability.RSR_PCP]
reduction_RSR_PCP [definition, in PCPUndecidability.RSR_PCP]
reduction_pcp_srs_no_epsilon [lemma, in PCPUndecidability.RSR_PCP]
reduction_string_rewriting_pcp [lemma, in PCPUndecidability.RSR_PCP]
reduction_srs_pcp [definition, in PCPUndecidability.RSR_PCP]
reduction_halt_sr [lemma, in PCPUndecidability.Halt_SR]
reduction_reach_sr [lemma, in PCPUndecidability.Halt_SR]
reduction_reach_rewrite [definition, in PCPUndecidability.Halt_SR]
red_trans [lemma, in PCPUndecidability.Reductions]
red' [definition, in PCPUndecidability.RSR_PCP]
remove_hash [lemma, in PCPUndecidability.SR_RSR]
remove_map_snd [lemma, in PCPUndecidability.Halt_MPCP]
remove_map_fst [lemma, in PCPUndecidability.Halt_MPCP]
replace_nil [definition, in PCPUndecidability.SR_RSR]
rev_nil [lemma, in PCPUndecidability.Prelim]
rev_eq [lemma, in PCPUndecidability.Prelim]
rew [inductive, in PCPUndecidability.String_rewriting]
rewR [constructor, in PCPUndecidability.String_rewriting]
rewrite_app [lemma, in PCPUndecidability.String_rewriting]
rewrite_solution [lemma, in PCPUndecidability.SR_MPCP]
rewrite_exists_pcp_list [lemma, in PCPUndecidability.SR_MPCP]
rewrite_SR_iff_rewrite_RSR [lemma, in PCPUndecidability.SR_RSR]
rewrite_exists_pcp_list [lemma, in PCPUndecidability.RSR_PCP]
rewrite_nil [lemma, in PCPUndecidability.Halt_SR]
rewrite_drules [lemma, in PCPUndecidability.Halt_SR]
rewrite_step_halt [lemma, in PCPUndecidability.Halt_SR]
rewrite_step_conf [lemma, in PCPUndecidability.Halt_SR]
rewt [inductive, in PCPUndecidability.String_rewriting]
rewtRefl [constructor, in PCPUndecidability.String_rewriting]
rewtRule [constructor, in PCPUndecidability.String_rewriting]
rewtTrans [lemma, in PCPUndecidability.String_rewriting]
rew_delRules_halt [lemma, in PCPUndecidability.Halt_SR]
Right [constructor, in PCPUndecidability.RSR_PCP]
right [definition, in PCPUndecidability.Single_TM]
rightof [constructor, in PCPUndecidability.Single_TM]
rightof_domino_config_element [lemma, in PCPUndecidability.Halt_MPCP]
right_some [definition, in PCPUndecidability.Halt_MPCP]
right_none_some [definition, in PCPUndecidability.Halt_MPCP]
right_none_none [definition, in PCPUndecidability.Halt_MPCP]
right_left_in_dominos [lemma, in PCPUndecidability.RSR_PCP]
rsig [inductive, in PCPUndecidability.Halt_SR]
rsig_finType [definition, in PCPUndecidability.Halt_SR]
rsig' [inductive, in PCPUndecidability.Halt_SR]
RSR [definition, in PCPUndecidability.String_rewriting]
RSR_PCP [library]
rule [definition, in PCPUndecidability.String_rewriting]
rule_takes_symbol_right [lemma, in PCPUndecidability.RSR_PCP]
rule_takes_symbol_left [lemma, in PCPUndecidability.RSR_PCP]
rule_RL_in_dominos [lemma, in PCPUndecidability.RSR_PCP]
rule_LR_in_dominos [lemma, in PCPUndecidability.RSR_PCP]
S
shift_hash_right [lemma, in PCPUndecidability.SR_RSR]shift_trans_lsig'_lists [lemma, in PCPUndecidability.MPCP_PCP]
shift_list_trans_lsig [lemma, in PCPUndecidability.MPCP_PCP]
sig [inductive, in PCPUndecidability.SR_RSR]
sig [inductive, in PCPUndecidability.MPCP_PCP]
sigma [constructor, in PCPUndecidability.SR_MPCP]
sigma [constructor, in PCPUndecidability.SR_RSR]
sigma [constructor, in PCPUndecidability.MPCP_PCP]
sigma [constructor, in PCPUndecidability.RSR_PCP]
sigma [constructor, in PCPUndecidability.Halt_SR]
sigma_hash_equal [lemma, in PCPUndecidability.SR_MPCP]
sigma_no_solution [lemma, in PCPUndecidability.MPCP_PCP]
sigma_psig_pair_list_lr [definition, in PCPUndecidability.RSR_PCP]
sigma_psig_lr [definition, in PCPUndecidability.RSR_PCP]
sig_psig [definition, in PCPUndecidability.SR_MPCP]
sig_finType [definition, in PCPUndecidability.SR_RSR]
Single_TM [library]
sizeOfTape [definition, in PCPUndecidability.Single_TM]
size_induction [lemma, in PCPUndecidability.Prelim]
solution [definition, in PCPUndecidability.PCP]
solution_trans_pcp [lemma, in PCPUndecidability.MPCP_PCP]
solution_subset [lemma, in PCPUndecidability.MPCP_PCP]
solution_Halt [lemma, in PCPUndecidability.Halt_MPCP]
split_sigma [lemma, in PCPUndecidability.SR_MPCP]
split_sig_psig [lemma, in PCPUndecidability.SR_MPCP]
split_map_snd_RL [lemma, in PCPUndecidability.RSR_PCP]
split_map_snd_LR [lemma, in PCPUndecidability.RSR_PCP]
split_map_fst_RL [lemma, in PCPUndecidability.RSR_PCP]
split_map_fst_LR [lemma, in PCPUndecidability.RSR_PCP]
SR [definition, in PCPUndecidability.String_rewriting]
srs [definition, in PCPUndecidability.String_rewriting]
srs_no_epsilon_reduction [definition, in PCPUndecidability.SR_RSR]
# [notation, in PCPUndecidability.RSR_PCP]
$ [notation, in PCPUndecidability.RSR_PCP]
srs_pcp.sig [variable, in PCPUndecidability.RSR_PCP]
srs_pcp [section, in PCPUndecidability.RSR_PCP]
sr_then_pcp_solution [lemma, in PCPUndecidability.SR_MPCP]
$ [notation, in PCPUndecidability.SR_MPCP]
# [notation, in PCPUndecidability.SR_MPCP]
sr_mpcp_reduction.sig [variable, in PCPUndecidability.SR_MPCP]
sr_mpcp_reduction [section, in PCPUndecidability.SR_MPCP]
SR_MPCP [library]
SR_RSR [library]
start [projection, in PCPUndecidability.Single_TM]
state [constructor, in PCPUndecidability.Halt_MPCP]
state [constructor, in PCPUndecidability.Halt_SR]
states [projection, in PCPUndecidability.Single_TM]
state_eqlist [lemma, in PCPUndecidability.Halt_SR]
state_not_sym [lemma, in PCPUndecidability.Halt_SR]
state_count_one [lemma, in PCPUndecidability.Halt_SR]
stay_some [definition, in PCPUndecidability.Halt_MPCP]
stay_none_some [definition, in PCPUndecidability.Halt_MPCP]
stay_none_none [definition, in PCPUndecidability.Halt_MPCP]
step [definition, in PCPUndecidability.Single_TM]
sTM [record, in PCPUndecidability.Single_TM]
string_rewriting.sig [variable, in PCPUndecidability.String_rewriting]
string_rewriting [section, in PCPUndecidability.String_rewriting]
String_rewriting [library]
subset_rewriting [lemma, in PCPUndecidability.String_rewriting]
sym [constructor, in PCPUndecidability.Halt_MPCP]
sym [definition, in PCPUndecidability.Halt_SR]
symb [constructor, in PCPUndecidability.Halt_SR]
symb_count_one [lemma, in PCPUndecidability.Halt_SR]
sym_inj [lemma, in PCPUndecidability.Halt_SR]
T
tagL [definition, in PCPUndecidability.RSR_PCP]tagR [definition, in PCPUndecidability.RSR_PCP]
tape [inductive, in PCPUndecidability.Single_TM]
tapeToList [definition, in PCPUndecidability.Single_TM]
tape_move_mono [definition, in PCPUndecidability.Single_TM]
tape_write [definition, in PCPUndecidability.Single_TM]
tape_move [definition, in PCPUndecidability.Single_TM]
tape_move_left [definition, in PCPUndecidability.Single_TM]
tape_move_right [definition, in PCPUndecidability.Single_TM]
TMdominoes [definition, in PCPUndecidability.Halt_MPCP]
TMrules [definition, in PCPUndecidability.Halt_SR]
TMterminates [definition, in PCPUndecidability.Single_TM]
TM_Halt_MPCP_solution [lemma, in PCPUndecidability.Halt_MPCP]
TM_Halt_solution [lemma, in PCPUndecidability.Halt_MPCP]
TM_terminates_Halt [lemma, in PCPUndecidability.Single_TM]
tm_srs_reduction [definition, in PCPUndecidability.Halt_SR]
trans [projection, in PCPUndecidability.Single_TM]
trans_pcp_pcp' [definition, in PCPUndecidability.MPCP_PCP]
trans_pair_sig'_sig [definition, in PCPUndecidability.MPCP_PCP]
trans_lsig'_lsig [definition, in PCPUndecidability.MPCP_PCP]
trans_sig'_sig [definition, in PCPUndecidability.MPCP_PCP]
trans_mpcp_pcp [definition, in PCPUndecidability.PCP]
type [projection, in PCPUndecidability.Prelim]
type_4_blank_l_element [lemma, in PCPUndecidability.Halt_MPCP]
type_4_blank_r_element [lemma, in PCPUndecidability.Halt_MPCP]
type_4_left_sig_element [lemma, in PCPUndecidability.Halt_MPCP]
type_4_right_sig_element [lemma, in PCPUndecidability.Halt_MPCP]
type_2_sig_element [lemma, in PCPUndecidability.Halt_MPCP]
type_2_hash_element [lemma, in PCPUndecidability.Halt_MPCP]
type_5_final_pair [definition, in PCPUndecidability.Halt_MPCP]
type_4_del_right [definition, in PCPUndecidability.Halt_MPCP]
type_4_del_left [definition, in PCPUndecidability.Halt_MPCP]
type_3_transitions [definition, in PCPUndecidability.Halt_MPCP]
type_3_transitions_some [definition, in PCPUndecidability.Halt_MPCP]
type_3_transitions_none [definition, in PCPUndecidability.Halt_MPCP]
type_2_hash [definition, in PCPUndecidability.Halt_MPCP]
type_2_copy [definition, in PCPUndecidability.Halt_MPCP]
type_1_first_card [definition, in PCPUndecidability.Halt_MPCP]
U
undecidable [definition, in PCPUndecidability.Reductions]other
_ <<= _ [notation, in PCPUndecidability.Prelim]_ el _ [notation, in PCPUndecidability.Prelim]
eq_dec _ [notation, in PCPUndecidability.Prelim]
| _ | [notation, in PCPUndecidability.Prelim]
Notation Index
E
# [in PCPUndecidability.SR_RSR]F
$ [in PCPUndecidability.Halt_MPCP]# [in PCPUndecidability.Halt_MPCP]
_ nel _ [in PCPUndecidability.Halt_MPCP]
$ [in PCPUndecidability.Halt_SR]
# [in PCPUndecidability.Halt_SR]
M
$ [in PCPUndecidability.MPCP_PCP]# [in PCPUndecidability.MPCP_PCP]
S
# [in PCPUndecidability.RSR_PCP]$ [in PCPUndecidability.RSR_PCP]
$ [in PCPUndecidability.SR_MPCP]
# [in PCPUndecidability.SR_MPCP]
other
_ <<= _ [in PCPUndecidability.Prelim]_ el _ [in PCPUndecidability.Prelim]
eq_dec _ [in PCPUndecidability.Prelim]
| _ | [in PCPUndecidability.Prelim]
Variable Index
E
epsilon_srs.esig [in PCPUndecidability.SR_RSR]F
fix_X.X [in PCPUndecidability.Prelim]Fix_TM.T [in PCPUndecidability.Halt_MPCP]
Fix_TM.sig [in PCPUndecidability.Halt_MPCP]
Fix_Sigma.sig [in PCPUndecidability.Single_TM]
Fix_TM.abstract_epsilon.fin [in PCPUndecidability.Halt_SR]
Fix_TM.abstract_epsilon.gam [in PCPUndecidability.Halt_SR]
Fix_TM.T [in PCPUndecidability.Halt_SR]
Fix_TM.sig [in PCPUndecidability.Halt_SR]
M
MPCP_PCP_Reduction.sig' [in PCPUndecidability.MPCP_PCP]P
pcp_definition.X [in PCPUndecidability.PCP]S
srs_pcp.sig [in PCPUndecidability.RSR_PCP]sr_mpcp_reduction.sig [in PCPUndecidability.SR_MPCP]
string_rewriting.sig [in PCPUndecidability.String_rewriting]
Library Index
H
Halt_SRHalt_MPCP
M
MPCP_PCPP
PCPPCP_undecidability
Prelim
R
ReductionsRSR_PCP
S
Single_TMSR_MPCP
SR_RSR
String_rewriting
Lemma Index
C
concat_map_snd_copy [in PCPUndecidability.SR_MPCP]concat_map_fst_copy [in PCPUndecidability.SR_MPCP]
concat_pcp_lsig_snd [in PCPUndecidability.MPCP_PCP]
concat_pcp_lsig_fst [in PCPUndecidability.MPCP_PCP]
concat_del_dominos_snd [in PCPUndecidability.MPCP_PCP]
concat_del_dominos_fst [in PCPUndecidability.MPCP_PCP]
concat_hash_right [in PCPUndecidability.MPCP_PCP]
concat_hash_left [in PCPUndecidability.MPCP_PCP]
copy_string_el [in PCPUndecidability.SR_MPCP]
countIn [in PCPUndecidability.Prelim]
countSplit [in PCPUndecidability.Prelim]
D
delete_fin [in PCPUndecidability.Halt_SR]delete_list_left [in PCPUndecidability.Halt_SR]
delete_list_right [in PCPUndecidability.Halt_SR]
deletion_dominoes [in PCPUndecidability.Halt_MPCP]
deletion_dominoes_left [in PCPUndecidability.Halt_MPCP]
deletion_dominoes_right [in PCPUndecidability.Halt_MPCP]
del_rule_fin_el [in PCPUndecidability.Halt_SR]
del_rule_l_el [in PCPUndecidability.Halt_SR]
del_rule_r_el [in PCPUndecidability.Halt_SR]
diff_constructors_count_zero [in PCPUndecidability.Prelim]
E
elem_spec [in PCPUndecidability.Prelim]F
fin_rewrite_nil [in PCPUndecidability.Halt_SR]G
get_type_5_element [in PCPUndecidability.Halt_MPCP]get_rules_el_TMrules [in PCPUndecidability.Halt_SR]
H
halting [in PCPUndecidability.Halt_SR]halting_states_false [in PCPUndecidability.Halt_MPCP]
Halt_SR_MPCP_PCP_reduction [in PCPUndecidability.PCP_undecidability]
Halt_SR_RSR_PCP_reduction [in PCPUndecidability.PCP_undecidability]
Halt_MPCP_PCP_reduction [in PCPUndecidability.PCP_undecidability]
halt_iff_rewriting [in PCPUndecidability.Halt_SR]
hash_right_inj [in PCPUndecidability.SR_RSR]
hash_hash_right [in PCPUndecidability.SR_RSR]
hash_trans_left_inv [in PCPUndecidability.MPCP_PCP]
hash_trans_right_inv [in PCPUndecidability.MPCP_PCP]
hash_hash_left [in PCPUndecidability.MPCP_PCP]
hash_hash_right [in PCPUndecidability.MPCP_PCP]
hash_equal_hash [in PCPUndecidability.MPCP_PCP]
hash_y_nil [in PCPUndecidability.RSR_PCP]
hd_modified_pcp [in PCPUndecidability.MPCP_PCP]
I
incl_nil [in PCPUndecidability.Prelim]inductive_count [in PCPUndecidability.Prelim]
inj_sigma [in PCPUndecidability.SR_MPCP]
in_count_app [in PCPUndecidability.Prelim]
in_concat_iff [in PCPUndecidability.Prelim]
in_sing [in PCPUndecidability.Prelim]
L
lastD_equal_symbols [in PCPUndecidability.RSR_PCP]lastD_false [in PCPUndecidability.RSR_PCP]
last_app_eq [in PCPUndecidability.Prelim]
leftof_domino_config_element [in PCPUndecidability.Halt_MPCP]
left_right_in_dominos [in PCPUndecidability.RSR_PCP]
loop_step_not [in PCPUndecidability.Single_TM]
M
make_domino_config_not_nil [in PCPUndecidability.Halt_MPCP]make_domino_config_element [in PCPUndecidability.Halt_MPCP]
map_inj [in PCPUndecidability.Prelim]
map_LR_in_dominos [in PCPUndecidability.RSR_PCP]
map_RL_in_dominos [in PCPUndecidability.RSR_PCP]
map_symb_sigma [in PCPUndecidability.Halt_SR]
midtape_domino_config_element [in PCPUndecidability.Halt_MPCP]
midtape_state [in PCPUndecidability.Halt_SR]
mkdomino_snd [in PCPUndecidability.Halt_MPCP]
mkdomino_fst [in PCPUndecidability.Halt_MPCP]
mk_srconf_not_nil [in PCPUndecidability.Halt_SR]
mk_srconf_inj [in PCPUndecidability.Halt_SR]
move_hash [in PCPUndecidability.SR_RSR]
mpcp_solution_then_sr [in PCPUndecidability.SR_MPCP]
mpcp_rewriting [in PCPUndecidability.SR_MPCP]
mpcp_solution_subset [in PCPUndecidability.MPCP_PCP]
mpcp_pcp [in PCPUndecidability.MPCP_PCP]
MPCP_solution_TM_Halt [in PCPUndecidability.Halt_MPCP]
N
next_cards_solution_list [in PCPUndecidability.Halt_MPCP]next_cards_midtape [in PCPUndecidability.Halt_MPCP]
next_cards_rightof [in PCPUndecidability.Halt_MPCP]
next_sigma_dominoes_right [in PCPUndecidability.Halt_MPCP]
next_cards_leftof [in PCPUndecidability.Halt_MPCP]
next_sigma_dominoes_left [in PCPUndecidability.Halt_MPCP]
next_cards_niltape [in PCPUndecidability.Halt_MPCP]
next_rules_right [in PCPUndecidability.RSR_PCP]
next_rules_left [in PCPUndecidability.RSR_PCP]
next_rules_left' [in PCPUndecidability.RSR_PCP]
niltape_domino_config_element [in PCPUndecidability.Halt_MPCP]
notInZero [in PCPUndecidability.Prelim]
not_halting [in PCPUndecidability.Halt_MPCP]
not_halting [in PCPUndecidability.Halt_SR]
no_nil_in_R [in PCPUndecidability.SR_RSR]
P
PCP_undecidability [in PCPUndecidability.PCP_undecidability]pcp_mpcp [in PCPUndecidability.MPCP_PCP]
pcp_mpcp_solution [in PCPUndecidability.MPCP_PCP]
pcp_rewriting [in PCPUndecidability.RSR_PCP]
pcp_first_rule [in PCPUndecidability.RSR_PCP]
R
reach_rewrite_nil [in PCPUndecidability.Halt_SR]reach_rewrite [in PCPUndecidability.Halt_SR]
reduction_sr_mpcp [in PCPUndecidability.SR_MPCP]
reduction_sr_restricted_sr [in PCPUndecidability.SR_RSR]
reduction_mpcp_pcp [in PCPUndecidability.MPCP_PCP]
reduction_halt_mpcp [in PCPUndecidability.Halt_MPCP]
reduction_restricted_sr_pcp [in PCPUndecidability.RSR_PCP]
reduction_pcp_srs_no_epsilon [in PCPUndecidability.RSR_PCP]
reduction_string_rewriting_pcp [in PCPUndecidability.RSR_PCP]
reduction_halt_sr [in PCPUndecidability.Halt_SR]
reduction_reach_sr [in PCPUndecidability.Halt_SR]
red_trans [in PCPUndecidability.Reductions]
remove_hash [in PCPUndecidability.SR_RSR]
remove_map_snd [in PCPUndecidability.Halt_MPCP]
remove_map_fst [in PCPUndecidability.Halt_MPCP]
rev_nil [in PCPUndecidability.Prelim]
rev_eq [in PCPUndecidability.Prelim]
rewrite_app [in PCPUndecidability.String_rewriting]
rewrite_solution [in PCPUndecidability.SR_MPCP]
rewrite_exists_pcp_list [in PCPUndecidability.SR_MPCP]
rewrite_SR_iff_rewrite_RSR [in PCPUndecidability.SR_RSR]
rewrite_exists_pcp_list [in PCPUndecidability.RSR_PCP]
rewrite_nil [in PCPUndecidability.Halt_SR]
rewrite_drules [in PCPUndecidability.Halt_SR]
rewrite_step_halt [in PCPUndecidability.Halt_SR]
rewrite_step_conf [in PCPUndecidability.Halt_SR]
rewtTrans [in PCPUndecidability.String_rewriting]
rew_delRules_halt [in PCPUndecidability.Halt_SR]
rightof_domino_config_element [in PCPUndecidability.Halt_MPCP]
right_left_in_dominos [in PCPUndecidability.RSR_PCP]
rule_takes_symbol_right [in PCPUndecidability.RSR_PCP]
rule_takes_symbol_left [in PCPUndecidability.RSR_PCP]
rule_RL_in_dominos [in PCPUndecidability.RSR_PCP]
rule_LR_in_dominos [in PCPUndecidability.RSR_PCP]
S
shift_hash_right [in PCPUndecidability.SR_RSR]shift_trans_lsig'_lists [in PCPUndecidability.MPCP_PCP]
shift_list_trans_lsig [in PCPUndecidability.MPCP_PCP]
sigma_hash_equal [in PCPUndecidability.SR_MPCP]
sigma_no_solution [in PCPUndecidability.MPCP_PCP]
size_induction [in PCPUndecidability.Prelim]
solution_trans_pcp [in PCPUndecidability.MPCP_PCP]
solution_subset [in PCPUndecidability.MPCP_PCP]
solution_Halt [in PCPUndecidability.Halt_MPCP]
split_sigma [in PCPUndecidability.SR_MPCP]
split_sig_psig [in PCPUndecidability.SR_MPCP]
split_map_snd_RL [in PCPUndecidability.RSR_PCP]
split_map_snd_LR [in PCPUndecidability.RSR_PCP]
split_map_fst_RL [in PCPUndecidability.RSR_PCP]
split_map_fst_LR [in PCPUndecidability.RSR_PCP]
sr_then_pcp_solution [in PCPUndecidability.SR_MPCP]
state_eqlist [in PCPUndecidability.Halt_SR]
state_not_sym [in PCPUndecidability.Halt_SR]
state_count_one [in PCPUndecidability.Halt_SR]
subset_rewriting [in PCPUndecidability.String_rewriting]
symb_count_one [in PCPUndecidability.Halt_SR]
sym_inj [in PCPUndecidability.Halt_SR]
T
TM_Halt_MPCP_solution [in PCPUndecidability.Halt_MPCP]TM_Halt_solution [in PCPUndecidability.Halt_MPCP]
TM_terminates_Halt [in PCPUndecidability.Single_TM]
type_4_blank_l_element [in PCPUndecidability.Halt_MPCP]
type_4_blank_r_element [in PCPUndecidability.Halt_MPCP]
type_4_left_sig_element [in PCPUndecidability.Halt_MPCP]
type_4_right_sig_element [in PCPUndecidability.Halt_MPCP]
type_2_sig_element [in PCPUndecidability.Halt_MPCP]
type_2_hash_element [in PCPUndecidability.Halt_MPCP]
Constructor Index
B
blank [in PCPUndecidability.Halt_MPCP]D
dollar [in PCPUndecidability.SR_MPCP]dollar [in PCPUndecidability.MPCP_PCP]
dollar [in PCPUndecidability.Halt_MPCP]
dollar [in PCPUndecidability.RSR_PCP]
dollar [in PCPUndecidability.Halt_SR]
E
EqType [in PCPUndecidability.Prelim]F
FinType [in PCPUndecidability.Prelim]FinTypeC [in PCPUndecidability.Prelim]
H
hash [in PCPUndecidability.SR_MPCP]hash [in PCPUndecidability.SR_RSR]
hash [in PCPUndecidability.MPCP_PCP]
hash [in PCPUndecidability.Halt_MPCP]
hash [in PCPUndecidability.RSR_PCP]
hash [in PCPUndecidability.Halt_SR]
L
L [in PCPUndecidability.Single_TM]Left [in PCPUndecidability.RSR_PCP]
leftof [in PCPUndecidability.Single_TM]
M
midtape [in PCPUndecidability.Single_TM]mk_mconfig [in PCPUndecidability.Single_TM]
N
N [in PCPUndecidability.Single_TM]niltape [in PCPUndecidability.Single_TM]
R
R [in PCPUndecidability.Single_TM]reachI [in PCPUndecidability.Single_TM]
reachS [in PCPUndecidability.Single_TM]
rewR [in PCPUndecidability.String_rewriting]
rewtRefl [in PCPUndecidability.String_rewriting]
rewtRule [in PCPUndecidability.String_rewriting]
Right [in PCPUndecidability.RSR_PCP]
rightof [in PCPUndecidability.Single_TM]
S
sigma [in PCPUndecidability.SR_MPCP]sigma [in PCPUndecidability.SR_RSR]
sigma [in PCPUndecidability.MPCP_PCP]
sigma [in PCPUndecidability.RSR_PCP]
sigma [in PCPUndecidability.Halt_SR]
state [in PCPUndecidability.Halt_MPCP]
state [in PCPUndecidability.Halt_SR]
sym [in PCPUndecidability.Halt_MPCP]
symb [in PCPUndecidability.Halt_SR]
Projection Index
C
class [in PCPUndecidability.Prelim]cstate [in PCPUndecidability.Single_TM]
ctape [in PCPUndecidability.Single_TM]
E
enum [in PCPUndecidability.Prelim]enum_ok [in PCPUndecidability.Prelim]
eqType_dec [in PCPUndecidability.Prelim]
eqType_X [in PCPUndecidability.Prelim]
H
halt [in PCPUndecidability.Single_TM]S
start [in PCPUndecidability.Single_TM]states [in PCPUndecidability.Single_TM]
T
trans [in PCPUndecidability.Single_TM]type [in PCPUndecidability.Prelim]
Inductive Index
M
move [in PCPUndecidability.Single_TM]P
psig [in PCPUndecidability.SR_MPCP]psig [in PCPUndecidability.Halt_MPCP]
psig [in PCPUndecidability.RSR_PCP]
psig' [in PCPUndecidability.RSR_PCP]
R
reach [in PCPUndecidability.Single_TM]rew [in PCPUndecidability.String_rewriting]
rewt [in PCPUndecidability.String_rewriting]
rsig [in PCPUndecidability.Halt_SR]
rsig' [in PCPUndecidability.Halt_SR]
S
sig [in PCPUndecidability.SR_RSR]sig [in PCPUndecidability.MPCP_PCP]
T
tape [in PCPUndecidability.Single_TM]Section Index
E
epsilon_srs [in PCPUndecidability.SR_RSR]F
fix_X [in PCPUndecidability.Prelim]Fix_TM [in PCPUndecidability.Halt_MPCP]
Fix_Sigma [in PCPUndecidability.Single_TM]
Fix_TM.abstract_epsilon [in PCPUndecidability.Halt_SR]
Fix_TM [in PCPUndecidability.Halt_SR]
M
MPCP_PCP_Reduction [in PCPUndecidability.MPCP_PCP]P
pcp_definition [in PCPUndecidability.PCP]S
srs_pcp [in PCPUndecidability.RSR_PCP]sr_mpcp_reduction [in PCPUndecidability.SR_MPCP]
string_rewriting [in PCPUndecidability.String_rewriting]
Instance Index
E
eq_dec_sig [in PCPUndecidability.SR_RSR]eq_dec_psig [in PCPUndecidability.Halt_MPCP]
eq_dec_states [in PCPUndecidability.Halt_MPCP]
eq_dec_sig [in PCPUndecidability.Halt_MPCP]
eq_dec_conf [in PCPUndecidability.Single_TM]
eq_dec_tape [in PCPUndecidability.Single_TM]
eq_dec_sig [in PCPUndecidability.Single_TM]
eq_dec_rsig [in PCPUndecidability.Halt_SR]
eq_dec_rsig' [in PCPUndecidability.Halt_SR]
eq_dec_states [in PCPUndecidability.Halt_SR]
F
finType_rsig [in PCPUndecidability.Halt_SR]finType_rsig' [in PCPUndecidability.Halt_SR]
L
list_eq_dec [in PCPUndecidability.Prelim]M
move_finC [in PCPUndecidability.Single_TM]move_eq_dec [in PCPUndecidability.Single_TM]
Definition Index
C
conf [in PCPUndecidability.Halt_MPCP]conf [in PCPUndecidability.Halt_SR]
copy_string [in PCPUndecidability.SR_MPCP]
count [in PCPUndecidability.Prelim]
current [in PCPUndecidability.Single_TM]
D
Dec [in PCPUndecidability.Prelim]dec [in PCPUndecidability.Prelim]
dec2bool [in PCPUndecidability.Prelim]
delRules [in PCPUndecidability.Halt_SR]
del_empty_dominos [in PCPUndecidability.MPCP_PCP]
del_rules_fin [in PCPUndecidability.Halt_SR]
del_rules_r [in PCPUndecidability.Halt_SR]
del_rules_l [in PCPUndecidability.Halt_SR]
domino [in PCPUndecidability.Halt_MPCP]
Drules [in PCPUndecidability.Halt_SR]
E
elem [in PCPUndecidability.Prelim]eqType_CS [in PCPUndecidability.Prelim]
esig_list_pair_sig [in PCPUndecidability.SR_RSR]
esig_sig [in PCPUndecidability.SR_RSR]
F
fcard [in PCPUndecidability.SR_MPCP]finType_CS [in PCPUndecidability.Prelim]
FinType_sig [in PCPUndecidability.SR_RSR]
firstD [in PCPUndecidability.RSR_PCP]
G
get_mpcp_solution [in PCPUndecidability.MPCP_PCP]get_type_2_sig [in PCPUndecidability.Halt_MPCP]
get_type_5_final [in PCPUndecidability.Halt_MPCP]
get_type_4_blank_r [in PCPUndecidability.Halt_MPCP]
get_type_4_blank_l [in PCPUndecidability.Halt_MPCP]
get_type_4_sig_r [in PCPUndecidability.Halt_MPCP]
get_type_4_sig_l [in PCPUndecidability.Halt_MPCP]
get_rule_fin [in PCPUndecidability.Halt_SR]
get_rule_r [in PCPUndecidability.Halt_SR]
get_rule_l [in PCPUndecidability.Halt_SR]
get_rules [in PCPUndecidability.Halt_SR]
get_rules_right [in PCPUndecidability.Halt_SR]
get_rules_left [in PCPUndecidability.Halt_SR]
H
Halt [in PCPUndecidability.Single_TM]HaltD [in PCPUndecidability.Single_TM]
HaltD' [in PCPUndecidability.Single_TM]
halting_states [in PCPUndecidability.Halt_MPCP]
halting_states [in PCPUndecidability.Halt_SR]
hash_left [in PCPUndecidability.SR_RSR]
hash_right [in PCPUndecidability.SR_RSR]
hash_list [in PCPUndecidability.MPCP_PCP]
hash_left [in PCPUndecidability.MPCP_PCP]
hash_right [in PCPUndecidability.MPCP_PCP]
I
initc [in PCPUndecidability.Single_TM]Injective [in PCPUndecidability.Prelim]
L
lastD [in PCPUndecidability.RSR_PCP]lcard [in PCPUndecidability.SR_MPCP]
left [in PCPUndecidability.Single_TM]
left_some [in PCPUndecidability.Halt_MPCP]
left_none_some [in PCPUndecidability.Halt_MPCP]
left_none_none [in PCPUndecidability.Halt_MPCP]
loop [in PCPUndecidability.Single_TM]
loopM [in PCPUndecidability.Single_TM]
lsig_lsig' [in PCPUndecidability.MPCP_PCP]
M
make_domino_config [in PCPUndecidability.Halt_MPCP]make_midtape_domino_config [in PCPUndecidability.Halt_MPCP]
make_rightof_domino_config [in PCPUndecidability.Halt_MPCP]
make_niltape_domino_config [in PCPUndecidability.Halt_MPCP]
make_leftof_domino_config [in PCPUndecidability.Halt_MPCP]
mconfig_pconfig [in PCPUndecidability.Halt_MPCP]
mk_tape [in PCPUndecidability.Single_TM]
mk_srconf [in PCPUndecidability.Halt_SR]
MPCP [in PCPUndecidability.PCP]
mpcp [in PCPUndecidability.PCP]
MPCPD [in PCPUndecidability.PCP]
mpcp_to_pcp_instance [in PCPUndecidability.MPCP_PCP]
mpcp_to_pcp [in PCPUndecidability.MPCP_PCP]
MPCP_instance [in PCPUndecidability.Halt_MPCP]
N
not_halting_states [in PCPUndecidability.Halt_MPCP]not_halting_states [in PCPUndecidability.Halt_SR]
P
PCP [in PCPUndecidability.PCP]pcp [in PCPUndecidability.PCP]
PCPD [in PCPUndecidability.PCP]
pcp_dominos [in PCPUndecidability.SR_MPCP]
pcp_dominos [in PCPUndecidability.RSR_PCP]
pcp_rules_right [in PCPUndecidability.RSR_PCP]
pcp_rules_left [in PCPUndecidability.RSR_PCP]
pcp_dominos' [in PCPUndecidability.RSR_PCP]
pcp_solution [in PCPUndecidability.PCP]
R
Reach [in PCPUndecidability.Single_TM]red [in PCPUndecidability.Reductions]
reduction_f [in PCPUndecidability.SR_MPCP]
reduction_RSR_PCP [in PCPUndecidability.RSR_PCP]
reduction_srs_pcp [in PCPUndecidability.RSR_PCP]
reduction_reach_rewrite [in PCPUndecidability.Halt_SR]
red' [in PCPUndecidability.RSR_PCP]
replace_nil [in PCPUndecidability.SR_RSR]
right [in PCPUndecidability.Single_TM]
right_some [in PCPUndecidability.Halt_MPCP]
right_none_some [in PCPUndecidability.Halt_MPCP]
right_none_none [in PCPUndecidability.Halt_MPCP]
rsig_finType [in PCPUndecidability.Halt_SR]
RSR [in PCPUndecidability.String_rewriting]
rule [in PCPUndecidability.String_rewriting]
S
sigma_psig_pair_list_lr [in PCPUndecidability.RSR_PCP]sigma_psig_lr [in PCPUndecidability.RSR_PCP]
sig_psig [in PCPUndecidability.SR_MPCP]
sig_finType [in PCPUndecidability.SR_RSR]
sizeOfTape [in PCPUndecidability.Single_TM]
solution [in PCPUndecidability.PCP]
SR [in PCPUndecidability.String_rewriting]
srs [in PCPUndecidability.String_rewriting]
srs_no_epsilon_reduction [in PCPUndecidability.SR_RSR]
stay_some [in PCPUndecidability.Halt_MPCP]
stay_none_some [in PCPUndecidability.Halt_MPCP]
stay_none_none [in PCPUndecidability.Halt_MPCP]
step [in PCPUndecidability.Single_TM]
sym [in PCPUndecidability.Halt_SR]
T
tagL [in PCPUndecidability.RSR_PCP]tagR [in PCPUndecidability.RSR_PCP]
tapeToList [in PCPUndecidability.Single_TM]
tape_move_mono [in PCPUndecidability.Single_TM]
tape_write [in PCPUndecidability.Single_TM]
tape_move [in PCPUndecidability.Single_TM]
tape_move_left [in PCPUndecidability.Single_TM]
tape_move_right [in PCPUndecidability.Single_TM]
TMdominoes [in PCPUndecidability.Halt_MPCP]
TMrules [in PCPUndecidability.Halt_SR]
TMterminates [in PCPUndecidability.Single_TM]
tm_srs_reduction [in PCPUndecidability.Halt_SR]
trans_pcp_pcp' [in PCPUndecidability.MPCP_PCP]
trans_pair_sig'_sig [in PCPUndecidability.MPCP_PCP]
trans_lsig'_lsig [in PCPUndecidability.MPCP_PCP]
trans_sig'_sig [in PCPUndecidability.MPCP_PCP]
trans_mpcp_pcp [in PCPUndecidability.PCP]
type_5_final_pair [in PCPUndecidability.Halt_MPCP]
type_4_del_right [in PCPUndecidability.Halt_MPCP]
type_4_del_left [in PCPUndecidability.Halt_MPCP]
type_3_transitions [in PCPUndecidability.Halt_MPCP]
type_3_transitions_some [in PCPUndecidability.Halt_MPCP]
type_3_transitions_none [in PCPUndecidability.Halt_MPCP]
type_2_hash [in PCPUndecidability.Halt_MPCP]
type_2_copy [in PCPUndecidability.Halt_MPCP]
type_1_first_card [in PCPUndecidability.Halt_MPCP]
U
undecidable [in PCPUndecidability.Reductions]Record Index
E
eqType [in PCPUndecidability.Prelim]F
finType [in PCPUndecidability.Prelim]finTypeC [in PCPUndecidability.Prelim]
M
mconfig [in PCPUndecidability.Single_TM]S
sTM [in PCPUndecidability.Single_TM]| 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 | (430 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 | (16 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 | (14 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 | (12 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 | (155 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 | (39 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) |
| 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 | (13 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 | (11 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 | (15 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 | (138 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 | (5 entries) |