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 | (391 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 | (19 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 | (11 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 | (148 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 | (27 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 | (11 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) |

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 | (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 | (17 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 | (4 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 | (107 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 PCP.Prelim]app_incl_l [lemma, in PCP.Prelim]

## C

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

cards_subset [lemma, in PCP.SR_MPCP]

CFG [definition, in PCP.Post_CFG]

cfg [definition, in PCP.Post_CFG]

CFGs [section, in PCP.Post_CFG]

CFI [definition, in PCP.Definitions]

CFI' [definition, in PCP.Post_CFG]

CFP [definition, in PCP.Definitions]

CFP_CFI [lemma, in PCP.CFP_CFI]

CFP_CFI [library]

CFP' [definition, in PCP.Post_CFG]

class [projection, in PCP.singleTM]

conf [definition, in PCP.TM_SRH]

cons_incl [lemma, in PCP.Prelim]

count [definition, in PCP.singleTM]

count [definition, in PCP.Prelim]

countIn [lemma, in PCP.singleTM]

countSplit [lemma, in PCP.singleTM]

countSplit [lemma, in PCP.Prelim]

cstate [projection, in PCP.singleTM]

ctape [projection, in PCP.singleTM]

current [definition, in PCP.singleTM]

## D

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

Dec [definition, in PCP.singleTM]

dec [definition, in PCP.singleTM]

dec2bool [definition, in PCP.singleTM]

Definitions [library]

diff_constructors_count_zero [lemma, in PCP.TM_SRH]

dollar [constructor, in PCP.TM_SRH]

dollar [definition, in PCP.MPCP_PCP]

dollar [definition, in PCP.SR_MPCP]

doll_hash_L [lemma, in PCP.MPCP_PCP]

doll_sig [lemma, in PCP.SR_MPCP]

## E

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

elem [definition, in PCP.singleTM]

elem_spec [lemma, in PCP.singleTM]

enum [projection, in PCP.singleTM]

enum_ok [projection, in PCP.singleTM]

eqType [record, in PCP.singleTM]

EqType [constructor, in PCP.singleTM]

eqType_CS [definition, in PCP.singleTM]

eqType_dec [projection, in PCP.singleTM]

eqType_X [projection, in PCP.singleTM]

equi [lemma, in PCP.SRH_SR]

eq_dec_rsig [instance, in PCP.TM_SRH]

eq_dec_rsig' [instance, in PCP.TM_SRH]

eq_dec_states [instance, in PCP.TM_SRH]

eq_dec_conf [instance, in PCP.singleTM]

eq_dec_tape [instance, in PCP.singleTM]

eq_dec_sig [instance, in PCP.singleTM]

## F

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

finTypeC [record, in PCP.singleTM]

FinTypeC [constructor, in PCP.singleTM]

finType_rsig [instance, in PCP.TM_SRH]

finType_rsig' [instance, in PCP.TM_SRH]

finType_CS [definition, in PCP.singleTM]

$ [notation, in PCP.TM_SRH]

# [notation, in PCP.TM_SRH]

Fix_TM.T [variable, in PCP.TM_SRH]

Fix_TM.sig [variable, in PCP.TM_SRH]

Fix_TM [section, in PCP.TM_SRH]

Fix_Sigma.sig [variable, in PCP.singleTM]

Fix_Sigma [section, in PCP.singleTM]

fix_X.X [variable, in PCP.Prelim]

fix_X [section, in PCP.Prelim]

fresh [definition, in PCP.Definitions]

fresh_spec [lemma, in PCP.Definitions]

fresh_spec' [lemma, in PCP.Definitions]

## G

G [definition, in PCP.Post_CFG]gamma [definition, in PCP.PCP_CFI]

gamma [definition, in PCP.PCP_CFP]

gamma [definition, in PCP.Post_CFG]

gamma_inj [lemma, in PCP.PCP_CFI]

gamma_mono [lemma, in PCP.PCP_CFP]

gamma_invol [lemma, in PCP.PCP_CFP]

gamma1 [definition, in PCP.PCP_CFI]

gamma1_spec [lemma, in PCP.PCP_CFI]

gamma2 [definition, in PCP.PCP_CFI]

gamma2_spec [lemma, in PCP.PCP_CFI]

get_rules_el_TMrules [lemma, in PCP.TM_SRH]

get_rules [definition, in PCP.TM_SRH]

get_rules_right [definition, in PCP.TM_SRH]

get_rules_left [definition, in PCP.TM_SRH]

G_char [lemma, in PCP.CFP_CFI]

G_left [lemma, in PCP.CFP_CFI]

## H

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

halting [lemma, in PCP.TM_SRH]

halting_states [definition, in PCP.TM_SRH]

Halt_SRH [lemma, in PCP.TM_SRH]

halt_SRH' [lemma, in PCP.TM_SRH]

Halt' [definition, in PCP.singleTM]

hash [constructor, in PCP.TM_SRH]

hash [definition, in PCP.MPCP_PCP]

hash [definition, in PCP.SR_MPCP]

hash_R_inv [lemma, in PCP.MPCP_PCP]

hash_L_diff [lemma, in PCP.MPCP_PCP]

hash_R_app [lemma, in PCP.MPCP_PCP]

hash_L_app [lemma, in PCP.MPCP_PCP]

hash_swap [lemma, in PCP.MPCP_PCP]

hash_r [definition, in PCP.MPCP_PCP]

hash_l [definition, in PCP.MPCP_PCP]

hash_sig [lemma, in PCP.SR_MPCP]

## I

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

index [definition, in PCP.singleTM]

inductive_count [lemma, in PCP.TM_SRH]

initc [definition, in PCP.singleTM]

Injective [definition, in PCP.Prelim]

inj_index [lemma, in PCP.singleTM]

in_concat_iff [lemma, in PCP.TM_SRH]

in_sing [lemma, in PCP.TM_SRH]

in_split [lemma, in PCP.Definitions]

is_cons_true_iff [lemma, in PCP.MPCP_PCP]

is_cons [definition, in PCP.MPCP_PCP]

## L

L [constructor, in PCP.singleTM]L [definition, in PCP.Post_CFG]

last_app_eq [lemma, in PCP.Prelim]

left [definition, in PCP.singleTM]

leftof [constructor, in PCP.singleTM]

listI [lemma, in PCP.CFP_CFI]

list_eq_dec [instance, in PCP.singleTM]

list_prefix_inv [lemma, in PCP.Definitions]

loop [definition, in PCP.singleTM]

loopM [definition, in PCP.singleTM]

loop_step_not [lemma, in PCP.singleTM]

## M

map_symb_sigma [lemma, in PCP.TM_SRH]map_app_inv [lemma, in PCP.singleTM]

map_inj [lemma, in PCP.Prelim]

match_start [lemma, in PCP.MPCP_PCP]

mconfig [record, in PCP.singleTM]

midtape [constructor, in PCP.singleTM]

midtape_state [lemma, in PCP.TM_SRH]

mk_srconf_state [lemma, in PCP.TM_SRH]

mk_srconf_inj [lemma, in PCP.TM_SRH]

mk_srconf [definition, in PCP.TM_SRH]

mk_mconfig [constructor, in PCP.singleTM]

mk_tape [definition, in PCP.singleTM]

move [inductive, in PCP.singleTM]

move_finC [instance, in PCP.singleTM]

move_eq_dec [instance, in PCP.singleTM]

MPCP [definition, in PCP.Definitions]

MPCP_PCP_cor [lemma, in PCP.MPCP_PCP]

MPCP_PCP [lemma, in PCP.MPCP_PCP]

#_R [notation, in PCP.MPCP_PCP]

#_L [notation, in PCP.MPCP_PCP]

# [notation, in PCP.MPCP_PCP]

$ [notation, in PCP.MPCP_PCP]

MPCP_PCP.y0 [variable, in PCP.MPCP_PCP]

MPCP_PCP.x0 [variable, in PCP.MPCP_PCP]

MPCP_PCP.R [variable, in PCP.MPCP_PCP]

MPCP_PCP [section, in PCP.MPCP_PCP]

MPCP_SR [lemma, in PCP.SR_MPCP]

MPCP_PCP [library]

## N

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

nil_app_nil [lemma, in PCP.Post_CFG]

notInZero [lemma, in PCP.TM_SRH]

notInZero [lemma, in PCP.CFP_CFI]

notInZero [lemma, in PCP.Prelim]

not_halting [lemma, in PCP.TM_SRH]

not_halting_states [definition, in PCP.TM_SRH]

nrewt_ind_left [lemma, in PCP.TM_SRH]

## P

P [definition, in PCP.SRH_SR]P [definition, in PCP.MPCP_PCP]

P [definition, in PCP.SR_MPCP]

palin [definition, in PCP.PCP_CFP]

Palindrome [section, in PCP.CFP_CFI]

Palindrome.Sigma [variable, in PCP.CFP_CFI]

palin_G [definition, in PCP.CFP_CFI]

PCP [definition, in PCP.Definitions]

# [notation, in PCP.PCP_CFI]

PCP_CFI.P [variable, in PCP.PCP_CFI]

PCP_CFI [section, in PCP.PCP_CFI]

PCP_CFP [lemma, in PCP.PCP_CFP]

# [notation, in PCP.PCP_CFP]

PCP_CFP.P [variable, in PCP.PCP_CFP]

PCP_CFP [section, in PCP.PCP_CFP]

PCP_MPCP [lemma, in PCP.MPCP_PCP]

PCP_CFI [library]

PCP_CFP [library]

pos [definition, in PCP.singleTM]

Post_G [definition, in PCP.Post_CFG]

Post_CFG_2 [lemma, in PCP.Post_CFG]

Post_CFG_1' [lemma, in PCP.Post_CFG]

Post_CFG.a [variable, in PCP.Post_CFG]

Post_CFG.R [variable, in PCP.Post_CFG]

Post_CFG [section, in PCP.Post_CFG]

Post_CFG [library]

pos_inj [lemma, in PCP.singleTM]

pos_el [definition, in PCP.singleTM]

pos_nth [lemma, in PCP.singleTM]

pos_length [lemma, in PCP.singleTM]

pos_el' [definition, in PCP.singleTM]

Prelim [library]

PreOrder_rewt [instance, in PCP.Definitions]

Proper_rewt [instance, in PCP.Definitions]

P_inv_bot [lemma, in PCP.MPCP_PCP]

P_inv_top [lemma, in PCP.MPCP_PCP]

P_inv [lemma, in PCP.MPCP_PCP]

P_inv [lemma, in PCP.SR_MPCP]

## R

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

reach [inductive, in PCP.singleTM]

reachI [constructor, in PCP.singleTM]

reachS [constructor, in PCP.singleTM]

reach_rewrite [lemma, in PCP.TM_SRH]

reduces [definition, in PCP.Definitions]

reduces_transitive [lemma, in PCP.Definitions]

reduce_CFI [lemma, in PCP.Post_CFG]

reduce_CFP [lemma, in PCP.Post_CFG]

reduce_grammars [lemma, in PCP.Post_CFG]

reduction [lemma, in PCP.PCP_CFI]

reduction [lemma, in PCP.SRH_SR]

reduction [lemma, in PCP.TM_SRH]

reduction [lemma, in PCP.MPCP_PCP]

reduction [lemma, in PCP.SR_MPCP]

reduction_reach_sr [lemma, in PCP.TM_SRH]

reduction_reach_rewrite [definition, in PCP.TM_SRH]

reduction_full [lemma, in PCP.Post_CFG]

red_rewt [lemma, in PCP.TM_SRH]

red_rew [lemma, in PCP.TM_SRH]

rev_palin [lemma, in PCP.CFP_CFI]

rev_nil [lemma, in PCP.Prelim]

rev_eq [lemma, in PCP.Prelim]

rew [inductive, in PCP.Definitions]

rewB [constructor, in PCP.Definitions]

rewR [constructor, in PCP.TM_SRH]

rewR [constructor, in PCP.Post_CFG]

rewR [constructor, in PCP.Definitions]

rewrite_steps_halt [lemma, in PCP.TM_SRH]

rewrite_step_halt [lemma, in PCP.TM_SRH]

rewrite_step_conf [lemma, in PCP.TM_SRH]

rewrite_right [lemma, in PCP.TM_SRH]

rewrite_app [lemma, in PCP.TM_SRH]

rewrite_proper [instance, in PCP.Post_CFG]

rewrite_sing [lemma, in PCP.Post_CFG]

rewS [constructor, in PCP.Definitions]

rewt [inductive, in PCP.Post_CFG]

rewt [inductive, in PCP.Definitions]

rewtRefl [constructor, in PCP.Post_CFG]

rewtRule [constructor, in PCP.Post_CFG]

rewtTrans [instance, in PCP.Post_CFG]

rewt_a0_R [lemma, in PCP.SRH_SR]

rewt_a0_L [lemma, in PCP.SRH_SR]

rewt_R_fresh [lemma, in PCP.TM_SRH]

rewt_inv [lemma, in PCP.TM_SRH]

rewt_count [lemma, in PCP.Post_CFG]

rewt_sym [lemma, in PCP.Definitions]

rewt_left [lemma, in PCP.Definitions]

rewt_subset [lemma, in PCP.Definitions]

rewt_app_L [lemma, in PCP.Definitions]

rewt_ind' [definition, in PCP.Definitions]

rewt_induct [lemma, in PCP.Definitions]

rewt' [inductive, in PCP.TM_SRH]

rewt'Refl [constructor, in PCP.TM_SRH]

rewt'Rule [constructor, in PCP.TM_SRH]

rewt'Trans [instance, in PCP.TM_SRH]

rewt'_ind_left [lemma, in PCP.TM_SRH]

rew_inv [lemma, in PCP.TM_SRH]

rew_subset [lemma, in PCP.SR_MPCP]

rew_cfg [inductive, in PCP.Post_CFG]

rew' [inductive, in PCP.TM_SRH]

right [definition, in PCP.singleTM]

rightof [constructor, in PCP.singleTM]

rsig [inductive, in PCP.TM_SRH]

rsig_finType [definition, in PCP.TM_SRH]

rsig' [inductive, in PCP.TM_SRH]

rule [definition, in PCP.TM_SRH]

rule [definition, in PCP.Post_CFG]

rules [definition, in PCP.Post_CFG]

R_Sigma [definition, in PCP.MPCP_PCP]

## S

S [definition, in PCP.Post_CFG]sep_doll [lemma, in PCP.SR_MPCP]

sig [abbreviation, in PCP.Post_CFG]

Sigma [definition, in PCP.PCP_CFI]

Sigma [abbreviation, in PCP.SRH_SR]

Sigma [definition, in PCP.PCP_CFP]

sigma [constructor, in PCP.TM_SRH]

Sigma [definition, in PCP.MPCP_PCP]

Sigma [abbreviation, in PCP.SR_MPCP]

Sigma [definition, in PCP.Post_CFG]

sigma [definition, in PCP.Definitions]

sigma_gamma2 [lemma, in PCP.PCP_CFI]

sigma_gamma1 [lemma, in PCP.PCP_CFI]

sigma_gamma [lemma, in PCP.PCP_CFP]

sigma_snoc [lemma, in PCP.Post_CFG]

sigma_inv [lemma, in PCP.Post_CFG]

sigma_eq [lemma, in PCP.Post_CFG]

sing [definition, in PCP.Definitions]

singleTM [library]

sizeOfTape [definition, in PCP.singleTM]

size_induction [lemma, in PCP.Prelim]

split_inv [lemma, in PCP.Definitions]

SR [definition, in PCP.Definitions]

SRH [definition, in PCP.Definitions]

SRH_SR.a0 [variable, in PCP.SRH_SR]

SRH_SR.x0 [variable, in PCP.SRH_SR]

SRH_SR.R [variable, in PCP.SRH_SR]

SRH_SR [section, in PCP.SRH_SR]

SRH_SR [library]

SRH' [definition, in PCP.TM_SRH]

SRH'_SRH [lemma, in PCP.TM_SRH]

srs [definition, in PCP.TM_SRH]

SRS [definition, in PCP.Definitions]

SR_SRH [lemma, in PCP.SRH_SR]

SR_fin [definition, in PCP.TM_SRH]

SR_MPCP_cor [lemma, in PCP.SR_MPCP]

SR_MPCP [lemma, in PCP.SR_MPCP]

# [notation, in PCP.SR_MPCP]

$ [notation, in PCP.SR_MPCP]

_ ≻* _ [notation, in PCP.SR_MPCP]

_ ≻ _ [notation, in PCP.SR_MPCP]

SR_to_MPCP.y0 [variable, in PCP.SR_MPCP]

SR_to_MPCP.x0 [variable, in PCP.SR_MPCP]

SR_to_MPCP.R [variable, in PCP.SR_MPCP]

SR_to_MPCP [section, in PCP.SR_MPCP]

SR_MPCP [library]

stack [definition, in PCP.Definitions]

start [projection, in PCP.singleTM]

StartG [abbreviation, in PCP.CFP_CFI]

startsym [definition, in PCP.Post_CFG]

Start_fresh [lemma, in PCP.CFP_CFI]

state [constructor, in PCP.TM_SRH]

states [projection, in PCP.singleTM]

state_eqlist [lemma, in PCP.TM_SRH]

state_not_sym [lemma, in PCP.TM_SRH]

state_count_one [lemma, in PCP.TM_SRH]

step [definition, in PCP.singleTM]

sTM [record, in PCP.singleTM]

string [definition, in PCP.Definitions]

string_rewriting.sig [variable, in PCP.TM_SRH]

string_rewriting [section, in PCP.TM_SRH]

subrel [instance, in PCP.Post_CFG]

subset_rewriting [lemma, in PCP.TM_SRH]

sym [definition, in PCP.TM_SRH]

sym [definition, in PCP.Definitions]

symb [constructor, in PCP.TM_SRH]

symbol [definition, in PCP.Definitions]

symb_count_one [lemma, in PCP.TM_SRH]

sym_P [lemma, in PCP.SRH_SR]

sym_inj [lemma, in PCP.TM_SRH]

sym_G_rewt [lemma, in PCP.Post_CFG]

sym_G [definition, in PCP.Post_CFG]

sym_mono [lemma, in PCP.Definitions]

sym_word_R [lemma, in PCP.Definitions]

sym_word_l [lemma, in PCP.Definitions]

sym_map [lemma, in PCP.Definitions]

sym_app [lemma, in PCP.Definitions]

## T

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

tape_move_mono [definition, in PCP.singleTM]

tape_write [definition, in PCP.singleTM]

tape_move [definition, in PCP.singleTM]

tape_move_left [definition, in PCP.singleTM]

tape_move_right [definition, in PCP.singleTM]

tau_eq_iff [lemma, in PCP.PCP_CFP]

tau1 [definition, in PCP.Definitions]

tau1_inv [lemma, in PCP.MPCP_PCP]

tau1_sym [lemma, in PCP.Definitions]

tau1_cards [lemma, in PCP.Definitions]

tau1_app [lemma, in PCP.Definitions]

tau2 [definition, in PCP.Definitions]

tau2_inv [lemma, in PCP.MPCP_PCP]

tau2_gamma [lemma, in PCP.Post_CFG]

tau2_sym [lemma, in PCP.Definitions]

tau2_cards [lemma, in PCP.Definitions]

tau2_app [lemma, in PCP.Definitions]

terminal [definition, in PCP.Post_CFG]

terminal_iff_G [lemma, in PCP.Post_CFG]

terminal_iff [lemma, in PCP.Post_CFG]

TMrules [definition, in PCP.TM_SRH]

TMterminates [definition, in PCP.singleTM]

TM_terminates_Halt [lemma, in PCP.singleTM]

TM_SRH [library]

trans [projection, in PCP.singleTM]

trans_R [definition, in PCP.TM_SRH]

type [projection, in PCP.singleTM]

## X

x_rewt_a0 [lemma, in PCP.SRH_SR]## other

_ <<= _ [notation, in PCP.Prelim]_ el _ [notation, in PCP.Prelim]

_ / _ [notation, in PCP.Definitions]

_ ⪯ _ [notation, in PCP.Definitions]

eq_dec _ [notation, in PCP.singleTM]

| _ | [notation, in PCP.Prelim]

# Notation Index

## F

$ [in PCP.TM_SRH]# [in PCP.TM_SRH]

## M

#_R [in PCP.MPCP_PCP]#_L [in PCP.MPCP_PCP]

# [in PCP.MPCP_PCP]

$ [in PCP.MPCP_PCP]

## P

# [in PCP.PCP_CFI]# [in PCP.PCP_CFP]

## S

# [in PCP.SR_MPCP]$ [in PCP.SR_MPCP]

_ ≻* _ [in PCP.SR_MPCP]

_ ≻ _ [in PCP.SR_MPCP]

## other

_ <<= _ [in PCP.Prelim]_ el _ [in PCP.Prelim]

_ / _ [in PCP.Definitions]

_ ⪯ _ [in PCP.Definitions]

eq_dec _ [in PCP.singleTM]

| _ | [in PCP.Prelim]

# Variable Index

## F

Fix_TM.T [in PCP.TM_SRH]Fix_TM.sig [in PCP.TM_SRH]

Fix_Sigma.sig [in PCP.singleTM]

fix_X.X [in PCP.Prelim]

## M

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

MPCP_PCP.R [in PCP.MPCP_PCP]

## P

Palindrome.Sigma [in PCP.CFP_CFI]PCP_CFI.P [in PCP.PCP_CFI]

PCP_CFP.P [in PCP.PCP_CFP]

Post_CFG.a [in PCP.Post_CFG]

Post_CFG.R [in PCP.Post_CFG]

## S

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

SRH_SR.R [in PCP.SRH_SR]

SR_to_MPCP.y0 [in PCP.SR_MPCP]

SR_to_MPCP.x0 [in PCP.SR_MPCP]

SR_to_MPCP.R [in PCP.SR_MPCP]

string_rewriting.sig [in PCP.TM_SRH]

# Library Index

## C

CFP_CFI## D

Definitions## M

MPCP_PCP## P

PCP_CFIPCP_CFP

Post_CFG

Prelim

## S

singleTMSRH_SR

SR_MPCP

## T

TM_SRH# Lemma Index

## A

app_incl_R [in PCP.Prelim]app_incl_l [in PCP.Prelim]

## C

cards_subset [in PCP.SR_MPCP]CFP_CFI [in PCP.CFP_CFI]

cons_incl [in PCP.Prelim]

countIn [in PCP.singleTM]

countSplit [in PCP.singleTM]

countSplit [in PCP.Prelim]

## D

diff_constructors_count_zero [in PCP.TM_SRH]doll_hash_L [in PCP.MPCP_PCP]

doll_sig [in PCP.SR_MPCP]

## E

elem_spec [in PCP.singleTM]equi [in PCP.SRH_SR]

## F

fresh_spec [in PCP.Definitions]fresh_spec' [in PCP.Definitions]

## G

gamma_inj [in PCP.PCP_CFI]gamma_mono [in PCP.PCP_CFP]

gamma_invol [in PCP.PCP_CFP]

gamma1_spec [in PCP.PCP_CFI]

gamma2_spec [in PCP.PCP_CFI]

get_rules_el_TMrules [in PCP.TM_SRH]

G_char [in PCP.CFP_CFI]

G_left [in PCP.CFP_CFI]

## H

halting [in PCP.TM_SRH]Halt_SRH [in PCP.TM_SRH]

halt_SRH' [in PCP.TM_SRH]

hash_R_inv [in PCP.MPCP_PCP]

hash_L_diff [in PCP.MPCP_PCP]

hash_R_app [in PCP.MPCP_PCP]

hash_L_app [in PCP.MPCP_PCP]

hash_swap [in PCP.MPCP_PCP]

hash_sig [in PCP.SR_MPCP]

## I

incl_sing [in PCP.Prelim]incl_nil [in PCP.Prelim]

inductive_count [in PCP.TM_SRH]

inj_index [in PCP.singleTM]

in_concat_iff [in PCP.TM_SRH]

in_sing [in PCP.TM_SRH]

in_split [in PCP.Definitions]

is_cons_true_iff [in PCP.MPCP_PCP]

## L

last_app_eq [in PCP.Prelim]listI [in PCP.CFP_CFI]

list_prefix_inv [in PCP.Definitions]

loop_step_not [in PCP.singleTM]

## M

map_symb_sigma [in PCP.TM_SRH]map_app_inv [in PCP.singleTM]

map_inj [in PCP.Prelim]

match_start [in PCP.MPCP_PCP]

midtape_state [in PCP.TM_SRH]

mk_srconf_state [in PCP.TM_SRH]

mk_srconf_inj [in PCP.TM_SRH]

MPCP_PCP_cor [in PCP.MPCP_PCP]

MPCP_PCP [in PCP.MPCP_PCP]

MPCP_SR [in PCP.SR_MPCP]

## N

nil_app_nil [in PCP.Post_CFG]notInZero [in PCP.TM_SRH]

notInZero [in PCP.CFP_CFI]

notInZero [in PCP.Prelim]

not_halting [in PCP.TM_SRH]

nrewt_ind_left [in PCP.TM_SRH]

## P

PCP_CFP [in PCP.PCP_CFP]PCP_MPCP [in PCP.MPCP_PCP]

Post_CFG_2 [in PCP.Post_CFG]

Post_CFG_1' [in PCP.Post_CFG]

pos_inj [in PCP.singleTM]

pos_nth [in PCP.singleTM]

pos_length [in PCP.singleTM]

P_inv_bot [in PCP.MPCP_PCP]

P_inv_top [in PCP.MPCP_PCP]

P_inv [in PCP.MPCP_PCP]

P_inv [in PCP.SR_MPCP]

## R

reach_rewrite [in PCP.TM_SRH]reduces_transitive [in PCP.Definitions]

reduce_CFI [in PCP.Post_CFG]

reduce_CFP [in PCP.Post_CFG]

reduce_grammars [in PCP.Post_CFG]

reduction [in PCP.PCP_CFI]

reduction [in PCP.SRH_SR]

reduction [in PCP.TM_SRH]

reduction [in PCP.MPCP_PCP]

reduction [in PCP.SR_MPCP]

reduction_reach_sr [in PCP.TM_SRH]

reduction_full [in PCP.Post_CFG]

red_rewt [in PCP.TM_SRH]

red_rew [in PCP.TM_SRH]

rev_palin [in PCP.CFP_CFI]

rev_nil [in PCP.Prelim]

rev_eq [in PCP.Prelim]

rewrite_steps_halt [in PCP.TM_SRH]

rewrite_step_halt [in PCP.TM_SRH]

rewrite_step_conf [in PCP.TM_SRH]

rewrite_right [in PCP.TM_SRH]

rewrite_app [in PCP.TM_SRH]

rewrite_sing [in PCP.Post_CFG]

rewt_a0_R [in PCP.SRH_SR]

rewt_a0_L [in PCP.SRH_SR]

rewt_R_fresh [in PCP.TM_SRH]

rewt_inv [in PCP.TM_SRH]

rewt_count [in PCP.Post_CFG]

rewt_sym [in PCP.Definitions]

rewt_left [in PCP.Definitions]

rewt_subset [in PCP.Definitions]

rewt_app_L [in PCP.Definitions]

rewt_induct [in PCP.Definitions]

rewt'_ind_left [in PCP.TM_SRH]

rew_inv [in PCP.TM_SRH]

rew_subset [in PCP.SR_MPCP]

## S

sep_doll [in PCP.SR_MPCP]sigma_gamma2 [in PCP.PCP_CFI]

sigma_gamma1 [in PCP.PCP_CFI]

sigma_gamma [in PCP.PCP_CFP]

sigma_snoc [in PCP.Post_CFG]

sigma_inv [in PCP.Post_CFG]

sigma_eq [in PCP.Post_CFG]

size_induction [in PCP.Prelim]

split_inv [in PCP.Definitions]

SRH'_SRH [in PCP.TM_SRH]

SR_SRH [in PCP.SRH_SR]

SR_MPCP_cor [in PCP.SR_MPCP]

SR_MPCP [in PCP.SR_MPCP]

Start_fresh [in PCP.CFP_CFI]

state_eqlist [in PCP.TM_SRH]

state_not_sym [in PCP.TM_SRH]

state_count_one [in PCP.TM_SRH]

subset_rewriting [in PCP.TM_SRH]

symb_count_one [in PCP.TM_SRH]

sym_P [in PCP.SRH_SR]

sym_inj [in PCP.TM_SRH]

sym_G_rewt [in PCP.Post_CFG]

sym_mono [in PCP.Definitions]

sym_word_R [in PCP.Definitions]

sym_word_l [in PCP.Definitions]

sym_map [in PCP.Definitions]

sym_app [in PCP.Definitions]

## T

tau_eq_iff [in PCP.PCP_CFP]tau1_inv [in PCP.MPCP_PCP]

tau1_sym [in PCP.Definitions]

tau1_cards [in PCP.Definitions]

tau1_app [in PCP.Definitions]

tau2_inv [in PCP.MPCP_PCP]

tau2_gamma [in PCP.Post_CFG]

tau2_sym [in PCP.Definitions]

tau2_cards [in PCP.Definitions]

tau2_app [in PCP.Definitions]

terminal_iff_G [in PCP.Post_CFG]

terminal_iff [in PCP.Post_CFG]

TM_terminates_Halt [in PCP.singleTM]

## X

x_rewt_a0 [in PCP.SRH_SR]# Constructor Index

## D

dollar [in PCP.TM_SRH]## E

EqType [in PCP.singleTM]## F

FinType [in PCP.singleTM]FinTypeC [in PCP.singleTM]

## H

hash [in PCP.TM_SRH]## L

L [in PCP.singleTM]leftof [in PCP.singleTM]

## M

midtape [in PCP.singleTM]mk_mconfig [in PCP.singleTM]

## N

N [in PCP.singleTM]niltape [in PCP.singleTM]

## R

R [in PCP.singleTM]reachI [in PCP.singleTM]

reachS [in PCP.singleTM]

rewB [in PCP.Definitions]

rewR [in PCP.TM_SRH]

rewR [in PCP.Post_CFG]

rewR [in PCP.Definitions]

rewS [in PCP.Definitions]

rewtRefl [in PCP.Post_CFG]

rewtRule [in PCP.Post_CFG]

rewt'Refl [in PCP.TM_SRH]

rewt'Rule [in PCP.TM_SRH]

rightof [in PCP.singleTM]

## S

sigma [in PCP.TM_SRH]state [in PCP.TM_SRH]

symb [in PCP.TM_SRH]

# Inductive Index

## M

move [in PCP.singleTM]## R

reach [in PCP.singleTM]rew [in PCP.Definitions]

rewt [in PCP.Post_CFG]

rewt [in PCP.Definitions]

rewt' [in PCP.TM_SRH]

rew_cfg [in PCP.Post_CFG]

rew' [in PCP.TM_SRH]

rsig [in PCP.TM_SRH]

rsig' [in PCP.TM_SRH]

## T

tape [in PCP.singleTM]# Projection Index

## C

class [in PCP.singleTM]cstate [in PCP.singleTM]

ctape [in PCP.singleTM]

## E

enum [in PCP.singleTM]enum_ok [in PCP.singleTM]

eqType_dec [in PCP.singleTM]

eqType_X [in PCP.singleTM]

## H

halt [in PCP.singleTM]## S

start [in PCP.singleTM]states [in PCP.singleTM]

## T

trans [in PCP.singleTM]type [in PCP.singleTM]

# Section Index

## C

CFGs [in PCP.Post_CFG]## F

Fix_TM [in PCP.TM_SRH]Fix_Sigma [in PCP.singleTM]

fix_X [in PCP.Prelim]

## M

MPCP_PCP [in PCP.MPCP_PCP]## P

Palindrome [in PCP.CFP_CFI]PCP_CFI [in PCP.PCP_CFI]

PCP_CFP [in PCP.PCP_CFP]

Post_CFG [in PCP.Post_CFG]

## S

SRH_SR [in PCP.SRH_SR]SR_to_MPCP [in PCP.SR_MPCP]

string_rewriting [in PCP.TM_SRH]

# Instance Index

## E

eq_dec_rsig [in PCP.TM_SRH]eq_dec_rsig' [in PCP.TM_SRH]

eq_dec_states [in PCP.TM_SRH]

eq_dec_conf [in PCP.singleTM]

eq_dec_tape [in PCP.singleTM]

eq_dec_sig [in PCP.singleTM]

## F

finType_rsig [in PCP.TM_SRH]finType_rsig' [in PCP.TM_SRH]

## L

list_eq_dec [in PCP.singleTM]## M

move_finC [in PCP.singleTM]move_eq_dec [in PCP.singleTM]

## P

PreOrder_rewt [in PCP.Definitions]Proper_rewt [in PCP.Definitions]

## R

rewrite_proper [in PCP.Post_CFG]rewtTrans [in PCP.Post_CFG]

rewt'Trans [in PCP.TM_SRH]

## S

subrel [in PCP.Post_CFG]# Abbreviation Index

## S

sig [in PCP.Post_CFG]Sigma [in PCP.SRH_SR]

Sigma [in PCP.SR_MPCP]

StartG [in PCP.CFP_CFI]

# Definition Index

## C

card [in PCP.Definitions]cards [in PCP.Definitions]

CFG [in PCP.Post_CFG]

cfg [in PCP.Post_CFG]

CFI [in PCP.Definitions]

CFI' [in PCP.Post_CFG]

CFP [in PCP.Definitions]

CFP' [in PCP.Post_CFG]

conf [in PCP.TM_SRH]

count [in PCP.singleTM]

count [in PCP.Prelim]

current [in PCP.singleTM]

## D

d [in PCP.MPCP_PCP]d [in PCP.SR_MPCP]

Dec [in PCP.singleTM]

dec [in PCP.singleTM]

dec2bool [in PCP.singleTM]

dollar [in PCP.MPCP_PCP]

dollar [in PCP.SR_MPCP]

## E

e [in PCP.MPCP_PCP]e [in PCP.SR_MPCP]

elem [in PCP.singleTM]

eqType_CS [in PCP.singleTM]

## F

finType_CS [in PCP.singleTM]fresh [in PCP.Definitions]

## G

G [in PCP.Post_CFG]gamma [in PCP.PCP_CFI]

gamma [in PCP.PCP_CFP]

gamma [in PCP.Post_CFG]

gamma1 [in PCP.PCP_CFI]

gamma2 [in PCP.PCP_CFI]

get_rules [in PCP.TM_SRH]

get_rules_right [in PCP.TM_SRH]

get_rules_left [in PCP.TM_SRH]

## H

Halt [in PCP.singleTM]halting_states [in PCP.TM_SRH]

Halt' [in PCP.singleTM]

hash [in PCP.MPCP_PCP]

hash [in PCP.SR_MPCP]

hash_r [in PCP.MPCP_PCP]

hash_l [in PCP.MPCP_PCP]

## I

index [in PCP.singleTM]initc [in PCP.singleTM]

Injective [in PCP.Prelim]

is_cons [in PCP.MPCP_PCP]

## L

L [in PCP.Post_CFG]left [in PCP.singleTM]

loop [in PCP.singleTM]

loopM [in PCP.singleTM]

## M

mk_srconf [in PCP.TM_SRH]mk_tape [in PCP.singleTM]

MPCP [in PCP.Definitions]

## N

not_halting_states [in PCP.TM_SRH]## P

P [in PCP.SRH_SR]P [in PCP.MPCP_PCP]

P [in PCP.SR_MPCP]

palin [in PCP.PCP_CFP]

palin_G [in PCP.CFP_CFI]

PCP [in PCP.Definitions]

pos [in PCP.singleTM]

Post_G [in PCP.Post_CFG]

pos_el [in PCP.singleTM]

pos_el' [in PCP.singleTM]

## R

Reach [in PCP.singleTM]reduces [in PCP.Definitions]

reduction_reach_rewrite [in PCP.TM_SRH]

rewt_ind' [in PCP.Definitions]

right [in PCP.singleTM]

rsig_finType [in PCP.TM_SRH]

rule [in PCP.TM_SRH]

rule [in PCP.Post_CFG]

rules [in PCP.Post_CFG]

R_Sigma [in PCP.MPCP_PCP]

## S

S [in PCP.Post_CFG]Sigma [in PCP.PCP_CFI]

Sigma [in PCP.PCP_CFP]

Sigma [in PCP.MPCP_PCP]

Sigma [in PCP.Post_CFG]

sigma [in PCP.Definitions]

sing [in PCP.Definitions]

sizeOfTape [in PCP.singleTM]

SR [in PCP.Definitions]

SRH [in PCP.Definitions]

SRH' [in PCP.TM_SRH]

srs [in PCP.TM_SRH]

SRS [in PCP.Definitions]

SR_fin [in PCP.TM_SRH]

stack [in PCP.Definitions]

startsym [in PCP.Post_CFG]

step [in PCP.singleTM]

string [in PCP.Definitions]

sym [in PCP.TM_SRH]

sym [in PCP.Definitions]

symbol [in PCP.Definitions]

sym_G [in PCP.Post_CFG]

## T

tapeToList [in PCP.singleTM]tape_move_mono [in PCP.singleTM]

tape_write [in PCP.singleTM]

tape_move [in PCP.singleTM]

tape_move_left [in PCP.singleTM]

tape_move_right [in PCP.singleTM]

tau1 [in PCP.Definitions]

tau2 [in PCP.Definitions]

terminal [in PCP.Post_CFG]

TMrules [in PCP.TM_SRH]

TMterminates [in PCP.singleTM]

trans_R [in PCP.TM_SRH]

# Record Index

## E

eqType [in PCP.singleTM]## F

finType [in PCP.singleTM]finTypeC [in PCP.singleTM]

## M

mconfig [in PCP.singleTM]## S

sTM [in PCP.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 | (391 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 | (19 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 | (11 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 | (148 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 | (27 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 | (11 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) |

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 | (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 | (17 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 | (4 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 | (107 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) |