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 | (331 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 | (18 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 | (16 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 | (9 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 | (123 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 | (24 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 | (9 entries) |

Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (12 entries) |

Instance Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (14 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 | (9 entries) |

Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (2 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 | (90 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

## A

app_incl_R [lemma, in Prelim]app_incl_l [lemma, in Prelim]

## C

card [definition, in Definitions]cards [definition, in Definitions]

cards_subset [lemma, in SR_MPCP]

CFI [definition, in Definitions]

CFP [definition, in Definitions]

class [projection, in singleTM]

conf [definition, in TM_SRH]

cons_incl [lemma, in Prelim]

count [definition, in singleTM]

countIn [lemma, in singleTM]

countSplit [lemma, in singleTM]

cstate [projection, in singleTM]

ctape [projection, in singleTM]

current [definition, in singleTM]

## D

d [definition, in MPCP_PCP]d [definition, in SR_MPCP]

Dec [definition, in singleTM]

dec [definition, in singleTM]

dec2bool [definition, in singleTM]

Definitions [library]

diff_constructors_count_zero [lemma, in TM_SRH]

dollar [constructor, in TM_SRH]

dollar [definition, in MPCP_PCP]

dollar [definition, in SR_MPCP]

doll_hash_L [lemma, in MPCP_PCP]

doll_sig [lemma, in SR_MPCP]

## E

e [definition, in MPCP_PCP]e [definition, in SR_MPCP]

elem [definition, in singleTM]

elem_spec [lemma, in singleTM]

enum [projection, in singleTM]

enum_ok [projection, in singleTM]

eqType [record, in singleTM]

EqType [constructor, in singleTM]

eqType_CS [definition, in singleTM]

eqType_dec [projection, in singleTM]

eqType_X [projection, in singleTM]

equi [lemma, in SRH_SR]

eq_dec_conf [instance, in singleTM]

eq_dec_tape [instance, in singleTM]

eq_dec_sig [instance, in singleTM]

eq_dec_rsig [instance, in TM_SRH]

eq_dec_rsig' [instance, in TM_SRH]

eq_dec_states [instance, in TM_SRH]

## F

finType [record, in singleTM]FinType [constructor, in singleTM]

finTypeC [record, in singleTM]

FinTypeC [constructor, in singleTM]

finType_CS [definition, in singleTM]

finType_rsig [instance, in TM_SRH]

finType_rsig' [instance, in TM_SRH]

Fix_Sigma.sig [variable, in singleTM]

Fix_Sigma [section, in singleTM]

$ [notation, in TM_SRH]

# [notation, in TM_SRH]

Fix_TM.T [variable, in TM_SRH]

Fix_TM.sig [variable, in TM_SRH]

Fix_TM [section, in TM_SRH]

fix_X.X [variable, in Prelim]

fix_X [section, in Prelim]

fresh [definition, in Definitions]

fresh_spec [lemma, in Definitions]

fresh_spec' [lemma, in Definitions]

## G

gamma [definition, in PCP_CFI]gamma [definition, in PCP_CFP]

gamma_inj [lemma, in PCP_CFI]

gamma_mono [lemma, in PCP_CFP]

gamma_invol [lemma, in PCP_CFP]

gamma1 [definition, in PCP_CFI]

gamma1_spec [lemma, in PCP_CFI]

gamma2 [definition, in PCP_CFI]

gamma2_spec [lemma, in PCP_CFI]

get_rules_el_TMrules [lemma, in TM_SRH]

get_rules [definition, in TM_SRH]

get_rules_right [definition, in TM_SRH]

get_rules_left [definition, in TM_SRH]

## H

Halt [definition, in singleTM]halt [projection, in singleTM]

halting [lemma, in TM_SRH]

halting_states [definition, in TM_SRH]

Halt_SRH [lemma, in TM_SRH]

halt_SRH' [lemma, in TM_SRH]

Halt' [definition, in singleTM]

hash [constructor, in TM_SRH]

hash [definition, in MPCP_PCP]

hash [definition, in SR_MPCP]

hash_R_inv [lemma, in MPCP_PCP]

hash_L_diff [lemma, in MPCP_PCP]

hash_R_app [lemma, in MPCP_PCP]

hash_L_app [lemma, in MPCP_PCP]

hash_swap [lemma, in MPCP_PCP]

hash_r [definition, in MPCP_PCP]

hash_l [definition, in MPCP_PCP]

hash_sig [lemma, in SR_MPCP]

## I

incl_sing [lemma, in Prelim]incl_nil [lemma, in Prelim]

index [definition, in singleTM]

inductive_count [lemma, in TM_SRH]

initc [definition, in singleTM]

Injective [definition, in Prelim]

inj_index [lemma, in singleTM]

in_concat_iff [lemma, in TM_SRH]

in_sing [lemma, in TM_SRH]

in_split [lemma, in Definitions]

is_cons_true_iff [lemma, in MPCP_PCP]

is_cons [definition, in MPCP_PCP]

## L

L [constructor, in singleTM]last_app_eq [lemma, in Prelim]

left [definition, in singleTM]

leftof [constructor, in singleTM]

list_eq_dec [instance, in singleTM]

list_prefix_inv [lemma, in Definitions]

loop [definition, in singleTM]

loopM [definition, in singleTM]

loop_step_not [lemma, in singleTM]

## M

main [lemma, in PCP_CFP]map_app_inv [lemma, in singleTM]

map_symb_sigma [lemma, in TM_SRH]

map_inj [lemma, in Prelim]

match_start [lemma, in MPCP_PCP]

mconfig [record, in singleTM]

midtape [constructor, in singleTM]

midtape_state [lemma, in TM_SRH]

mk_mconfig [constructor, in singleTM]

mk_tape [definition, in singleTM]

mk_srconf_state [lemma, in TM_SRH]

mk_srconf_inj [lemma, in TM_SRH]

mk_srconf [definition, in TM_SRH]

move [inductive, in singleTM]

move_finC [instance, in singleTM]

move_eq_dec [instance, in singleTM]

MPCP [definition, in Definitions]

MPCP_PCP_cor [lemma, in MPCP_PCP]

MPCP_PCP [lemma, in MPCP_PCP]

#_R [notation, in MPCP_PCP]

#_L [notation, in MPCP_PCP]

# [notation, in MPCP_PCP]

$ [notation, in MPCP_PCP]

MPCP_PCP.y0 [variable, in MPCP_PCP]

MPCP_PCP.x0 [variable, in MPCP_PCP]

MPCP_PCP.R [variable, in MPCP_PCP]

MPCP_PCP [section, in MPCP_PCP]

MPCP_SR [lemma, in SR_MPCP]

MPCP_PCP [library]

## N

N [constructor, in singleTM]niltape [constructor, in singleTM]

notInZero [lemma, in TM_SRH]

not_halting [lemma, in TM_SRH]

not_halting_states [definition, in TM_SRH]

nrewt_ind_left [lemma, in TM_SRH]

## P

P [definition, in MPCP_PCP]P [definition, in SR_MPCP]

P [definition, in SRH_SR]

palin [definition, in PCP_CFP]

PCP [definition, in Definitions]

# [notation, in PCP_CFI]

PCP_CFI.P [variable, in PCP_CFI]

PCP_CFI [section, in PCP_CFI]

PCP_MPCP [lemma, in MPCP_PCP]

PCP_CFP [lemma, in PCP_CFP]

# [notation, in PCP_CFP]

PCP_CFP.P [variable, in PCP_CFP]

PCP_CFP [section, in PCP_CFP]

PCP_CFI [library]

PCP_CFP [library]

pos [definition, in singleTM]

pos_inj [lemma, in singleTM]

pos_el [definition, in singleTM]

pos_nth [lemma, in singleTM]

pos_length [lemma, in singleTM]

pos_el' [definition, in singleTM]

Prelim [library]

PreOrder_rewt [instance, in Definitions]

Proper_rewt [instance, in Definitions]

P_inv_bot [lemma, in MPCP_PCP]

P_inv_top [lemma, in MPCP_PCP]

P_inv [lemma, in MPCP_PCP]

P_inv [lemma, in SR_MPCP]

## R

R [constructor, in singleTM]Reach [definition, in singleTM]

reach [inductive, in singleTM]

reachI [constructor, in singleTM]

reachS [constructor, in singleTM]

reach_rewrite [lemma, in TM_SRH]

reduces [definition, in Definitions]

reduces_transitive [lemma, in Definitions]

reduction [lemma, in TM_SRH]

reduction [lemma, in PCP_CFI]

reduction [lemma, in MPCP_PCP]

reduction [lemma, in SR_MPCP]

reduction [lemma, in SRH_SR]

reduction_reach_sr [lemma, in TM_SRH]

reduction_reach_rewrite [definition, in TM_SRH]

red_rewt [lemma, in TM_SRH]

red_rew [lemma, in TM_SRH]

rev_nil [lemma, in Prelim]

rev_eq [lemma, in Prelim]

rew [inductive, in Definitions]

rewB [constructor, in Definitions]

rewR [constructor, in TM_SRH]

rewR [constructor, in Definitions]

rewrite_steps_halt [lemma, in TM_SRH]

rewrite_step_halt [lemma, in TM_SRH]

rewrite_step_conf [lemma, in TM_SRH]

rewrite_right [lemma, in TM_SRH]

rewrite_app [lemma, in TM_SRH]

rewS [constructor, in Definitions]

rewt [inductive, in Definitions]

rewt_R_fresh [lemma, in TM_SRH]

rewt_inv [lemma, in TM_SRH]

rewt_sym [lemma, in Definitions]

rewt_left [lemma, in Definitions]

rewt_subset [lemma, in Definitions]

rewt_app_L [lemma, in Definitions]

rewt_ind' [definition, in Definitions]

rewt_induct [lemma, in Definitions]

rewt_a0_R [lemma, in SRH_SR]

rewt_a0_L [lemma, in SRH_SR]

rewt' [inductive, in TM_SRH]

rewt'Refl [constructor, in TM_SRH]

rewt'Rule [constructor, in TM_SRH]

rewt'Trans [instance, in TM_SRH]

rewt'_ind_left [lemma, in TM_SRH]

rew_inv [lemma, in TM_SRH]

rew_subset [lemma, in SR_MPCP]

rew' [inductive, in TM_SRH]

right [definition, in singleTM]

rightof [constructor, in singleTM]

rsig [inductive, in TM_SRH]

rsig_finType [definition, in TM_SRH]

rsig' [inductive, in TM_SRH]

rule [definition, in TM_SRH]

R_Sigma [definition, in MPCP_PCP]

## S

sep_doll [lemma, in SR_MPCP]sigma [constructor, in TM_SRH]

Sigma [definition, in PCP_CFI]

Sigma [definition, in MPCP_PCP]

sigma [definition, in Definitions]

Sigma [abbreviation, in SR_MPCP]

Sigma [abbreviation, in SRH_SR]

Sigma [definition, in PCP_CFP]

sigma_gamma2 [lemma, in PCP_CFI]

sigma_gamma1 [lemma, in PCP_CFI]

sigma_gamma [lemma, in PCP_CFP]

sing [definition, in Definitions]

singleTM [library]

sizeOfTape [definition, in singleTM]

size_induction [lemma, in Prelim]

split_inv [lemma, in Definitions]

SR [definition, in Definitions]

SRH [definition, in Definitions]

SRH_SR.a0 [variable, in SRH_SR]

SRH_SR.x0 [variable, in SRH_SR]

SRH_SR.R [variable, in SRH_SR]

SRH_SR [section, in SRH_SR]

SRH_SR [library]

SRH' [definition, in TM_SRH]

SRH'_SRH [lemma, in TM_SRH]

srs [definition, in TM_SRH]

SRS [definition, in Definitions]

SR_fin [definition, in TM_SRH]

SR_MPCP_cor [lemma, in SR_MPCP]

SR_MPCP [lemma, in SR_MPCP]

# [notation, in SR_MPCP]

$ [notation, in SR_MPCP]

_ ≻* _ [notation, in SR_MPCP]

_ ≻ _ [notation, in SR_MPCP]

SR_to_MPCP.y0 [variable, in SR_MPCP]

SR_to_MPCP.x0 [variable, in SR_MPCP]

SR_to_MPCP.R [variable, in SR_MPCP]

SR_to_MPCP [section, in SR_MPCP]

SR_SRH [lemma, in SRH_SR]

SR_MPCP [library]

stack [definition, in Definitions]

start [projection, in singleTM]

state [constructor, in TM_SRH]

states [projection, in singleTM]

state_eqlist [lemma, in TM_SRH]

state_not_sym [lemma, in TM_SRH]

state_count_one [lemma, in TM_SRH]

step [definition, in singleTM]

sTM [record, in singleTM]

string [definition, in Definitions]

string_rewriting.sig [variable, in TM_SRH]

string_rewriting [section, in TM_SRH]

subset_rewriting [lemma, in TM_SRH]

sym [definition, in TM_SRH]

sym [definition, in Definitions]

symb [constructor, in TM_SRH]

symbol [definition, in Definitions]

symb_count_one [lemma, in TM_SRH]

sym_inj [lemma, in TM_SRH]

sym_mono [lemma, in Definitions]

sym_word_R [lemma, in Definitions]

sym_word_l [lemma, in Definitions]

sym_map [lemma, in Definitions]

sym_app [lemma, in Definitions]

sym_P [lemma, in SRH_SR]

## T

tape [inductive, in singleTM]tapeToList [definition, in singleTM]

tape_move_mono [definition, in singleTM]

tape_write [definition, in singleTM]

tape_move [definition, in singleTM]

tape_move_left [definition, in singleTM]

tape_move_right [definition, in singleTM]

tau1 [definition, in Definitions]

tau1_inv [lemma, in MPCP_PCP]

tau1_sym [lemma, in Definitions]

tau1_cards [lemma, in Definitions]

tau1_app [lemma, in Definitions]

tau2 [definition, in Definitions]

tau2_inv [lemma, in MPCP_PCP]

tau2_sym [lemma, in Definitions]

tau2_cards [lemma, in Definitions]

tau2_app [lemma, in Definitions]

TMrules [definition, in TM_SRH]

TMterminates [definition, in singleTM]

TM_terminates_Halt [lemma, in singleTM]

TM_SRH [library]

trans [projection, in singleTM]

trans_R [definition, in TM_SRH]

type [projection, in singleTM]

## X

x_rewt_a0 [lemma, in SRH_SR]## other

_ / _ [notation, in Definitions]_ ⪯ _ [notation, in Definitions]

_ <<= _ [notation, in Prelim]

_ el _ [notation, in Prelim]

eq_dec _ [notation, in singleTM]

| _ | [notation, in Prelim]

# Notation Index

## F

$ [in TM_SRH]# [in TM_SRH]

## M

#_R [in MPCP_PCP]#_L [in MPCP_PCP]

# [in MPCP_PCP]

$ [in MPCP_PCP]

## P

# [in PCP_CFI]# [in PCP_CFP]

## S

# [in SR_MPCP]$ [in SR_MPCP]

_ ≻* _ [in SR_MPCP]

_ ≻ _ [in SR_MPCP]

## other

_ / _ [in Definitions]_ ⪯ _ [in Definitions]

_ <<= _ [in Prelim]

_ el _ [in Prelim]

eq_dec _ [in singleTM]

| _ | [in Prelim]

# Variable Index

## F

Fix_Sigma.sig [in singleTM]Fix_TM.T [in TM_SRH]

Fix_TM.sig [in TM_SRH]

fix_X.X [in Prelim]

## M

MPCP_PCP.y0 [in MPCP_PCP]MPCP_PCP.x0 [in MPCP_PCP]

MPCP_PCP.R [in MPCP_PCP]

## P

PCP_CFI.P [in PCP_CFI]PCP_CFP.P [in PCP_CFP]

## S

SRH_SR.a0 [in SRH_SR]SRH_SR.x0 [in SRH_SR]

SRH_SR.R [in SRH_SR]

SR_to_MPCP.y0 [in SR_MPCP]

SR_to_MPCP.x0 [in SR_MPCP]

SR_to_MPCP.R [in SR_MPCP]

string_rewriting.sig [in TM_SRH]

# Library Index

## D

Definitions## M

MPCP_PCP## P

PCP_CFIPCP_CFP

Prelim

## S

singleTMSRH_SR

SR_MPCP

## T

TM_SRH# Lemma Index

## A

app_incl_R [in Prelim]app_incl_l [in Prelim]

## C

cards_subset [in SR_MPCP]cons_incl [in Prelim]

countIn [in singleTM]

countSplit [in singleTM]

## D

diff_constructors_count_zero [in TM_SRH]doll_hash_L [in MPCP_PCP]

doll_sig [in SR_MPCP]

## E

elem_spec [in singleTM]equi [in SRH_SR]

## F

fresh_spec [in Definitions]fresh_spec' [in Definitions]

## G

gamma_inj [in PCP_CFI]gamma_mono [in PCP_CFP]

gamma_invol [in PCP_CFP]

gamma1_spec [in PCP_CFI]

gamma2_spec [in PCP_CFI]

get_rules_el_TMrules [in TM_SRH]

## H

halting [in TM_SRH]Halt_SRH [in TM_SRH]

halt_SRH' [in TM_SRH]

hash_R_inv [in MPCP_PCP]

hash_L_diff [in MPCP_PCP]

hash_R_app [in MPCP_PCP]

hash_L_app [in MPCP_PCP]

hash_swap [in MPCP_PCP]

hash_sig [in SR_MPCP]

## I

incl_sing [in Prelim]incl_nil [in Prelim]

inductive_count [in TM_SRH]

inj_index [in singleTM]

in_concat_iff [in TM_SRH]

in_sing [in TM_SRH]

in_split [in Definitions]

is_cons_true_iff [in MPCP_PCP]

## L

last_app_eq [in Prelim]list_prefix_inv [in Definitions]

loop_step_not [in singleTM]

## M

main [in PCP_CFP]map_app_inv [in singleTM]

map_symb_sigma [in TM_SRH]

map_inj [in Prelim]

match_start [in MPCP_PCP]

midtape_state [in TM_SRH]

mk_srconf_state [in TM_SRH]

mk_srconf_inj [in TM_SRH]

MPCP_PCP_cor [in MPCP_PCP]

MPCP_PCP [in MPCP_PCP]

MPCP_SR [in SR_MPCP]

## N

notInZero [in TM_SRH]not_halting [in TM_SRH]

nrewt_ind_left [in TM_SRH]

## P

PCP_MPCP [in MPCP_PCP]PCP_CFP [in PCP_CFP]

pos_inj [in singleTM]

pos_nth [in singleTM]

pos_length [in singleTM]

P_inv_bot [in MPCP_PCP]

P_inv_top [in MPCP_PCP]

P_inv [in MPCP_PCP]

P_inv [in SR_MPCP]

## R

reach_rewrite [in TM_SRH]reduces_transitive [in Definitions]

reduction [in TM_SRH]

reduction [in PCP_CFI]

reduction [in MPCP_PCP]

reduction [in SR_MPCP]

reduction [in SRH_SR]

reduction_reach_sr [in TM_SRH]

red_rewt [in TM_SRH]

red_rew [in TM_SRH]

rev_nil [in Prelim]

rev_eq [in Prelim]

rewrite_steps_halt [in TM_SRH]

rewrite_step_halt [in TM_SRH]

rewrite_step_conf [in TM_SRH]

rewrite_right [in TM_SRH]

rewrite_app [in TM_SRH]

rewt_R_fresh [in TM_SRH]

rewt_inv [in TM_SRH]

rewt_sym [in Definitions]

rewt_left [in Definitions]

rewt_subset [in Definitions]

rewt_app_L [in Definitions]

rewt_induct [in Definitions]

rewt_a0_R [in SRH_SR]

rewt_a0_L [in SRH_SR]

rewt'_ind_left [in TM_SRH]

rew_inv [in TM_SRH]

rew_subset [in SR_MPCP]

## S

sep_doll [in SR_MPCP]sigma_gamma2 [in PCP_CFI]

sigma_gamma1 [in PCP_CFI]

sigma_gamma [in PCP_CFP]

size_induction [in Prelim]

split_inv [in Definitions]

SRH'_SRH [in TM_SRH]

SR_MPCP_cor [in SR_MPCP]

SR_MPCP [in SR_MPCP]

SR_SRH [in SRH_SR]

state_eqlist [in TM_SRH]

state_not_sym [in TM_SRH]

state_count_one [in TM_SRH]

subset_rewriting [in TM_SRH]

symb_count_one [in TM_SRH]

sym_inj [in TM_SRH]

sym_mono [in Definitions]

sym_word_R [in Definitions]

sym_word_l [in Definitions]

sym_map [in Definitions]

sym_app [in Definitions]

sym_P [in SRH_SR]

## T

tau1_inv [in MPCP_PCP]tau1_sym [in Definitions]

tau1_cards [in Definitions]

tau1_app [in Definitions]

tau2_inv [in MPCP_PCP]

tau2_sym [in Definitions]

tau2_cards [in Definitions]

tau2_app [in Definitions]

TM_terminates_Halt [in singleTM]

## X

x_rewt_a0 [in SRH_SR]# Constructor Index

## D

dollar [in TM_SRH]## E

EqType [in singleTM]## F

FinType [in singleTM]FinTypeC [in singleTM]

## H

hash [in TM_SRH]## L

L [in singleTM]leftof [in singleTM]

## M

midtape [in singleTM]mk_mconfig [in singleTM]

## N

N [in singleTM]niltape [in singleTM]

## R

R [in singleTM]reachI [in singleTM]

reachS [in singleTM]

rewB [in Definitions]

rewR [in TM_SRH]

rewR [in Definitions]

rewS [in Definitions]

rewt'Refl [in TM_SRH]

rewt'Rule [in TM_SRH]

rightof [in singleTM]

## S

sigma [in TM_SRH]state [in TM_SRH]

symb [in TM_SRH]

# Inductive Index

## M

move [in singleTM]## R

reach [in singleTM]rew [in Definitions]

rewt [in Definitions]

rewt' [in TM_SRH]

rew' [in TM_SRH]

rsig [in TM_SRH]

rsig' [in TM_SRH]

## T

tape [in singleTM]# Projection Index

## C

class [in singleTM]cstate [in singleTM]

ctape [in singleTM]

## E

enum [in singleTM]enum_ok [in singleTM]

eqType_dec [in singleTM]

eqType_X [in singleTM]

## H

halt [in singleTM]## S

start [in singleTM]states [in singleTM]

## T

trans [in singleTM]type [in singleTM]

# Instance Index

## E

eq_dec_conf [in singleTM]eq_dec_tape [in singleTM]

eq_dec_sig [in singleTM]

eq_dec_rsig [in TM_SRH]

eq_dec_rsig' [in TM_SRH]

eq_dec_states [in TM_SRH]

## F

finType_rsig [in TM_SRH]finType_rsig' [in TM_SRH]

## L

list_eq_dec [in singleTM]## M

move_finC [in singleTM]move_eq_dec [in singleTM]

## P

PreOrder_rewt [in Definitions]Proper_rewt [in Definitions]

## R

rewt'Trans [in TM_SRH]# Section Index

## F

Fix_Sigma [in singleTM]Fix_TM [in TM_SRH]

fix_X [in Prelim]

## M

MPCP_PCP [in MPCP_PCP]## P

PCP_CFI [in PCP_CFI]PCP_CFP [in PCP_CFP]

## S

SRH_SR [in SRH_SR]SR_to_MPCP [in SR_MPCP]

string_rewriting [in TM_SRH]

# Abbreviation Index

## S

Sigma [in SR_MPCP]Sigma [in SRH_SR]

# Definition Index

## C

card [in Definitions]cards [in Definitions]

CFI [in Definitions]

CFP [in Definitions]

conf [in TM_SRH]

count [in singleTM]

current [in singleTM]

## D

d [in MPCP_PCP]d [in SR_MPCP]

Dec [in singleTM]

dec [in singleTM]

dec2bool [in singleTM]

dollar [in MPCP_PCP]

dollar [in SR_MPCP]

## E

e [in MPCP_PCP]e [in SR_MPCP]

elem [in singleTM]

eqType_CS [in singleTM]

## F

finType_CS [in singleTM]fresh [in Definitions]

## G

gamma [in PCP_CFI]gamma [in PCP_CFP]

gamma1 [in PCP_CFI]

gamma2 [in PCP_CFI]

get_rules [in TM_SRH]

get_rules_right [in TM_SRH]

get_rules_left [in TM_SRH]

## H

Halt [in singleTM]halting_states [in TM_SRH]

Halt' [in singleTM]

hash [in MPCP_PCP]

hash [in SR_MPCP]

hash_r [in MPCP_PCP]

hash_l [in MPCP_PCP]

## I

index [in singleTM]initc [in singleTM]

Injective [in Prelim]

is_cons [in MPCP_PCP]

## L

left [in singleTM]loop [in singleTM]

loopM [in singleTM]

## M

mk_tape [in singleTM]mk_srconf [in TM_SRH]

MPCP [in Definitions]

## N

not_halting_states [in TM_SRH]## P

P [in MPCP_PCP]P [in SR_MPCP]

P [in SRH_SR]

palin [in PCP_CFP]

PCP [in Definitions]

pos [in singleTM]

pos_el [in singleTM]

pos_el' [in singleTM]

## R

Reach [in singleTM]reduces [in Definitions]

reduction_reach_rewrite [in TM_SRH]

rewt_ind' [in Definitions]

right [in singleTM]

rsig_finType [in TM_SRH]

rule [in TM_SRH]

R_Sigma [in MPCP_PCP]

## S

Sigma [in PCP_CFI]Sigma [in MPCP_PCP]

sigma [in Definitions]

Sigma [in PCP_CFP]

sing [in Definitions]

sizeOfTape [in singleTM]

SR [in Definitions]

SRH [in Definitions]

SRH' [in TM_SRH]

srs [in TM_SRH]

SRS [in Definitions]

SR_fin [in TM_SRH]

stack [in Definitions]

step [in singleTM]

string [in Definitions]

sym [in TM_SRH]

sym [in Definitions]

symbol [in Definitions]

## T

tapeToList [in singleTM]tape_move_mono [in singleTM]

tape_write [in singleTM]

tape_move [in singleTM]

tape_move_left [in singleTM]

tape_move_right [in singleTM]

tau1 [in Definitions]

tau2 [in Definitions]

TMrules [in TM_SRH]

TMterminates [in singleTM]

trans_R [in TM_SRH]

# Record Index

## E

eqType [in singleTM]## F

finType [in singleTM]finTypeC [in singleTM]

## M

mconfig [in singleTM]## S

sTM [in singleTM]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 | (331 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 | (18 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 | (16 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 | (9 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 | (123 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 | (24 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 | (9 entries) |

Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (12 entries) |

Instance Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (14 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 | (9 entries) |

Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (2 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 | (90 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) |