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

(1662 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

(63 entries)

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

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

(238 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

(16 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

(731 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

(56 entries)

Axiom 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

(6 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

(14 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

(101 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

(46 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

(69 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

(77 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

(224 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

(19 entries)

---

Global Index

A

above_largest [lemma, in graphs.preliminaries]
add_edge_remove_edgesK [lemma, in graphs.open_confluence]
add_vertexK [lemma, in graphs.open_confluence]
add_testK [lemma, in graphs.open_confluence]
add_edgeKl [lemma, in graphs.open_confluence]
add_edgeKr [definition, in graphs.open_confluence]
add_edge_remove_vertex [lemma, in graphs.open_confluence]
add_test_morphism [instance, in graphs.open_confluence]
add_edge_morphism [instance, in graphs.open_confluence]
add_edge_morphism' [instance, in graphs.open_confluence]
add_test_merge [lemma, in graphs.open_confluence]
add_edge_edge [lemma, in graphs.open_confluence]
add_test_edge [lemma, in graphs.open_confluence]
add_edge_remove_edges [lemma, in graphs.open_confluence]
add_edge_test [lemma, in graphs.open_confluence]
add_testC [lemma, in graphs.open_confluence]
add_edgeV [lemma, in graphs.open_confluence]
add_test_graph [instance, in graphs.open_confluence]
add_test [definition, in graphs.open_confluence]
add_edge_graph [lemma, in graphs.open_confluence]
add_edge_graph'' [lemma, in graphs.open_confluence]
add_edge_graph' [lemma, in graphs.open_confluence]
add_edge [definition, in graphs.open_confluence]
add_edge' [definition, in graphs.open_confluence]
add_vertex_graph [instance, in graphs.open_confluence]
add_vertex [definition, in graphs.open_confluence]
add_edge_flip [lemma, in graphs.transfer]
add_vertex_iso [instance, in graphs.mgraph]
add_vlabel_edge [lemma, in graphs.mgraph]
add_vlabel_two [lemma, in graphs.mgraph]
add_vlabel_mon0 [lemma, in graphs.mgraph]
add_vlabel_unit [lemma, in graphs.mgraph]
add_vlabel_C [lemma, in graphs.mgraph]
add_vlabel_iso [lemma, in graphs.mgraph]
add_vlabel_iso' [lemma, in graphs.mgraph]
add_vlabel_iso'' [lemma, in graphs.mgraph]
add_edge_vlabel [lemma, in graphs.mgraph]
add_edge_rev [lemma, in graphs.mgraph]
add_edge_C [lemma, in graphs.mgraph]
add_edge_iso [lemma, in graphs.mgraph]
add_edge_iso' [lemma, in graphs.mgraph]
add_edge_iso'' [lemma, in graphs.mgraph]
add_vertex [definition, in graphs.mgraph]
add_vlabel [definition, in graphs.mgraph]
add_edge [definition, in graphs.mgraph]
add_test_cong [abbreviation, in graphs.mgraph2]
add_test [abbreviation, in graphs.mgraph2]
add_vlabel2_mon0 [lemma, in graphs.mgraph2]
add_vlabel2_edge [lemma, in graphs.mgraph2]
add_vlabel2_two [lemma, in graphs.mgraph2]
add_vlabel2_unit' [lemma, in graphs.mgraph2]
add_vlabel2_unit [lemma, in graphs.mgraph2]
add_vlabel2_C [lemma, in graphs.mgraph2]
add_vlabel2_iso [lemma, in graphs.mgraph2]
add_vlabel2_iso' [lemma, in graphs.mgraph2]
add_vlabel2_iso'' [lemma, in graphs.mgraph2]
add_edge2_vlabel [lemma, in graphs.mgraph2]
add_edge2_rev [lemma, in graphs.mgraph2]
add_edge2_C [lemma, in graphs.mgraph2]
add_edge2_iso [lemma, in graphs.mgraph2]
add_edge2_iso' [lemma, in graphs.mgraph2]
add_edge2_iso'' [lemma, in graphs.mgraph2]
add_vertex2_iso [instance, in graphs.mgraph2]
add_vlabel2 [definition, in graphs.mgraph2]
add_edge2 [definition, in graphs.mgraph2]
add_vertex2 [definition, in graphs.mgraph2]
admissible_map [lemma, in graphs.reduction]
admissible_l [definition, in graphs.reduction]
admitted_case [axiom, in graphs.preliminaries]
all_cons [lemma, in graphs.preliminaries]
A10 [projection, in graphs.pttdom]
A10_ [projection, in graphs.ptt]
A11 [projection, in graphs.ptt]
A12 [projection, in graphs.ptt]
A13 [projection, in graphs.pttdom]
A13_ [lemma, in graphs.ptt]
A14 [projection, in graphs.pttdom]
A14_ [lemma, in graphs.ptt]

B

b [section, in graphs.finite_quotient]
below_smallest [lemma, in graphs.preliminaries]
bigcup_set1 [lemma, in graphs.preliminaries]
bigD1 [lemma, in graphs.structures]
bigID [lemma, in graphs.structures]
big_unit [lemma, in graphs.structures]
big_sum [lemma, in graphs.structures]
big_pred1 [lemma, in graphs.structures]
big_pred1_eq [lemma, in graphs.structures]
big_seq1 [lemma, in graphs.structures]
big_split [lemma, in graphs.structures]
big_cat [lemma, in graphs.structures]
big_mkcond [lemma, in graphs.structures]
bij [record, in graphs.bij]
Bij [constructor, in graphs.bij]
Bij [section, in graphs.finmap_plus]
bij [library]
BijCast [section, in graphs.finmap_plus]
BijCast.A [variable, in graphs.finmap_plus]
BijCast.A' [variable, in graphs.finmap_plus]
BijCast.eqA [variable, in graphs.finmap_plus]
BijCast.T [variable, in graphs.finmap_plus]
bijD1 [definition, in graphs.bij]
BijD1 [section, in graphs.bij]
bijD1_bwd [definition, in graphs.bij]
bijD1_fwd [definition, in graphs.bij]
BijD1.T [variable, in graphs.bij]
BijD1.z [variable, in graphs.bij]
bijK [projection, in graphs.bij]
bijK' [projection, in graphs.bij]
BijT [section, in graphs.bij]
BijT.inP [variable, in graphs.bij]
BijT.P [variable, in graphs.bij]
BijT.T [variable, in graphs.bij]
bij_quotE' [lemma, in graphs.finite_quotient]
bij_quotE [lemma, in graphs.finite_quotient]
bij_quot [definition, in graphs.finite_quotient]
bij_perm_enum [lemma, in graphs.bij]
bij_same [lemma, in graphs.bij]
bij_sumA [lemma, in graphs.bij]
bij_sumC [lemma, in graphs.bij]
bij_Equivalence [instance, in graphs.bij]
bij_comp [definition, in graphs.bij]
bij_sym [definition, in graphs.bij]
bij_id [definition, in graphs.bij]
bij_eqLR [lemma, in graphs.bij]
bij_imsetC [lemma, in graphs.bij]
bij_mem_imset [lemma, in graphs.bij]
bij_injective' [lemma, in graphs.bij]
bij_injective [lemma, in graphs.bij]
bij_bijective' [lemma, in graphs.bij]
bij_bijective [lemma, in graphs.bij]
bij_bwd [projection, in graphs.bij]
bij_fwd [projection, in graphs.bij]
bij_castE [lemma, in graphs.finmap_plus]
bij_cast [definition, in graphs.finmap_plus]
bij_setD [definition, in graphs.finmap_plus]
bij_surj [lemma, in graphs.preliminaries]
bij_card_eq [lemma, in graphs.preliminaries]
Bij.g [variable, in graphs.finmap_plus]
Bij.G [variable, in graphs.finmap_plus]
Bij.g_inj [variable, in graphs.finmap_plus]
Bij.T [variable, in graphs.finmap_plus]
Bij.vset [variable, in graphs.finmap_plus]
bool_option_unit [definition, in graphs.bij]
bool_two [lemma, in graphs.bij]
bool_swap [definition, in graphs.bij]
box [record, in graphs.open_confluence]
Box [constructor, in graphs.open_confluence]
boxed [projection, in graphs.open_confluence]
b.e [variable, in graphs.finite_quotient]
b.h [variable, in graphs.finite_quotient]
b.S [variable, in graphs.finite_quotient]
b.T [variable, in graphs.finite_quotient]

C

can_bijD1_bwd [lemma, in graphs.bij]
can_bijD1_fwd [lemma, in graphs.bij]
can_vset' [lemma, in graphs.finmap_plus]
can_vset [lemma, in graphs.finmap_plus]
car [projection, in graphs.structures]
cardsCT [lemma, in graphs.preliminaries]
cardsDsub [lemma, in graphs.finmap_plus]
cardsI [lemma, in graphs.preliminaries]
cardsIsub [lemma, in graphs.finmap_plus]
cards2P [lemma, in graphs.preliminaries]
cards3 [lemma, in graphs.preliminaries]
card_bij [lemma, in graphs.bij]
card_void [lemma, in graphs.preliminaries]
card_le1P [lemma, in graphs.preliminaries]
card_gt2P [lemma, in graphs.preliminaries]
card_gt1P [lemma, in graphs.preliminaries]
card_gtnP [lemma, in graphs.preliminaries]
card_le1 [lemma, in graphs.preliminaries]
card_ltnT [lemma, in graphs.preliminaries]
card1P [lemma, in graphs.preliminaries]
card12 [lemma, in graphs.preliminaries]
cast_proof [lemma, in graphs.finmap_plus]
CEquivalence [abbreviation, in graphs.structures]
close_same_step [lemma, in graphs.open_confluence]
cnv [projection, in graphs.pttdom]
cnvdot [projection, in graphs.pttdom]
cnvdot_ [projection, in graphs.ptt]
cnvI [projection, in graphs.pttdom]
cnvI_ [projection, in graphs.ptt]
cnvpar [projection, in graphs.pttdom]
cnvpar_ [projection, in graphs.ptt]
cnvtop [lemma, in graphs.ptt]
cnvtst [lemma, in graphs.pttdom]
cnv_test [lemma, in graphs.pttdom]
cnv_inj [lemma, in graphs.pttdom]
cnv_eqv [projection, in graphs.pttdom]
cnv_eqv_ [projection, in graphs.ptt]
cnv_iso2 [instance, in graphs.mgraph2]
cnv_steps [instance, in graphs.reduction]
cnv1 [lemma, in graphs.pttdom]
cnv2dot [lemma, in graphs.mgraph2]
cnv2I [lemma, in graphs.mgraph2]
cnv2par [lemma, in graphs.mgraph2]
codom_Some [lemma, in graphs.preliminaries]
completeness [lemma, in graphs.completeness]
completeness [library]
confluence [lemma, in graphs.completeness]
connectUP [lemma, in graphs.preliminaries]
connect_img [lemma, in graphs.preliminaries]
connect_symI [lemma, in graphs.preliminaries]
connect_restrict_mono [lemma, in graphs.preliminaries]
connect_mono [lemma, in graphs.preliminaries]
consistent [definition, in graphs.mgraph]
consistentT [lemma, in graphs.mgraph]
consistentTT [lemma, in graphs.mgraph]
consistentU [lemma, in graphs.mgraph]
consistent_del1 [lemma, in graphs.mgraph]
cons_step [constructor, in graphs.rewriting]
cons_step_steps [lemma, in graphs.reduction]
cons_iso_steps [lemma, in graphs.reduction]
contraNnot [lemma, in graphs.preliminaries]
contraPeq [lemma, in graphs.preliminaries]
contraPN [lemma, in graphs.preliminaries]
contraPneq [lemma, in graphs.preliminaries]
contraPT [lemma, in graphs.preliminaries]
contraTnot [lemma, in graphs.preliminaries]
contra_notT [lemma, in graphs.preliminaries]
CProper [section, in graphs.structures]
CProper [abbreviation, in graphs.structures]
CProper.A [variable, in graphs.structures]
CProper.B [variable, in graphs.structures]
CProper.C [variable, in graphs.structures]
CProper.f [variable, in graphs.structures]
CProper.g [variable, in graphs.structures]
CProper.Hf [variable, in graphs.structures]
CProper.Hg [variable, in graphs.structures]
CProper.R [variable, in graphs.structures]
CProper.S [variable, in graphs.structures]
CProper.T [variable, in graphs.structures]
CProper1 [lemma, in graphs.structures]
CProper2 [lemma, in graphs.structures]
cr [definition, in graphs.preliminaries]
critical_pair3 [lemma, in graphs.open_confluence]
critical_pair2 [lemma, in graphs.open_confluence]
critical_pair1 [lemma, in graphs.open_confluence]
crK [lemma, in graphs.preliminaries]

D

default [projection, in graphs.open_confluence]
degree_one_two [lemma, in graphs.open_confluence]
derived [section, in graphs.pttdom]
derived [section, in graphs.ptt]
derived.X [variable, in graphs.pttdom]
derived.X [variable, in graphs.ptt]
[ _ ] [notation, in graphs.pttdom]
disjointE [lemma, in graphs.preliminaries]
disjointFl [lemma, in graphs.preliminaries]
disjointFr [lemma, in graphs.preliminaries]
disjointNI [lemma, in graphs.preliminaries]
disjointP [lemma, in graphs.preliminaries]
disjointsU [lemma, in graphs.preliminaries]
disjoints1 [lemma, in graphs.preliminaries]
disjointW [lemma, in graphs.preliminaries]
disjoint_transR [lemma, in graphs.preliminaries]
disjoint_transL [definition, in graphs.preliminaries]
disjoint_exists [lemma, in graphs.preliminaries]
Disjoint3 [section, in graphs.preliminaries]
disjoint3P [lemma, in graphs.preliminaries]
disjoint3_cases [inductive, in graphs.preliminaries]
Disjoint3.A [variable, in graphs.preliminaries]
Disjoint3.B [variable, in graphs.preliminaries]
Disjoint3.C [variable, in graphs.preliminaries]
Disjoint3.T [variable, in graphs.preliminaries]
Dis3In1 [constructor, in graphs.preliminaries]
Dis3In2 [constructor, in graphs.preliminaries]
Dis3In3 [constructor, in graphs.preliminaries]
Dis3Notin [constructor, in graphs.preliminaries]
dom [projection, in graphs.pttdom]
domE [projection, in graphs.ptt]
domtst [lemma, in graphs.pttdom]
dom_tst [lemma, in graphs.pttdom]
dom_test [lemma, in graphs.pttdom]
dom_eqv [projection, in graphs.pttdom]
dom_eqv_ [instance, in graphs.ptt]
dom_iso2 [instance, in graphs.mgraph2]
dom_steps [instance, in graphs.reduction]
dom2E [lemma, in graphs.mgraph2]
dot [projection, in graphs.pttdom]
dotA [projection, in graphs.pttdom]
dotA_ [projection, in graphs.ptt]
dotcnv [lemma, in graphs.pttdom]
dotx1 [projection, in graphs.pttdom]
dotx1_ [projection, in graphs.ptt]
dot_test [lemma, in graphs.pttdom]
dot_eqv [projection, in graphs.pttdom]
dot_eqv_ [projection, in graphs.ptt]
dot_iso2 [instance, in graphs.mgraph2]
dot_steps [instance, in graphs.reduction]
dot_steps_r [lemma, in graphs.reduction]
dot_steps_l [lemma, in graphs.reduction]
dot_edges [lemma, in graphs.reduction]
dot1x [lemma, in graphs.pttdom]
dot2A [lemma, in graphs.mgraph2]
dot2Aflat [lemma, in graphs.mgraph2]
dot2one [lemma, in graphs.mgraph2]
dot2one' [lemma, in graphs.mgraph2]
dot2unit_l [lemma, in graphs.mgraph2]
dot2unit_r' [lemma, in graphs.mgraph2]
dot2unit_r [lemma, in graphs.mgraph2]

E

eC [abbreviation, in graphs.finite_quotient]
edge [projection, in graphs.mgraph]
edges [definition, in graphs.mgraph]
edges_replace [lemma, in graphs.open_confluence]
edges_at_flip_edge [lemma, in graphs.open_confluence]
edges_at_remove_edges [lemma, in graphs.open_confluence]
edges_at_added_vertex [lemma, in graphs.open_confluence]
edges_atC [lemma, in graphs.open_confluence]
edges_at_add_edge' [lemma, in graphs.open_confluence]
edges_at_add_edgeL [lemma, in graphs.open_confluence]
edges_at_add_edge [lemma, in graphs.open_confluence]
edges_at_del [lemma, in graphs.open_confluence]
edges_at_test [lemma, in graphs.open_confluence]
edges_at_oarc [lemma, in graphs.open_confluence]
edges_atF [lemma, in graphs.open_confluence]
edges_atP [lemma, in graphs.open_confluence]
edges_atE [lemma, in graphs.open_confluence]
edges_at [definition, in graphs.open_confluence]
edges_at_iso [lemma, in graphs.mgraph]
edges_in1 [lemma, in graphs.mgraph]
edges_in [definition, in graphs.mgraph]
edges_at [definition, in graphs.mgraph]
edge_in_set [lemma, in graphs.mgraph]
edge_set1 [lemma, in graphs.mgraph]
edge_set [definition, in graphs.mgraph]
edge_graph [definition, in graphs.mgraph]
edge_graph2_iso [instance, in graphs.mgraph2]
edge_graph2 [definition, in graphs.mgraph2]
edir_bodyE [lemma, in graphs.transfer]
edir_of [definition, in graphs.transfer]
edir_body [definition, in graphs.transfer]
edone [library]
efun_of_bij [lemma, in graphs.transfer]
efun_of_inj [lemma, in graphs.transfer]
efun_bodyE [lemma, in graphs.transfer]
efun_of [definition, in graphs.transfer]
efun_body [definition, in graphs.transfer]
elabel [projection, in graphs.mgraph]
elabel_iso' [lemma, in graphs.mgraph]
elabel_iso [lemma, in graphs.mgraph]
elabel_hom [projection, in graphs.mgraph]
elem_of [projection, in graphs.pttdom]
empty_uniqe [lemma, in graphs.preliminaries]
endpoint [projection, in graphs.mgraph]
endpoint_iso' [lemma, in graphs.mgraph]
endpoint_iso [lemma, in graphs.mgraph]
endpoint_hom [projection, in graphs.mgraph]
endpt [projection, in graphs.open_confluence]
endptP [projection, in graphs.open_confluence]
endpt_add_edge [lemma, in graphs.open_confluence]
endpt_proof [lemma, in graphs.transfer]
enum_unit [lemma, in graphs.preliminaries]
enum_sum [lemma, in graphs.preliminaries]
eqb_negR [lemma, in graphs.preliminaries]
eqmodE [lemma, in graphs.finite_quotient]
equiv [library]
Equivalence [section, in graphs.preliminaries]
equivalence_partition_gt1P [lemma, in graphs.preliminaries]
equivalence_rel_of_sym [lemma, in graphs.preliminaries]
Equivalence.e [variable, in graphs.preliminaries]
Equivalence.T [variable, in graphs.preliminaries]
equiv_comp_pi [lemma, in graphs.finite_quotient]
equiv_compE [lemma, in graphs.finite_quotient]
equiv_comp [definition, in graphs.finite_quotient]
equiv_of_fn [lemma, in graphs.equiv]
equiv_of_nn [lemma, in graphs.equiv]
equiv_of_ff [lemma, in graphs.equiv]
equiv_rel_Equivalence [instance, in graphs.equiv]
equiv_of_sub' [lemma, in graphs.equiv]
equiv_of_sub [lemma, in graphs.equiv]
equiv_of_transfer [lemma, in graphs.equiv]
equiv_ofE [lemma, in graphs.equiv]
equiv_of_class [lemma, in graphs.equiv]
equiv_clot_Kl [lemma, in graphs.mgraph]
equiv_of_trans [definition, in graphs.preliminaries]
equiv_of_sym [lemma, in graphs.preliminaries]
equiv_of_refl [definition, in graphs.preliminaries]
equiv_of [definition, in graphs.preliminaries]
Eqv [projection, in graphs.structures]
eqv [projection, in graphs.structures]
eqvbN [lemma, in graphs.pttdom]
eqvbT [lemma, in graphs.pttdom]
eqvb_neq [lemma, in graphs.pttdom]
eqvb_par1 [lemma, in graphs.pttdom]
eqvb_transL [lemma, in graphs.structures]
eqvb_transR [lemma, in graphs.structures]
eqvb_trans [lemma, in graphs.structures]
eqvG [record, in graphs.open_confluence]
eqvG_stepL [lemma, in graphs.open_confluence]
eqvG_step [constructor, in graphs.open_confluence]
eqvG_edges_at [lemma, in graphs.open_confluence]
eqvG_graph [lemma, in graphs.open_confluence]
eqvG_sym [lemma, in graphs.open_confluence]
eqvG_Equivalence [instance, in graphs.open_confluence]
eqvG_pack [lemma, in graphs.transfer]
eqvG_iso2E [lemma, in graphs.transfer]
eqvG_iso2R [definition, in graphs.transfer]
eqvG_iso2L [definition, in graphs.transfer]
eqvG_iso2 [definition, in graphs.transfer]
eqvxx [lemma, in graphs.structures]
eqv_le [projection, in graphs.open_confluence]
eqv_lv [projection, in graphs.open_confluence]
eqv_test_equiv [lemma, in graphs.pttdom]
eqv_test [definition, in graphs.pttdom]
eqv_clot_LR [lemma, in graphs.equiv]
eqv_clot_injR [lemma, in graphs.equiv]
eqv_clot_injL [lemma, in graphs.equiv]
eqv_clot1E [lemma, in graphs.equiv]
eqv_clot_cat [lemma, in graphs.equiv]
eqv_clot_map_eq [lemma, in graphs.equiv]
eqv_clot_mapF [lemma, in graphs.equiv]
eqv_clot_map [lemma, in graphs.equiv]
eqv_inj.f_inj [variable, in graphs.equiv]
eqv_inj.eq2E [variable, in graphs.equiv]
eqv_inj.eq_e [variable, in graphs.equiv]
eqv_inj.f [variable, in graphs.equiv]
eqv_inj.e2 [variable, in graphs.equiv]
eqv_inj.e1 [variable, in graphs.equiv]
eqv_inj.T2 [variable, in graphs.equiv]
eqv_inj.T1 [variable, in graphs.equiv]
eqv_inj [section, in graphs.equiv]
eqv_clot_nothing' [lemma, in graphs.equiv]
eqv_clot_nothing [lemma, in graphs.equiv]
eqv_clot_eq [lemma, in graphs.equiv]
eqv_clot_subrel [lemma, in graphs.equiv]
eqv_clot_tl [lemma, in graphs.equiv]
eqv_clot_hd' [lemma, in graphs.equiv]
eqv_clot_hd [lemma, in graphs.equiv]
eqv_clot_trans [lemma, in graphs.equiv]
eqv_clot_iso [lemma, in graphs.equiv]
eqv_clot_map' [lemma, in graphs.equiv]
eqv_clot_subset [lemma, in graphs.equiv]
eqv_clot_pair [lemma, in graphs.equiv]
eqv_clotE [lemma, in graphs.equiv]
eqv_clot [definition, in graphs.equiv]
eqv_clot_union_rel [lemma, in graphs.mgraph]
eqv_clot_map_lr [lemma, in graphs.mgraph]
eqv_update [lemma, in graphs.finmap_plus]
eqv_big [lemma, in graphs.structures]
eqv_bigl [lemma, in graphs.structures]
eqv_bigr [lemma, in graphs.structures]
eqv_big_bij [lemma, in graphs.structures]
eqv_map [lemma, in graphs.structures]
eqv_morphim [instance, in graphs.structures]
eqv_sym [instance, in graphs.structures]
eqv_ [definition, in graphs.structures]
eqv' [definition, in graphs.pttdom]
eqv' [projection, in graphs.structures]
eqv'_sym [lemma, in graphs.pttdom]
Eqv'_sym [projection, in graphs.structures]
eqv01 [lemma, in graphs.pttdom]
eqv01 [projection, in graphs.structures]
eqv10 [lemma, in graphs.structures]
eqv11 [lemma, in graphs.pttdom]
eqv11 [projection, in graphs.structures]
eq_quot_finMixin [lemma, in graphs.finite_quotient]
eq_equiv_class [lemma, in graphs.equiv]
eq_equiv [lemma, in graphs.equiv]
eq_eqv [lemma, in graphs.mgraph]
eq_unit [lemma, in graphs.structures]
eq_setoid [definition, in graphs.structures]
eq_set1P [lemma, in graphs.preliminaries]
ereprK [abbreviation, in graphs.finite_quotient]
eset [projection, in graphs.open_confluence]
ET [definition, in graphs.open_confluence]
eval [definition, in graphs.pttdom]
eval [definition, in graphs.ptt]
existsb_case [lemma, in graphs.preliminaries]
existsb_eq [lemma, in graphs.preliminaries]
existsPn [lemma, in graphs.preliminaries]
exists_inPn [lemma, in graphs.preliminaries]
expand_parallel [lemma, in graphs.transfer]
expand_loop [lemma, in graphs.transfer]
expand_chain [lemma, in graphs.transfer]
expand_pendant [lemma, in graphs.transfer]
expand_isolated [lemma, in graphs.transfer]
ex_smallest [lemma, in graphs.preliminaries]
ex2_iff_morphism [instance, in graphs.preliminaries]

F

FinEncodingModuloRel [section, in graphs.finite_quotient]
FinEncodingModuloRel.C [variable, in graphs.finite_quotient]
FinEncodingModuloRel.CD [variable, in graphs.finite_quotient]
FinEncodingModuloRel.D [variable, in graphs.finite_quotient]
FinEncodingModuloRel.DC [variable, in graphs.finite_quotient]
FinEncodingModuloRel.eD [variable, in graphs.finite_quotient]
FinEncodingModuloRel.encD [variable, in graphs.finite_quotient]
finite_quotient [library]
finmap_plus [library]
flat_labels [definition, in graphs.structures]
flipped_edge [lemma, in graphs.open_confluence]
flip_step [constructor, in graphs.open_confluence]
flip_edgeK' [lemma, in graphs.open_confluence]
flip_edgeK [lemma, in graphs.open_confluence]
flip_edge_add_test [lemma, in graphs.open_confluence]
flip_edge_graph [instance, in graphs.open_confluence]
flip_edge [definition, in graphs.open_confluence]
flip_edge_iso [lemma, in graphs.transfer]
Foldr1 [section, in graphs.preliminaries]
foldr1 [definition, in graphs.preliminaries]
foldr1_set_default [lemma, in graphs.preliminaries]
Foldr1.F [variable, in graphs.preliminaries]
Foldr1.I [variable, in graphs.preliminaries]
Foldr1.op [variable, in graphs.preliminaries]
Foldr1.R [variable, in graphs.preliminaries]
ForallE [lemma, in graphs.equiv]
forallPn [lemma, in graphs.preliminaries]
forall_inPn [lemma, in graphs.preliminaries]
fresh [definition, in graphs.open_confluence]
freshP [lemma, in graphs.open_confluence]
freshP' [lemma, in graphs.open_confluence]
fresh_eqF [lemma, in graphs.open_confluence]
fresh_bijE' [lemma, in graphs.finmap_plus]
fresh_bij' [lemma, in graphs.finmap_plus]
fresh_bijE [lemma, in graphs.finmap_plus]
fresh_bij [lemma, in graphs.finmap_plus]
Fresh2Bij [section, in graphs.finmap_plus]
Fresh2Bij.A [variable, in graphs.finmap_plus]
Fresh2Bij.B [variable, in graphs.finmap_plus]
Fresh2Bij.f [variable, in graphs.finmap_plus]
Fresh2Bij.Hx [variable, in graphs.finmap_plus]
Fresh2Bij.Hy [variable, in graphs.finmap_plus]
Fresh2Bij.T [variable, in graphs.finmap_plus]
Fresh2Bij.x [variable, in graphs.finmap_plus]
Fresh2Bij.y [variable, in graphs.finmap_plus]
fresh2_bij [definition, in graphs.finmap_plus]
fsetDDD [lemma, in graphs.finmap_plus]
fsetDEl [lemma, in graphs.finmap_plus]
fsetDl [lemma, in graphs.finmap_plus]
fsetD_bijE [lemma, in graphs.finmap_plus]
fsetD_bij [definition, in graphs.finmap_plus]
fsetD_bij_can_bwd [lemma, in graphs.finmap_plus]
fsetD_bij_can_fwd [lemma, in graphs.finmap_plus]
fsetD_bij_bwd [definition, in graphs.finmap_plus]
fsetD_bij_fwd [definition, in graphs.finmap_plus]
fsetD_bij_bwd_proof [lemma, in graphs.finmap_plus]
fsetD_bij_fwd_proof [lemma, in graphs.finmap_plus]
fsetD_bij.E [variable, in graphs.finmap_plus]
fsetD_bij.f [variable, in graphs.finmap_plus]
fsetD_bij.C' [variable, in graphs.finmap_plus]
fsetD_bij.C [variable, in graphs.finmap_plus]
fsetD_bij.B [variable, in graphs.finmap_plus]
fsetD_bij.A [variable, in graphs.finmap_plus]
fsetD_bij.T [variable, in graphs.finmap_plus]
fsetD_bij [section, in graphs.finmap_plus]
fsetUDU [lemma, in graphs.finmap_plus]
FsetU1Fun [section, in graphs.finmap_plus]
FsetU1Fun.A [variable, in graphs.finmap_plus]
FsetU1Fun.B [variable, in graphs.finmap_plus]
FsetU1Fun.f [variable, in graphs.finmap_plus]
FsetU1Fun.T [variable, in graphs.finmap_plus]
FsetU1Fun.x [variable, in graphs.finmap_plus]
FsetU1Fun.y [variable, in graphs.finmap_plus]
fsetU1_fun_can [lemma, in graphs.finmap_plus]
fsetU1_fun [definition, in graphs.finmap_plus]
fset01 [lemma, in graphs.finmap_plus]
fset1D [lemma, in graphs.finmap_plus]
fset1UE [lemma, in graphs.finmap_plus]
fset1U0 [lemma, in graphs.finmap_plus]
fset2_maxn_neq [lemma, in graphs.finmap_plus]
fset2_cases [lemma, in graphs.finmap_plus]
fset2_inv [lemma, in graphs.finmap_plus]
fstep [inductive, in graphs.open_confluence]
fstep_step [constructor, in graphs.open_confluence]
fsvalK [lemma, in graphs.finmap_plus]
fsval_eqF [lemma, in graphs.finmap_plus]
fun_decompose [lemma, in graphs.preliminaries]

G

graph [abbreviation, in graphs.open_confluence]
graph [abbreviation, in graphs.transfer]
graph [abbreviation, in graphs.transfer]
graph [abbreviation, in graphs.transfer]
graph [abbreviation, in graphs.completeness]
graph [abbreviation, in graphs.rewriting]
graph [abbreviation, in graphs.mgraph]
graph [record, in graphs.mgraph]
Graph [constructor, in graphs.mgraph]
graph [abbreviation, in graphs.mgraph2]
graph [abbreviation, in graphs.reduction]
graph [abbreviation, in graphs.reduction]
graph [abbreviation, in graphs.reduction]
graph_of [projection, in graphs.mgraph2]
graph_of_term [definition, in graphs.reduction]
graph2 [abbreviation, in graphs.open_confluence]
graph2 [abbreviation, in graphs.transfer]
graph2 [abbreviation, in graphs.transfer]
graph2 [abbreviation, in graphs.transfer]
graph2 [abbreviation, in graphs.completeness]
graph2 [abbreviation, in graphs.rewriting]
graph2 [record, in graphs.mgraph2]
Graph2 [constructor, in graphs.mgraph2]
graph2 [abbreviation, in graphs.reduction]
graph2 [abbreviation, in graphs.reduction]
graph2 [abbreviation, in graphs.reduction]
G1 [abbreviation, in graphs.mgraph]
G12 [abbreviation, in graphs.mgraph]
G2 [abbreviation, in graphs.mgraph]
g2_pttdom [definition, in graphs.mgraph2]
g2_ptt [definition, in graphs.mgraph2]
g2_A12 [lemma, in graphs.mgraph2]
g2_A12' [lemma, in graphs.mgraph2]
g2_A11 [lemma, in graphs.mgraph2]
g2_A10 [lemma, in graphs.mgraph2]
g2_var [definition, in graphs.mgraph2]
g2_top [definition, in graphs.mgraph2]
g2_one [definition, in graphs.mgraph2]
g2_dom [definition, in graphs.mgraph2]
g2_cnv [definition, in graphs.mgraph2]
g2_dot [definition, in graphs.mgraph2]
g2_par [definition, in graphs.mgraph2]

H

h [section, in graphs.mgraph2]
Hom [constructor, in graphs.mgraph]
hom_merge_union_K [lemma, in graphs.mgraph]
hom_union_merge_l [lemma, in graphs.mgraph]
hom_merge_merge [lemma, in graphs.mgraph]
hom_sym [lemma, in graphs.mgraph]
hom_comp [lemma, in graphs.mgraph]
hom_id [lemma, in graphs.mgraph]
h_merge_union_Ke [definition, in graphs.mgraph]
h_merge_union_Ke1 [definition, in graphs.mgraph]
h_merge_union_K [definition, in graphs.mgraph]
h_union_merge_l [definition, in graphs.mgraph]
h_mergeE [lemma, in graphs.mgraph]
h_merge [definition, in graphs.mgraph]
h' [definition, in graphs.mgraph]
h.fe [variable, in graphs.mgraph2]
h.fv [variable, in graphs.mgraph2]
h.Hfe [variable, in graphs.mgraph2]
h.Hfv [variable, in graphs.mgraph2]
h.Hfvmon0 [variable, in graphs.mgraph2]
h.Hfvmon2 [variable, in graphs.mgraph2]
h.X [variable, in graphs.mgraph2]
h.Y [variable, in graphs.mgraph2]

I

i [abbreviation, in graphs.structures]
id_surj [lemma, in graphs.preliminaries]
id_bij [lemma, in graphs.preliminaries]
imfsetU [lemma, in graphs.finmap_plus]
imfset_bij_bwdE [lemma, in graphs.finmap_plus]
imfset_bij [definition, in graphs.finmap_plus]
imfset_bij_bwd [definition, in graphs.finmap_plus]
imfset_bij_fwd [definition, in graphs.finmap_plus]
imfset_inv [lemma, in graphs.finmap_plus]
imfset_comp [lemma, in graphs.finmap_plus]
imfset_sep [lemma, in graphs.finmap_plus]
imfset0 [lemma, in graphs.finmap_plus]
imfset1 [lemma, in graphs.finmap_plus]
imfset1U [lemma, in graphs.finmap_plus]
imset_valT [lemma, in graphs.preliminaries]
imset_pre_val [lemma, in graphs.preliminaries]
im_efun_of [lemma, in graphs.transfer]
incident [definition, in graphs.open_confluence]
incident [definition, in graphs.mgraph]
incident_vset [lemma, in graphs.open_confluence]
incident_flip_edge [lemma, in graphs.open_confluence]
incident_flip [lemma, in graphs.open_confluence]
incident_addv [lemma, in graphs.open_confluence]
incident_dele [lemma, in graphs.open_confluence]
incident_delv [lemma, in graphs.open_confluence]
incident_iso [lemma, in graphs.mgraph]
induced [definition, in graphs.mgraph]
induced_sub [lemma, in graphs.mgraph]
induced_proof [definition, in graphs.mgraph]
infer_testE [lemma, in graphs.pttdom]
infer_test [definition, in graphs.pttdom]
inh_type [record, in graphs.open_confluence]
inject [section, in graphs.transfer]
inject.T [variable, in graphs.transfer]
inj_vNfresh [lemma, in graphs.transfer]
inj_v_fresh [lemma, in graphs.transfer]
inj_v_open [lemma, in graphs.transfer]
inj_vK [lemma, in graphs.transfer]
inj_eK [lemma, in graphs.transfer]
inj_e_inj [lemma, in graphs.transfer]
inj_v_inj [lemma, in graphs.transfer]
inj_e [definition, in graphs.transfer]
inj_v [definition, in graphs.transfer]
inj_imset [lemma, in graphs.preliminaries]
inj_card_onto_pred [lemma, in graphs.preliminaries]
inj_omap [lemma, in graphs.preliminaries]
inj_card_leq [lemma, in graphs.preliminaries]
inl_codom_inr [lemma, in graphs.preliminaries]
inl_inj [lemma, in graphs.preliminaries]
inl_eqE [lemma, in graphs.preliminaries]
input [projection, in graphs.mgraph2]
inr_codom_inl [lemma, in graphs.preliminaries]
inr_inj [lemma, in graphs.preliminaries]
inr_eqE [lemma, in graphs.preliminaries]
in_vsetAV' [lemma, in graphs.open_confluence]
in_vsetAE [lemma, in graphs.open_confluence]
in_vsetAV [lemma, in graphs.open_confluence]
in_vsetDE [lemma, in graphs.open_confluence]
in_vsetDV [lemma, in graphs.open_confluence]
in_eqv_update [lemma, in graphs.finmap_plus]
in_fsep [lemma, in graphs.finmap_plus]
in_imfsetT [lemma, in graphs.finmap_plus]
IO [abbreviation, in graphs.mgraph2]
iso [record, in graphs.mgraph]
Iso [constructor, in graphs.mgraph]
isop_step [instance, in graphs.rewriting]
iso_of_oiso [lemma, in graphs.transfer]
iso_stagnates [lemma, in graphs.completeness]
iso_step [constructor, in graphs.rewriting]
iso_subgraph_forT [definition, in graphs.mgraph]
iso_Equivalence [instance, in graphs.mgraph]
iso_comp [definition, in graphs.mgraph]
iso_sym [definition, in graphs.mgraph]
iso_id [definition, in graphs.mgraph]
iso_hom [projection, in graphs.mgraph]
iso_d [projection, in graphs.mgraph]
iso_e [projection, in graphs.mgraph]
iso_v [projection, in graphs.mgraph]
iso_iso2' [lemma, in graphs.mgraph2]
iso_iso2 [lemma, in graphs.mgraph2]
Iso' [definition, in graphs.mgraph]
iso2 [record, in graphs.mgraph2]
Iso2 [constructor, in graphs.mgraph2]
iso2prop [definition, in graphs.mgraph2]
iso2prop_Equivalence [instance, in graphs.mgraph2]
iso2_intro [lemma, in graphs.transfer]
iso2_subgraph_forT [lemma, in graphs.mgraph2]
iso2_Equivalence [instance, in graphs.mgraph2]
iso2_comp [definition, in graphs.mgraph2]
iso2_sym [definition, in graphs.mgraph2]
iso2_id [definition, in graphs.mgraph2]
iso2_output [projection, in graphs.mgraph2]
iso2_input [projection, in graphs.mgraph2]
iso2_iso [projection, in graphs.mgraph2]
is_edge_flip_edge [lemma, in graphs.open_confluence]
is_edge_remove_edges [lemma, in graphs.open_confluence]
is_edge_vsetR [lemma, in graphs.open_confluence]
is_edge_vsetL [lemma, in graphs.open_confluence]
is_edge [definition, in graphs.open_confluence]
is_graph [record, in graphs.open_confluence]
is_test_alt [lemma, in graphs.pttdom]
is_test [definition, in graphs.pttdom]
is_hom [record, in graphs.mgraph]

K

kernel [definition, in graphs.finite_quotient]
kernelb [definition, in graphs.finite_quotient]
kernelP [lemma, in graphs.finite_quotient]
kernel_equivalence [lemma, in graphs.finite_quotient]
kernel_eqv_clot [lemma, in graphs.equiv]

L

labels [record, in graphs.structures]
Labels [constructor, in graphs.structures]
largest [definition, in graphs.preliminaries]
last_belast_eq [lemma, in graphs.preliminaries]
last_take [lemma, in graphs.preliminaries]
le [projection, in graphs.open_confluence]
Le [abbreviation, in graphs.transfer]
Le [abbreviation, in graphs.transfer]
Le [abbreviation, in graphs.mgraph]
Le [abbreviation, in graphs.mgraph2]
le [projection, in graphs.structures]
Le [abbreviation, in graphs.reduction]
leq_subn [lemma, in graphs.preliminaries]
lift_equiv [lemma, in graphs.preliminaries]
lift_path [lemma, in graphs.preliminaries]
local_confluence [lemma, in graphs.open_confluence]
local_confluence_aux [lemma, in graphs.open_confluence]
local_confluence [lemma, in graphs.completeness]
lv [projection, in graphs.open_confluence]
Lv [abbreviation, in graphs.transfer]
Lv [abbreviation, in graphs.transfer]
Lv [abbreviation, in graphs.mgraph]
Lv [abbreviation, in graphs.mgraph2]
lv [projection, in graphs.structures]
Lv [abbreviation, in graphs.reduction]
lv_add_edge [lemma, in graphs.open_confluence]
lv_monoid [projection, in graphs.structures]

M

map_equivE [lemma, in graphs.finite_quotient]
map_equiv_class [lemma, in graphs.finite_quotient]
map_equiv_rel [definition, in graphs.finite_quotient]
map_equiv.e [variable, in graphs.finite_quotient]
map_equiv.h [variable, in graphs.finite_quotient]
map_equiv.T [variable, in graphs.finite_quotient]
map_equiv.S [variable, in graphs.finite_quotient]
map_equiv [section, in graphs.finite_quotient]
map_pairs [definition, in graphs.equiv]
map_pairs_id [lemma, in graphs.mgraph]
map_map_pairs [lemma, in graphs.mgraph]
MaxnL [constructor, in graphs.preliminaries]
maxnP [lemma, in graphs.preliminaries]
MaxnR [constructor, in graphs.preliminaries]
maxn_fsetD [lemma, in graphs.finmap_plus]
maxn_fset2 [lemma, in graphs.finmap_plus]
maxn_eq [lemma, in graphs.preliminaries]
maxn_cases [inductive, in graphs.preliminaries]
max_mono [lemma, in graphs.preliminaries]
measure [definition, in graphs.completeness]
memKset [lemma, in graphs.preliminaries]
mem_maxn [lemma, in graphs.finmap_plus]
mem_cover [lemma, in graphs.preliminaries]
mem_preim [lemma, in graphs.preliminaries]
mem_catD [lemma, in graphs.preliminaries]
mem_tail [lemma, in graphs.preliminaries]
mentions [definition, in graphs.reduction]
merge [definition, in graphs.mgraph]
MergeSubgraph [section, in graphs.mgraph]
MergeSubgraph.A [variable, in graphs.mgraph]
MergeSubgraph.con1 [variable, in graphs.mgraph]
MergeSubgraph.con2 [variable, in graphs.mgraph]
MergeSubgraph.disE [variable, in graphs.mgraph]
MergeSubgraph.eqvI [variable, in graphs.mgraph]
MergeSubgraph.E1 [variable, in graphs.mgraph]
MergeSubgraph.E2 [variable, in graphs.mgraph]
MergeSubgraph.G [variable, in graphs.mgraph]
MergeSubgraph.h [variable, in graphs.mgraph]
MergeSubgraph.V1 [variable, in graphs.mgraph]
MergeSubgraph.V2 [variable, in graphs.mgraph]
merge_unionE [lemma, in graphs.finite_quotient]
merge_union [definition, in graphs.finite_quotient]
merge_union_bwd_hom [lemma, in graphs.finite_quotient]
merge_union_fwd_hom [lemma, in graphs.finite_quotient]
merge_union_can' [lemma, in graphs.finite_quotient]
merge_union_can [lemma, in graphs.finite_quotient]
merge_union_rel [definition, in graphs.finite_quotient]
merge_disjoint_union [definition, in graphs.finite_quotient]
merge_disjoint_union_can' [lemma, in graphs.finite_quotient]
merge_disjoint_union_can [lemma, in graphs.finite_quotient]
merge_union_bwdEr [definition, in graphs.finite_quotient]
merge_union_bwdEl [definition, in graphs.finite_quotient]
merge_union_bwdP [lemma, in graphs.finite_quotient]
merge_union_bwdR [constructor, in graphs.finite_quotient]
merge_union_bwdL [constructor, in graphs.finite_quotient]
merge_union_bwd_spec [inductive, in graphs.finite_quotient]
merge_union_bwd [definition, in graphs.finite_quotient]
merge_union_fwd [definition, in graphs.finite_quotient]
merge_subgraph_isoE [lemma, in graphs.mgraph]
merge_subgraph_iso [definition, in graphs.mgraph]
merge_subgraph_hom [lemma, in graphs.mgraph]
merge_subgraph_e [definition, in graphs.mgraph]
merge_subgraph_v [definition, in graphs.mgraph]
merge_seq [abbreviation, in graphs.mgraph]
merge_union_KE [lemma, in graphs.mgraph]
merge_union_K [definition, in graphs.mgraph]
merge_add_vlabelE [lemma, in graphs.mgraph]
merge_add_vlabel [lemma, in graphs.mgraph]
merge_add_edgeE [lemma, in graphs.mgraph]
merge_add_edge [lemma, in graphs.mgraph]
merge_merge_seqE [lemma, in graphs.mgraph]
merge_merge_seq [definition, in graphs.mgraph]
merge_nothingE [lemma, in graphs.mgraph]
merge_nothing [definition, in graphs.mgraph]
merge_sameE [definition, in graphs.mgraph]
merge_same [definition, in graphs.mgraph]
merge_same'E [lemma, in graphs.mgraph]
merge_same' [definition, in graphs.mgraph]
merge_same'_hom [lemma, in graphs.mgraph]
merge_isoE [lemma, in graphs.mgraph]
merge_iso [definition, in graphs.mgraph]
merge_hom [lemma, in graphs.mgraph]
merge_mergeE [lemma, in graphs.mgraph]
merge_merge [lemma, in graphs.mgraph]
merge_nothing'E [lemma, in graphs.mgraph]
merge_nothing' [lemma, in graphs.mgraph]
merge_surjE [lemma, in graphs.mgraph]
merge_surj [lemma, in graphs.mgraph]
merge_seq [abbreviation, in graphs.mgraph]
merge_union_K_l [lemma, in graphs.mgraph2]
merge_merge [lemma, in graphs.mgraph2]
merge_nothing [lemma, in graphs.mgraph2]
merge_same' [lemma, in graphs.mgraph2]
merge_same [lemma, in graphs.mgraph2]
merge_iso2 [lemma, in graphs.mgraph2]
merge_step [lemma, in graphs.reduction]
merge_add_vlabelL [definition, in graphs.reduction]
merge_add_vertexLE [lemma, in graphs.reduction]
merge_add_vertexL [lemma, in graphs.reduction]
merge_add_edgeLE [lemma, in graphs.reduction]
merge_add_edgeL [lemma, in graphs.reduction]
merge2 [definition, in graphs.mgraph2]
merge2_seq [abbreviation, in graphs.mgraph2]
merge2_add_vlabel [lemma, in graphs.mgraph2]
merge2_add_edge [lemma, in graphs.mgraph2]
merge2_merge [lemma, in graphs.mgraph2]
merge2_nothing [lemma, in graphs.mgraph2]
merge2_same' [lemma, in graphs.mgraph2]
merge2_same [lemma, in graphs.mgraph2]
merge2_surj [lemma, in graphs.mgraph2]
merge2_iso2 [lemma, in graphs.mgraph2]
merge2_seq [abbreviation, in graphs.mgraph2]
mgraph [library]
mgraph2 [library]
monA [projection, in graphs.structures]
monC [projection, in graphs.structures]
monoidLaws [record, in graphs.structures]
MonoidLaws [constructor, in graphs.structures]
monU [projection, in graphs.structures]
monUl [lemma, in graphs.structures]
mon_eqv [projection, in graphs.structures]
mon0 [projection, in graphs.structures]
mon2 [projection, in graphs.structures]

N

nat_size_ind [lemma, in graphs.preliminaries]
Nopicks [constructor, in graphs.preliminaries]
normal_iso [lemma, in graphs.completeness]
normal_steps [lemma, in graphs.completeness]
notin_tail [lemma, in graphs.preliminaries]
nt [definition, in graphs.pttdom]
nterm [inductive, in graphs.pttdom]
nterm [abbreviation, in graphs.completeness]
nterm [abbreviation, in graphs.reduction]
nt_correct [lemma, in graphs.pttdom]
nt_par [definition, in graphs.pttdom]
nt_dot [definition, in graphs.pttdom]
nt_dom [definition, in graphs.pttdom]
nt_cnv [definition, in graphs.pttdom]
nt_var [definition, in graphs.pttdom]
nt_one [definition, in graphs.pttdom]
nt_conn [constructor, in graphs.pttdom]
nt_test [constructor, in graphs.pttdom]

O

oarc [definition, in graphs.open_confluence]
oarcxx_le [lemma, in graphs.open_confluence]
oarc_flip_edge [lemma, in graphs.open_confluence]
oarc_remove_vertex [lemma, in graphs.open_confluence]
oarc_remove_edges [lemma, in graphs.open_confluence]
oarc_added_edge [lemma, in graphs.open_confluence]
oarc_add_edge [lemma, in graphs.open_confluence]
oarc_eqv [lemma, in graphs.open_confluence]
oarc_loop [lemma, in graphs.open_confluence]
oarc_injR [lemma, in graphs.open_confluence]
oarc_injL [lemma, in graphs.open_confluence]
oarc_uniqeL [lemma, in graphs.open_confluence]
oarc_uniqeR [lemma, in graphs.open_confluence]
oarc_vsetR [lemma, in graphs.open_confluence]
oarc_vsetL [lemma, in graphs.open_confluence]
oarc_cases [lemma, in graphs.open_confluence]
oarc_edge_atR [lemma, in graphs.open_confluence]
oarc_edge_atL [lemma, in graphs.open_confluence]
oarc_cnv [lemma, in graphs.open_confluence]
oarc_morphism [instance, in graphs.open_confluence]
oiso_of [lemma, in graphs.transfer]
oiso2 [record, in graphs.transfer]
OIso2 [constructor, in graphs.transfer]
oiso2E [definition, in graphs.transfer]
oiso2_transE [lemma, in graphs.transfer]
oiso2_add_edgeE' [lemma, in graphs.transfer]
oiso2_add_edge' [lemma, in graphs.transfer]
oiso2_remove_edgesE [lemma, in graphs.transfer]
oiso2_remove_edges [lemma, in graphs.transfer]
oiso2_add_edge [lemma, in graphs.transfer]
oiso2_remove_vertex_ [lemma, in graphs.transfer]
oiso2_remove_vertexE [lemma, in graphs.transfer]
oiso2_remove_vertex [lemma, in graphs.transfer]
oiso2_add_testE [lemma, in graphs.transfer]
oiso2_add_test [lemma, in graphs.transfer]
oiso2_oarc [lemma, in graphs.transfer]
oiso2_edges_at [lemma, in graphs.transfer]
oiso2_incident [lemma, in graphs.transfer]
oiso2_le [lemma, in graphs.transfer]
oiso2_lv [lemma, in graphs.transfer]
oiso2_endpoint [lemma, in graphs.transfer]
oiso2_pIO_vfun [lemma, in graphs.transfer]
oiso2_pIO [lemma, in graphs.transfer]
oiso2_idE [lemma, in graphs.transfer]
oiso2_id [lemma, in graphs.transfer]
oiso2_output [lemma, in graphs.transfer]
oiso2_input [lemma, in graphs.transfer]
oiso2_vset [lemma, in graphs.transfer]
oiso2_Equivalence [instance, in graphs.transfer]
oiso2_sym [lemma, in graphs.transfer]
oiso2_trans [lemma, in graphs.transfer]
oiso2_iso [projection, in graphs.transfer]
oiso2_graphR [projection, in graphs.transfer]
oiso2_graphL [projection, in graphs.transfer]
one [projection, in graphs.pttdom]
one_test [lemma, in graphs.pttdom]
one_step [instance, in graphs.rewriting]
open [definition, in graphs.transfer]
Open [section, in graphs.transfer]
OpenGraphs [section, in graphs.open_confluence]
OpenGraphs.Le [variable, in graphs.open_confluence]
OpenGraphs.Lv [variable, in graphs.open_confluence]
openK [lemma, in graphs.transfer]
openKE [lemma, in graphs.transfer]
open_add_test [definition, in graphs.transfer]
open_add_edgeE [lemma, in graphs.transfer]
open_add_edge [lemma, in graphs.transfer]
open_add_vertexE [lemma, in graphs.transfer]
open_add_vertex [definition, in graphs.transfer]
open_is_graph [instance, in graphs.transfer]
open_confluence [library]
Open.G [variable, in graphs.transfer]
Open.L [variable, in graphs.transfer]
ops [projection, in graphs.pttdom]
ops [projection, in graphs.ptt]
ops_ [record, in graphs.pttdom]
option_void [definition, in graphs.bij]
option_sum_unit [lemma, in graphs.bij]
option_bij [definition, in graphs.bij]
option2x [definition, in graphs.bij]
option2_swap [definition, in graphs.bij]
orb_sum [lemma, in graphs.preliminaries]
ord_fresh [lemma, in graphs.preliminaries]
ord_size_enum [lemma, in graphs.preliminaries]
ord1 [definition, in graphs.preliminaries]
ord2 [definition, in graphs.preliminaries]
ord3 [definition, in graphs.preliminaries]
ostep [inductive, in graphs.open_confluence]
ostepL [lemma, in graphs.open_confluence]
osteps [inductive, in graphs.open_confluence]
osteps_graph [lemma, in graphs.open_confluence]
osteps_refl [lemma, in graphs.open_confluence]
osteps_preorder [instance, in graphs.open_confluence]
osteps_trans [constructor, in graphs.open_confluence]
osteps_iso [lemma, in graphs.transfer]
ostep_graph [lemma, in graphs.open_confluence]
ostep_step [constructor, in graphs.open_confluence]
ostep_e2 [constructor, in graphs.open_confluence]
ostep_e0 [constructor, in graphs.open_confluence]
ostep_v2 [constructor, in graphs.open_confluence]
ostep_v1 [constructor, in graphs.open_confluence]
ostep_v0 [constructor, in graphs.open_confluence]
ostep_of [lemma, in graphs.transfer]
ostep_of' [lemma, in graphs.transfer]
ostep_iso [lemma, in graphs.transfer]
output [projection, in graphs.mgraph2]

P

pack [definition, in graphs.transfer]
Pack [section, in graphs.transfer]
packK [lemma, in graphs.transfer]
pack_add_test [definition, in graphs.transfer]
pack_add_vertex [definition, in graphs.transfer]
pack_add_edge [lemma, in graphs.transfer]
pack_add_edge' [lemma, in graphs.transfer]
pack_v_IO [lemma, in graphs.transfer]
pack_irrelevance [lemma, in graphs.transfer]
pack_fsval [lemma, in graphs.transfer]
pack_vK [lemma, in graphs.transfer]
pack_vE [lemma, in graphs.transfer]
pack_v [definition, in graphs.transfer]
pack' [definition, in graphs.transfer]
Pack.G [variable, in graphs.transfer]
Pack.L [variable, in graphs.transfer]
pairs [definition, in graphs.equiv]
par [projection, in graphs.pttdom]
parA [projection, in graphs.pttdom]
paratst [lemma, in graphs.pttdom]
parA_ [projection, in graphs.ptt]
parC [projection, in graphs.pttdom]
parC_ [projection, in graphs.ptt]
pardot [lemma, in graphs.pttdom]
partition_big [lemma, in graphs.structures]
partopx [lemma, in graphs.ptt]
partst [lemma, in graphs.pttdom]
parxtop [lemma, in graphs.ptt]
par_nontest [lemma, in graphs.pttdom]
par_tst_cnv [lemma, in graphs.pttdom]
par_test [lemma, in graphs.pttdom]
par_eqv [projection, in graphs.pttdom]
par_eqv_ [projection, in graphs.ptt]
par_iso2 [instance, in graphs.mgraph2]
par_steps [instance, in graphs.reduction]
par_steps_r [lemma, in graphs.reduction]
par_steps_l [lemma, in graphs.reduction]
par_edges [lemma, in graphs.reduction]
par1tst [lemma, in graphs.pttdom]
par11 [projection, in graphs.pttdom]
par11_ [projection, in graphs.ptt]
par2A [lemma, in graphs.mgraph2]
par2C [lemma, in graphs.mgraph2]
par2dot [lemma, in graphs.mgraph2]
par2edgeunit [lemma, in graphs.mgraph2]
par2oneone [lemma, in graphs.mgraph2]
par2top [lemma, in graphs.mgraph2]
par2unitunit [lemma, in graphs.mgraph2]
path_restrict [lemma, in graphs.preliminaries]
pblock_eqvE [lemma, in graphs.preliminaries]
perm_index_enum [lemma, in graphs.bij]
perm_big [lemma, in graphs.structures]
pe_partition [definition, in graphs.preliminaries]
Picks [constructor, in graphs.preliminaries]
picksP [lemma, in graphs.preliminaries]
picks_spec [inductive, in graphs.preliminaries]
piK [lemma, in graphs.finite_quotient]
piK' [lemma, in graphs.finite_quotient]
pimset [definition, in graphs.preliminaries]
pimsetP [lemma, in graphs.preliminaries]
pimset_card [lemma, in graphs.preliminaries]
pIO [definition, in graphs.open_confluence]
pIO_add [definition, in graphs.open_confluence]
pIO_add_test [lemma, in graphs.open_confluence]
pIO_add_edge [lemma, in graphs.open_confluence]
pIO_add_vertex [lemma, in graphs.open_confluence]
pIO_fresh [lemma, in graphs.open_confluence]
pIO_No [lemma, in graphs.open_confluence]
pIO_Ni [lemma, in graphs.open_confluence]
piP [lemma, in graphs.finite_quotient]
PiSpec [constructor, in graphs.finite_quotient]
pi_surj [lemma, in graphs.finite_quotient]
pi_spec [inductive, in graphs.finite_quotient]
point [abbreviation, in graphs.mgraph2]
point [abbreviation, in graphs.mgraph2]
preim_omap_None [lemma, in graphs.preliminaries]
preim_omap_Some [lemma, in graphs.preliminaries]
prelim [section, in graphs.reduction]
preliminaries [library]
prelim.L [variable, in graphs.reduction]
PreOrder_steps [instance, in graphs.rewriting]
pre_graph [abbreviation, in graphs.open_confluence]
pre_graph [record, in graphs.open_confluence]
pre_graph [abbreviation, in graphs.transfer]
project_path [lemma, in graphs.preliminaries]
proj_v [definition, in graphs.transfer]
proj_e [definition, in graphs.transfer]
propers_ind [lemma, in graphs.preliminaries]
proper_ind [lemma, in graphs.preliminaries]
ptt [record, in graphs.ptt]
ptt [library]
pttdom [record, in graphs.pttdom]
pttdom [library]
PttdomGraphTheory [section, in graphs.open_confluence]
PttdomGraphTheory [section, in graphs.transfer]
PttdomGraphTheory.Open [section, in graphs.transfer]
PttdomGraphTheory.Open.G [variable, in graphs.transfer]
PttdomGraphTheory.ostep [section, in graphs.open_confluence]
PttdomGraphTheory.PreGraphOps [section, in graphs.open_confluence]
PttdomGraphTheory.PreGraphOps.G [variable, in graphs.open_confluence]
PttdomGraphTheory.PreGraphTheory [section, in graphs.open_confluence]
PttdomGraphTheory.PreGraphTheory.G [variable, in graphs.open_confluence]
PttdomGraphTheory.tm [variable, in graphs.open_confluence]
PttdomGraphTheory.tm [variable, in graphs.transfer]
_ [adt _ <- _ ] (open_scope) [notation, in graphs.open_confluence]
_ ∔ [ _ , _ , _ , _ ] (open_scope) [notation, in graphs.open_confluence]
_ ∔ [ _ , _ , _ ] (open_scope) [notation, in graphs.open_confluence]
_ - _ (open_scope) [notation, in graphs.open_confluence]
_ ∔ [ _ , _ ] (open_scope) [notation, in graphs.open_confluence]
_ \ _ (open_scope) [notation, in graphs.open_confluence]
_ ≡G _ [notation, in graphs.open_confluence]
_ ⩭2 _ [notation, in graphs.transfer]
src _ _ [notation, in graphs.open_confluence]
tgt _ _ [notation, in graphs.open_confluence]
p_outP [projection, in graphs.open_confluence]
p_inP [projection, in graphs.open_confluence]
p_out [projection, in graphs.open_confluence]
p_in [projection, in graphs.open_confluence]

Q

quot [module, in graphs.finite_quotient]
QUOT [module, in graphs.finite_quotient]
QuotBij [section, in graphs.finite_quotient]
QuotBij.e1 [variable, in graphs.finite_quotient]
QuotBij.e2 [variable, in graphs.finite_quotient]
QuotBij.h [variable, in graphs.finite_quotient]
QuotBij.h_inv_can [variable, in graphs.finite_quotient]
QuotBij.h_can [variable, in graphs.finite_quotient]
QuotBij.h_inv_homo [variable, in graphs.finite_quotient]
QuotBij.h_homo [variable, in graphs.finite_quotient]
QuotBij.h_inv [variable, in graphs.finite_quotient]
QuotBij.T1 [variable, in graphs.finite_quotient]
QuotBij.T2 [variable, in graphs.finite_quotient]
QuotFun [section, in graphs.finite_quotient]
QuotFun.e1 [variable, in graphs.finite_quotient]
QuotFun.e2 [variable, in graphs.finite_quotient]
QuotFun.h1 [variable, in graphs.finite_quotient]
QuotFun.T1 [variable, in graphs.finite_quotient]
QuotFun.T2 [variable, in graphs.finite_quotient]
quot_union_KE [lemma, in graphs.finite_quotient]
quot_union_K [definition, in graphs.finite_quotient]
quot_union_K.kh [variable, in graphs.finite_quotient]
quot_union_K.k [variable, in graphs.finite_quotient]
quot_union_K.e [variable, in graphs.finite_quotient]
quot_union_K.K [variable, in graphs.finite_quotient]
quot_union_K.S [variable, in graphs.finite_quotient]
quot_union_K [section, in graphs.finite_quotient]
quot_idE [lemma, in graphs.finite_quotient]
quot_id [definition, in graphs.finite_quotient]
quot_id.H [variable, in graphs.finite_quotient]
quot_id.e [variable, in graphs.finite_quotient]
quot_id.T [variable, in graphs.finite_quotient]
quot_id [section, in graphs.finite_quotient]
quot_quotE [lemma, in graphs.finite_quotient]
quot_quot [definition, in graphs.finite_quotient]
quot_quot.e' [variable, in graphs.finite_quotient]
quot_quot.e [variable, in graphs.finite_quotient]
quot_quot.T [variable, in graphs.finite_quotient]
quot_quot [section, in graphs.finite_quotient]
quot_bijE' [lemma, in graphs.finite_quotient]
quot_bijE [lemma, in graphs.finite_quotient]
quot_bij [definition, in graphs.finite_quotient]
quot_kernelE' [lemma, in graphs.finite_quotient]
quot_kernelE [lemma, in graphs.finite_quotient]
quot_kernel [definition, in graphs.finite_quotient]
quot_kernel_can' [lemma, in graphs.finite_quotient]
quot_kernel_can [lemma, in graphs.finite_quotient]
quot_kernel.Hf [variable, in graphs.finite_quotient]
quot_kernel.Hr [variable, in graphs.finite_quotient]
quot_kernel.f' [variable, in graphs.finite_quotient]
quot_kernel.f [variable, in graphs.finite_quotient]
quot_kernel.r [variable, in graphs.finite_quotient]
quot_kernel [section, in graphs.finite_quotient]
quot_sameE' [lemma, in graphs.finite_quotient]
quot_sameE [lemma, in graphs.finite_quotient]
quot_same [definition, in graphs.finite_quotient]
quot_fun_can [lemma, in graphs.finite_quotient]
quot_fun [definition, in graphs.finite_quotient]
quot.eqquotP [lemma, in graphs.finite_quotient]
QUOT.eqquotP [axiom, in graphs.finite_quotient]
quot.pi [definition, in graphs.finite_quotient]
QUOT.pi [axiom, in graphs.finite_quotient]
quot.quot [definition, in graphs.finite_quotient]
QUOT.quot [axiom, in graphs.finite_quotient]
quot.repr [definition, in graphs.finite_quotient]
QUOT.repr [axiom, in graphs.finite_quotient]
quot.reprK [lemma, in graphs.finite_quotient]
QUOT.reprK [axiom, in graphs.finite_quotient]
quot.s [section, in graphs.finite_quotient]
quot.s.e [variable, in graphs.finite_quotient]
quot.s.T [variable, in graphs.finite_quotient]

R

reduce [lemma, in graphs.reduction]
reduce_shuffle [lemma, in graphs.pttdom]
reduction [library]
reindex [lemma, in graphs.structures]
reindex_onto [lemma, in graphs.structures]
relabel [definition, in graphs.mgraph2]
relabel_edge [lemma, in graphs.mgraph2]
relabel_two [lemma, in graphs.mgraph2]
relabel_unit [lemma, in graphs.mgraph2]
relabel_add_edge [lemma, in graphs.mgraph2]
relabel_merge [lemma, in graphs.mgraph2]
relabel_union [lemma, in graphs.mgraph2]
relabel_iso [instance, in graphs.mgraph2]
relabel2 [definition, in graphs.mgraph2]
relabel2_var [lemma, in graphs.mgraph2]
relabel2_top [lemma, in graphs.mgraph2]
relabel2_one [lemma, in graphs.mgraph2]
relabel2_dom [lemma, in graphs.mgraph2]
relabel2_cnv [lemma, in graphs.mgraph2]
relabel2_par [lemma, in graphs.mgraph2]
relabel2_dot [lemma, in graphs.mgraph2]
relabel2_iso [instance, in graphs.mgraph2]
relU_sym' [lemma, in graphs.preliminaries]
rel_of_pairs_mapE [lemma, in graphs.equiv]
rel_of_pairs_map_eq [lemma, in graphs.equiv]
rel_of_pairs_mono [lemma, in graphs.equiv]
rel_of_pairs [definition, in graphs.equiv]
rel0 [abbreviation, in graphs.preliminaries]
rel0_sym [lemma, in graphs.preliminaries]
rel0_irrefl [lemma, in graphs.preliminaries]
remove_edges_vertexK [lemma, in graphs.open_confluence]
remove_edgeK [lemma, in graphs.open_confluence]
remove_edgesK [lemma, in graphs.open_confluence]
remove_vertexK [lemma, in graphs.open_confluence]
remove_vertex_morphism [instance, in graphs.open_confluence]
remove_edges_edges [lemma, in graphs.open_confluence]
remove_edges_vertex [lemma, in graphs.open_confluence]
remove_edges_add_test [lemma, in graphs.open_confluence]
remove_vertex_edges [lemma, in graphs.open_confluence]
remove_vertex_add_edge [lemma, in graphs.open_confluence]
remove_vertex_add_test [lemma, in graphs.open_confluence]
remove_vertexC [lemma, in graphs.open_confluence]
remove_edges_graph [instance, in graphs.open_confluence]
remove_edges0 [lemma, in graphs.open_confluence]
remove_edges [definition, in graphs.open_confluence]
remove_vertex_graph [instance, in graphs.open_confluence]
remove_vertex [definition, in graphs.open_confluence]
remove_edgesD [lemma, in graphs.transfer]
remove_vertex [definition, in graphs.mgraph]
remove_edges_sub [lemma, in graphs.mgraph]
remove_edges [definition, in graphs.mgraph]
replace_ioE [lemma, in graphs.reduction]
replace_ioL [definition, in graphs.reduction]
restrict [definition, in graphs.preliminaries]
restrictE [lemma, in graphs.preliminaries]
restrict_path [lemma, in graphs.preliminaries]
restrict_mono [lemma, in graphs.preliminaries]
rev_inj [lemma, in graphs.preliminaries]
rewriting [library]
rwT [lemma, in graphs.pttdom]

S

s [section, in graphs.completeness]
s [section, in graphs.rewriting]
s [section, in graphs.mgraph]
s [section, in graphs.mgraph2]
s [section, in graphs.reduction]
sameE [projection, in graphs.open_confluence]
sameV [projection, in graphs.open_confluence]
same_oarc [lemma, in graphs.open_confluence]
same_out [projection, in graphs.open_confluence]
same_in [projection, in graphs.open_confluence]
same_endpt [projection, in graphs.open_confluence]
sc [definition, in graphs.preliminaries]
sc_eq [lemma, in graphs.preliminaries]
sc_sym [lemma, in graphs.preliminaries]
setN01E [lemma, in graphs.preliminaries]
setoid [record, in graphs.structures]
Setoid [constructor, in graphs.structures]
setoid_of_ops [projection, in graphs.pttdom]
setT_bij [definition, in graphs.bij]
setT_bij_hom [lemma, in graphs.mgraph]
setU_dec [lemma, in graphs.finite_quotient]
setU1_neq [lemma, in graphs.preliminaries]
setU1_mem [lemma, in graphs.preliminaries]
set1_inj [lemma, in graphs.preliminaries]
set10 [lemma, in graphs.preliminaries]
set2C [lemma, in graphs.preliminaries]
sig [abbreviation, in graphs.finite_quotient]
sig_sum_bij.NonDisjoint.eqvI [variable, in graphs.finite_quotient]
sig_sum_bij.NonDisjoint.e [variable, in graphs.finite_quotient]
sig_sum_bij.NonDisjoint [section, in graphs.finite_quotient]
sig_sum_bij.Disjoint.disUV [variable, in graphs.finite_quotient]
sig_sum_bij.Disjoint [section, in graphs.finite_quotient]
sig_sum_bij.V [variable, in graphs.finite_quotient]
sig_sum_bij.U [variable, in graphs.finite_quotient]
sig_sum_bij.T [variable, in graphs.finite_quotient]
sig_sum_bij [section, in graphs.finite_quotient]
size_ind [definition, in graphs.preliminaries]
smallest [definition, in graphs.preliminaries]
Some_eqE [lemma, in graphs.preliminaries]
soundness_and_completeness [lemma, in graphs.completeness]
source [abbreviation, in graphs.mgraph]
source [abbreviation, in graphs.mgraph]
step [abbreviation, in graphs.completeness]
step [inductive, in graphs.rewriting]
step [abbreviation, in graphs.reduction]
step [abbreviation, in graphs.reduction]
steps [abbreviation, in graphs.completeness]
steps [inductive, in graphs.rewriting]
steps [abbreviation, in graphs.reduction]
steps [abbreviation, in graphs.reduction]
steps_of [lemma, in graphs.transfer]
steps_of_ostep [lemma, in graphs.transfer]
steps_refl [lemma, in graphs.rewriting]
step_order [definition, in graphs.open_confluence]
step_decreases [lemma, in graphs.completeness]
step_e2 [constructor, in graphs.rewriting]
step_e0 [constructor, in graphs.rewriting]
step_v2 [constructor, in graphs.rewriting]
step_v1 [constructor, in graphs.rewriting]
step_v0 [constructor, in graphs.rewriting]
step_to_steps [lemma, in graphs.reduction]
step_IO [lemma, in graphs.reduction]
structures [library]
subgraph [definition, in graphs.mgraph]
subgraph_sub [lemma, in graphs.mgraph]
subgraph_for [definition, in graphs.mgraph]
subgraph_for_iso [lemma, in graphs.mgraph2]
subrelP [lemma, in graphs.preliminaries]
subrel_restrict [lemma, in graphs.preliminaries]
subset_tl [lemma, in graphs.equiv]
subset_catR [lemma, in graphs.equiv]
subset_catL [lemma, in graphs.equiv]
subset_seqL [lemma, in graphs.preliminaries]
subset_seqR [lemma, in graphs.preliminaries]
subset_cons [lemma, in graphs.preliminaries]
subT_bij [definition, in graphs.bij]
Sub_endpt [lemma, in graphs.transfer]
sub_edge [definition, in graphs.mgraph]
sub_vertex [definition, in graphs.mgraph]
sub_equiv_of [lemma, in graphs.preliminaries]
sub_restrict_connect [lemma, in graphs.preliminaries]
sub_trans [lemma, in graphs.preliminaries]
sub_connect [lemma, in graphs.preliminaries]
sub_in11W [lemma, in graphs.preliminaries]
sub_val_eq [lemma, in graphs.preliminaries]
sumA [definition, in graphs.bij]
sumA' [definition, in graphs.bij]
sumC [definition, in graphs.bij]
sumf [definition, in graphs.bij]
sumUx [lemma, in graphs.bij]
sumxU [lemma, in graphs.bij]
sum_left [definition, in graphs.finite_quotient]
sum_option_r [lemma, in graphs.bij]
sum_option_l [lemma, in graphs.bij]
sum_bij [instance, in graphs.bij]
sum_eqE [definition, in graphs.preliminaries]
surjective [definition, in graphs.preliminaries]
surj_repr_pi [lemma, in graphs.finite_quotient]
symmetric_restrict [lemma, in graphs.preliminaries]
s' [section, in graphs.reduction]
s'.A [variable, in graphs.reduction]
s.A [variable, in graphs.completeness]
s.a [section, in graphs.reduction]
s.a.A [variable, in graphs.reduction]
s.a.a [variable, in graphs.reduction]
s.a.G [variable, in graphs.reduction]
s.a.H [variable, in graphs.reduction]
s.a.l [variable, in graphs.reduction]
s.Edges [section, in graphs.mgraph]
s.Edges.G [variable, in graphs.mgraph]
s.h_merge_nothing'.H [variable, in graphs.mgraph]
s.h_merge_nothing'.r [variable, in graphs.mgraph]
s.h_merge_nothing'.F [variable, in graphs.mgraph]
s.h_merge_nothing' [section, in graphs.mgraph]
s.L [variable, in graphs.mgraph]
s.L [variable, in graphs.mgraph2]
s.merge [section, in graphs.mgraph]
s.merge_union_K.ke [variable, in graphs.mgraph]
s.merge_union_K.kh [variable, in graphs.mgraph]
s.merge_union_K.kv [variable, in graphs.mgraph]
s.merge_union_K.k [variable, in graphs.mgraph]
s.merge_union_K.h [variable, in graphs.mgraph]
s.merge_union_K.K [variable, in graphs.mgraph]
s.merge_union_K.F [variable, in graphs.mgraph]
s.merge_union_K [section, in graphs.mgraph]
s.merge_merge_seq.kk' [variable, in graphs.mgraph]
s.merge_merge_seq.k' [variable, in graphs.mgraph]
s.merge_merge_seq.k [variable, in graphs.mgraph]
s.merge_merge_seq.h [variable, in graphs.mgraph]
s.merge_merge_seq.F [variable, in graphs.mgraph]
s.merge_merge_seq [section, in graphs.mgraph]
s.merge_nothing.H [variable, in graphs.mgraph]
s.merge_nothing.h [variable, in graphs.mgraph]
s.merge_nothing.F [variable, in graphs.mgraph]
s.merge_nothing [section, in graphs.mgraph]
s.merge_same.H [variable, in graphs.mgraph]
s.merge_same.k [variable, in graphs.mgraph]
s.merge_same.h [variable, in graphs.mgraph]
s.merge_same.F [variable, in graphs.mgraph]
s.merge_same [section, in graphs.mgraph]
s.merge_same'.H [variable, in graphs.mgraph]
s.merge_same'.k [variable, in graphs.mgraph]
s.merge_same'.h [variable, in graphs.mgraph]
s.merge_same'.F [variable, in graphs.mgraph]
s.merge_same' [section, in graphs.mgraph]
s.merge_merge.e' [variable, in graphs.mgraph]
s.merge_merge.e [variable, in graphs.mgraph]
s.merge_merge.F [variable, in graphs.mgraph]
s.merge_merge [section, in graphs.mgraph]
s.merge_surj.Hvlabel [variable, in graphs.mgraph]
s.merge_surj.Helabel [variable, in graphs.mgraph]
s.merge_surj.Hendpoints [variable, in graphs.mgraph]
s.merge_surj.Hsurj [variable, in graphs.mgraph]
s.merge_surj.Hr [variable, in graphs.mgraph]
s.merge_surj.fe [variable, in graphs.mgraph]
s.merge_surj.fv' [variable, in graphs.mgraph]
s.merge_surj.fv [variable, in graphs.mgraph]
s.merge_surj.H [variable, in graphs.mgraph]
s.merge_surj.r [variable, in graphs.mgraph]
s.merge_surj.G [variable, in graphs.mgraph]
s.merge_surj [section, in graphs.mgraph]
s.merge.F [variable, in graphs.mgraph]
s.merge.G [variable, in graphs.mgraph]
s.merge.h [variable, in graphs.mgraph]
s.merge.l [variable, in graphs.mgraph]
s.Subgraphs [section, in graphs.mgraph]
s.Subgraphs.E [variable, in graphs.mgraph]
s.Subgraphs.G [variable, in graphs.mgraph]
s.Subgraphs.in_V [variable, in graphs.mgraph]
s.Subgraphs.V [variable, in graphs.mgraph]
s.union_merge_r.l [variable, in graphs.mgraph]
s.union_merge_r.G [variable, in graphs.mgraph]
s.union_merge_r.F [variable, in graphs.mgraph]
s.union_merge_r [section, in graphs.mgraph]
s.union_merge_l.l [variable, in graphs.mgraph]
s.union_merge_l.G [variable, in graphs.mgraph]
s.union_merge_l.F [variable, in graphs.mgraph]
s.union_merge_l [section, in graphs.mgraph]
s.X [variable, in graphs.rewriting]
s.X [variable, in graphs.reduction]
_ .d [notation, in graphs.mgraph]
_ .e [notation, in graphs.mgraph]
_ ≃ _ [notation, in graphs.mgraph]
_ ∔ _ [notation, in graphs.mgraph]
_ ⊎ _ [notation, in graphs.mgraph]
_ [tst _ <- _ ] [notation, in graphs.mgraph]
_ ∔ [ _ , _ , _ ] [notation, in graphs.mgraph]
_ ≃2p _ [notation, in graphs.mgraph2]
_ ≃2 _ [notation, in graphs.mgraph2]
_ [tst _ <- _ ] [notation, in graphs.mgraph2]
_ ∔ [ _ , _ , _ ] [notation, in graphs.mgraph2]
_ ∔ _ [notation, in graphs.mgraph2]

T

t [section, in graphs.finite_quotient]
take_find [lemma, in graphs.preliminaries]
target [abbreviation, in graphs.mgraph]
target [abbreviation, in graphs.mgraph]
term [inductive, in graphs.pttdom]
term [abbreviation, in graphs.completeness]
term [inductive, in graphs.ptt]
term [abbreviation, in graphs.reduction]
terms [section, in graphs.pttdom]
terms [section, in graphs.ptt]
terms.A [variable, in graphs.pttdom]
terms.A [variable, in graphs.ptt]
terms.e [section, in graphs.pttdom]
terms.e [section, in graphs.ptt]
terms.e.f [variable, in graphs.pttdom]
terms.e.f [variable, in graphs.ptt]
terms.e.X [variable, in graphs.pttdom]
terms.e.X [variable, in graphs.ptt]
term_of_nterm [definition, in graphs.pttdom]
test [abbreviation, in graphs.open_confluence]
test [abbreviation, in graphs.pttdom]
test [record, in graphs.pttdom]
Test [constructor, in graphs.pttdom]
test [abbreviation, in graphs.transfer]
test [abbreviation, in graphs.completeness]
test [abbreviation, in graphs.rewriting]
test [abbreviation, in graphs.reduction]
test [abbreviation, in graphs.reduction]
testE [projection, in graphs.pttdom]
tgraph [abbreviation, in graphs.completeness]
tgraph [abbreviation, in graphs.reduction]
tgraph_graph_iso [lemma, in graphs.completeness]
tgraph_graph [lemma, in graphs.completeness]
tgraph_of_nterm [definition, in graphs.reduction]
tgraph_of_term [definition, in graphs.reduction]
tgraph2 [abbreviation, in graphs.completeness]
tgraph2 [abbreviation, in graphs.reduction]
Theory [section, in graphs.structures]
Theory.mon0 [variable, in graphs.structures]
Theory.mon2 [variable, in graphs.structures]
Theory.X [variable, in graphs.structures]
_ ⊗ _ [notation, in graphs.structures]
1 [notation, in graphs.structures]
tm_inh_type [instance, in graphs.open_confluence]
tm_pttdom [definition, in graphs.pttdom]
tm_eqv_equivalence [lemma, in graphs.pttdom]
tm_eqv [definition, in graphs.pttdom]
tm_var [constructor, in graphs.pttdom]
tm_one [constructor, in graphs.pttdom]
tm_dom [constructor, in graphs.pttdom]
tm_cnv [constructor, in graphs.pttdom]
tm_par [constructor, in graphs.pttdom]
tm_dot [constructor, in graphs.pttdom]
tm_ptt [definition, in graphs.ptt]
tm_eqv_equivalence [lemma, in graphs.ptt]
tm_eqv [definition, in graphs.ptt]
tm_var [constructor, in graphs.ptt]
tm_top [constructor, in graphs.ptt]
tm_one [constructor, in graphs.ptt]
tm_dom [constructor, in graphs.ptt]
tm_cnv [constructor, in graphs.ptt]
tm_par [constructor, in graphs.ptt]
tm_dot [constructor, in graphs.ptt]
tnth_cons [lemma, in graphs.preliminaries]
tnth_map_in [lemma, in graphs.preliminaries]
tnth_uniq [lemma, in graphs.preliminaries]
top [projection, in graphs.pttdom]
topL [lemma, in graphs.mgraph2]
topR [lemma, in graphs.mgraph2]
transfer [library]
trivIset3 [lemma, in graphs.preliminaries]
tstpar [lemma, in graphs.pttdom]
tstpar1 [lemma, in graphs.pttdom]
tst_dotU [lemma, in graphs.pttdom]
tst_dotC [lemma, in graphs.pttdom]
tst_dotA [lemma, in graphs.pttdom]
tst_dot_eqv [lemma, in graphs.pttdom]
two_graph_swap [lemma, in graphs.mgraph]
two_graph [definition, in graphs.mgraph]
two_graph2_iso [instance, in graphs.mgraph2]
two_graph2 [definition, in graphs.mgraph2]
two_option_void' [definition, in graphs.reduction]
two_option_void [definition, in graphs.reduction]
two_edges [lemma, in graphs.reduction]
t.e [variable, in graphs.finite_quotient]
t.f [variable, in graphs.finite_quotient]
t.H [variable, in graphs.finite_quotient]
t.S [variable, in graphs.finite_quotient]

U

union [definition, in graphs.mgraph]
union_bij_proofR [lemma, in graphs.finite_quotient]
union_bij_proofL [lemma, in graphs.finite_quotient]
union_K_equiv [definition, in graphs.finite_quotient]
union_quot_rEl [lemma, in graphs.finite_quotient]
union_quot_rEr [lemma, in graphs.finite_quotient]
union_quot_r [definition, in graphs.finite_quotient]
union_equiv_r [definition, in graphs.finite_quotient]
union_quot_r.e [variable, in graphs.finite_quotient]
union_quot_r.T [variable, in graphs.finite_quotient]
union_quot_r.S [variable, in graphs.finite_quotient]
union_quot_r [section, in graphs.finite_quotient]
union_quot_lE' [lemma, in graphs.finite_quotient]
union_quot_lEr [lemma, in graphs.finite_quotient]
union_quot_lEl [lemma, in graphs.finite_quotient]
union_quot_l [definition, in graphs.finite_quotient]
union_equiv_l_class [lemma, in graphs.finite_quotient]
union_equiv_l_rel [definition, in graphs.finite_quotient]
union_quot_l.e [variable, in graphs.finite_quotient]
union_quot_l.T [variable, in graphs.finite_quotient]
union_quot_l.S [variable, in graphs.finite_quotient]
union_quot_l [section, in graphs.finite_quotient]
union_K_pairs [definition, in graphs.mgraph]
union_merge_rEl [lemma, in graphs.mgraph]
union_merge_rEr [lemma, in graphs.mgraph]
union_merge_r [lemma, in graphs.mgraph]
union_merge_lE' [lemma, in graphs.mgraph]
union_merge_lEr [lemma, in graphs.mgraph]
union_merge_lEl [lemma, in graphs.mgraph]
union_merge_l [definition, in graphs.mgraph]
union_equiv_l_eqv_clot [lemma, in graphs.mgraph]
union_add_vlabel_r [lemma, in graphs.mgraph]
union_add_vlabel_l [lemma, in graphs.mgraph]
union_add_edge_r [lemma, in graphs.mgraph]
union_add_edge_l [lemma, in graphs.mgraph]
union_A [lemma, in graphs.mgraph]
union_C [lemma, in graphs.mgraph]
union_iso [instance, in graphs.mgraph]
unique [definition, in graphs.preliminaries]
uniq_take [lemma, in graphs.preliminaries]
unit_graph_iso [instance, in graphs.mgraph]
unit_graph [definition, in graphs.mgraph]
unit_graph2_iso [instance, in graphs.mgraph2]
unit_graph2 [definition, in graphs.mgraph2]
unl [definition, in graphs.mgraph]
unr [definition, in graphs.mgraph]
update [definition, in graphs.preliminaries]
update [section, in graphs.preliminaries]
updateE [definition, in graphs.preliminaries]
update_fx [lemma, in graphs.preliminaries]
update_same [lemma, in graphs.preliminaries]
update_eq [lemma, in graphs.preliminaries]
update_neq [lemma, in graphs.preliminaries]
update.aT [variable, in graphs.preliminaries]
update.f [variable, in graphs.preliminaries]
update.rT [variable, in graphs.preliminaries]

V

valK' [lemma, in graphs.preliminaries]
valK'' [lemma, in graphs.preliminaries]
vertex [projection, in graphs.mgraph]
vfun [abbreviation, in graphs.preliminaries]
vfun_of_inj [lemma, in graphs.transfer]
vfun_bodyEinj [lemma, in graphs.transfer]
vfun_bodyE [lemma, in graphs.transfer]
vfun_of [definition, in graphs.transfer]
vfun_body [definition, in graphs.transfer]
vlabel [projection, in graphs.mgraph]
vlabel_iso' [lemma, in graphs.mgraph]
vlabel_iso [lemma, in graphs.mgraph]
vlabel_hom [projection, in graphs.mgraph]
void [inductive, in graphs.preliminaries]
void_graph [definition, in graphs.mgraph]
void_enumP [lemma, in graphs.preliminaries]
void_countMixin [definition, in graphs.preliminaries]
void_choiceMixin [definition, in graphs.preliminaries]
void_pcancel [lemma, in graphs.preliminaries]
void_eqP [lemma, in graphs.preliminaries]
vset [projection, in graphs.open_confluence]
vset_add_vertex [lemma, in graphs.transfer]
VT [definition, in graphs.open_confluence]
VT_inh_type [instance, in graphs.transfer]

W

WeqG [constructor, in graphs.open_confluence]
wf_propers [lemma, in graphs.preliminaries]
wf_proper [lemma, in graphs.preliminaries]
wf_leq [lemma, in graphs.preliminaries]

other

_ ==> _ (csignature) [notation, in graphs.structures]
_ [tst _ <- _ ] (graph_scope) [notation, in graphs.mgraph]
_ ∔ _ (graph_scope) [notation, in graphs.mgraph]
_ ∔ [ _ , _ , _ ] (graph_scope) [notation, in graphs.mgraph]
_ ⊎ _ (graph_scope) [notation, in graphs.mgraph]
_ [tst _ <- _ ] (graph2_scope) [notation, in graphs.mgraph2]
_ ∔ _ (graph2_scope) [notation, in graphs.mgraph2]
_ ∔ [ _ , _ , _ ] (graph2_scope) [notation, in graphs.mgraph2]
_ ⊗ _ (labels) [notation, in graphs.structures]
1 (labels) [notation, in graphs.structures]
_ [adt _ <- _ ] (open_scope) [notation, in graphs.open_confluence]
_ ∔ [ _ , _ , _ , _ ] (open_scope) [notation, in graphs.open_confluence]
_ ∔ [ _ , _ , _ ] (open_scope) [notation, in graphs.open_confluence]
_ - _ (open_scope) [notation, in graphs.open_confluence]
_ ∔ [ _ , _ ] (open_scope) [notation, in graphs.open_confluence]
_ \ _ (open_scope) [notation, in graphs.open_confluence]
[ _ ] (pttdom_ops) [notation, in graphs.pttdom]
1 (pttdom_ops) [notation, in graphs.pttdom]
_ ° (pttdom_ops) [notation, in graphs.pttdom]
_ · _ (pttdom_ops) [notation, in graphs.pttdom]
_ ∥ _ (pttdom_ops) [notation, in graphs.pttdom]
_ @^-1 _ (set_scope) [notation, in graphs.preliminaries]
_ ≡G _ [notation, in graphs.open_confluence]
_ == _ %[mod _ ] [notation, in graphs.finite_quotient]
_ = _ %[mod _ ] [notation, in graphs.finite_quotient]
_ ^-1 [notation, in graphs.bij]
_ .d [notation, in graphs.mgraph]
_ .e [notation, in graphs.mgraph]
_ ≃ _ [notation, in graphs.mgraph]
_ ≃2p _ [notation, in graphs.mgraph2]
_ ≃2 _ [notation, in graphs.mgraph2]
_ ≡[ _ ] _ [notation, in graphs.structures]
_ ≡' _ [notation, in graphs.structures]
_ ≡ _ [notation, in graphs.structures]
_ [upd _ := _ ] [notation, in graphs.preliminaries]
[ disjoint3 _ & _ & _ ] [notation, in graphs.preliminaries]
\pi _ [notation, in graphs.finite_quotient]
Σ _ .. _ , _ [notation, in graphs.preliminaries]

---

Notation Index

D

[ _ ] [in graphs.pttdom]

P

_ [adt _ <- _ ] (open_scope) [in graphs.open_confluence]
_ ∔ [ _ , _ , _ , _ ] (open_scope) [in graphs.open_confluence]
_ ∔ [ _ , _ , _ ] (open_scope) [in graphs.open_confluence]
_ - _ (open_scope) [in graphs.open_confluence]
_ ∔ [ _ , _ ] (open_scope) [in graphs.open_confluence]
_ \ _ (open_scope) [in graphs.open_confluence]
_ ≡G _ [in graphs.open_confluence]
_ ⩭2 _ [in graphs.transfer]
src _ _ [in graphs.open_confluence]
tgt _ _ [in graphs.open_confluence]

S

_ .d [in graphs.mgraph]
_ .e [in graphs.mgraph]
_ ≃ _ [in graphs.mgraph]
_ ∔ _ [in graphs.mgraph]
_ ⊎ _ [in graphs.mgraph]
_ [tst _ <- _ ] [in graphs.mgraph]
_ ∔ [ _ , _ , _ ] [in graphs.mgraph]
_ ≃2p _ [in graphs.mgraph2]
_ ≃2 _ [in graphs.mgraph2]
_ [tst _ <- _ ] [in graphs.mgraph2]
_ ∔ [ _ , _ , _ ] [in graphs.mgraph2]
_ ∔ _ [in graphs.mgraph2]

T

_ ⊗ _ [in graphs.structures]
1 [in graphs.structures]

other

_ ==> _ (csignature) [in graphs.structures]
_ [tst _ <- _ ] (graph_scope) [in graphs.mgraph]
_ ∔ _ (graph_scope) [in graphs.mgraph]
_ ∔ [ _ , _ , _ ] (graph_scope) [in graphs.mgraph]
_ ⊎ _ (graph_scope) [in graphs.mgraph]
_ [tst _ <- _ ] (graph2_scope) [in graphs.mgraph2]
_ ∔ _ (graph2_scope) [in graphs.mgraph2]
_ ∔ [ _ , _ , _ ] (graph2_scope) [in graphs.mgraph2]
_ ⊗ _ (labels) [in graphs.structures]
1 (labels) [in graphs.structures]
_ [adt _ <- _ ] (open_scope) [in graphs.open_confluence]
_ ∔ [ _ , _ , _ , _ ] (open_scope) [in graphs.open_confluence]
_ ∔ [ _ , _ , _ ] (open_scope) [in graphs.open_confluence]
_ - _ (open_scope) [in graphs.open_confluence]
_ ∔ [ _ , _ ] (open_scope) [in graphs.open_confluence]
_ \ _ (open_scope) [in graphs.open_confluence]
[ _ ] (pttdom_ops) [in graphs.pttdom]
1 (pttdom_ops) [in graphs.pttdom]
_ ° (pttdom_ops) [in graphs.pttdom]
_ · _ (pttdom_ops) [in graphs.pttdom]
_ ∥ _ (pttdom_ops) [in graphs.pttdom]
_ @^-1 _ (set_scope) [in graphs.preliminaries]
_ ≡G _ [in graphs.open_confluence]
_ == _ %[mod _ ] [in graphs.finite_quotient]
_ = _ %[mod _ ] [in graphs.finite_quotient]
_ ^-1 [in graphs.bij]
_ .d [in graphs.mgraph]
_ .e [in graphs.mgraph]
_ ≃ _ [in graphs.mgraph]
_ ≃2p _ [in graphs.mgraph2]
_ ≃2 _ [in graphs.mgraph2]
_ ≡[ _ ] _ [in graphs.structures]
_ ≡' _ [in graphs.structures]
_ ≡ _ [in graphs.structures]
_ [upd _ := _ ] [in graphs.preliminaries]
[ disjoint3 _ & _ & _ ] [in graphs.preliminaries]
\pi _ [in graphs.finite_quotient]
Σ _ .. _ , _ [in graphs.preliminaries]

---

Module Index

Q

quot [in graphs.finite_quotient]
QUOT [in graphs.finite_quotient]

---

Variable Index

B

BijCast.A [in graphs.finmap_plus]
BijCast.A' [in graphs.finmap_plus]
BijCast.eqA [in graphs.finmap_plus]
BijCast.T [in graphs.finmap_plus]
BijD1.T [in graphs.bij]
BijD1.z [in graphs.bij]
BijT.inP [in graphs.bij]
BijT.P [in graphs.bij]
BijT.T [in graphs.bij]
Bij.g [in graphs.finmap_plus]
Bij.G [in graphs.finmap_plus]
Bij.g_inj [in graphs.finmap_plus]
Bij.T [in graphs.finmap_plus]
Bij.vset [in graphs.finmap_plus]
b.e [in graphs.finite_quotient]
b.h [in graphs.finite_quotient]
b.S [in graphs.finite_quotient]
b.T [in graphs.finite_quotient]

C

CProper.A [in graphs.structures]
CProper.B [in graphs.structures]
CProper.C [in graphs.structures]
CProper.f [in graphs.structures]
CProper.g [in graphs.structures]
CProper.Hf [in graphs.structures]
CProper.Hg [in graphs.structures]
CProper.R [in graphs.structures]
CProper.S [in graphs.structures]
CProper.T [in graphs.structures]

D

derived.X [in graphs.pttdom]
derived.X [in graphs.ptt]
Disjoint3.A [in graphs.preliminaries]
Disjoint3.B [in graphs.preliminaries]
Disjoint3.C [in graphs.preliminaries]
Disjoint3.T [in graphs.preliminaries]

E

Equivalence.e [in graphs.preliminaries]
Equivalence.T [in graphs.preliminaries]
eqv_inj.f_inj [in graphs.equiv]
eqv_inj.eq2E [in graphs.equiv]
eqv_inj.eq_e [in graphs.equiv]
eqv_inj.f [in graphs.equiv]
eqv_inj.e2 [in graphs.equiv]
eqv_inj.e1 [in graphs.equiv]
eqv_inj.T2 [in graphs.equiv]
eqv_inj.T1 [in graphs.equiv]

F

FinEncodingModuloRel.C [in graphs.finite_quotient]
FinEncodingModuloRel.CD [in graphs.finite_quotient]
FinEncodingModuloRel.D [in graphs.finite_quotient]
FinEncodingModuloRel.DC [in graphs.finite_quotient]
FinEncodingModuloRel.eD [in graphs.finite_quotient]
FinEncodingModuloRel.encD [in graphs.finite_quotient]
Foldr1.F [in graphs.preliminaries]
Foldr1.I [in graphs.preliminaries]
Foldr1.op [in graphs.preliminaries]
Foldr1.R [in graphs.preliminaries]
Fresh2Bij.A [in graphs.finmap_plus]
Fresh2Bij.B [in graphs.finmap_plus]
Fresh2Bij.f [in graphs.finmap_plus]
Fresh2Bij.Hx [in graphs.finmap_plus]
Fresh2Bij.Hy [in graphs.finmap_plus]
Fresh2Bij.T [in graphs.finmap_plus]
Fresh2Bij.x [in graphs.finmap_plus]
Fresh2Bij.y [in graphs.finmap_plus]
fsetD_bij.E [in graphs.finmap_plus]
fsetD_bij.f [in graphs.finmap_plus]
fsetD_bij.C' [in graphs.finmap_plus]
fsetD_bij.C [in graphs.finmap_plus]
fsetD_bij.B [in graphs.finmap_plus]
fsetD_bij.A [in graphs.finmap_plus]
fsetD_bij.T [in graphs.finmap_plus]
FsetU1Fun.A [in graphs.finmap_plus]
FsetU1Fun.B [in graphs.finmap_plus]
FsetU1Fun.f [in graphs.finmap_plus]
FsetU1Fun.T [in graphs.finmap_plus]
FsetU1Fun.x [in graphs.finmap_plus]
FsetU1Fun.y [in graphs.finmap_plus]

H

h.fe [in graphs.mgraph2]
h.fv [in graphs.mgraph2]
h.Hfe [in graphs.mgraph2]
h.Hfv [in graphs.mgraph2]
h.Hfvmon0 [in graphs.mgraph2]
h.Hfvmon2 [in graphs.mgraph2]
h.X [in graphs.mgraph2]
h.Y [in graphs.mgraph2]

I

inject.T [in graphs.transfer]

M

map_equiv.e [in graphs.finite_quotient]
map_equiv.h [in graphs.finite_quotient]
map_equiv.T [in graphs.finite_quotient]
map_equiv.S [in graphs.finite_quotient]
MergeSubgraph.A [in graphs.mgraph]
MergeSubgraph.con1 [in graphs.mgraph]
MergeSubgraph.con2 [in graphs.mgraph]
MergeSubgraph.disE [in graphs.mgraph]
MergeSubgraph.eqvI [in graphs.mgraph]
MergeSubgraph.E1 [in graphs.mgraph]
MergeSubgraph.E2 [in graphs.mgraph]
MergeSubgraph.G [in graphs.mgraph]
MergeSubgraph.h [in graphs.mgraph]
MergeSubgraph.V1 [in graphs.mgraph]
MergeSubgraph.V2 [in graphs.mgraph]

O

OpenGraphs.Le [in graphs.open_confluence]
OpenGraphs.Lv [in graphs.open_confluence]
Open.G [in graphs.transfer]
Open.L [in graphs.transfer]

P

Pack.G [in graphs.transfer]
Pack.L [in graphs.transfer]
prelim.L [in graphs.reduction]
PttdomGraphTheory.Open.G [in graphs.transfer]
PttdomGraphTheory.PreGraphOps.G [in graphs.open_confluence]
PttdomGraphTheory.PreGraphTheory.G [in graphs.open_confluence]
PttdomGraphTheory.tm [in graphs.open_confluence]
PttdomGraphTheory.tm [in graphs.transfer]

Q

QuotBij.e1 [in graphs.finite_quotient]
QuotBij.e2 [in graphs.finite_quotient]
QuotBij.h [in graphs.finite_quotient]
QuotBij.h_inv_can [in graphs.finite_quotient]
QuotBij.h_can [in graphs.finite_quotient]
QuotBij.h_inv_homo [in graphs.finite_quotient]
QuotBij.h_homo [in graphs.finite_quotient]
QuotBij.h_inv [in graphs.finite_quotient]
QuotBij.T1 [in graphs.finite_quotient]
QuotBij.T2 [in graphs.finite_quotient]
QuotFun.e1 [in graphs.finite_quotient]
QuotFun.e2 [in graphs.finite_quotient]
QuotFun.h1 [in graphs.finite_quotient]
QuotFun.T1 [in graphs.finite_quotient]
QuotFun.T2 [in graphs.finite_quotient]
quot_union_K.kh [in graphs.finite_quotient]
quot_union_K.k [in graphs.finite_quotient]
quot_union_K.e [in graphs.finite_quotient]
quot_union_K.K [in graphs.finite_quotient]
quot_union_K.S [in graphs.finite_quotient]
quot_id.H [in graphs.finite_quotient]
quot_id.e [in graphs.finite_quotient]
quot_id.T [in graphs.finite_quotient]
quot_quot.e' [in graphs.finite_quotient]
quot_quot.e [in graphs.finite_quotient]
quot_quot.T [in graphs.finite_quotient]
quot_kernel.Hf [in graphs.finite_quotient]
quot_kernel.Hr [in graphs.finite_quotient]
quot_kernel.f' [in graphs.finite_quotient]
quot_kernel.f [in graphs.finite_quotient]
quot_kernel.r [in graphs.finite_quotient]
quot.s.e [in graphs.finite_quotient]
quot.s.T [in graphs.finite_quotient]

S

sig_sum_bij.NonDisjoint.eqvI [in graphs.finite_quotient]
sig_sum_bij.NonDisjoint.e [in graphs.finite_quotient]
sig_sum_bij.Disjoint.disUV [in graphs.finite_quotient]
sig_sum_bij.V [in graphs.finite_quotient]
sig_sum_bij.U [in graphs.finite_quotient]
sig_sum_bij.T [in graphs.finite_quotient]
s'.A [in graphs.reduction]
s.A [in graphs.completeness]
s.a.A [in graphs.reduction]
s.a.a [in graphs.reduction]
s.a.G [in graphs.reduction]
s.a.H [in graphs.reduction]
s.a.l [in graphs.reduction]
s.Edges.G [in graphs.mgraph]
s.h_merge_nothing'.H [in graphs.mgraph]
s.h_merge_nothing'.r [in graphs.mgraph]
s.h_merge_nothing'.F [in graphs.mgraph]
s.L [in graphs.mgraph]
s.L [in graphs.mgraph2]
s.merge_union_K.ke [in graphs.mgraph]
s.merge_union_K.kh [in graphs.mgraph]
s.merge_union_K.kv [in graphs.mgraph]
s.merge_union_K.k [in graphs.mgraph]
s.merge_union_K.h [in graphs.mgraph]
s.merge_union_K.K [in graphs.mgraph]
s.merge_union_K.F [in graphs.mgraph]
s.merge_merge_seq.kk' [in graphs.mgraph]
s.merge_merge_seq.k' [in graphs.mgraph]
s.merge_merge_seq.k [in graphs.mgraph]
s.merge_merge_seq.h [in graphs.mgraph]
s.merge_merge_seq.F [in graphs.mgraph]
s.merge_nothing.H [in graphs.mgraph]
s.merge_nothing.h [in graphs.mgraph]
s.merge_nothing.F [in graphs.mgraph]
s.merge_same.H [in graphs.mgraph]
s.merge_same.k [in graphs.mgraph]
s.merge_same.h [in graphs.mgraph]
s.merge_same.F [in graphs.mgraph]
s.merge_same'.H [in graphs.mgraph]
s.merge_same'.k [in graphs.mgraph]
s.merge_same'.h [in graphs.mgraph]
s.merge_same'.F [in graphs.mgraph]
s.merge_merge.e' [in graphs.mgraph]
s.merge_merge.e [in graphs.mgraph]
s.merge_merge.F [in graphs.mgraph]
s.merge_surj.Hvlabel [in graphs.mgraph]
s.merge_surj.Helabel [in graphs.mgraph]
s.merge_surj.Hendpoints [in graphs.mgraph]
s.merge_surj.Hsurj [in graphs.mgraph]
s.merge_surj.Hr [in graphs.mgraph]
s.merge_surj.fe [in graphs.mgraph]
s.merge_surj.fv' [in graphs.mgraph]
s.merge_surj.fv [in graphs.mgraph]
s.merge_surj.H [in graphs.mgraph]
s.merge_surj.r [in graphs.mgraph]
s.merge_surj.G [in graphs.mgraph]
s.merge.F [in graphs.mgraph]
s.merge.G [in graphs.mgraph]
s.merge.h [in graphs.mgraph]
s.merge.l [in graphs.mgraph]
s.Subgraphs.E [in graphs.mgraph]
s.Subgraphs.G [in graphs.mgraph]
s.Subgraphs.in_V [in graphs.mgraph]
s.Subgraphs.V [in graphs.mgraph]
s.union_merge_r.l [in graphs.mgraph]
s.union_merge_r.G [in graphs.mgraph]
s.union_merge_r.F [in graphs.mgraph]
s.union_merge_l.l [in graphs.mgraph]
s.union_merge_l.G [in graphs.mgraph]
s.union_merge_l.F [in graphs.mgraph]
s.X [in graphs.rewriting]
s.X [in graphs.reduction]

T

terms.A [in graphs.pttdom]
terms.A [in graphs.ptt]
terms.e.f [in graphs.pttdom]
terms.e.f [in graphs.ptt]
terms.e.X [in graphs.pttdom]
terms.e.X [in graphs.ptt]
Theory.mon0 [in graphs.structures]
Theory.mon2 [in graphs.structures]
Theory.X [in graphs.structures]
t.e [in graphs.finite_quotient]
t.f [in graphs.finite_quotient]
t.H [in graphs.finite_quotient]
t.S [in graphs.finite_quotient]

U

union_quot_r.e [in graphs.finite_quotient]
union_quot_r.T [in graphs.finite_quotient]
union_quot_r.S [in graphs.finite_quotient]
union_quot_l.e [in graphs.finite_quotient]
union_quot_l.T [in graphs.finite_quotient]
union_quot_l.S [in graphs.finite_quotient]
update.aT [in graphs.preliminaries]
update.f [in graphs.preliminaries]
update.rT [in graphs.preliminaries]

---

Library Index

B

bij

C

completeness

E

edone
equiv

F

finite_quotient
finmap_plus

M

mgraph
mgraph2

O

open_confluence

P

preliminaries
ptt
pttdom

R

reduction
rewriting

S

structures

T

transfer

---

Lemma Index

A

above_largest [in graphs.preliminaries]
add_edge_remove_edgesK [in graphs.open_confluence]
add_vertexK [in graphs.open_confluence]
add_testK [in graphs.open_confluence]
add_edgeKl [in graphs.open_confluence]
add_edge_remove_vertex [in graphs.open_confluence]
add_test_merge [in graphs.open_confluence]
add_edge_edge [in graphs.open_confluence]
add_test_edge [in graphs.open_confluence]
add_edge_remove_edges [in graphs.open_confluence]
add_edge_test [in graphs.open_confluence]
add_testC [in graphs.open_confluence]
add_edgeV [in graphs.open_confluence]
add_edge_graph [in graphs.open_confluence]
add_edge_graph'' [in graphs.open_confluence]
add_edge_graph' [in graphs.open_confluence]
add_edge_flip [in graphs.transfer]
add_vlabel_edge [in graphs.mgraph]
add_vlabel_two [in graphs.mgraph]
add_vlabel_mon0 [in graphs.mgraph]
add_vlabel_unit [in graphs.mgraph]
add_vlabel_C [in graphs.mgraph]
add_vlabel_iso [in graphs.mgraph]
add_vlabel_iso' [in graphs.mgraph]
add_vlabel_iso'' [in graphs.mgraph]
add_edge_vlabel [in graphs.mgraph]
add_edge_rev [in graphs.mgraph]
add_edge_C [in graphs.mgraph]
add_edge_iso [in graphs.mgraph]
add_edge_iso' [in graphs.mgraph]
add_edge_iso'' [in graphs.mgraph]
add_vlabel2_mon0 [in graphs.mgraph2]
add_vlabel2_edge [in graphs.mgraph2]
add_vlabel2_two [in graphs.mgraph2]
add_vlabel2_unit' [in graphs.mgraph2]
add_vlabel2_unit [in graphs.mgraph2]
add_vlabel2_C [in graphs.mgraph2]
add_vlabel2_iso [in graphs.mgraph2]
add_vlabel2_iso' [in graphs.mgraph2]
add_vlabel2_iso'' [in graphs.mgraph2]
add_edge2_vlabel [in graphs.mgraph2]
add_edge2_rev [in graphs.mgraph2]
add_edge2_C [in graphs.mgraph2]
add_edge2_iso [in graphs.mgraph2]
add_edge2_iso' [in graphs.mgraph2]
add_edge2_iso'' [in graphs.mgraph2]
admissible_map [in graphs.reduction]
all_cons [in graphs.preliminaries]
A13_ [in graphs.ptt]
A14_ [in graphs.ptt]

B

below_smallest [in graphs.preliminaries]
bigcup_set1 [in graphs.preliminaries]
bigD1 [in graphs.structures]
bigID [in graphs.structures]
big_unit [in graphs.structures]
big_sum [in graphs.structures]
big_pred1 [in graphs.structures]
big_pred1_eq [in graphs.structures]
big_seq1 [in graphs.structures]
big_split [in graphs.structures]
big_cat [in graphs.structures]
big_mkcond [in graphs.structures]
bij_quotE' [in graphs.finite_quotient]
bij_quotE [in graphs.finite_quotient]
bij_perm_enum [in graphs.bij]
bij_same [in graphs.bij]
bij_sumA [in graphs.bij]
bij_sumC [in graphs.bij]
bij_eqLR [in graphs.bij]
bij_imsetC [in graphs.bij]
bij_mem_imset [in graphs.bij]
bij_injective' [in graphs.bij]
bij_injective [in graphs.bij]
bij_bijective' [in graphs.bij]
bij_bijective [in graphs.bij]
bij_castE [in graphs.finmap_plus]
bij_surj [in graphs.preliminaries]
bij_card_eq [in graphs.preliminaries]
bool_two [in graphs.bij]

C

can_bijD1_bwd [in graphs.bij]
can_bijD1_fwd [in graphs.bij]
can_vset' [in graphs.finmap_plus]
can_vset [in graphs.finmap_plus]
cardsCT [in graphs.preliminaries]
cardsDsub [in graphs.finmap_plus]
cardsI [in graphs.preliminaries]
cardsIsub [in graphs.finmap_plus]
cards2P [in graphs.preliminaries]
cards3 [in graphs.preliminaries]
card_bij [in graphs.bij]
card_void [in graphs.preliminaries]
card_le1P [in graphs.preliminaries]
card_gt2P [in graphs.preliminaries]
card_gt1P [in graphs.preliminaries]
card_gtnP [in graphs.preliminaries]
card_le1 [in graphs.preliminaries]
card_ltnT [in graphs.preliminaries]
card1P [in graphs.preliminaries]
card12 [in graphs.preliminaries]
cast_proof [in graphs.finmap_plus]
close_same_step [in graphs.open_confluence]
cnvtop [in graphs.ptt]
cnvtst [in graphs.pttdom]
cnv_test [in graphs.pttdom]
cnv_inj [in graphs.pttdom]
cnv1 [in graphs.pttdom]
cnv2dot [in graphs.mgraph2]
cnv2I [in graphs.mgraph2]
cnv2par [in graphs.mgraph2]
codom_Some [in graphs.preliminaries]
completeness [in graphs.completeness]
confluence [in graphs.completeness]
connectUP [in graphs.preliminaries]
connect_img [in graphs.preliminaries]
connect_symI [in graphs.preliminaries]
connect_restrict_mono [in graphs.preliminaries]
connect_mono [in graphs.preliminaries]
consistentT [in graphs.mgraph]
consistentTT [in graphs.mgraph]
consistentU [in graphs.mgraph]
consistent_del1 [in graphs.mgraph]
cons_step_steps [in graphs.reduction]
cons_iso_steps [in graphs.reduction]
contraNnot [in graphs.preliminaries]
contraPeq [in graphs.preliminaries]
contraPN [in graphs.preliminaries]
contraPneq [in graphs.preliminaries]
contraPT [in graphs.preliminaries]
contraTnot [in graphs.preliminaries]
contra_notT [in graphs.preliminaries]
CProper1 [in graphs.structures]
CProper2 [in graphs.structures]
critical_pair3 [in graphs.open_confluence]
critical_pair2 [in graphs.open_confluence]
critical_pair1 [in graphs.open_confluence]
crK [in graphs.preliminaries]

D

degree_one_two [in graphs.open_confluence]
disjointE [in graphs.preliminaries]
disjointFl [in graphs.preliminaries]
disjointFr [in graphs.preliminaries]
disjointNI [in graphs.preliminaries]
disjointP [in graphs.preliminaries]
disjointsU [in graphs.preliminaries]
disjoints1 [in graphs.preliminaries]
disjointW [in graphs.preliminaries]
disjoint_transR [in graphs.preliminaries]
disjoint_exists [in graphs.preliminaries]
disjoint3P [in graphs.preliminaries]
domtst [in graphs.pttdom]
dom_tst [in graphs.pttdom]
dom_test [in graphs.pttdom]
dom2E [in graphs.mgraph2]
dotcnv [in graphs.pttdom]
dot_test [in graphs.pttdom]
dot_steps_r [in graphs.reduction]
dot_steps_l [in graphs.reduction]
dot_edges [in graphs.reduction]
dot1x [in graphs.pttdom]
dot2A [in graphs.mgraph2]
dot2Aflat [in graphs.mgraph2]
dot2one [in graphs.mgraph2]
dot2one' [in graphs.mgraph2]
dot2unit_l [in graphs.mgraph2]
dot2unit_r' [in graphs.mgraph2]
dot2unit_r [in graphs.mgraph2]

E

edges_replace [in graphs.open_confluence]
edges_at_flip_edge [in graphs.open_confluence]
edges_at_remove_edges [in graphs.open_confluence]
edges_at_added_vertex [in graphs.open_confluence]
edges_atC [in graphs.open_confluence]
edges_at_add_edge' [in graphs.open_confluence]
edges_at_add_edgeL [in graphs.open_confluence]
edges_at_add_edge [in graphs.open_confluence]
edges_at_del [in graphs.open_confluence]
edges_at_test [in graphs.open_confluence]
edges_at_oarc [in graphs.open_confluence]
edges_atF [in graphs.open_confluence]
edges_atP [in graphs.open_confluence]
edges_atE [in graphs.open_confluence]
edges_at_iso [in graphs.mgraph]
edges_in1 [in graphs.mgraph]
edge_in_set [in graphs.mgraph]
edge_set1 [in graphs.mgraph]
edir_bodyE [in graphs.transfer]
efun_of_bij [in graphs.transfer]
efun_of_inj [in graphs.transfer]
efun_bodyE [in graphs.transfer]
elabel_iso' [in graphs.mgraph]
elabel_iso [in graphs.mgraph]
empty_uniqe [in graphs.preliminaries]
endpoint_iso' [in graphs.mgraph]
endpoint_iso [in graphs.mgraph]
endpt_add_edge [in graphs.open_confluence]
endpt_proof [in graphs.transfer]
enum_unit [in graphs.preliminaries]
enum_sum [in graphs.preliminaries]
eqb_negR [in graphs.preliminaries]
eqmodE [in graphs.finite_quotient]
equivalence_partition_gt1P [in graphs.preliminaries]
equivalence_rel_of_sym [in graphs.preliminaries]
equiv_comp_pi [in graphs.finite_quotient]
equiv_compE [in graphs.finite_quotient]
equiv_of_fn [in graphs.equiv]
equiv_of_nn [in graphs.equiv]
equiv_of_ff [in graphs.equiv]
equiv_of_sub' [in graphs.equiv]
equiv_of_sub [in graphs.equiv]
equiv_of_transfer [in graphs.equiv]
equiv_ofE [in graphs.equiv]
equiv_of_class [in graphs.equiv]
equiv_clot_Kl [in graphs.mgraph]
equiv_of_sym [in graphs.preliminaries]
eqvbN [in graphs.pttdom]
eqvbT [in graphs.pttdom]
eqvb_neq [in graphs.pttdom]
eqvb_par1 [in graphs.pttdom]
eqvb_transL [in graphs.structures]
eqvb_transR [in graphs.structures]
eqvb_trans [in graphs.structures]
eqvG_stepL [in graphs.open_confluence]
eqvG_edges_at [in graphs.open_confluence]
eqvG_graph [in graphs.open_confluence]
eqvG_sym [in graphs.open_confluence]
eqvG_pack [in graphs.transfer]
eqvG_iso2E [in graphs.transfer]
eqvxx [in graphs.structures]
eqv_test_equiv [in graphs.pttdom]
eqv_clot_LR [in graphs.equiv]
eqv_clot_injR [in graphs.equiv]
eqv_clot_injL [in graphs.equiv]
eqv_clot1E [in graphs.equiv]
eqv_clot_cat [in graphs.equiv]
eqv_clot_map_eq [in graphs.equiv]
eqv_clot_mapF [in graphs.equiv]
eqv_clot_map [in graphs.equiv]
eqv_clot_nothing' [in graphs.equiv]
eqv_clot_nothing [in graphs.equiv]
eqv_clot_eq [in graphs.equiv]
eqv_clot_subrel [in graphs.equiv]
eqv_clot_tl [in graphs.equiv]
eqv_clot_hd' [in graphs.equiv]
eqv_clot_hd [in graphs.equiv]
eqv_clot_trans [in graphs.equiv]
eqv_clot_iso [in graphs.equiv]
eqv_clot_map' [in graphs.equiv]
eqv_clot_subset [in graphs.equiv]
eqv_clot_pair [in graphs.equiv]
eqv_clotE [in graphs.equiv]
eqv_clot_union_rel [in graphs.mgraph]
eqv_clot_map_lr [in graphs.mgraph]
eqv_update [in graphs.finmap_plus]
eqv_big [in graphs.structures]
eqv_bigl [in graphs.structures]
eqv_bigr [in graphs.structures]
eqv_big_bij [in graphs.structures]
eqv_map [in graphs.structures]
eqv'_sym [in graphs.pttdom]
eqv01 [in graphs.pttdom]
eqv10 [in graphs.structures]
eqv11 [in graphs.pttdom]
eq_quot_finMixin [in graphs.finite_quotient]
eq_equiv_class [in graphs.equiv]
eq_equiv [in graphs.equiv]
eq_eqv [in graphs.mgraph]
eq_unit [in graphs.structures]
eq_set1P [in graphs.preliminaries]
existsb_case [in graphs.preliminaries]
existsb_eq [in graphs.preliminaries]
existsPn [in graphs.preliminaries]
exists_inPn [in graphs.preliminaries]
expand_parallel [in graphs.transfer]
expand_loop [in graphs.transfer]
expand_chain [in graphs.transfer]
expand_pendant [in graphs.transfer]
expand_isolated [in graphs.transfer]
ex_smallest [in graphs.preliminaries]

F

flipped_edge [in graphs.open_confluence]
flip_edgeK' [in graphs.open_confluence]
flip_edgeK [in graphs.open_confluence]
flip_edge_add_test [in graphs.open_confluence]
flip_edge_iso [in graphs.transfer]
foldr1_set_default [in graphs.preliminaries]
ForallE [in graphs.equiv]
forallPn [in graphs.preliminaries]
forall_inPn [in graphs.preliminaries]
freshP [in graphs.open_confluence]
freshP' [in graphs.open_confluence]
fresh_eqF [in graphs.open_confluence]
fresh_bijE' [in graphs.finmap_plus]
fresh_bij' [in graphs.finmap_plus]
fresh_bijE [in graphs.finmap_plus]
fresh_bij [in graphs.finmap_plus]
fsetDDD [in graphs.finmap_plus]
fsetDEl [in graphs.finmap_plus]
fsetDl [in graphs.finmap_plus]
fsetD_bijE [in graphs.finmap_plus]
fsetD_bij_can_bwd [in graphs.finmap_plus]
fsetD_bij_can_fwd [in graphs.finmap_plus]
fsetD_bij_bwd_proof [in graphs.finmap_plus]
fsetD_bij_fwd_proof [in graphs.finmap_plus]
fsetUDU [in graphs.finmap_plus]
fsetU1_fun_can [in graphs.finmap_plus]
fset01 [in graphs.finmap_plus]
fset1D [in graphs.finmap_plus]
fset1UE [in graphs.finmap_plus]
fset1U0 [in graphs.finmap_plus]
fset2_maxn_neq [in graphs.finmap_plus]
fset2_cases [in graphs.finmap_plus]
fset2_inv [in graphs.finmap_plus]
fsvalK [in graphs.finmap_plus]
fsval_eqF [in graphs.finmap_plus]
fun_decompose [in graphs.preliminaries]

G

g2_A12 [in graphs.mgraph2]
g2_A12' [in graphs.mgraph2]
g2_A11 [in graphs.mgraph2]
g2_A10 [in graphs.mgraph2]

H

hom_merge_union_K [in graphs.mgraph]
hom_union_merge_l [in graphs.mgraph]
hom_merge_merge [in graphs.mgraph]
hom_sym [in graphs.mgraph]
hom_comp [in graphs.mgraph]
hom_id [in graphs.mgraph]
h_mergeE [in graphs.mgraph]

I

id_surj [in graphs.preliminaries]
id_bij [in graphs.preliminaries]
imfsetU [in graphs.finmap_plus]
imfset_bij_bwdE [in graphs.finmap_plus]
imfset_inv [in graphs.finmap_plus]
imfset_comp [in graphs.finmap_plus]
imfset_sep [in graphs.finmap_plus]
imfset0 [in graphs.finmap_plus]
imfset1 [in graphs.finmap_plus]
imfset1U [in graphs.finmap_plus]
imset_valT [in graphs.preliminaries]
imset_pre_val [in graphs.preliminaries]
im_efun_of [in graphs.transfer]
incident_vset [in graphs.open_confluence]
incident_flip_edge [in graphs.open_confluence]
incident_flip [in graphs.open_confluence]
incident_addv [in graphs.open_confluence]
incident_dele [in graphs.open_confluence]
incident_delv [in graphs.open_confluence]
incident_iso [in graphs.mgraph]
induced_sub [in graphs.mgraph]
infer_testE [in graphs.pttdom]
inj_vNfresh [in graphs.transfer]
inj_v_fresh [in graphs.transfer]
inj_v_open [in graphs.transfer]
inj_vK [in graphs.transfer]
inj_eK [in graphs.transfer]
inj_e_inj [in graphs.transfer]
inj_v_inj [in graphs.transfer]
inj_imset [in graphs.preliminaries]
inj_card_onto_pred [in graphs.preliminaries]
inj_omap [in graphs.preliminaries]
inj_card_leq [in graphs.preliminaries]
inl_codom_inr [in graphs.preliminaries]
inl_inj [in graphs.preliminaries]
inl_eqE [in graphs.preliminaries]
inr_codom_inl [in graphs.preliminaries]
inr_inj [in graphs.preliminaries]
inr_eqE [in graphs.preliminaries]
in_vsetAV' [in graphs.open_confluence]
in_vsetAE [in graphs.open_confluence]
in_vsetAV [in graphs.open_confluence]
in_vsetDE [in graphs.open_confluence]
in_vsetDV [in graphs.open_confluence]
in_eqv_update [in graphs.finmap_plus]
in_fsep [in graphs.finmap_plus]
in_imfsetT [in graphs.finmap_plus]
iso_of_oiso [in graphs.transfer]
iso_stagnates [in graphs.completeness]
iso_iso2' [in graphs.mgraph2]
iso_iso2 [in graphs.mgraph2]
iso2_intro [in graphs.transfer]
iso2_subgraph_forT [in graphs.mgraph2]
is_edge_flip_edge [in graphs.open_confluence]
is_edge_remove_edges [in graphs.open_confluence]
is_edge_vsetR [in graphs.open_confluence]
is_edge_vsetL [in graphs.open_confluence]
is_test_alt [in graphs.pttdom]

K

kernelP [in graphs.finite_quotient]
kernel_equivalence [in graphs.finite_quotient]
kernel_eqv_clot [in graphs.equiv]

L

last_belast_eq [in graphs.preliminaries]
last_take [in graphs.preliminaries]
leq_subn [in graphs.preliminaries]
lift_equiv [in graphs.preliminaries]
lift_path [in graphs.preliminaries]
local_confluence [in graphs.open_confluence]
local_confluence_aux [in graphs.open_confluence]
local_confluence [in graphs.completeness]
lv_add_edge [in graphs.open_confluence]

M

map_equivE [in graphs.finite_quotient]
map_equiv_class [in graphs.finite_quotient]
map_pairs_id [in graphs.mgraph]
map_map_pairs [in graphs.mgraph]
maxnP [in graphs.preliminaries]
maxn_fsetD [in graphs.finmap_plus]
maxn_fset2 [in graphs.finmap_plus]
maxn_eq [in graphs.preliminaries]
max_mono [in graphs.preliminaries]
memKset [in graphs.preliminaries]
mem_maxn [in graphs.finmap_plus]
mem_cover [in graphs.preliminaries]
mem_preim [in graphs.preliminaries]
mem_catD [in graphs.preliminaries]
mem_tail [in graphs.preliminaries]
merge_unionE [in graphs.finite_quotient]
merge_union_bwd_hom [in graphs.finite_quotient]
merge_union_fwd_hom [in graphs.finite_quotient]
merge_union_can' [in graphs.finite_quotient]
merge_union_can [in graphs.finite_quotient]
merge_disjoint_union_can' [in graphs.finite_quotient]
merge_disjoint_union_can [in graphs.finite_quotient]
merge_union_bwdP [in graphs.finite_quotient]
merge_subgraph_isoE [in graphs.mgraph]
merge_subgraph_hom [in graphs.mgraph]
merge_union_KE [in graphs.mgraph]
merge_add_vlabelE [in graphs.mgraph]
merge_add_vlabel [in graphs.mgraph]
merge_add_edgeE [in graphs.mgraph]
merge_add_edge [in graphs.mgraph]
merge_merge_seqE [in graphs.mgraph]
merge_nothingE [in graphs.mgraph]
merge_same'E [in graphs.mgraph]
merge_same'_hom [in graphs.mgraph]
merge_isoE [in graphs.mgraph]
merge_hom [in graphs.mgraph]
merge_mergeE [in graphs.mgraph]
merge_merge [in graphs.mgraph]
merge_nothing'E [in graphs.mgraph]
merge_nothing' [in graphs.mgraph]
merge_surjE [in graphs.mgraph]
merge_surj [in graphs.mgraph]
merge_union_K_l [in graphs.mgraph2]
merge_merge [in graphs.mgraph2]
merge_nothing [in graphs.mgraph2]
merge_same' [in graphs.mgraph2]
merge_same [in graphs.mgraph2]
merge_iso2 [in graphs.mgraph2]
merge_step [in graphs.reduction]
merge_add_vertexLE [in graphs.reduction]
merge_add_vertexL [in graphs.reduction]
merge_add_edgeLE [in graphs.reduction]
merge_add_edgeL [in graphs.reduction]
merge2_add_vlabel [in graphs.mgraph2]
merge2_add_edge [in graphs.mgraph2]
merge2_merge [in graphs.mgraph2]
merge2_nothing [in graphs.mgraph2]
merge2_same' [in graphs.mgraph2]
merge2_same [in graphs.mgraph2]
merge2_surj [in graphs.mgraph2]
merge2_iso2 [in graphs.mgraph2]
monUl [in graphs.structures]

N

nat_size_ind [in graphs.preliminaries]
normal_iso [in graphs.completeness]
normal_steps [in graphs.completeness]
notin_tail [in graphs.preliminaries]
nt_correct [in graphs.pttdom]

O

oarcxx_le [in graphs.open_confluence]
oarc_flip_edge [in graphs.open_confluence]
oarc_remove_vertex [in graphs.open_confluence]
oarc_remove_edges [in graphs.open_confluence]
oarc_added_edge [in graphs.open_confluence]
oarc_add_edge [in graphs.open_confluence]
oarc_eqv [in graphs.open_confluence]
oarc_loop [in graphs.open_confluence]
oarc_injR [in graphs.open_confluence]
oarc_injL [in graphs.open_confluence]
oarc_uniqeL [in graphs.open_confluence]
oarc_uniqeR [in graphs.open_confluence]
oarc_vsetR [in graphs.open_confluence]
oarc_vsetL [in graphs.open_confluence]
oarc_cases [in graphs.open_confluence]
oarc_edge_atR [in graphs.open_confluence]
oarc_edge_atL [in graphs.open_confluence]
oarc_cnv [in graphs.open_confluence]
oiso_of [in graphs.transfer]
oiso2_transE [in graphs.transfer]
oiso2_add_edgeE' [in graphs.transfer]
oiso2_add_edge' [in graphs.transfer]
oiso2_remove_edgesE [in graphs.transfer]
oiso2_remove_edges [in graphs.transfer]
oiso2_add_edge [in graphs.transfer]
oiso2_remove_vertex_ [in graphs.transfer]
oiso2_remove_vertexE [in graphs.transfer]
oiso2_remove_vertex [in graphs.transfer]
oiso2_add_testE [in graphs.transfer]
oiso2_add_test [in graphs.transfer]
oiso2_oarc [in graphs.transfer]
oiso2_edges_at [in graphs.transfer]
oiso2_incident [in graphs.transfer]
oiso2_le [in graphs.transfer]
oiso2_lv [in graphs.transfer]
oiso2_endpoint [in graphs.transfer]
oiso2_pIO_vfun [in graphs.transfer]
oiso2_pIO [in graphs.transfer]
oiso2_idE [in graphs.transfer]
oiso2_id [in graphs.transfer]
oiso2_output [in graphs.transfer]
oiso2_input [in graphs.transfer]
oiso2_vset [in graphs.transfer]
oiso2_sym [in graphs.transfer]
oiso2_trans [in graphs.transfer]
one_test [in graphs.pttdom]
openK [in graphs.transfer]
openKE [in graphs.transfer]
open_add_edgeE [in graphs.transfer]
open_add_edge [in graphs.transfer]
open_add_vertexE [in graphs.transfer]
option_sum_unit [in graphs.bij]
orb_sum [in graphs.preliminaries]
ord_fresh [in graphs.preliminaries]
ord_size_enum [in graphs.preliminaries]
ostepL [in graphs.open_confluence]
osteps_graph [in graphs.open_confluence]
osteps_refl [in graphs.open_confluence]
osteps_iso [in graphs.transfer]
ostep_graph [in graphs.open_confluence]
ostep_of [in graphs.transfer]
ostep_of' [in graphs.transfer]
ostep_iso [in graphs.transfer]

P

packK [in graphs.transfer]
pack_add_edge [in graphs.transfer]
pack_add_edge' [in graphs.transfer]
pack_v_IO [in graphs.transfer]
pack_irrelevance [in graphs.transfer]
pack_fsval [in graphs.transfer]
pack_vK [in graphs.transfer]
pack_vE [in graphs.transfer]
paratst [in graphs.pttdom]
pardot [in graphs.pttdom]
partition_big [in graphs.structures]
partopx [in graphs.ptt]
partst [in graphs.pttdom]
parxtop [in graphs.ptt]
par_nontest [in graphs.pttdom]
par_tst_cnv [in graphs.pttdom]
par_test [in graphs.pttdom]
par_steps_r [in graphs.reduction]
par_steps_l [in graphs.reduction]
par_edges [in graphs.reduction]
par1tst [in graphs.pttdom]
par2A [in graphs.mgraph2]
par2C [in graphs.mgraph2]
par2dot [in graphs.mgraph2]
par2edgeunit [in graphs.mgraph2]
par2oneone [in graphs.mgraph2]
par2top [in graphs.mgraph2]
par2unitunit [in graphs.mgraph2]
path_restrict [in graphs.preliminaries]
pblock_eqvE [in graphs.preliminaries]
perm_index_enum [in graphs.bij]
perm_big [in graphs.structures]
picksP [in graphs.preliminaries]
piK [in graphs.finite_quotient]
piK' [in graphs.finite_quotient]
pimsetP [in graphs.preliminaries]
pimset_card [in graphs.preliminaries]
pIO_add_test [in graphs.open_confluence]
pIO_add_edge [in graphs.open_confluence]
pIO_add_vertex [in graphs.open_confluence]
pIO_fresh [in graphs.open_confluence]
pIO_No [in graphs.open_confluence]
pIO_Ni [in graphs.open_confluence]
piP [in graphs.finite_quotient]
pi_surj [in graphs.finite_quotient]
preim_omap_None [in graphs.preliminaries]
preim_omap_Some [in graphs.preliminaries]
project_path [in graphs.preliminaries]
propers_ind [in graphs.preliminaries]
proper_ind [in graphs.preliminaries]

Q

quot_union_KE [in graphs.finite_quotient]
quot_idE [in graphs.finite_quotient]
quot_quotE [in graphs.finite_quotient]
quot_bijE' [in graphs.finite_quotient]
quot_bijE [in graphs.finite_quotient]
quot_kernelE' [in graphs.finite_quotient]
quot_kernelE [in graphs.finite_quotient]
quot_kernel_can' [in graphs.finite_quotient]
quot_kernel_can [in graphs.finite_quotient]
quot_sameE' [in graphs.finite_quotient]
quot_sameE [in graphs.finite_quotient]
quot_fun_can [in graphs.finite_quotient]
quot.eqquotP [in graphs.finite_quotient]
quot.reprK [in graphs.finite_quotient]

R

reduce [in graphs.reduction]
reduce_shuffle [in graphs.pttdom]
reindex [in graphs.structures]
reindex_onto [in graphs.structures]
relabel_edge [in graphs.mgraph2]
relabel_two [in graphs.mgraph2]
relabel_unit [in graphs.mgraph2]
relabel_add_edge [in graphs.mgraph2]
relabel_merge [in graphs.mgraph2]
relabel_union [in graphs.mgraph2]
relabel2_var [in graphs.mgraph2]
relabel2_top [in graphs.mgraph2]
relabel2_one [in graphs.mgraph2]
relabel2_dom [in graphs.mgraph2]
relabel2_cnv [in graphs.mgraph2]
relabel2_par [in graphs.mgraph2]
relabel2_dot [in graphs.mgraph2]
relU_sym' [in graphs.preliminaries]
rel_of_pairs_mapE [in graphs.equiv]
rel_of_pairs_map_eq [in graphs.equiv]
rel_of_pairs_mono [in graphs.equiv]
rel0_sym [in graphs.preliminaries]
rel0_irrefl [in graphs.preliminaries]
remove_edges_vertexK [in graphs.open_confluence]
remove_edgeK [in graphs.open_confluence]
remove_edgesK [in graphs.open_confluence]
remove_vertexK [in graphs.open_confluence]
remove_edges_edges [in graphs.open_confluence]
remove_edges_vertex [in graphs.open_confluence]
remove_edges_add_test [in graphs.open_confluence]
remove_vertex_edges [in graphs.open_confluence]
remove_vertex_add_edge [in graphs.open_confluence]
remove_vertex_add_test [in graphs.open_confluence]
remove_vertexC [in graphs.open_confluence]
remove_edges0 [in graphs.open_confluence]
remove_edgesD [in graphs.transfer]
remove_edges_sub [in graphs.mgraph]
replace_ioE [in graphs.reduction]
restrictE [in graphs.preliminaries]
restrict_path [in graphs.preliminaries]
restrict_mono [in graphs.preliminaries]
rev_inj [in graphs.preliminaries]
rwT [in graphs.pttdom]

S

same_oarc [in graphs.open_confluence]
sc_eq [in graphs.preliminaries]
sc_sym [in graphs.preliminaries]
setN01E [in graphs.preliminaries]
setT_bij_hom [in graphs.mgraph]
setU_dec [in graphs.finite_quotient]
setU1_neq [in graphs.preliminaries]
setU1_mem [in graphs.preliminaries]
set1_inj [in graphs.preliminaries]
set10 [in graphs.preliminaries]
set2C [in graphs.preliminaries]
Some_eqE [in graphs.preliminaries]
soundness_and_completeness [in graphs.completeness]
steps_of [in graphs.transfer]
steps_of_ostep [in graphs.transfer]
steps_refl [in graphs.rewriting]
step_decreases [in graphs.completeness]
step_to_steps [in graphs.reduction]
step_IO [in graphs.reduction]
subgraph_sub [in graphs.mgraph]
subgraph_for_iso [in graphs.mgraph2]
subrelP [in graphs.preliminaries]
subrel_restrict [in graphs.preliminaries]
subset_tl [in graphs.equiv]
subset_catR [in graphs.equiv]
subset_catL [in graphs.equiv]
subset_seqL [in graphs.preliminaries]
subset_seqR [in graphs.preliminaries]
subset_cons [in graphs.preliminaries]
Sub_endpt [in graphs.transfer]
sub_equiv_of [in graphs.preliminaries]
sub_restrict_connect [in graphs.preliminaries]
sub_trans [in graphs.preliminaries]
sub_connect [in graphs.preliminaries]
sub_in11W [in graphs.preliminaries]
sub_val_eq [in graphs.preliminaries]
sumUx [in graphs.bij]
sumxU [in graphs.bij]
sum_option_r [in graphs.bij]
sum_option_l [in graphs.bij]
surj_repr_pi [in graphs.finite_quotient]
symmetric_restrict [in graphs.preliminaries]

T

take_find [in graphs.preliminaries]
tgraph_graph_iso [in graphs.completeness]
tgraph_graph [in graphs.completeness]
tm_eqv_equivalence [in graphs.pttdom]
tm_eqv_equivalence [in graphs.ptt]
tnth_cons [in graphs.preliminaries]
tnth_map_in [in graphs.preliminaries]
tnth_uniq [in graphs.preliminaries]
topL [in graphs.mgraph2]
topR [in graphs.mgraph2]
trivIset3 [in graphs.preliminaries]
tstpar [in graphs.pttdom]
tstpar1 [in graphs.pttdom]
tst_dotU [in graphs.pttdom]
tst_dotC [in graphs.pttdom]
tst_dotA [in graphs.pttdom]
tst_dot_eqv [in graphs.pttdom]
two_graph_swap [in graphs.mgraph]
two_edges [in graphs.reduction]

U

union_bij_proofR [in graphs.finite_quotient]
union_bij_proofL [in graphs.finite_quotient]
union_quot_rEl [in graphs.finite_quotient]
union_quot_rEr [in graphs.finite_quotient]
union_quot_lE' [in graphs.finite_quotient]
union_quot_lEr [in graphs.finite_quotient]
union_quot_lEl [in graphs.finite_quotient]
union_equiv_l_class [in graphs.finite_quotient]
union_merge_rEl [in graphs.mgraph]
union_merge_rEr [in graphs.mgraph]
union_merge_r [in graphs.mgraph]
union_merge_lE' [in graphs.mgraph]
union_merge_lEr [in graphs.mgraph]
union_merge_lEl [in graphs.mgraph]
union_equiv_l_eqv_clot [in graphs.mgraph]
union_add_vlabel_r [in graphs.mgraph]
union_add_vlabel_l [in graphs.mgraph]
union_add_edge_r [in graphs.mgraph]
union_add_edge_l [in graphs.mgraph]
union_A [in graphs.mgraph]
union_C [in graphs.mgraph]
uniq_take [in graphs.preliminaries]
update_fx [in graphs.preliminaries]
update_same [in graphs.preliminaries]
update_eq [in graphs.preliminaries]
update_neq [in graphs.preliminaries]

V

valK' [in graphs.preliminaries]
valK'' [in graphs.preliminaries]
vfun_of_inj [in graphs.transfer]
vfun_bodyEinj [in graphs.transfer]
vfun_bodyE [in graphs.transfer]
vlabel_iso' [in graphs.mgraph]
vlabel_iso [in graphs.mgraph]
void_enumP [in graphs.preliminaries]
void_pcancel [in graphs.preliminaries]
void_eqP [in graphs.preliminaries]
vset_add_vertex [in graphs.transfer]

W

wf_propers [in graphs.preliminaries]
wf_proper [in graphs.preliminaries]
wf_leq [in graphs.preliminaries]

---

Constructor Index

B

Bij [in graphs.bij]
Box [in graphs.open_confluence]

C

cons_step [in graphs.rewriting]

D

Dis3In1 [in graphs.preliminaries]
Dis3In2 [in graphs.preliminaries]
Dis3In3 [in graphs.preliminaries]
Dis3Notin [in graphs.preliminaries]

E

eqvG_step [in graphs.open_confluence]

F

flip_step [in graphs.open_confluence]
fstep_step [in graphs.open_confluence]

G

Graph [in graphs.mgraph]
Graph2 [in graphs.mgraph2]

H

Hom [in graphs.mgraph]

I

Iso [in graphs.mgraph]
iso_step [in graphs.rewriting]
Iso2 [in graphs.mgraph2]

L

Labels [in graphs.structures]

M

MaxnL [in graphs.preliminaries]
MaxnR [in graphs.preliminaries]
merge_union_bwdR [in graphs.finite_quotient]
merge_union_bwdL [in graphs.finite_quotient]
MonoidLaws [in graphs.structures]

N

Nopicks [in graphs.preliminaries]
nt_conn [in graphs.pttdom]
nt_test [in graphs.pttdom]

O

OIso2 [in graphs.transfer]
osteps_trans [in graphs.open_confluence]
ostep_step [in graphs.open_confluence]
ostep_e2 [in graphs.open_confluence]
ostep_e0 [in graphs.open_confluence]
ostep_v2 [in graphs.open_confluence]
ostep_v1 [in graphs.open_confluence]
ostep_v0 [in graphs.open_confluence]

P

Picks [in graphs.preliminaries]
PiSpec [in graphs.finite_quotient]

S

Setoid [in graphs.structures]
step_e2 [in graphs.rewriting]
step_e0 [in graphs.rewriting]
step_v2 [in graphs.rewriting]
step_v1 [in graphs.rewriting]
step_v0 [in graphs.rewriting]

T

Test [in graphs.pttdom]
tm_var [in graphs.pttdom]
tm_one [in graphs.pttdom]
tm_dom [in graphs.pttdom]
tm_cnv [in graphs.pttdom]
tm_par [in graphs.pttdom]
tm_dot [in graphs.pttdom]
tm_var [in graphs.ptt]
tm_top [in graphs.ptt]
tm_one [in graphs.ptt]
tm_dom [in graphs.ptt]
tm_cnv [in graphs.ptt]
tm_par [in graphs.ptt]
tm_dot [in graphs.ptt]

W

WeqG [in graphs.open_confluence]

---

Axiom Index

A

admitted_case [in graphs.preliminaries]

Q

QUOT.eqquotP [in graphs.finite_quotient]
QUOT.pi [in graphs.finite_quotient]
QUOT.quot [in graphs.finite_quotient]
QUOT.repr [in graphs.finite_quotient]
QUOT.reprK [in graphs.finite_quotient]

---

Inductive Index

D

disjoint3_cases [in graphs.preliminaries]

F

fstep [in graphs.open_confluence]

M

maxn_cases [in graphs.preliminaries]
merge_union_bwd_spec [in graphs.finite_quotient]

N

nterm [in graphs.pttdom]

O

ostep [in graphs.open_confluence]
osteps [in graphs.open_confluence]

P

picks_spec [in graphs.preliminaries]
pi_spec [in graphs.finite_quotient]

S

step [in graphs.rewriting]
steps [in graphs.rewriting]

T

term [in graphs.pttdom]
term [in graphs.ptt]

V

void [in graphs.preliminaries]

---

Projection Index

A

A10 [in graphs.pttdom]
A10_ [in graphs.ptt]
A11 [in graphs.ptt]
A12 [in graphs.ptt]
A13 [in graphs.pttdom]
A14 [in graphs.pttdom]

B

bijK [in graphs.bij]
bijK' [in graphs.bij]
bij_bwd [in graphs.bij]
bij_fwd [in graphs.bij]
boxed [in graphs.open_confluence]

C

car [in graphs.structures]
cnv [in graphs.pttdom]
cnvdot [in graphs.pttdom]
cnvdot_ [in graphs.ptt]
cnvI [in graphs.pttdom]
cnvI_ [in graphs.ptt]
cnvpar [in graphs.pttdom]
cnvpar_ [in graphs.ptt]
cnv_eqv [in graphs.pttdom]
cnv_eqv_ [in graphs.ptt]

D

default [in graphs.open_confluence]
dom [in graphs.pttdom]
domE [in graphs.ptt]
dom_eqv [in graphs.pttdom]
dot [in graphs.pttdom]
dotA [in graphs.pttdom]
dotA_ [in graphs.ptt]
dotx1 [in graphs.pttdom]
dotx1_ [in graphs.ptt]
dot_eqv [in graphs.pttdom]
dot_eqv_ [in graphs.ptt]

E

edge [in graphs.mgraph]
elabel [in graphs.mgraph]
elabel_hom [in graphs.mgraph]
elem_of [in graphs.pttdom]
endpoint [in graphs.mgraph]
endpoint_hom [in graphs.mgraph]
endpt [in graphs.open_confluence]
endptP [in graphs.open_confluence]
Eqv [in graphs.structures]
eqv [in graphs.structures]
eqv_le [in graphs.open_confluence]
eqv_lv [in graphs.open_confluence]
eqv' [in graphs.structures]
Eqv'_sym [in graphs.structures]
eqv01 [in graphs.structures]
eqv11 [in graphs.structures]
eset [in graphs.open_confluence]

G

graph_of [in graphs.mgraph2]

I

input [in graphs.mgraph2]
iso_hom [in graphs.mgraph]
iso_d [in graphs.mgraph]
iso_e [in graphs.mgraph]
iso_v [in graphs.mgraph]
iso2_output [in graphs.mgraph2]
iso2_input [in graphs.mgraph2]
iso2_iso [in graphs.mgraph2]

L

le [in graphs.open_confluence]
le [in graphs.structures]
lv [in graphs.open_confluence]
lv [in graphs.structures]
lv_monoid [in graphs.structures]

M

monA [in graphs.structures]
monC [in graphs.structures]
monU [in graphs.structures]
mon_eqv [in graphs.structures]
mon0 [in graphs.structures]
mon2 [in graphs.structures]

O

oiso2_iso [in graphs.transfer]
oiso2_graphR [in graphs.transfer]
oiso2_graphL [in graphs.transfer]
one [in graphs.pttdom]
ops [in graphs.pttdom]
ops [in graphs.ptt]
output [in graphs.mgraph2]

P

par [in graphs.pttdom]
parA [in graphs.pttdom]
parA_ [in graphs.ptt]
parC [in graphs.pttdom]
parC_ [in graphs.ptt]
par_eqv [in graphs.pttdom]
par_eqv_ [in graphs.ptt]
par11 [in graphs.pttdom]
par11_ [in graphs.ptt]
p_outP [in graphs.open_confluence]
p_inP [in graphs.open_confluence]
p_out [in graphs.open_confluence]
p_in [in graphs.open_confluence]

S

sameE [in graphs.open_confluence]
sameV [in graphs.open_confluence]
same_out [in graphs.open_confluence]
same_in [in graphs.open_confluence]
same_endpt [in graphs.open_confluence]
setoid_of_ops [in graphs.pttdom]

T

testE [in graphs.pttdom]
top [in graphs.pttdom]

V

vertex [in graphs.mgraph]
vlabel [in graphs.mgraph]
vlabel_hom [in graphs.mgraph]
vset [in graphs.open_confluence]

---

Instance Index

A

add_test_morphism [in graphs.open_confluence]
add_edge_morphism [in graphs.open_confluence]
add_edge_morphism' [in graphs.open_confluence]
add_test_graph [in graphs.open_confluence]
add_vertex_graph [in graphs.open_confluence]
add_vertex_iso [in graphs.mgraph]
add_vertex2_iso [in graphs.mgraph2]

B

bij_Equivalence [in graphs.bij]

C

cnv_iso2 [in graphs.mgraph2]
cnv_steps [in graphs.reduction]

D

dom_eqv_ [in graphs.ptt]
dom_iso2 [in graphs.mgraph2]
dom_steps [in graphs.reduction]
dot_iso2 [in graphs.mgraph2]
dot_steps [in graphs.reduction]

E

edge_graph2_iso [in graphs.mgraph2]
equiv_rel_Equivalence [in graphs.equiv]
eqvG_Equivalence [in graphs.open_confluence]
eqv_morphim [in graphs.structures]
eqv_sym [in graphs.structures]
ex2_iff_morphism [in graphs.preliminaries]

F

flip_edge_graph [in graphs.open_confluence]

I

isop_step [in graphs.rewriting]
iso_Equivalence [in graphs.mgraph]
iso2prop_Equivalence [in graphs.mgraph2]
iso2_Equivalence [in graphs.mgraph2]

O

oarc_morphism [in graphs.open_confluence]
oiso2_Equivalence [in graphs.transfer]
one_step [in graphs.rewriting]
open_is_graph [in graphs.transfer]
osteps_preorder [in graphs.open_confluence]

P

par_iso2 [in graphs.mgraph2]
par_steps [in graphs.reduction]
PreOrder_steps [in graphs.rewriting]

R

relabel_iso [in graphs.mgraph2]
relabel2_iso [in graphs.mgraph2]
remove_vertex_morphism [in graphs.open_confluence]
remove_edges_graph [in graphs.open_confluence]
remove_vertex_graph [in graphs.open_confluence]

S

sum_bij [in graphs.bij]

T

tm_inh_type [in graphs.open_confluence]
two_graph2_iso [in graphs.mgraph2]

U

union_iso [in graphs.mgraph]
unit_graph_iso [in graphs.mgraph]
unit_graph2_iso [in graphs.mgraph2]

V

VT_inh_type [in graphs.transfer]

---

Section Index

B

b [in graphs.finite_quotient]
Bij [in graphs.finmap_plus]
BijCast [in graphs.finmap_plus]
BijD1 [in graphs.bij]
BijT [in graphs.bij]

C

CProper [in graphs.structures]

D

derived [in graphs.pttdom]
derived [in graphs.ptt]
Disjoint3 [in graphs.preliminaries]

E

Equivalence [in graphs.preliminaries]
eqv_inj [in graphs.equiv]

F

FinEncodingModuloRel [in graphs.finite_quotient]
Foldr1 [in graphs.preliminaries]
Fresh2Bij [in graphs.finmap_plus]
fsetD_bij [in graphs.finmap_plus]
FsetU1Fun [in graphs.finmap_plus]

H

h [in graphs.mgraph2]

I

inject [in graphs.transfer]

M

map_equiv [in graphs.finite_quotient]
MergeSubgraph [in graphs.mgraph]

O

Open [in graphs.transfer]
OpenGraphs [in graphs.open_confluence]

P

Pack [in graphs.transfer]
prelim [in graphs.reduction]
PttdomGraphTheory [in graphs.open_confluence]
PttdomGraphTheory [in graphs.transfer]
PttdomGraphTheory.Open [in graphs.transfer]
PttdomGraphTheory.ostep [in graphs.open_confluence]
PttdomGraphTheory.PreGraphOps [in graphs.open_confluence]
PttdomGraphTheory.PreGraphTheory [in graphs.open_confluence]

Q

QuotBij [in graphs.finite_quotient]
QuotFun [in graphs.finite_quotient]
quot_union_K [in graphs.finite_quotient]
quot_id [in graphs.finite_quotient]
quot_quot [in graphs.finite_quotient]
quot_kernel [in graphs.finite_quotient]
quot.s [in graphs.finite_quotient]

S

s [in graphs.completeness]
s [in graphs.rewriting]
s [in graphs.mgraph]
s [in graphs.mgraph2]
s [in graphs.reduction]
sig_sum_bij.NonDisjoint [in graphs.finite_quotient]
sig_sum_bij.Disjoint [in graphs.finite_quotient]
sig_sum_bij [in graphs.finite_quotient]
s' [in graphs.reduction]
s.a [in graphs.reduction]
s.Edges [in graphs.mgraph]
s.h_merge_nothing' [in graphs.mgraph]
s.merge [in graphs.mgraph]
s.merge_union_K [in graphs.mgraph]
s.merge_merge_seq [in graphs.mgraph]
s.merge_nothing [in graphs.mgraph]
s.merge_same [in graphs.mgraph]
s.merge_same' [in graphs.mgraph]
s.merge_merge [in graphs.mgraph]
s.merge_surj [in graphs.mgraph]
s.Subgraphs [in graphs.mgraph]
s.union_merge_r [in graphs.mgraph]
s.union_merge_l [in graphs.mgraph]

T

t [in graphs.finite_quotient]
terms [in graphs.pttdom]
terms [in graphs.ptt]
terms.e [in graphs.pttdom]
terms.e [in graphs.ptt]
Theory [in graphs.structures]

U

union_quot_r [in graphs.finite_quotient]
union_quot_l [in graphs.finite_quotient]
update [in graphs.preliminaries]

---

Abbreviation Index

A

add_test_cong [in graphs.mgraph2]
add_test [in graphs.mgraph2]

C

CEquivalence [in graphs.structures]
CProper [in graphs.structures]

E

eC [in graphs.finite_quotient]
ereprK [in graphs.finite_quotient]

G

graph [in graphs.open_confluence]
graph [in graphs.transfer]
graph [in graphs.transfer]
graph [in graphs.transfer]
graph [in graphs.completeness]
graph [in graphs.rewriting]
graph [in graphs.mgraph]
graph [in graphs.mgraph2]
graph [in graphs.reduction]
graph [in graphs.reduction]
graph [in graphs.reduction]
graph2 [in graphs.open_confluence]
graph2 [in graphs.transfer]
graph2 [in graphs.transfer]
graph2 [in graphs.transfer]
graph2 [in graphs.completeness]
graph2 [in graphs.rewriting]
graph2 [in graphs.reduction]
graph2 [in graphs.reduction]
graph2 [in graphs.reduction]
G1 [in graphs.mgraph]
G12 [in graphs.mgraph]
G2 [in graphs.mgraph]

I

i [in graphs.structures]
IO [in graphs.mgraph2]

L

Le [in graphs.transfer]
Le [in graphs.transfer]
Le [in graphs.mgraph]
Le [in graphs.mgraph2]
Le [in graphs.reduction]
Lv [in graphs.transfer]
Lv [in graphs.transfer]
Lv [in graphs.mgraph]
Lv [in graphs.mgraph2]
Lv [in graphs.reduction]

M

merge_seq [in graphs.mgraph]
merge_seq [in graphs.mgraph]
merge2_seq [in graphs.mgraph2]
merge2_seq [in graphs.mgraph2]

N

nterm [in graphs.completeness]
nterm [in graphs.reduction]

P

point [in graphs.mgraph2]
point [in graphs.mgraph2]
pre_graph [in graphs.open_confluence]
pre_graph [in graphs.transfer]

R

rel0 [in graphs.preliminaries]

S

sig [in graphs.finite_quotient]
source [in graphs.mgraph]
source [in graphs.mgraph]
step [in graphs.completeness]
step [in graphs.reduction]
step [in graphs.reduction]
steps [in graphs.completeness]
steps [in graphs.reduction]
steps [in graphs.reduction]

T

target [in graphs.mgraph]
target [in graphs.mgraph]
term [in graphs.completeness]
term [in graphs.reduction]
test [in graphs.open_confluence]
test [in graphs.pttdom]
test [in graphs.transfer]
test [in graphs.completeness]
test [in graphs.rewriting]
test [in graphs.reduction]
test [in graphs.reduction]
tgraph [in graphs.completeness]
tgraph [in graphs.reduction]
tgraph2 [in graphs.completeness]
tgraph2 [in graphs.reduction]

V

vfun [in graphs.preliminaries]

---

Definition Index

A

add_edgeKr [in graphs.open_confluence]
add_test [in graphs.open_confluence]
add_edge [in graphs.open_confluence]
add_edge' [in graphs.open_confluence]
add_vertex [in graphs.open_confluence]
add_vertex [in graphs.mgraph]
add_vlabel [in graphs.mgraph]
add_edge [in graphs.mgraph]
add_vlabel2 [in graphs.mgraph2]
add_edge2 [in graphs.mgraph2]
add_vertex2 [in graphs.mgraph2]
admissible_l [in graphs.reduction]

B

bijD1 [in graphs.bij]
bijD1_bwd [in graphs.bij]
bijD1_fwd [in graphs.bij]
bij_quot [in graphs.finite_quotient]
bij_comp [in graphs.bij]
bij_sym [in graphs.bij]
bij_id [in graphs.bij]
bij_cast [in graphs.finmap_plus]
bij_setD [in graphs.finmap_plus]
bool_option_unit [in graphs.bij]
bool_swap [in graphs.bij]

C

consistent [in graphs.mgraph]
cr [in graphs.preliminaries]

D

disjoint_transL [in graphs.preliminaries]

E

edges [in graphs.mgraph]
edges_at [in graphs.open_confluence]
edges_in [in graphs.mgraph]
edges_at [in graphs.mgraph]
edge_set [in graphs.mgraph]
edge_graph [in graphs.mgraph]
edge_graph2 [in graphs.mgraph2]
edir_of [in graphs.transfer]
edir_body [in graphs.transfer]
efun_of [in graphs.transfer]
efun_body [in graphs.transfer]
equiv_comp [in graphs.finite_quotient]
equiv_of_trans [in graphs.preliminaries]
equiv_of_refl [in graphs.preliminaries]
equiv_of [in graphs.preliminaries]
eqvG_iso2R [in graphs.transfer]
eqvG_iso2L [in graphs.transfer]
eqvG_iso2 [in graphs.transfer]
eqv_test [in graphs.pttdom]
eqv_clot [in graphs.equiv]
eqv_ [in graphs.structures]
eqv' [in graphs.pttdom]
eq_setoid [in graphs.structures]
ET [in graphs.open_confluence]
eval [in graphs.pttdom]
eval [in graphs.ptt]

F

flat_labels [in graphs.structures]
flip_edge [in graphs.open_confluence]
foldr1 [in graphs.preliminaries]
fresh [in graphs.open_confluence]
fresh2_bij [in graphs.finmap_plus]
fsetD_bij [in graphs.finmap_plus]
fsetD_bij_bwd [in graphs.finmap_plus]
fsetD_bij_fwd [in graphs.finmap_plus]
fsetU1_fun [in graphs.finmap_plus]

G

graph_of_term [in graphs.reduction]
g2_pttdom [in graphs.mgraph2]
g2_ptt [in graphs.mgraph2]
g2_var [in graphs.mgraph2]
g2_top [in graphs.mgraph2]
g2_one [in graphs.mgraph2]
g2_dom [in graphs.mgraph2]
g2_cnv [in graphs.mgraph2]
g2_dot [in graphs.mgraph2]
g2_par [in graphs.mgraph2]

H

h_merge_union_Ke [in graphs.mgraph]
h_merge_union_Ke1 [in graphs.mgraph]
h_merge_union_K [in graphs.mgraph]
h_union_merge_l [in graphs.mgraph]
h_merge [in graphs.mgraph]
h' [in graphs.mgraph]

I

imfset_bij [in graphs.finmap_plus]
imfset_bij_bwd [in graphs.finmap_plus]
imfset_bij_fwd [in graphs.finmap_plus]
incident [in graphs.open_confluence]
incident [in graphs.mgraph]
induced [in graphs.mgraph]
induced_proof [in graphs.mgraph]
infer_test [in graphs.pttdom]
inj_e [in graphs.transfer]
inj_v [in graphs.transfer]
iso_subgraph_forT [in graphs.mgraph]
iso_comp [in graphs.mgraph]
iso_sym [in graphs.mgraph]
iso_id [in graphs.mgraph]
Iso' [in graphs.mgraph]
iso2prop [in graphs.mgraph2]
iso2_comp [in graphs.mgraph2]
iso2_sym [in graphs.mgraph2]
iso2_id [in graphs.mgraph2]
is_edge [in graphs.open_confluence]
is_test [in graphs.pttdom]

K

kernel [in graphs.finite_quotient]
kernelb [in graphs.finite_quotient]

L

largest [in graphs.preliminaries]

M

map_equiv_rel [in graphs.finite_quotient]
map_pairs [in graphs.equiv]
measure [in graphs.completeness]
mentions [in graphs.reduction]
merge [in graphs.mgraph]
merge_union [in graphs.finite_quotient]
merge_union_rel [in graphs.finite_quotient]
merge_disjoint_union [in graphs.finite_quotient]
merge_union_bwdEr [in graphs.finite_quotient]
merge_union_bwdEl [in graphs.finite_quotient]
merge_union_bwd [in graphs.finite_quotient]
merge_union_fwd [in graphs.finite_quotient]
merge_subgraph_iso [in graphs.mgraph]
merge_subgraph_e [in graphs.mgraph]
merge_subgraph_v [in graphs.mgraph]
merge_union_K [in graphs.mgraph]
merge_merge_seq [in graphs.mgraph]
merge_nothing [in graphs.mgraph]
merge_sameE [in graphs.mgraph]
merge_same [in graphs.mgraph]
merge_same' [in graphs.mgraph]
merge_iso [in graphs.mgraph]
merge_add_vlabelL [in graphs.reduction]
merge2 [in graphs.mgraph2]

N

nt [in graphs.pttdom]
nt_par [in graphs.pttdom]
nt_dot [in graphs.pttdom]
nt_dom [in graphs.pttdom]
nt_cnv [in graphs.pttdom]
nt_var [in graphs.pttdom]
nt_one [in graphs.pttdom]

O

oarc [in graphs.open_confluence]
oiso2E [in graphs.transfer]
open [in graphs.transfer]
open_add_test [in graphs.transfer]
open_add_vertex [in graphs.transfer]
option_void [in graphs.bij]
option_bij [in graphs.bij]
option2x [in graphs.bij]
option2_swap [in graphs.bij]
ord1 [in graphs.preliminaries]
ord2 [in graphs.preliminaries]
ord3 [in graphs.preliminaries]

P

pack [in graphs.transfer]
pack_add_test [in graphs.transfer]
pack_add_vertex [in graphs.transfer]
pack_v [in graphs.transfer]
pack' [in graphs.transfer]
pairs [in graphs.equiv]
pe_partition [in graphs.preliminaries]
pimset [in graphs.preliminaries]
pIO [in graphs.open_confluence]
pIO_add [in graphs.open_confluence]
proj_v [in graphs.transfer]
proj_e [in graphs.transfer]

Q

quot_union_K [in graphs.finite_quotient]
quot_id [in graphs.finite_quotient]
quot_quot [in graphs.finite_quotient]
quot_bij [in graphs.finite_quotient]
quot_kernel [in graphs.finite_quotient]
quot_same [in graphs.finite_quotient]
quot_fun [in graphs.finite_quotient]
quot.pi [in graphs.finite_quotient]
quot.quot [in graphs.finite_quotient]
quot.repr [in graphs.finite_quotient]

R

relabel [in graphs.mgraph2]
relabel2 [in graphs.mgraph2]
rel_of_pairs [in graphs.equiv]
remove_edges [in graphs.open_confluence]
remove_vertex [in graphs.open_confluence]
remove_vertex [in graphs.mgraph]
remove_edges [in graphs.mgraph]
replace_ioL [in graphs.reduction]
restrict [in graphs.preliminaries]

S

sc [in graphs.preliminaries]
setT_bij [in graphs.bij]
size_ind [in graphs.preliminaries]
smallest [in graphs.preliminaries]
step_order [in graphs.open_confluence]
subgraph [in graphs.mgraph]
subgraph_for [in graphs.mgraph]
subT_bij [in graphs.bij]
sub_edge [in graphs.mgraph]
sub_vertex [in graphs.mgraph]
sumA [in graphs.bij]
sumA' [in graphs.bij]
sumC [in graphs.bij]
sumf [in graphs.bij]
sum_left [in graphs.finite_quotient]
sum_eqE [in graphs.preliminaries]
surjective [in graphs.preliminaries]

T

term_of_nterm [in graphs.pttdom]
tgraph_of_nterm [in graphs.reduction]
tgraph_of_term [in graphs.reduction]
tm_pttdom [in graphs.pttdom]
tm_eqv [in graphs.pttdom]
tm_ptt [in graphs.ptt]
tm_eqv [in graphs.ptt]
two_graph [in graphs.mgraph]
two_graph2 [in graphs.mgraph2]
two_option_void' [in graphs.reduction]
two_option_void [in graphs.reduction]

U

union [in graphs.mgraph]
union_K_equiv [in graphs.finite_quotient]
union_quot_r [in graphs.finite_quotient]
union_equiv_r [in graphs.finite_quotient]
union_quot_l [in graphs.finite_quotient]
union_equiv_l_rel [in graphs.finite_quotient]
union_K_pairs [in graphs.mgraph]
union_merge_l [in graphs.mgraph]
unique [in graphs.preliminaries]
unit_graph [in graphs.mgraph]
unit_graph2 [in graphs.mgraph2]
unl [in graphs.mgraph]
unr [in graphs.mgraph]
update [in graphs.preliminaries]
updateE [in graphs.preliminaries]

V

vfun_of [in graphs.transfer]
vfun_body [in graphs.transfer]
void_graph [in graphs.mgraph]
void_countMixin [in graphs.preliminaries]
void_choiceMixin [in graphs.preliminaries]
VT [in graphs.open_confluence]

---

Record Index

B

bij [in graphs.bij]
box [in graphs.open_confluence]

E

eqvG [in graphs.open_confluence]

G

graph [in graphs.mgraph]
graph2 [in graphs.mgraph2]

I

inh_type [in graphs.open_confluence]
iso [in graphs.mgraph]
iso2 [in graphs.mgraph2]
is_graph [in graphs.open_confluence]
is_hom [in graphs.mgraph]

L

labels [in graphs.structures]

M

monoidLaws [in graphs.structures]

O

oiso2 [in graphs.transfer]
ops_ [in graphs.pttdom]

P

pre_graph [in graphs.open_confluence]
ptt [in graphs.ptt]
pttdom [in graphs.pttdom]

S

setoid [in graphs.structures]

T

test [in graphs.pttdom]

---

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

(1662 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

(63 entries)

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

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

(238 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

(16 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

(731 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

(56 entries)

Axiom 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

(6 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

(14 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

(101 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

(46 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

(69 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

(77 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

(224 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

(19 entries)