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_PCP## P

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) |