| 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_CFID
DefinitionsM
MPCP_PCPP
PCP_CFIPCP_CFP
Post_CFG
Prelim
S
singleTMSRH_SR
SR_MPCP
T
TM_SRHLemma 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) |