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_CFI
PCP_CFP
Prelim


S

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