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

edoneequiv

## F

finite_quotientfinmap_plus

## M

mgraphmgraph2

## O

open_confluence## P

preliminariesptt

pttdom

## R

reductionrewriting

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