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

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

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

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

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

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

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

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

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

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

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

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

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

(13 entries)

---

Global Index

A

acyclic [definition, in LangAlg.graph]
add_inverse [lemma, in LangAlg.algebra]
algebra [library]
Alphabet [record, in LangAlg.tools]
Alphabet [inductive, in LangAlg.tools]
andb_prop_iff [lemma, in LangAlg.tools]
assignment [definition, in LangAlg.language]
ax [inductive, in LangAlg.expr]
axiom_is_lang_alg [lemma, in LangAlg.algebra]
axiom_inter_1_inter [projection, in LangAlg.algebra]
axiom_inter_1_comm_fois [projection, in LangAlg.algebra]
axiom_inter_1_conv [projection, in LangAlg.algebra]
axiom_inter_1_fois [projection, in LangAlg.algebra]
axiom_inter_idem [projection, in LangAlg.algebra]
axiom_inter_comm [projection, in LangAlg.algebra]
axiom_inter_assoc [projection, in LangAlg.algebra]
axiom_1_fois [projection, in LangAlg.algebra]
axiom_fois_1 [projection, in LangAlg.algebra]
axiom_fois_assoc [projection, in LangAlg.algebra]
axiom_inter_plus [projection, in LangAlg.algebra]
axiom_plus_inter [projection, in LangAlg.algebra]
axiom_inter_0 [projection, in LangAlg.algebra]
axiom_fois_plus [projection, in LangAlg.algebra]
axiom_plus_fois [projection, in LangAlg.algebra]
axiom_0_fois [projection, in LangAlg.algebra]
axiom_fois_0 [projection, in LangAlg.algebra]
axiom_plus_0 [projection, in LangAlg.algebra]
axiom_plus_ass [projection, in LangAlg.algebra]
axiom_plus_idem [projection, in LangAlg.algebra]
axiom_plus_com [projection, in LangAlg.algebra]
axiom_conv_conv [projection, in LangAlg.algebra]
axiom_conv_inter [projection, in LangAlg.algebra]
axiom_conv_fois [projection, in LangAlg.algebra]
axiom_conv_plus [projection, in LangAlg.algebra]
axiom_conv_0 [projection, in LangAlg.algebra]
axiom_conv_1 [projection, in LangAlg.algebra]
ax_𝐄_to_𝐓s_incl [lemma, in LangAlg.expr_terms]
ax_inter_1_inter [constructor, in LangAlg.expr]
ax_inter_1_comm_seq [constructor, in LangAlg.expr]
ax_inter_1_conv [constructor, in LangAlg.expr]
ax_inter_1_seq [constructor, in LangAlg.expr]
ax_conv_inter [constructor, in LangAlg.expr]
ax_conv_seq [constructor, in LangAlg.expr]
ax_conv_plus [constructor, in LangAlg.expr]
ax_conv_0 [constructor, in LangAlg.expr]
ax_conv_1 [constructor, in LangAlg.expr]
ax_conv_conv [constructor, in LangAlg.expr]
ax_inter_0 [constructor, in LangAlg.expr]
ax_inter_plus [constructor, in LangAlg.expr]
ax_plus_inter [constructor, in LangAlg.expr]
ax_inter_idem [constructor, in LangAlg.expr]
ax_inter_comm [constructor, in LangAlg.expr]
ax_inter_assoc [constructor, in LangAlg.expr]
ax_seq_plus [constructor, in LangAlg.expr]
ax_plus_seq [constructor, in LangAlg.expr]
ax_0_seq [constructor, in LangAlg.expr]
ax_seq_0 [constructor, in LangAlg.expr]
ax_plus_0 [constructor, in LangAlg.expr]
ax_plus_ass [constructor, in LangAlg.expr]
ax_plus_idem [constructor, in LangAlg.expr]
ax_plus_com [constructor, in LangAlg.expr]
ax_1_seq [constructor, in LangAlg.expr]
ax_seq_1 [constructor, in LangAlg.expr]
ax_seq_assoc [constructor, in LangAlg.expr]

B

balanced_nil [lemma, in LangAlg.tools]
bimap [definition, in LangAlg.tools]
bimap_equiv [instance, in LangAlg.tools]
Boolean [instance, in LangAlg.tools]
bottom_subst [lemma, in LangAlg.algebra]

C

comb [definition, in LangAlg.expr]
comb_lang [lemma, in LangAlg.expr]
comb_equiv [lemma, in LangAlg.expr]
completeness [library]
completeness_𝐄_equiv [lemma, in LangAlg.completeness]
completeness_𝐄_inf [lemma, in LangAlg.completeness]
completeness_𝐓_equiv [lemma, in LangAlg.completeness]
completeness_𝐓_inf [lemma, in LangAlg.completeness]
concat [inductive, in LangAlg.algebra]
concat_In [constructor, in LangAlg.algebra]
connected [definition, in LangAlg.graph]
contractible_graph [lemma, in LangAlg.graph]
conv_smaller [instance, in LangAlg.expr]
conv_equiv [instance, in LangAlg.expr]
conv_subst [lemma, in LangAlg.algebra]
co_nth_app_left [lemma, in LangAlg.to_lang_witness]
co_nth_app_right [lemma, in LangAlg.to_lang_witness]
co_nth_nth [lemma, in LangAlg.to_lang_witness]
co_nth_inj [lemma, in LangAlg.to_lang_witness]
co_nth_range [lemma, in LangAlg.to_lang_witness]
co_nth_In [lemma, in LangAlg.to_lang_witness]
co_nth [definition, in LangAlg.to_lang_witness]

D

decidable [section, in LangAlg.tools]
decidable_𝐄_equiv [lemma, in LangAlg.expr_graphs]
decidable_𝐄_inf [lemma, in LangAlg.expr_graphs]
decidable_edges [instance, in LangAlg.graph]
decidable_set [record, in LangAlg.tools]
decr [definition, in LangAlg.tools]
dec_hom.L [variable, in LangAlg.graph]
dec_hom.V2 [variable, in LangAlg.graph]
dec_hom.V1 [variable, in LangAlg.graph]
dec_hom.lbl [variable, in LangAlg.graph]
dec_hom.vert2 [variable, in LangAlg.graph]
dec_hom.vert1 [variable, in LangAlg.graph]
dec_hom [section, in LangAlg.graph]
dec_g.L [variable, in LangAlg.graph]
dec_g.V [variable, in LangAlg.graph]
dec_g.lbl [variable, in LangAlg.graph]
dec_g.vert [variable, in LangAlg.graph]
dec_g [section, in LangAlg.graph]
dec_X' [instance, in LangAlg.tools]
_ ⧼ _ ⧽ _ [notation, in LangAlg.tools]
dec_list [instance, in LangAlg.tools]
dec_list [section, in LangAlg.tools]
dec_option [lemma, in LangAlg.tools]
dec_prod [lemma, in LangAlg.tools]
def [section, in LangAlg.terms]
defs [section, in LangAlg.language]
defs.Σ [variable, in LangAlg.language]
def.X [variable, in LangAlg.terms]
_ ∩ _ (term_scope) [notation, in LangAlg.terms]
_ ⋅ _ (term_scope) [notation, in LangAlg.terms]
1 (term_scope) [notation, in LangAlg.terms]
def.Λ [variable, in LangAlg.terms]
domain [definition, in LangAlg.finite_functions]

E

edg [abbreviation, in LangAlg.sp_terms_graphs]
edge [definition, in LangAlg.graph]
edges [definition, in LangAlg.graph]
edges_filter_graph [lemma, in LangAlg.graph]
edges_graph_union [lemma, in LangAlg.graph]
edges_vertices [lemma, in LangAlg.graph]
edges_graph_map [lemma, in LangAlg.graph]
empty [definition, in LangAlg.language]
emptyset_inverse [lemma, in LangAlg.algebra]
eqA_Equivalence [projection, in LangAlg.algebra]
eqb [definition, in LangAlg.expr]
eqb_reflect [lemma, in LangAlg.expr]
eqB_Equivalence [projection, in LangAlg.algebra]
eqf [instance, in LangAlg.finite_functions]
eqf_Equivalence [instance, in LangAlg.finite_functions]
eqLang [definition, in LangAlg.algebra]
eqLang_Equivalence [lemma, in LangAlg.algebra]
equal_list_spec [lemma, in LangAlg.tools]
equal_list [definition, in LangAlg.tools]
equiv [projection, in LangAlg.tools]
Equiv [record, in LangAlg.tools]
equiv [constructor, in LangAlg.tools]
Equiv [inductive, in LangAlg.tools]
equivalent [definition, in LangAlg.tools]
equivalent_cons_Proper [instance, in LangAlg.tools]
equivalent_app_Proper [instance, in LangAlg.tools]
equivalent_Equivalence [instance, in LangAlg.tools]
equiv_0_inter [lemma, in LangAlg.expr]
equiv_Equivalence [instance, in LangAlg.expr]
equiv_𝕲e [lemma, in LangAlg.expr_graphs]
eqX [projection, in LangAlg.tools]
eqX_refl [lemma, in LangAlg.tools]
eqX_false [lemma, in LangAlg.tools]
eqX_correct [lemma, in LangAlg.tools]
eqX_eq [projection, in LangAlg.tools]
eqX' [definition, in LangAlg.tools]
eqX'_spec [lemma, in LangAlg.tools]
eq_ax [constructor, in LangAlg.expr]
eq_conv [constructor, in LangAlg.expr]
eq_inter [constructor, in LangAlg.expr]
eq_seq [constructor, in LangAlg.expr]
eq_plus [constructor, in LangAlg.expr]
eq_sym [constructor, in LangAlg.expr]
eq_trans [constructor, in LangAlg.expr]
eq_refl [constructor, in LangAlg.expr]
exists_path_spec [lemma, in LangAlg.graph]
exists_path [definition, in LangAlg.graph]
expr [library]
expr_terms [library]
expr_graphs [library]
ex_is_morphismb_correct [lemma, in LangAlg.graph]
ex_is_morphismb [definition, in LangAlg.graph]
ex_path_spec [lemma, in LangAlg.graph]
ex_path [definition, in LangAlg.graph]

F

filter_graph_visible [lemma, in LangAlg.graph]
filter_graph_map [lemma, in LangAlg.graph]
filter_graph_union [lemma, in LangAlg.graph]
filter_graph_true [lemma, in LangAlg.graph]
filter_graph_morphism [lemma, in LangAlg.graph]
filter_graph_path [lemma, in LangAlg.graph]
filter_graph [definition, in LangAlg.graph]
filter_equivalent_Proper [instance, in LangAlg.tools]
filter_incl_Proper [instance, in LangAlg.tools]
filter_NoDup [lemma, in LangAlg.tools]
filter_true [lemma, in LangAlg.tools]
filter_ext [lemma, in LangAlg.tools]
filter_ext_In [lemma, in LangAlg.tools]
filter_map [lemma, in LangAlg.tools]
filter_length_eq [lemma, in LangAlg.tools]
filter_length [lemma, in LangAlg.tools]
filter_app [lemma, in LangAlg.tools]
finite_concat [lemma, in LangAlg.algebra]
finite_inverse [lemma, in LangAlg.algebra]
finite_support_functions [definition, in LangAlg.finite_functions]
finite_support_finite_function [lemma, in LangAlg.finite_functions]
finite_support [definition, in LangAlg.finite_functions]
finite_function_is_finite [lemma, in LangAlg.finite_functions]
finite_functions [definition, in LangAlg.finite_functions]
finite_function [definition, in LangAlg.finite_functions]
finite_functions [library]
firstn_seq [lemma, in LangAlg.to_lang_witness]
fold_right_incl_smaller [lemma, in LangAlg.expr]
forall_existsb [lemma, in LangAlg.tools]
fst_𝐒𝐏_variables [lemma, in LangAlg.sp_terms]
funky_alg_𝐄 [lemma, in LangAlg.algebra]
funky_𝐄 [lemma, in LangAlg.algebra]
funky_is_lang_alg [lemma, in LangAlg.algebra]
funky_ax_ρ_prod_meet [projection, in LangAlg.algebra]
funky_ax_ρ_prod [projection, in LangAlg.algebra]
funky_ax_inter_idem [projection, in LangAlg.algebra]
funky_ax_inter_comm [projection, in LangAlg.algebra]
funky_ax_inter_assoc [projection, in LangAlg.algebra]
funky_ax_1_fois [projection, in LangAlg.algebra]
funky_ax_fois_1 [projection, in LangAlg.algebra]
funky_ax_fois_assoc [projection, in LangAlg.algebra]
funky_ax_inter_plus [projection, in LangAlg.algebra]
funky_ax_plus_inter [projection, in LangAlg.algebra]
funky_ax_inter_0 [projection, in LangAlg.algebra]
funky_ax_fois_plus [projection, in LangAlg.algebra]
funky_ax_plus_fois [projection, in LangAlg.algebra]
funky_ax_0_fois [projection, in LangAlg.algebra]
funky_ax_fois_0 [projection, in LangAlg.algebra]
funky_ax_plus_0 [projection, in LangAlg.algebra]
funky_ax_plus_ass [projection, in LangAlg.algebra]
funky_ax_plus_idem [projection, in LangAlg.algebra]
funky_ax_plus_com [projection, in LangAlg.algebra]
funky_ax_conv_conv [projection, in LangAlg.algebra]
funky_ax_conv_inter [projection, in LangAlg.algebra]
funky_ax_conv_fois [projection, in LangAlg.algebra]
funky_ax_conv_plus [projection, in LangAlg.algebra]
funky_ax_conv_0 [projection, in LangAlg.algebra]
funky_ax_conv_1 [projection, in LangAlg.algebra]
funky_alg [record, in LangAlg.algebra]
_ ==' _ [notation, in LangAlg.algebra]
⊥ [notation, in LangAlg.algebra]
⊤ [notation, in LangAlg.algebra]
_ ∨ _ [notation, in LangAlg.algebra]
_ ∧ _ [notation, in LangAlg.algebra]
_ • _ [notation, in LangAlg.algebra]
_ ⋆ [notation, in LangAlg.algebra]
_ == _ [notation, in LangAlg.algebra]
funky_alg.funky [variable, in LangAlg.algebra]
funky_lang_sig [projection, in LangAlg.algebra]
funky_alg_sig [record, in LangAlg.algebra]
funky_alg.ρ [variable, in LangAlg.algebra]
funky_alg.π [variable, in LangAlg.algebra]
funky_alg.eqB [variable, in LangAlg.algebra]
funky_alg.unit [variable, in LangAlg.algebra]
funky_alg.bottom [variable, in LangAlg.algebra]
funky_alg.inv [variable, in LangAlg.algebra]
funky_alg.meet [variable, in LangAlg.algebra]
funky_alg.prod [variable, in LangAlg.algebra]
funky_alg.join [variable, in LangAlg.algebra]
funky_alg.eqA [variable, in LangAlg.algebra]
funky_alg.B [variable, in LangAlg.algebra]
funky_alg.A [variable, in LangAlg.algebra]
funky_alg [section, in LangAlg.algebra]

G

g [section, in LangAlg.graph]
get_finite_support_function [lemma, in LangAlg.finite_functions]
good [definition, in LangAlg.graph]
good_for_par_𝕲 [lemma, in LangAlg.sp_terms_graphs]
good_for_seq_𝕲 [lemma, in LangAlg.sp_terms_graphs]
good_par_graph_union [lemma, in LangAlg.graph]
good_seq_graph_union [lemma, in LangAlg.graph]
good_for_par [definition, in LangAlg.graph]
good_for_seq [definition, in LangAlg.graph]
graph [definition, in LangAlg.graph]
graph [library]
graphs_equivb_correct [lemma, in LangAlg.expr_graphs]
graphs_smallerb_correct [lemma, in LangAlg.expr_graphs]
graphs_smallerb [definition, in LangAlg.expr_graphs]
graphs_equiv [instance, in LangAlg.expr_graphs]
graphs_smaller [instance, in LangAlg.expr_graphs]
graph_output [lemma, in LangAlg.sp_terms_graphs]
graph_input [lemma, in LangAlg.sp_terms_graphs]
graph_variables [lemma, in LangAlg.sp_terms_graphs]
graph_map_injective_good [lemma, in LangAlg.graph]
graph_map_injective_acyclic [lemma, in LangAlg.graph]
graph_union_assoc [lemma, in LangAlg.graph]
graph_map_union [lemma, in LangAlg.graph]
graph_union [definition, in LangAlg.graph]
graph_map_injective_connected [lemma, in LangAlg.graph]
graph_map_path [lemma, in LangAlg.graph]
graph_map_morphism [lemma, in LangAlg.graph]
graph_vertices_map [lemma, in LangAlg.graph]
graph_map_ext_in [lemma, in LangAlg.graph]
graph_vertices [instance, in LangAlg.graph]
graph_map_id [lemma, in LangAlg.graph]
graph_map_map [lemma, in LangAlg.graph]
graph_map [definition, in LangAlg.graph]
grph [abbreviation, in LangAlg.sp_terms_graphs]
grph [abbreviation, in LangAlg.graph]
g.L [variable, in LangAlg.graph]
_ ⋄ _ [notation, in LangAlg.graph]
_ ⋈ _ [notation, in LangAlg.graph]
_ -[ _ ]→ _ [notation, in LangAlg.graph]
_ ⊨ _ ⊲ _ [notation, in LangAlg.graph]
_ ⊨ _ -{ _ }→ _ [notation, in LangAlg.graph]
_ ⊨ _ -{ _ }⇀ _ [notation, in LangAlg.graph]

H

hom [abbreviation, in LangAlg.finite_functions]
hom_eq_Equivalence [instance, in LangAlg.graph]
hom_eq [definition, in LangAlg.graph]
hom_order_incl [lemma, in LangAlg.graph]
hom_order_PreOrder [instance, in LangAlg.graph]
hom_order [definition, in LangAlg.graph]

I

inb [definition, in LangAlg.tools]
inb_dec [lemma, in LangAlg.tools]
inb_false [lemma, in LangAlg.tools]
inb_spec [lemma, in LangAlg.tools]
inclb [definition, in LangAlg.tools]
inclb_correct [lemma, in LangAlg.tools]
incl_𝐒𝐏_inf [lemma, in LangAlg.sp_terms]
incl_app_split [lemma, in LangAlg.tools]
incl_app_or [lemma, in LangAlg.tools]
incl_nil [lemma, in LangAlg.tools]
incl_cons_Proper [instance, in LangAlg.tools]
incl_app_Proper [instance, in LangAlg.tools]
incl_PartialOrder [instance, in LangAlg.tools]
incl_PreOrder [instance, in LangAlg.tools]
incr [definition, in LangAlg.tools]
inf_ax_inter_r [lemma, in LangAlg.expr]
inf_ax_inter_l [lemma, in LangAlg.expr]
inf_zero [constructor, in LangAlg.expr]
inf_ax [constructor, in LangAlg.expr]
inf_conv [constructor, in LangAlg.expr]
inf_inter [constructor, in LangAlg.expr]
inf_seq [constructor, in LangAlg.expr]
inf_plus [constructor, in LangAlg.expr]
inf_trans [constructor, in LangAlg.expr]
inf_refl [constructor, in LangAlg.expr]
injective [definition, in LangAlg.tools]
injective_par_map_right [lemma, in LangAlg.sp_terms_graphs]
injective_par_map_left [lemma, in LangAlg.sp_terms_graphs]
injective_morphism_connected [lemma, in LangAlg.graph]
injective_map_hom_eq [lemma, in LangAlg.graph]
injective_graph_map_path [lemma, in LangAlg.graph]
injective_add_left [lemma, in LangAlg.tools]
injective_replace [lemma, in LangAlg.tools]
injective_compose [lemma, in LangAlg.tools]
input [definition, in LangAlg.graph]
input_filter_graph [lemma, in LangAlg.graph]
input_graph_union [lemma, in LangAlg.graph]
input_graph_map [lemma, in LangAlg.graph]
internal_map_b_spec [lemma, in LangAlg.graph]
internal_map_b [definition, in LangAlg.graph]
internal_map_graph_map [lemma, in LangAlg.graph]
internal_map [definition, in LangAlg.graph]
interpr [abbreviation, in LangAlg.algebra]
interpretation [definition, in LangAlg.algebra]
interprete [projection, in LangAlg.tools]
interprete [constructor, in LangAlg.tools]
intersection [definition, in LangAlg.language]
intersection_lang_eq [instance, in LangAlg.language]
intersection_lang_incl [instance, in LangAlg.language]
inter_distr [lemma, in LangAlg.expr]
inter_oner [lemma, in LangAlg.expr]
inter_onel [lemma, in LangAlg.expr]
inter_1_abs [lemma, in LangAlg.expr]
inter_plus [lemma, in LangAlg.expr]
inter_smaller [instance, in LangAlg.expr]
inter_equiv [instance, in LangAlg.expr]
inter_subst [lemma, in LangAlg.algebra]
inverse [inductive, in LangAlg.algebra]
inverse [definition, in LangAlg.tools]
inverse_par_map_right [lemma, in LangAlg.sp_terms_graphs]
inverse_par_map_left [lemma, in LangAlg.sp_terms_graphs]
inverse_graph_map_morphism [lemma, in LangAlg.graph]
inverse_In [constructor, in LangAlg.algebra]
inverse_add_left [lemma, in LangAlg.tools]
inverse_replace [lemma, in LangAlg.tools]
inverse_composition [lemma, in LangAlg.tools]
inv_eqLang [lemma, in LangAlg.algebra]
inv_eqA [projection, in LangAlg.algebra]
In_vertices [lemma, in LangAlg.sp_terms_graphs]
in_graph_vertices [lemma, in LangAlg.graph]
in_map [lemma, in LangAlg.graph]
in_bimap [lemma, in LangAlg.tools]
in_rm [lemma, in LangAlg.tools]
in_split_strict [lemma, in LangAlg.tools]
In_dec [lemma, in LangAlg.tools]
In_equivalent_Proper [instance, in LangAlg.tools]
In_incl_Proper [instance, in LangAlg.tools]
ispath [definition, in LangAlg.graph]
ispathb [definition, in LangAlg.graph]
ispathb_ispath [lemma, in LangAlg.graph]
ispath_app [lemma, in LangAlg.graph]
ispath_path [lemma, in LangAlg.graph]
is_term_comb [lemma, in LangAlg.expr]
is_term [definition, in LangAlg.expr]
is_balanced_𝐒𝐏'_variables [lemma, in LangAlg.sp_terms]
is_morph_𝐒𝐏_inf [lemma, in LangAlg.sp_terms_graphs]
is_morph_𝐒𝐏_ax [lemma, in LangAlg.sp_terms_graphs]
is_morphism_vertices [lemma, in LangAlg.sp_terms_graphs]
is_morphismb_correct [lemma, in LangAlg.graph]
is_morphismb [definition, in LangAlg.graph]
is_morphism_finite_function [lemma, in LangAlg.graph]
is_morphism_compose_weak [lemma, in LangAlg.graph]
is_morphism_compose [lemma, in LangAlg.graph]
is_morphism_id [lemma, in LangAlg.graph]
is_morphism_incl [lemma, in LangAlg.graph]
is_morphism [definition, in LangAlg.graph]
is_premorphism_compose_weak [lemma, in LangAlg.graph]
is_premorphism_incl [lemma, in LangAlg.graph]
is_premorphism_compose [lemma, in LangAlg.graph]
is_premorphism [definition, in LangAlg.graph]
is_lang_alg_𝐄 [lemma, in LangAlg.algebra]
is_lang_alg_languages [lemma, in LangAlg.algebra]
is_lang_alg_equiv [lemma, in LangAlg.algebra]
is_lang_alg_axiom [lemma, in LangAlg.algebra]
is_free_lang_alg_spec [lemma, in LangAlg.algebra]
is_free_lang_alg [definition, in LangAlg.algebra]
is_lang_alg_ax [lemma, in LangAlg.algebra]
is_lang_alg [definition, in LangAlg.algebra]
is_balanced_𝐖'_variables [lemma, in LangAlg.w_terms]
is_balanced_app [lemma, in LangAlg.tools]
is_balanced [definition, in LangAlg.tools]

J

join_eqLang [lemma, in LangAlg.algebra]
join_eqA [projection, in LangAlg.algebra]

L

labels [instance, in LangAlg.graph]
language [section, in LangAlg.expr]
language [definition, in LangAlg.language]
language [section, in LangAlg.sp_terms]
language [section, in LangAlg.w_terms]
language [section, in LangAlg.terms]
language [library]
languages [section, in LangAlg.algebra]
languages.Σ [variable, in LangAlg.algebra]
_ ⎣ _ ⎦ [notation, in LangAlg.algebra]
_ == _ [notation, in LangAlg.algebra]
_ ∨ _ [notation, in LangAlg.algebra]
_ ∧ _ [notation, in LangAlg.algebra]
_ • _ [notation, in LangAlg.algebra]
_ ⋆ [notation, in LangAlg.algebra]
language_algebra.lang_sig [variable, in LangAlg.algebra]
language_algebra.eqA [variable, in LangAlg.algebra]
language_algebra.unit [variable, in LangAlg.algebra]
language_algebra.bottom [variable, in LangAlg.algebra]
language_algebra.inv [variable, in LangAlg.algebra]
language_algebra.meet [variable, in LangAlg.algebra]
language_algebra.prod [variable, in LangAlg.algebra]
language_algebra.join [variable, in LangAlg.algebra]
language_algebra.A [variable, in LangAlg.algebra]
language_algebra [section, in LangAlg.algebra]
language.invert [section, in LangAlg.sp_terms]
language.invert [section, in LangAlg.terms]
language.rsimpl [section, in LangAlg.expr]
language.Ξ [section, in LangAlg.w_terms]
language.Ξ.Σ [variable, in LangAlg.w_terms]
lang_incl_PartialOrder [instance, in LangAlg.language]
lang_incl_PreOrder [instance, in LangAlg.language]
lang_eq_Equivalence [instance, in LangAlg.language]
lang_incl [instance, in LangAlg.language]
lang_eq [instance, in LangAlg.language]
lang_σΞ_even [lemma, in LangAlg.to_lang_witness]
lang_ω_morph [lemma, in LangAlg.to_lang_witness]
lang_nil [lemma, in LangAlg.to_lang_witness]
lang_even [lemma, in LangAlg.to_lang_witness]
lang_alg_is_funky_alg [lemma, in LangAlg.algebra]
lang_alg_is_funky_alg_sig [lemma, in LangAlg.algebra]
lang_to_funky.lang_alg [variable, in LangAlg.algebra]
lang_to_funky.lang_sig [variable, in LangAlg.algebra]
_ == _ [notation, in LangAlg.algebra]
_ ∨ _ [notation, in LangAlg.algebra]
_ ∧ _ [notation, in LangAlg.algebra]
_ • _ [notation, in LangAlg.algebra]
_ ⋆ [notation, in LangAlg.algebra]
lang_to_funky.eqA [variable, in LangAlg.algebra]
lang_to_funky.unit [variable, in LangAlg.algebra]
lang_to_funky.bottom [variable, in LangAlg.algebra]
lang_to_funky.inv [variable, in LangAlg.algebra]
lang_to_funky.meet [variable, in LangAlg.algebra]
lang_to_funky.prod [variable, in LangAlg.algebra]
lang_to_funky.join [variable, in LangAlg.algebra]
lang_to_funky.A [variable, in LangAlg.algebra]
lang_to_funky [section, in LangAlg.algebra]
lang_alg [record, in LangAlg.algebra]
lang_sig [record, in LangAlg.algebra]
length_rm_not_in [lemma, in LangAlg.tools]
length_app [lemma, in LangAlg.tools]
ln [definition, in LangAlg.sp_terms_graphs]
ln_pref_split_point [lemma, in LangAlg.sp_terms_graphs]
ln_non_zero [lemma, in LangAlg.sp_terms_graphs]
ln_smaller_size [lemma, in LangAlg.sp_terms_graphs]

M

make_total [definition, in LangAlg.finite_functions]
map [definition, in LangAlg.graph]
map_app [lemma, in LangAlg.graph]
map_map [lemma, in LangAlg.graph]
map_id [lemma, in LangAlg.graph]
map_bimap [lemma, in LangAlg.tools]
map_equivalent_Proper [instance, in LangAlg.tools]
map_incl_Proper [instance, in LangAlg.tools]
meet_eqLang [lemma, in LangAlg.algebra]
meet_eqA [projection, in LangAlg.algebra]
mirror [definition, in LangAlg.language]
mirror_nil [lemma, in LangAlg.language]
mirror_lang_eq [instance, in LangAlg.language]
mirror_lang_incl [instance, in LangAlg.language]
morphism_seq_step [lemma, in LangAlg.sp_terms_graphs]
morphism_seq_split [lemma, in LangAlg.sp_terms_graphs]
morphism_is_order_preserving [lemma, in LangAlg.graph]
morphism_ext_vertices [lemma, in LangAlg.graph]
morph_var [lemma, in LangAlg.sp_terms_graphs]
moustache [definition, in LangAlg.sp_terms_graphs]

N

N [definition, in LangAlg.to_lang_witness]
NatNum [instance, in LangAlg.tools]
neighbour [definition, in LangAlg.graph]
neighbour_spec [lemma, in LangAlg.graph]
NoDup_length [lemma, in LangAlg.tools]
NoDup_remove_3 [lemma, in LangAlg.tools]
not_incl_witness_Ξ [lemma, in LangAlg.to_lang_witness]
not_incl_witness [lemma, in LangAlg.to_lang_witness]
nth_NoDup [lemma, in LangAlg.to_lang_witness]
N_non_zero [lemma, in LangAlg.to_lang_witness]

O

option_bimap [definition, in LangAlg.tools]
orb_prop_iff [lemma, in LangAlg.tools]
output [definition, in LangAlg.graph]
output_filter_graph [lemma, in LangAlg.graph]
output_graph_union [lemma, in LangAlg.graph]
output_graph_map [lemma, in LangAlg.graph]

P

p [section, in LangAlg.graph]
par_𝐒𝐏_inf [instance, in LangAlg.sp_terms]
par_morphism_graph_union_right [lemma, in LangAlg.graph]
par_morphism_graph_union_left [lemma, in LangAlg.graph]
par_hom_order [lemma, in LangAlg.graph]
par_smaller_hom_order [lemma, in LangAlg.graph]
par_hom_order_weak_right [lemma, in LangAlg.graph]
par_hom_order_weak_left [lemma, in LangAlg.graph]
par_par_morphism_graph_union [lemma, in LangAlg.graph]
par_morphism_graph_union [lemma, in LangAlg.graph]
par_internal_graph_union [lemma, in LangAlg.graph]
par_graph_union_connected [lemma, in LangAlg.graph]
par_graph_union_decomp_right [lemma, in LangAlg.graph]
par_graph_union_decomp_left [lemma, in LangAlg.graph]
par_graph_union_decomp [lemma, in LangAlg.graph]
par_vertices_graph_union [lemma, in LangAlg.graph]
path [inductive, in LangAlg.graph]
path_par_right [lemma, in LangAlg.sp_terms_graphs]
path_par_left [lemma, in LangAlg.sp_terms_graphs]
path_par_cross [lemma, in LangAlg.sp_terms_graphs]
path_par [lemma, in LangAlg.sp_terms_graphs]
path_seq_right [lemma, in LangAlg.sp_terms_graphs]
path_seq_left [lemma, in LangAlg.sp_terms_graphs]
path_vertices [lemma, in LangAlg.sp_terms_graphs]
path_𝕲 [lemma, in LangAlg.sp_terms_graphs]
path_is_vertices [lemma, in LangAlg.graph]
path_ispath_short [lemma, in LangAlg.graph]
path_ispath [lemma, in LangAlg.graph]
path_seq [lemma, in LangAlg.graph]
path_graph_union [lemma, in LangAlg.graph]
path_par_union_right [lemma, in LangAlg.graph]
path_par_union_left [lemma, in LangAlg.graph]
path_par_union_cross [lemma, in LangAlg.graph]
path_par_union [lemma, in LangAlg.graph]
path_graph_vertices [lemma, in LangAlg.graph]
path_in_vertices [lemma, in LangAlg.graph]
path_non_trivial_only_for_vertices [lemma, in LangAlg.graph]
path_PreOrder [instance, in LangAlg.graph]
path_edge [constructor, in LangAlg.graph]
path_trans [constructor, in LangAlg.graph]
path_re [constructor, in LangAlg.graph]
plus_smaller [instance, in LangAlg.expr]
plus_equiv [instance, in LangAlg.expr]
powermonoid [section, in LangAlg.algebra]
powermonoid.associativity [variable, in LangAlg.algebra]
powermonoid.inv [variable, in LangAlg.algebra]
powermonoid.inv_prod [variable, in LangAlg.algebra]
powermonoid.inv_inv [variable, in LangAlg.algebra]
powermonoid.inv_unit [variable, in LangAlg.algebra]
powermonoid.left_neutrality [variable, in LangAlg.algebra]
powermonoid.M [variable, in LangAlg.algebra]
powermonoid.prod [variable, in LangAlg.algebra]
powermonoid.right_neutrality [variable, in LangAlg.algebra]
powermonoid.unit [variable, in LangAlg.algebra]
powermonoid.unit_not_prod [variable, in LangAlg.algebra]
_ @ _ [notation, in LangAlg.algebra]
_ @@ _ [notation, in LangAlg.algebra]
_ == _ [notation, in LangAlg.algebra]
_ ⊑ _ [notation, in LangAlg.algebra]
_ # [notation, in LangAlg.algebra]
_ ∨ _ [notation, in LangAlg.algebra]
_ ∧ _ [notation, in LangAlg.algebra]
_ • _ [notation, in LangAlg.algebra]
_ ⋆ [notation, in LangAlg.algebra]
{ _ } [notation, in LangAlg.algebra]
powermon_lang_alg [lemma, in LangAlg.algebra]
powermon_lang_sig [lemma, in LangAlg.algebra]
pref [definition, in LangAlg.sp_terms_graphs]
premorphism_ω [lemma, in LangAlg.to_lang_witness]
primed [section, in LangAlg.sp_terms]
primed [section, in LangAlg.w_terms]
primed [section, in LangAlg.tools]
_ ⊕' _ [notation, in LangAlg.w_terms]
_ ⊗' _ [notation, in LangAlg.w_terms]
𝟭' [notation, in LangAlg.w_terms]
prod [definition, in LangAlg.language]
prod_lang_eq [instance, in LangAlg.language]
prod_lang_incl [instance, in LangAlg.language]
prod_eqLang [lemma, in LangAlg.algebra]
prod_subst [lemma, in LangAlg.algebra]
prod_eqA [projection, in LangAlg.algebra]
proper_morphism_diff [lemma, in LangAlg.graph]
p.L [variable, in LangAlg.graph]
p.lbl [variable, in LangAlg.graph]
p.V [variable, in LangAlg.graph]
p.vert [variable, in LangAlg.graph]
_ -?→ _ [notation, in LangAlg.graph]
_ → _ [notation, in LangAlg.graph]

R

range [definition, in LangAlg.finite_functions]
replace [definition, in LangAlg.tools]
restriction [definition, in LangAlg.finite_functions]
rev_seq [lemma, in LangAlg.to_lang_witness]
rm [definition, in LangAlg.tools]
rm_equivalent_Proper [instance, in LangAlg.tools]
rm_incl_Proper [instance, in LangAlg.tools]
rm_length_in [lemma, in LangAlg.tools]
rm_length [lemma, in LangAlg.tools]
rm_app [lemma, in LangAlg.tools]
rm_notin [lemma, in LangAlg.tools]

S

s [section, in LangAlg.expr_terms]
s [section, in LangAlg.expr]
s [section, in LangAlg.sp_terms]
s [section, in LangAlg.to_lang_witness]
s [section, in LangAlg.sp_terms_graphs]
s [section, in LangAlg.expr_graphs]
s [section, in LangAlg.w_terms]
s [section, in LangAlg.finite_functions]
s [section, in LangAlg.w_terms_graphs]
s [section, in LangAlg.terms]
s [section, in LangAlg.terms_w_terms]
semantics [record, in LangAlg.tools]
semantics [inductive, in LangAlg.tools]
semantic_containment_PartialOrder [instance, in LangAlg.tools]
semantic_containment_PreOrder [instance, in LangAlg.tools]
semantic_equality_Equivalence [instance, in LangAlg.tools]
semantic_containment [definition, in LangAlg.tools]
semantic_equality [definition, in LangAlg.tools]
SemEquiv [record, in LangAlg.tools]
SemEquiv [inductive, in LangAlg.tools]
semEquiv_𝐄 [instance, in LangAlg.expr]
semEquiv_𝐒𝐏 [instance, in LangAlg.sp_terms]
semEquiv_𝐖 [instance, in LangAlg.w_terms]
semEquiv_𝐓 [instance, in LangAlg.terms]
SemSmaller [record, in LangAlg.tools]
SemSmaller [inductive, in LangAlg.tools]
semSmaller_𝐄 [instance, in LangAlg.expr]
semSmaller_𝐒𝐏 [instance, in LangAlg.sp_terms]
semSmaller_𝐖 [instance, in LangAlg.w_terms]
semSmaller_𝐓 [instance, in LangAlg.terms]
sem_eq_𝐄_conv [instance, in LangAlg.expr]
sem_eq_𝐄_inter [instance, in LangAlg.expr]
sem_eq_𝐄_seq [instance, in LangAlg.expr]
sem_eq_𝐄_plus [instance, in LangAlg.expr]
sem_incl_𝐄_conv [instance, in LangAlg.expr]
sem_incl_𝐄_inter [instance, in LangAlg.expr]
sem_incl_𝐄_fois [instance, in LangAlg.expr]
sem_incl_𝐄_plus [instance, in LangAlg.expr]
sem_eq_op [instance, in LangAlg.language]
sem_eq_𝐒𝐏_inter [instance, in LangAlg.sp_terms]
sem_eq_𝐒𝐏_seq [instance, in LangAlg.sp_terms]
sem_incl_𝐒𝐏_inter [instance, in LangAlg.sp_terms]
sem_incl_𝐒𝐏_seq [instance, in LangAlg.sp_terms]
sem_eq_𝐖_inter [instance, in LangAlg.w_terms]
sem_eq_𝐖_seq [instance, in LangAlg.w_terms]
sem_incl_𝐖_inter [instance, in LangAlg.w_terms]
sem_incl_𝐖_seq [instance, in LangAlg.w_terms]
sem_eq_𝐓_inter [instance, in LangAlg.terms]
sem_eq_𝐓_seq [instance, in LangAlg.terms]
sem_incl_𝐓_inter [instance, in LangAlg.terms]
sem_incl_𝐓_seq [instance, in LangAlg.terms]
sequiv [projection, in LangAlg.tools]
sequiv [constructor, in LangAlg.tools]
seq_distr [lemma, in LangAlg.expr]
seq_smaller [instance, in LangAlg.expr]
seq_equiv [instance, in LangAlg.expr]
seq_𝐒𝐏_inf [instance, in LangAlg.sp_terms]
seq_lang_prod [lemma, in LangAlg.to_lang_witness]
seq_lang_vertices [lemma, in LangAlg.to_lang_witness]
seq_last [lemma, in LangAlg.to_lang_witness]
seq_app [lemma, in LangAlg.to_lang_witness]
seq_morphism_graph_union_left [lemma, in LangAlg.graph]
seq_hom_order [lemma, in LangAlg.graph]
seq_morphism_graph_union [lemma, in LangAlg.graph]
seq_internal_graph_union [lemma, in LangAlg.graph]
seq_graph_union_connected [lemma, in LangAlg.graph]
seq_vertices_connected_graph_union [lemma, in LangAlg.graph]
seq_graph_union_decomp [lemma, in LangAlg.graph]
seq_morph_equivalent [lemma, in LangAlg.tools]
seq_morph_not_in [lemma, in LangAlg.tools]
seq_morph_in [lemma, in LangAlg.tools]
seq_morph [definition, in LangAlg.tools]
short_path [lemma, in LangAlg.graph]
size [projection, in LangAlg.tools]
Size [record, in LangAlg.tools]
size [constructor, in LangAlg.tools]
Size [inductive, in LangAlg.tools]
size_𝐄 [instance, in LangAlg.expr]
size_ln [lemma, in LangAlg.sp_terms_graphs]
size_𝐖'_to_𝐓 [lemma, in LangAlg.terms_w_terms]
size_term_to_𝐖' [lemma, in LangAlg.terms_w_terms]
size_𝐒𝐏_to_𝐓 [lemma, in LangAlg.terms_w_terms]
skipn_seq [lemma, in LangAlg.to_lang_witness]
smaller [projection, in LangAlg.tools]
Smaller [record, in LangAlg.tools]
smaller [constructor, in LangAlg.tools]
Smaller [inductive, in LangAlg.tools]
smaller_equiv_iff_inter [lemma, in LangAlg.expr]
smaller_conv_iff [lemma, in LangAlg.expr]
smaller_equiv_iff_plus [lemma, in LangAlg.expr]
smaller_PartialOrder [instance, in LangAlg.expr]
smaller_equiv [lemma, in LangAlg.expr]
smaller_PreOrder [instance, in LangAlg.expr]
smaller_𝕲e [lemma, in LangAlg.expr_graphs]
smaller_par_hom_order [lemma, in LangAlg.graph]
split_list [lemma, in LangAlg.expr]
split_one [lemma, in LangAlg.expr]
split_point_in_moustache [lemma, in LangAlg.sp_terms_graphs]
split_moustache_inf [lemma, in LangAlg.sp_terms_graphs]
split_moustache [lemma, in LangAlg.sp_terms_graphs]
split_point [definition, in LangAlg.sp_terms_graphs]
split_path [lemma, in LangAlg.graph]
sp_terms_graphs [library]
sp_terms [library]
ssmaller [projection, in LangAlg.tools]
ssmaller [constructor, in LangAlg.tools]
sub_identity_par_one [lemma, in LangAlg.w_terms]
suf [definition, in LangAlg.sp_terms_graphs]
sum [definition, in LangAlg.expr]
sum_lang [lemma, in LangAlg.expr]
sum_app [lemma, in LangAlg.expr]
supid_hom_order [lemma, in LangAlg.sp_terms_graphs]
support [projection, in LangAlg.tools]
Support [record, in LangAlg.tools]
support [constructor, in LangAlg.tools]
Support [inductive, in LangAlg.tools]
suppT [instance, in LangAlg.terms]
swap [definition, in LangAlg.graph]
s.D [variable, in LangAlg.finite_functions]
s.dec_X [variable, in LangAlg.expr_terms]
s.dec_X [variable, in LangAlg.expr]
s.dec_X [variable, in LangAlg.to_lang_witness]
s.dec_X [variable, in LangAlg.expr_graphs]
s.dec_X [variable, in LangAlg.terms_w_terms]
s.R [variable, in LangAlg.finite_functions]
s.seq [section, in LangAlg.sp_terms_graphs]
s.src [variable, in LangAlg.finite_functions]
s.trg [variable, in LangAlg.finite_functions]
s.u [variable, in LangAlg.to_lang_witness]
s.X [variable, in LangAlg.expr_terms]
s.X [variable, in LangAlg.expr]
s.X [variable, in LangAlg.to_lang_witness]
s.X [variable, in LangAlg.sp_terms_graphs]
s.X [variable, in LangAlg.expr_graphs]
s.X [variable, in LangAlg.w_terms_graphs]
s.X [variable, in LangAlg.terms_w_terms]
0 (expr_scope) [notation, in LangAlg.expr]
1 (expr_scope) [notation, in LangAlg.expr]
_ ° (expr_scope) [notation, in LangAlg.expr]
_ ∩ _ (expr_scope) [notation, in LangAlg.expr]
_ + _ (expr_scope) [notation, in LangAlg.expr]
_ ⋅ _ (expr_scope) [notation, in LangAlg.expr]
_ ° (term_scope) [notation, in LangAlg.terms]
⟨ _ ⟩ (term_scope) [notation, in LangAlg.terms]
_ ⊨ _ << _ [notation, in LangAlg.sp_terms]
_ ⤏ _ [notation, in LangAlg.to_lang_witness]
_ ⊕ _ [notation, in LangAlg.w_terms]
_ ⊗ _ [notation, in LangAlg.w_terms]
⋃ _ [notation, in LangAlg.expr]
s.Λ [variable, in LangAlg.sp_terms_graphs]
s.Λ [variable, in LangAlg.w_terms_graphs]
s.𝐀 [variable, in LangAlg.to_lang_witness]
s0 [section, in LangAlg.sp_terms]
s0 [section, in LangAlg.w_terms]
s0.X [variable, in LangAlg.sp_terms]
s0.X [variable, in LangAlg.w_terms]

T

t [section, in LangAlg.to_lang_witness]
T [definition, in LangAlg.w_terms]
t [section, in LangAlg.completeness]
terms [library]
terms_w_terms [library]
terms_graphs [library]
test_compatible_app [lemma, in LangAlg.language]
test_compatible [definition, in LangAlg.language]
test_compatible_nil [lemma, in LangAlg.sp_terms]
test_compatible_Ξ [lemma, in LangAlg.w_terms]
test_compatible_𝐓_to_test_not_empty [lemma, in LangAlg.terms]
test_compatible_𝐓_to_test_false [lemma, in LangAlg.terms]
test_compatible_𝐓_to_test_true [lemma, in LangAlg.terms]
test_compatible_𝐓_to_test [lemma, in LangAlg.terms]
tools [library]
to_lang_𝐄 [instance, in LangAlg.expr]
to_lang_𝐒𝐏 [instance, in LangAlg.sp_terms]
to_lang_𝐄_interpretation [lemma, in LangAlg.algebra]
to_lang_𝐖 [instance, in LangAlg.w_terms]
to_lang_𝐓 [instance, in LangAlg.terms]
to_test_equivalent [instance, in LangAlg.terms]
to_test_inf_flip [instance, in LangAlg.terms]
to_test_inf [instance, in LangAlg.terms]
to_test [definition, in LangAlg.terms]
to_lang_witness [library]
t.dec_X [variable, in LangAlg.to_lang_witness]
t.dec_X [variable, in LangAlg.completeness]
t.X [variable, in LangAlg.to_lang_witness]
t.X [variable, in LangAlg.completeness]

U

union [definition, in LangAlg.language]
union_lang_eq [instance, in LangAlg.language]
union_lang_incl [instance, in LangAlg.language]
union_subst [lemma, in LangAlg.algebra]
unit [definition, in LangAlg.language]
unit_subst [lemma, in LangAlg.algebra]

V

variables [projection, in LangAlg.tools]
variables [constructor, in LangAlg.tools]
variables_graph_union [lemma, in LangAlg.graph]
variables_hom_eq [lemma, in LangAlg.graph]
variables_hom_order [lemma, in LangAlg.graph]
variables_morphism [lemma, in LangAlg.graph]
variables_premorphism [lemma, in LangAlg.graph]
variables_graph_map [lemma, in LangAlg.graph]
variables_𝐖'_seq [lemma, in LangAlg.w_terms]
variables_𝐖'_par [lemma, in LangAlg.w_terms]
variables_𝐖_seq [lemma, in LangAlg.w_terms]
variables_𝐖_par [lemma, in LangAlg.w_terms]
variables_𝐒𝐏_to_𝐓 [lemma, in LangAlg.terms_w_terms]
variables_𝐓_to_𝐖' [lemma, in LangAlg.terms_w_terms]
Vert [definition, in LangAlg.to_lang_witness]
vertex_0 [lemma, in LangAlg.sp_terms_graphs]
vertex_ln [lemma, in LangAlg.sp_terms_graphs]
vertices [definition, in LangAlg.sp_terms_graphs]
vertices_graph_vertices [lemma, in LangAlg.sp_terms_graphs]
vertices_bounded [lemma, in LangAlg.sp_terms_graphs]
vertices_graph_union [lemma, in LangAlg.graph]
Vert_vertices [lemma, in LangAlg.to_lang_witness]
Vert_NoDup [lemma, in LangAlg.to_lang_witness]
visible [definition, in LangAlg.graph]
visible_moustache [lemma, in LangAlg.sp_terms_graphs]

W

w [section, in LangAlg.to_lang_witness]
weak_graph_infb_correct [lemma, in LangAlg.w_terms_graphs]
weak_graph_infb [definition, in LangAlg.w_terms_graphs]
weak_graph_inf [instance, in LangAlg.w_terms_graphs]
weak_graph [definition, in LangAlg.w_terms_graphs]
witness_Ξ [lemma, in LangAlg.to_lang_witness]
word [definition, in LangAlg.to_lang_witness]
word_of_term_correct [lemma, in LangAlg.to_lang_witness]
w_u [definition, in LangAlg.to_lang_witness]
w_terms_graphs [library]
w_terms [library]
w.dec_X [variable, in LangAlg.to_lang_witness]
w.X [variable, in LangAlg.to_lang_witness]

X

X_dec [lemma, in LangAlg.tools]
X' [definition, in LangAlg.tools]

other

0 (expr_scope) [notation, in LangAlg.expr]
1 (expr_scope) [notation, in LangAlg.expr]
_ ° (expr_scope) [notation, in LangAlg.expr]
_ ∩ _ (expr_scope) [notation, in LangAlg.expr]
_ + _ (expr_scope) [notation, in LangAlg.expr]
_ ⋅ _ (expr_scope) [notation, in LangAlg.expr]
1 (lang_scope) [notation, in LangAlg.language]
0 (lang_scope) [notation, in LangAlg.language]
_ ° (lang_scope) [notation, in LangAlg.language]
_ + _ (lang_scope) [notation, in LangAlg.language]
_ ∩ _ (lang_scope) [notation, in LangAlg.language]
_ ⋅ _ (lang_scope) [notation, in LangAlg.language]
⟨ _ ⟩ (term_scope) [notation, in LangAlg.terms]
_ ° (term_scope) [notation, in LangAlg.terms]
_ ∩ _ (term_scope) [notation, in LangAlg.terms]
_ ⋅ _ (term_scope) [notation, in LangAlg.terms]
1 (term_scope) [notation, in LangAlg.terms]
_ ⊢ _ [notation, in LangAlg.language]
_ ⋵ _ [notation, in LangAlg.language]
_ ⊨ _ << _ [notation, in LangAlg.sp_terms]
_ ∥ _ [notation, in LangAlg.sp_terms]
_ ⨾ _ [notation, in LangAlg.sp_terms]
_ -[ _ ]?→ _ [notation, in LangAlg.graph]
_ ⋄ _ [notation, in LangAlg.graph]
_ -[ _ ]→ _ [notation, in LangAlg.graph]
_ ⋈ _ [notation, in LangAlg.graph]
_ ⊨ _ ⊲ _ [notation, in LangAlg.graph]
_ ⊨ _ -{ _ }⇀ _ [notation, in LangAlg.graph]
_ ⊨ _ -{ _ }→ _ [notation, in LangAlg.graph]
_ ⊗' _ [notation, in LangAlg.w_terms]
_ ⊕' _ [notation, in LangAlg.w_terms]
_ ⊕ _ [notation, in LangAlg.w_terms]
_ ⊗ _ [notation, in LangAlg.w_terms]
_ ⧼ _ ⧽ _ [notation, in LangAlg.tools]
_ ≈ _ [notation, in LangAlg.tools]
_ ∈ _ [notation, in LangAlg.tools]
_ ⊆ _ [notation, in LangAlg.tools]
_ ≲ _ [notation, in LangAlg.tools]
_ ≤ _ [notation, in LangAlg.tools]
_ ≃ _ [notation, in LangAlg.tools]
_ ≡ _ [notation, in LangAlg.tools]
_ ∘ _ [notation, in LangAlg.tools]
{| _ \ _ |} [notation, in LangAlg.tools]
⋃ _ [notation, in LangAlg.expr]
⌈ _ ⌉ [notation, in LangAlg.tools]
⌊ _ ⌋ [notation, in LangAlg.tools]
⟦ _ ⟧ _ [notation, in LangAlg.tools]
⦃ _ ⦄ [notation, in LangAlg.tools]
⨥ [notation, in LangAlg.tools]
⨪ [notation, in LangAlg.tools]
π{ _ } [notation, in LangAlg.tools]
𝕬[ _ → _ ] [notation, in LangAlg.language]
𝟭 [notation, in LangAlg.w_terms]
𝟭' [notation, in LangAlg.w_terms]
ø [definition, in LangAlg.algebra]
Ξ [definition, in LangAlg.w_terms]
Ξ_σΞ_nil [lemma, in LangAlg.to_lang_witness]
γ [definition, in LangAlg.to_lang_witness]
γN [lemma, in LangAlg.to_lang_witness]
γ_path [lemma, in LangAlg.to_lang_witness]
γ_le [lemma, in LangAlg.to_lang_witness]
γ_bij [lemma, in LangAlg.to_lang_witness]
γ_inj [lemma, in LangAlg.to_lang_witness]
γ0 [lemma, in LangAlg.to_lang_witness]
ε [definition, in LangAlg.algebra]
μ [definition, in LangAlg.sp_terms_graphs]
μ_morph [lemma, in LangAlg.sp_terms_graphs]
μ_internal [lemma, in LangAlg.sp_terms_graphs]
μ_k [lemma, in LangAlg.sp_terms_graphs]
μ_ln [lemma, in LangAlg.sp_terms_graphs]
μ_0 [lemma, in LangAlg.sp_terms_graphs]
π_inv [projection, in LangAlg.algebra]
π_prod [projection, in LangAlg.algebra]
ρ_morph [projection, in LangAlg.algebra]
ρπ [projection, in LangAlg.algebra]
σ [definition, in LangAlg.to_lang_witness]
σ_spec [lemma, in LangAlg.to_lang_witness]
σ_nil [lemma, in LangAlg.to_lang_witness]
σ' [definition, in LangAlg.to_lang_witness]
σ'_nil [lemma, in LangAlg.to_lang_witness]
σΞ [definition, in LangAlg.to_lang_witness]
σΞ_σ_subword [lemma, in LangAlg.to_lang_witness]
σΞ_nil [lemma, in LangAlg.to_lang_witness]
ω [definition, in LangAlg.to_lang_witness]
ω_seq [lemma, in LangAlg.to_lang_witness]
ω_nil [lemma, in LangAlg.to_lang_witness]
ω_word [lemma, in LangAlg.to_lang_witness]
𝐄 [inductive, in LangAlg.expr]
𝐄_to_𝐓s_lang [lemma, in LangAlg.expr_terms]
𝐄_to_𝐓_lang [lemma, in LangAlg.expr_terms]
𝐄_to_𝐓s_inf_iff [lemma, in LangAlg.expr_terms]
𝐄_to_𝐓s_inf [lemma, in LangAlg.expr_terms]
𝐄_to_𝐓_comb [lemma, in LangAlg.expr_terms]
𝐄_to_𝐓_to_𝐄 [lemma, in LangAlg.expr_terms]
𝐄_to_𝐓s [definition, in LangAlg.expr_terms]
𝐄_to_𝐓 [definition, in LangAlg.expr_terms]
𝐄_inf_incl_lang [lemma, in LangAlg.expr]
𝐄_eq_equiv_lang [lemma, in LangAlg.expr]
𝐄_sem_PartialOrder [instance, in LangAlg.expr]
𝐄_sem_PreOrder [instance, in LangAlg.expr]
𝐄_sem_equiv [instance, in LangAlg.expr]
𝐄_empty [lemma, in LangAlg.expr]
𝐄_unit [lemma, in LangAlg.expr]
𝐄_variable [lemma, in LangAlg.expr]
𝐄_mirror [lemma, in LangAlg.expr]
𝐄_intersection [lemma, in LangAlg.expr]
𝐄_prod [lemma, in LangAlg.expr]
𝐄_union [lemma, in LangAlg.expr]
𝐄_Smaller [instance, in LangAlg.expr]
𝐄_inf [inductive, in LangAlg.expr]
𝐄_Equiv [instance, in LangAlg.expr]
𝐄_eq [inductive, in LangAlg.expr]
𝐄_decidable_set [instance, in LangAlg.expr]
𝐄_size_conv [lemma, in LangAlg.expr]
𝐄_size_plus [lemma, in LangAlg.expr]
𝐄_size_inter [lemma, in LangAlg.expr]
𝐄_size_seq [lemma, in LangAlg.expr]
𝐄_size_var [lemma, in LangAlg.expr]
𝐄_size_zero [lemma, in LangAlg.expr]
𝐄_size_one [lemma, in LangAlg.expr]
𝐄_conv [constructor, in LangAlg.expr]
𝐄_plus [constructor, in LangAlg.expr]
𝐄_inter [constructor, in LangAlg.expr]
𝐄_seq [constructor, in LangAlg.expr]
𝐄_var [constructor, in LangAlg.expr]
𝐄_zero [constructor, in LangAlg.expr]
𝐄_one [constructor, in LangAlg.expr]
𝐄_neq_𝐓s_neq [lemma, in LangAlg.expr_graphs]
𝐒𝐏 [inductive, in LangAlg.sp_terms]
𝐒𝐏_variable [lemma, in LangAlg.sp_terms]
𝐒𝐏_intersection [lemma, in LangAlg.sp_terms]
𝐒𝐏_prod [lemma, in LangAlg.sp_terms]
𝐒𝐏_sem_PartialOrder [instance, in LangAlg.sp_terms]
𝐒𝐏_sem_equiv [instance, in LangAlg.sp_terms]
𝐒𝐏_sem_PreOrder [instance, in LangAlg.sp_terms]
𝐒𝐏_size_𝐒𝐏'_variables [lemma, in LangAlg.sp_terms]
𝐒𝐏_variables_𝐒𝐏'_variables_iff [lemma, in LangAlg.sp_terms]
𝐒𝐏_variables_𝐒𝐏'_variables [lemma, in LangAlg.sp_terms]
𝐒𝐏_inf_variables [lemma, in LangAlg.sp_terms]
𝐒𝐏_inf_PreOrder [instance, in LangAlg.sp_terms]
𝐒𝐏_inf_par [constructor, in LangAlg.sp_terms]
𝐒𝐏_inf_seq [constructor, in LangAlg.sp_terms]
𝐒𝐏_inf_axinf [constructor, in LangAlg.sp_terms]
𝐒𝐏_inf_ax [constructor, in LangAlg.sp_terms]
𝐒𝐏_inf_trans [constructor, in LangAlg.sp_terms]
𝐒𝐏_inf_re [constructor, in LangAlg.sp_terms]
𝐒𝐏_inf [inductive, in LangAlg.sp_terms]
𝐒𝐏_axinf_1_seqr [constructor, in LangAlg.sp_terms]
𝐒𝐏_axinf_1_seql [constructor, in LangAlg.sp_terms]
𝐒𝐏_axinf_weak [constructor, in LangAlg.sp_terms]
𝐒𝐏_axinf [inductive, in LangAlg.sp_terms]
𝐒𝐏_par_idem [constructor, in LangAlg.sp_terms]
𝐒𝐏_par_comm [constructor, in LangAlg.sp_terms]
𝐒𝐏_par_assoc [constructor, in LangAlg.sp_terms]
𝐒𝐏_seq_assoc [constructor, in LangAlg.sp_terms]
𝐒𝐏_ax [inductive, in LangAlg.sp_terms]
𝐒𝐏_size_𝐒𝐏_variables_eq [lemma, in LangAlg.sp_terms]
𝐒𝐏_size_𝐒𝐏_variables [lemma, in LangAlg.sp_terms]
𝐒𝐏_size_par [lemma, in LangAlg.sp_terms]
𝐒𝐏_size_seq [lemma, in LangAlg.sp_terms]
𝐒𝐏_size_var [lemma, in LangAlg.sp_terms]
𝐒𝐏_size [instance, in LangAlg.sp_terms]
𝐒𝐏_variables_par [lemma, in LangAlg.sp_terms]
𝐒𝐏_variables_seq [lemma, in LangAlg.sp_terms]
𝐒𝐏_variables_var [lemma, in LangAlg.sp_terms]
𝐒𝐏_variables [instance, in LangAlg.sp_terms]
𝐒𝐏_par [constructor, in LangAlg.sp_terms]
𝐒𝐏_seq [constructor, in LangAlg.sp_terms]
𝐒𝐏_var [constructor, in LangAlg.sp_terms]
𝐒𝐏_inf_is_morph_iff [lemma, in LangAlg.sp_terms_graphs]
𝐒𝐏_inf_is_morph [lemma, in LangAlg.sp_terms_graphs]
𝐒𝐏_inf_moustache [lemma, in LangAlg.sp_terms_graphs]
𝐒𝐏_inf_pref_suf [lemma, in LangAlg.sp_terms_graphs]
𝐒𝐏_to_𝐓_lang [lemma, in LangAlg.terms_w_terms]
𝐒𝐏_to_𝐓 [definition, in LangAlg.terms_w_terms]
𝐒𝐏'_variables [definition, in LangAlg.sp_terms]
𝐓 [inductive, in LangAlg.terms]
𝐓s_eq [instance, in LangAlg.expr_terms]
𝐓s_inf [instance, in LangAlg.expr_terms]
𝐓_inf_incl_lang [lemma, in LangAlg.expr_terms]
𝐓_to_𝐄_lang [lemma, in LangAlg.expr_terms]
𝐓_to_𝐄_inf [lemma, in LangAlg.expr_terms]
𝐓_to_𝐄_to_𝐓 [lemma, in LangAlg.expr_terms]
𝐓_to_𝐄 [definition, in LangAlg.expr_terms]
𝐓_incl_lang_inf [lemma, in LangAlg.completeness]
𝐓_inf_is_weak_graph_inf [lemma, in LangAlg.terms_graphs]
𝐓_unit [lemma, in LangAlg.terms]
𝐓_variable [lemma, in LangAlg.terms]
𝐓_mirror [lemma, in LangAlg.terms]
𝐓_intersection [lemma, in LangAlg.terms]
𝐓_prod [lemma, in LangAlg.terms]
𝐓_sem_PartialOrder [instance, in LangAlg.terms]
𝐓_sem_PreOrder [instance, in LangAlg.terms]
𝐓_sem_equiv [instance, in LangAlg.terms]
𝐓_conv_inf [instance, in LangAlg.terms]
𝐓_conv_equiv [instance, in LangAlg.terms]
𝐓_conv_one [lemma, in LangAlg.terms]
𝐓_conv_idem [lemma, in LangAlg.terms]
𝐓_conv [definition, in LangAlg.terms]
𝐓_weak_par [lemma, in LangAlg.terms]
𝐓_weak_seq [lemma, in LangAlg.terms]
𝐓_to_test_distr [lemma, in LangAlg.terms]
𝐓_to_test_distr2 [lemma, in LangAlg.terms]
𝐓_to_test_distr1 [lemma, in LangAlg.terms]
𝐓_to_test_dupl [lemma, in LangAlg.terms]
𝐓_to_test_comm [lemma, in LangAlg.terms]
𝐓_to_test_is_par_one [lemma, in LangAlg.terms]
𝐓_to_test_incl_inf [lemma, in LangAlg.terms]
𝐓_to_test_in [lemma, in LangAlg.terms]
𝐓_to_test_app [lemma, in LangAlg.terms]
𝐓_to_test_one [lemma, in LangAlg.terms]
𝐓_size_to_test [lemma, in LangAlg.terms]
𝐓_variables_to_test [lemma, in LangAlg.terms]
𝐓_inf_variables_incl [lemma, in LangAlg.terms]
𝐓_var_inter [lemma, in LangAlg.terms]
𝐓_var_seq [lemma, in LangAlg.terms]
𝐓_var_cvar [lemma, in LangAlg.terms]
𝐓_var_var [lemma, in LangAlg.terms]
𝐓_var_1 [lemma, in LangAlg.terms]
𝐓_size_inter [lemma, in LangAlg.terms]
𝐓_size_seq [lemma, in LangAlg.terms]
𝐓_size_var [lemma, in LangAlg.terms]
𝐓_size_cvar [lemma, in LangAlg.terms]
𝐓_size_1 [lemma, in LangAlg.terms]
𝐓_size [instance, in LangAlg.terms]
𝐓_inf_one_prod_is_inter [lemma, in LangAlg.terms]
𝐓_inter_oner [lemma, in LangAlg.terms]
𝐓_inter_onel [lemma, in LangAlg.terms]
𝐓_inter_one_abs [lemma, in LangAlg.terms]
𝐓_inf_PartialOrder [instance, in LangAlg.terms]
𝐓_inf_eq_inter [lemma, in LangAlg.terms]
𝐓_eq_inf [lemma, in LangAlg.terms]
𝐓_inter_intro [lemma, in LangAlg.terms]
𝐓_inter_elim [lemma, in LangAlg.terms]
𝐓_seq_smaller [instance, in LangAlg.terms]
𝐓_inter_smaller [instance, in LangAlg.terms]
𝐓_seq_equiv [instance, in LangAlg.terms]
𝐓_inter_equiv [instance, in LangAlg.terms]
𝐓_inf_PreOrder [instance, in LangAlg.terms]
𝐓_eq_Equivalence [instance, in LangAlg.terms]
𝐓_exchange [lemma, in LangAlg.terms]
𝐓_inter_one_inter [lemma, in LangAlg.terms]
𝐓_inter_one_comm_seq [lemma, in LangAlg.terms]
𝐓_inter_one_conv [lemma, in LangAlg.terms]
𝐓_inter_one_seq [lemma, in LangAlg.terms]
𝐓_inter_idem [lemma, in LangAlg.terms]
𝐓_inter_comm [lemma, in LangAlg.terms]
𝐓_inter_assoc [lemma, in LangAlg.terms]
𝐓_seq_one_right [lemma, in LangAlg.terms]
𝐓_seq_one_left [lemma, in LangAlg.terms]
𝐓_seq_assoc [lemma, in LangAlg.terms]
𝐓_Equiv [instance, in LangAlg.terms]
𝐓_eq_ax [constructor, in LangAlg.terms]
𝐓_eq_inter [constructor, in LangAlg.terms]
𝐓_eq_seq [constructor, in LangAlg.terms]
𝐓_eq_sym [constructor, in LangAlg.terms]
𝐓_eq_trans [constructor, in LangAlg.terms]
𝐓_eq_refl [constructor, in LangAlg.terms]
𝐓_eq [inductive, in LangAlg.terms]
𝐓_Smaller [instance, in LangAlg.terms]
𝐓_inf_inter [constructor, in LangAlg.terms]
𝐓_inf_seq [constructor, in LangAlg.terms]
𝐓_inf_ax [constructor, in LangAlg.terms]
𝐓_inf_axinf [constructor, in LangAlg.terms]
𝐓_inf_trans [constructor, in LangAlg.terms]
𝐓_inf_refl [constructor, in LangAlg.terms]
𝐓_inf [inductive, in LangAlg.terms]
𝐓_ax_exchange [constructor, in LangAlg.terms]
𝐓_axeq [inductive, in LangAlg.terms]
𝐓_inter_inf [constructor, in LangAlg.terms]
𝐓_axinf [inductive, in LangAlg.terms]
𝐓_ax_inter_one_inter [constructor, in LangAlg.terms]
𝐓_ax_inter_one_comm_seq [constructor, in LangAlg.terms]
𝐓_ax_inter_one_conv [constructor, in LangAlg.terms]
𝐓_ax_inter_one_seq [constructor, in LangAlg.terms]
𝐓_ax_inter_idem [constructor, in LangAlg.terms]
𝐓_ax_inter_comm [constructor, in LangAlg.terms]
𝐓_ax_inter_assoc [constructor, in LangAlg.terms]
𝐓_ax_seq_one_right [constructor, in LangAlg.terms]
𝐓_ax_seq_one_left [constructor, in LangAlg.terms]
𝐓_ax_seq_assoc [constructor, in LangAlg.terms]
𝐓_ax [inductive, in LangAlg.terms]
𝐓_inter [constructor, in LangAlg.terms]
𝐓_seq [constructor, in LangAlg.terms]
𝐓_cvar [constructor, in LangAlg.terms]
𝐓_var [constructor, in LangAlg.terms]
𝐓_one [constructor, in LangAlg.terms]
𝐓_to_𝐖'_lang [lemma, in LangAlg.terms_w_terms]
𝐓_to_𝐖'_inf_iff [lemma, in LangAlg.terms_w_terms]
𝐓_to_𝐖'_to_𝐓 [lemma, in LangAlg.terms_w_terms]
𝐓_to_𝐖'_to_test [lemma, in LangAlg.terms_w_terms]
𝐓_to_𝐖'_inf [lemma, in LangAlg.terms_w_terms]
𝐓_to_𝐖' [definition, in LangAlg.terms_w_terms]
𝐖 [definition, in LangAlg.w_terms]
𝐖_intersection_semantics [lemma, in LangAlg.w_terms]
𝐖_prod_semantics [lemma, in LangAlg.w_terms]
𝐖_sem_PartialOrder [instance, in LangAlg.w_terms]
𝐖_sem_PreOrder [instance, in LangAlg.w_terms]
𝐖_sem_equiv [instance, in LangAlg.w_terms]
𝐖_size_𝐖_seq [lemma, in LangAlg.w_terms]
𝐖_size_𝐖_par [lemma, in LangAlg.w_terms]
𝐖_par_one_par [lemma, in LangAlg.w_terms]
𝐖_par_one_seq [lemma, in LangAlg.w_terms]
𝐖_par_one_seq_par_one [lemma, in LangAlg.w_terms]
𝐖_par_one_seq_par [lemma, in LangAlg.w_terms]
𝐖_par_one_r [lemma, in LangAlg.w_terms]
𝐖_par_one_l [lemma, in LangAlg.w_terms]
𝐖_par_inf [lemma, in LangAlg.w_terms]
𝐖_seq_one_r [lemma, in LangAlg.w_terms]
𝐖_seq_one_l [lemma, in LangAlg.w_terms]
𝐖_par_assoc [lemma, in LangAlg.w_terms]
𝐖_seq_assoc [lemma, in LangAlg.w_terms]
𝐖_par_idem [lemma, in LangAlg.w_terms]
𝐖_par_comm [lemma, in LangAlg.w_terms]
𝐖_par_𝐖_equiv [instance, in LangAlg.w_terms]
𝐖_par_𝐖_inf [instance, in LangAlg.w_terms]
𝐖_seq_𝐖_equiv [instance, in LangAlg.w_terms]
𝐖_seq_𝐖_inf [instance, in LangAlg.w_terms]
𝐖_variables_Some [lemma, in LangAlg.w_terms]
𝐖_variables_None [lemma, in LangAlg.w_terms]
𝐖_size_Some [lemma, in LangAlg.w_terms]
𝐖_size_None [lemma, in LangAlg.w_terms]
𝐖_variables [instance, in LangAlg.w_terms]
𝐖_size [instance, in LangAlg.w_terms]
𝐖_inf_PartialOrder [instance, in LangAlg.w_terms]
𝐖_equiv_Equivalence [instance, in LangAlg.w_terms]
𝐖_equiv_inf [lemma, in LangAlg.w_terms]
𝐖_equiv [instance, in LangAlg.w_terms]
𝐖_inf_PreOrder [instance, in LangAlg.w_terms]
𝐖_inf_Some_Some [lemma, in LangAlg.w_terms]
𝐖_inf_None_Some [lemma, in LangAlg.w_terms]
𝐖_inf_Some_None [lemma, in LangAlg.w_terms]
𝐖_inf_None_None [lemma, in LangAlg.w_terms]
𝐖_par_Some_Some [lemma, in LangAlg.w_terms]
𝐖_par_Some_None [lemma, in LangAlg.w_terms]
𝐖_par_None_Some [lemma, in LangAlg.w_terms]
𝐖_par_None_None [lemma, in LangAlg.w_terms]
𝐖_seq_Some_Some [lemma, in LangAlg.w_terms]
𝐖_seq_s_None [lemma, in LangAlg.w_terms]
𝐖_seq_None_s [lemma, in LangAlg.w_terms]
𝐖_inf [instance, in LangAlg.w_terms]
𝐖_par [definition, in LangAlg.w_terms]
𝐖_seq [definition, in LangAlg.w_terms]
𝐖_one [definition, in LangAlg.w_terms]
𝐖_inf_is_weak_graph_inf [lemma, in LangAlg.w_terms_graphs]
𝐖' [definition, in LangAlg.w_terms]
𝐖'_size_𝐖'_seq [lemma, in LangAlg.w_terms]
𝐖'_size_𝐖'_par [lemma, in LangAlg.w_terms]
𝐖'_par_one_par [lemma, in LangAlg.w_terms]
𝐖'_par_one_seq [lemma, in LangAlg.w_terms]
𝐖'_par_one_seq_par_one [lemma, in LangAlg.w_terms]
𝐖'_par_one_seq_par [lemma, in LangAlg.w_terms]
𝐖'_par_one_r [lemma, in LangAlg.w_terms]
𝐖'_par_one_l [lemma, in LangAlg.w_terms]
𝐖'_par_inf [lemma, in LangAlg.w_terms]
𝐖'_seq_one_r [lemma, in LangAlg.w_terms]
𝐖'_seq_one_l [lemma, in LangAlg.w_terms]
𝐖'_par_assoc [lemma, in LangAlg.w_terms]
𝐖'_seq_assoc [lemma, in LangAlg.w_terms]
𝐖'_par_idem [lemma, in LangAlg.w_terms]
𝐖'_par_comm [lemma, in LangAlg.w_terms]
𝐖'_seq_𝐖'_equiv [instance, in LangAlg.w_terms]
𝐖'_par_𝐖'_equiv [instance, in LangAlg.w_terms]
𝐖'_seq_𝐖'_inf [instance, in LangAlg.w_terms]
𝐖'_par_𝐖'_inf [instance, in LangAlg.w_terms]
𝐖'_inf_PartialOrder [instance, in LangAlg.w_terms]
𝐖'_equiv_Equivalence [instance, in LangAlg.w_terms]
𝐖'_inf_PreOrder [instance, in LangAlg.w_terms]
𝐖'_equiv [instance, in LangAlg.w_terms]
𝐖'_inf [instance, in LangAlg.w_terms]
𝐖'_par [definition, in LangAlg.w_terms]
𝐖'_seq [definition, in LangAlg.w_terms]
𝐖'_size_simpl [lemma, in LangAlg.w_terms]
𝐖'_size [instance, in LangAlg.w_terms]
𝐖'_variables [definition, in LangAlg.w_terms]
𝐖'_one [definition, in LangAlg.w_terms]
𝐖'_to_𝐓_lang [lemma, in LangAlg.terms_w_terms]
𝐖'_to_𝐓_inf_iff [lemma, in LangAlg.terms_w_terms]
𝐖'_to_𝐓_inf [lemma, in LangAlg.terms_w_terms]
𝐖'_to_𝐓_to_𝐖' [lemma, in LangAlg.terms_w_terms]
𝐖'_to_𝐓 [definition, in LangAlg.terms_w_terms]
𝕲 [definition, in LangAlg.sp_terms_graphs]
𝕲e [definition, in LangAlg.expr_graphs]
𝕲t [definition, in LangAlg.terms_graphs]
𝕲w [definition, in LangAlg.w_terms_graphs]
𝕲_connected [lemma, in LangAlg.sp_terms_graphs]
𝕲_good [lemma, in LangAlg.sp_terms_graphs]
𝕲_acyclic [lemma, in LangAlg.sp_terms_graphs]
𝕲_bounded [lemma, in LangAlg.sp_terms_graphs]

---

Notation Index

D

_ ⧼ _ ⧽ _ [in LangAlg.tools]
_ ∩ _ (term_scope) [in LangAlg.terms]
_ ⋅ _ (term_scope) [in LangAlg.terms]
1 (term_scope) [in LangAlg.terms]

F

_ ==' _ [in LangAlg.algebra]
⊥ [in LangAlg.algebra]
⊤ [in LangAlg.algebra]
_ ∨ _ [in LangAlg.algebra]
_ ∧ _ [in LangAlg.algebra]
_ • _ [in LangAlg.algebra]
_ ⋆ [in LangAlg.algebra]
_ == _ [in LangAlg.algebra]

G

_ ⋄ _ [in LangAlg.graph]
_ ⋈ _ [in LangAlg.graph]
_ -[ _ ]→ _ [in LangAlg.graph]
_ ⊨ _ ⊲ _ [in LangAlg.graph]
_ ⊨ _ -{ _ }→ _ [in LangAlg.graph]
_ ⊨ _ -{ _ }⇀ _ [in LangAlg.graph]

L

_ ⎣ _ ⎦ [in LangAlg.algebra]
_ == _ [in LangAlg.algebra]
_ ∨ _ [in LangAlg.algebra]
_ ∧ _ [in LangAlg.algebra]
_ • _ [in LangAlg.algebra]
_ ⋆ [in LangAlg.algebra]
_ == _ [in LangAlg.algebra]
_ ∨ _ [in LangAlg.algebra]
_ ∧ _ [in LangAlg.algebra]
_ • _ [in LangAlg.algebra]
_ ⋆ [in LangAlg.algebra]

P

_ @ _ [in LangAlg.algebra]
_ @@ _ [in LangAlg.algebra]
_ == _ [in LangAlg.algebra]
_ ⊑ _ [in LangAlg.algebra]
_ # [in LangAlg.algebra]
_ ∨ _ [in LangAlg.algebra]
_ ∧ _ [in LangAlg.algebra]
_ • _ [in LangAlg.algebra]
_ ⋆ [in LangAlg.algebra]
{ _ } [in LangAlg.algebra]
_ ⊕' _ [in LangAlg.w_terms]
_ ⊗' _ [in LangAlg.w_terms]
𝟭' [in LangAlg.w_terms]
_ -?→ _ [in LangAlg.graph]
_ → _ [in LangAlg.graph]

S

0 (expr_scope) [in LangAlg.expr]
1 (expr_scope) [in LangAlg.expr]
_ ° (expr_scope) [in LangAlg.expr]
_ ∩ _ (expr_scope) [in LangAlg.expr]
_ + _ (expr_scope) [in LangAlg.expr]
_ ⋅ _ (expr_scope) [in LangAlg.expr]
_ ° (term_scope) [in LangAlg.terms]
⟨ _ ⟩ (term_scope) [in LangAlg.terms]
_ ⊨ _ << _ [in LangAlg.sp_terms]
_ ⤏ _ [in LangAlg.to_lang_witness]
_ ⊕ _ [in LangAlg.w_terms]
_ ⊗ _ [in LangAlg.w_terms]
⋃ _ [in LangAlg.expr]

other

0 (expr_scope) [in LangAlg.expr]
1 (expr_scope) [in LangAlg.expr]
_ ° (expr_scope) [in LangAlg.expr]
_ ∩ _ (expr_scope) [in LangAlg.expr]
_ + _ (expr_scope) [in LangAlg.expr]
_ ⋅ _ (expr_scope) [in LangAlg.expr]
1 (lang_scope) [in LangAlg.language]
0 (lang_scope) [in LangAlg.language]
_ ° (lang_scope) [in LangAlg.language]
_ + _ (lang_scope) [in LangAlg.language]
_ ∩ _ (lang_scope) [in LangAlg.language]
_ ⋅ _ (lang_scope) [in LangAlg.language]
⟨ _ ⟩ (term_scope) [in LangAlg.terms]
_ ° (term_scope) [in LangAlg.terms]
_ ∩ _ (term_scope) [in LangAlg.terms]
_ ⋅ _ (term_scope) [in LangAlg.terms]
1 (term_scope) [in LangAlg.terms]
_ ⊢ _ [in LangAlg.language]
_ ⋵ _ [in LangAlg.language]
_ ⊨ _ << _ [in LangAlg.sp_terms]
_ ∥ _ [in LangAlg.sp_terms]
_ ⨾ _ [in LangAlg.sp_terms]
_ -[ _ ]?→ _ [in LangAlg.graph]
_ ⋄ _ [in LangAlg.graph]
_ -[ _ ]→ _ [in LangAlg.graph]
_ ⋈ _ [in LangAlg.graph]
_ ⊨ _ ⊲ _ [in LangAlg.graph]
_ ⊨ _ -{ _ }⇀ _ [in LangAlg.graph]
_ ⊨ _ -{ _ }→ _ [in LangAlg.graph]
_ ⊗' _ [in LangAlg.w_terms]
_ ⊕' _ [in LangAlg.w_terms]
_ ⊕ _ [in LangAlg.w_terms]
_ ⊗ _ [in LangAlg.w_terms]
_ ⧼ _ ⧽ _ [in LangAlg.tools]
_ ≈ _ [in LangAlg.tools]
_ ∈ _ [in LangAlg.tools]
_ ⊆ _ [in LangAlg.tools]
_ ≲ _ [in LangAlg.tools]
_ ≤ _ [in LangAlg.tools]
_ ≃ _ [in LangAlg.tools]
_ ≡ _ [in LangAlg.tools]
_ ∘ _ [in LangAlg.tools]
{| _ \ _ |} [in LangAlg.tools]
⋃ _ [in LangAlg.expr]
⌈ _ ⌉ [in LangAlg.tools]
⌊ _ ⌋ [in LangAlg.tools]
⟦ _ ⟧ _ [in LangAlg.tools]
⦃ _ ⦄ [in LangAlg.tools]
⨥ [in LangAlg.tools]
⨪ [in LangAlg.tools]
π{ _ } [in LangAlg.tools]
𝕬[ _ → _ ] [in LangAlg.language]
𝟭 [in LangAlg.w_terms]
𝟭' [in LangAlg.w_terms]

---

Variable Index

D

dec_hom.L [in LangAlg.graph]
dec_hom.V2 [in LangAlg.graph]
dec_hom.V1 [in LangAlg.graph]
dec_hom.lbl [in LangAlg.graph]
dec_hom.vert2 [in LangAlg.graph]
dec_hom.vert1 [in LangAlg.graph]
dec_g.L [in LangAlg.graph]
dec_g.V [in LangAlg.graph]
dec_g.lbl [in LangAlg.graph]
dec_g.vert [in LangAlg.graph]
defs.Σ [in LangAlg.language]
def.X [in LangAlg.terms]
def.Λ [in LangAlg.terms]

F

funky_alg.funky [in LangAlg.algebra]
funky_alg.ρ [in LangAlg.algebra]
funky_alg.π [in LangAlg.algebra]
funky_alg.eqB [in LangAlg.algebra]
funky_alg.unit [in LangAlg.algebra]
funky_alg.bottom [in LangAlg.algebra]
funky_alg.inv [in LangAlg.algebra]
funky_alg.meet [in LangAlg.algebra]
funky_alg.prod [in LangAlg.algebra]
funky_alg.join [in LangAlg.algebra]
funky_alg.eqA [in LangAlg.algebra]
funky_alg.B [in LangAlg.algebra]
funky_alg.A [in LangAlg.algebra]

G

g.L [in LangAlg.graph]

L

languages.Σ [in LangAlg.algebra]
language_algebra.lang_sig [in LangAlg.algebra]
language_algebra.eqA [in LangAlg.algebra]
language_algebra.unit [in LangAlg.algebra]
language_algebra.bottom [in LangAlg.algebra]
language_algebra.inv [in LangAlg.algebra]
language_algebra.meet [in LangAlg.algebra]
language_algebra.prod [in LangAlg.algebra]
language_algebra.join [in LangAlg.algebra]
language_algebra.A [in LangAlg.algebra]
language.Ξ.Σ [in LangAlg.w_terms]
lang_to_funky.lang_alg [in LangAlg.algebra]
lang_to_funky.lang_sig [in LangAlg.algebra]
lang_to_funky.eqA [in LangAlg.algebra]
lang_to_funky.unit [in LangAlg.algebra]
lang_to_funky.bottom [in LangAlg.algebra]
lang_to_funky.inv [in LangAlg.algebra]
lang_to_funky.meet [in LangAlg.algebra]
lang_to_funky.prod [in LangAlg.algebra]
lang_to_funky.join [in LangAlg.algebra]
lang_to_funky.A [in LangAlg.algebra]

P

powermonoid.associativity [in LangAlg.algebra]
powermonoid.inv [in LangAlg.algebra]
powermonoid.inv_prod [in LangAlg.algebra]
powermonoid.inv_inv [in LangAlg.algebra]
powermonoid.inv_unit [in LangAlg.algebra]
powermonoid.left_neutrality [in LangAlg.algebra]
powermonoid.M [in LangAlg.algebra]
powermonoid.prod [in LangAlg.algebra]
powermonoid.right_neutrality [in LangAlg.algebra]
powermonoid.unit [in LangAlg.algebra]
powermonoid.unit_not_prod [in LangAlg.algebra]
p.L [in LangAlg.graph]
p.lbl [in LangAlg.graph]
p.V [in LangAlg.graph]
p.vert [in LangAlg.graph]

S

s.D [in LangAlg.finite_functions]
s.dec_X [in LangAlg.expr_terms]
s.dec_X [in LangAlg.expr]
s.dec_X [in LangAlg.to_lang_witness]
s.dec_X [in LangAlg.expr_graphs]
s.dec_X [in LangAlg.terms_w_terms]
s.R [in LangAlg.finite_functions]
s.src [in LangAlg.finite_functions]
s.trg [in LangAlg.finite_functions]
s.u [in LangAlg.to_lang_witness]
s.X [in LangAlg.expr_terms]
s.X [in LangAlg.expr]
s.X [in LangAlg.to_lang_witness]
s.X [in LangAlg.sp_terms_graphs]
s.X [in LangAlg.expr_graphs]
s.X [in LangAlg.w_terms_graphs]
s.X [in LangAlg.terms_w_terms]
s.Λ [in LangAlg.sp_terms_graphs]
s.Λ [in LangAlg.w_terms_graphs]
s.𝐀 [in LangAlg.to_lang_witness]
s0.X [in LangAlg.sp_terms]
s0.X [in LangAlg.w_terms]

T

t.dec_X [in LangAlg.to_lang_witness]
t.dec_X [in LangAlg.completeness]
t.X [in LangAlg.to_lang_witness]
t.X [in LangAlg.completeness]

W

w.dec_X [in LangAlg.to_lang_witness]
w.X [in LangAlg.to_lang_witness]

---

Library Index

A

algebra

C

completeness

E

expr
expr_terms
expr_graphs

F

finite_functions

G

graph

L

language

S

sp_terms_graphs
sp_terms

T

terms
terms_w_terms
terms_graphs
tools
to_lang_witness

W

w_terms_graphs
w_terms

---

Lemma Index

A

add_inverse [in LangAlg.algebra]
andb_prop_iff [in LangAlg.tools]
axiom_is_lang_alg [in LangAlg.algebra]
ax_𝐄_to_𝐓s_incl [in LangAlg.expr_terms]

B

balanced_nil [in LangAlg.tools]
bottom_subst [in LangAlg.algebra]

C

comb_lang [in LangAlg.expr]
comb_equiv [in LangAlg.expr]
completeness_𝐄_equiv [in LangAlg.completeness]
completeness_𝐄_inf [in LangAlg.completeness]
completeness_𝐓_equiv [in LangAlg.completeness]
completeness_𝐓_inf [in LangAlg.completeness]
contractible_graph [in LangAlg.graph]
conv_subst [in LangAlg.algebra]
co_nth_app_left [in LangAlg.to_lang_witness]
co_nth_app_right [in LangAlg.to_lang_witness]
co_nth_nth [in LangAlg.to_lang_witness]
co_nth_inj [in LangAlg.to_lang_witness]
co_nth_range [in LangAlg.to_lang_witness]
co_nth_In [in LangAlg.to_lang_witness]

D

decidable_𝐄_equiv [in LangAlg.expr_graphs]
decidable_𝐄_inf [in LangAlg.expr_graphs]
dec_option [in LangAlg.tools]
dec_prod [in LangAlg.tools]

E

edges_filter_graph [in LangAlg.graph]
edges_graph_union [in LangAlg.graph]
edges_vertices [in LangAlg.graph]
edges_graph_map [in LangAlg.graph]
emptyset_inverse [in LangAlg.algebra]
eqb_reflect [in LangAlg.expr]
eqLang_Equivalence [in LangAlg.algebra]
equal_list_spec [in LangAlg.tools]
equiv_0_inter [in LangAlg.expr]
equiv_𝕲e [in LangAlg.expr_graphs]
eqX_refl [in LangAlg.tools]
eqX_false [in LangAlg.tools]
eqX_correct [in LangAlg.tools]
eqX'_spec [in LangAlg.tools]
exists_path_spec [in LangAlg.graph]
ex_is_morphismb_correct [in LangAlg.graph]
ex_path_spec [in LangAlg.graph]

F

filter_graph_visible [in LangAlg.graph]
filter_graph_map [in LangAlg.graph]
filter_graph_union [in LangAlg.graph]
filter_graph_true [in LangAlg.graph]
filter_graph_morphism [in LangAlg.graph]
filter_graph_path [in LangAlg.graph]
filter_NoDup [in LangAlg.tools]
filter_true [in LangAlg.tools]
filter_ext [in LangAlg.tools]
filter_ext_In [in LangAlg.tools]
filter_map [in LangAlg.tools]
filter_length_eq [in LangAlg.tools]
filter_length [in LangAlg.tools]
filter_app [in LangAlg.tools]
finite_concat [in LangAlg.algebra]
finite_inverse [in LangAlg.algebra]
finite_support_finite_function [in LangAlg.finite_functions]
finite_function_is_finite [in LangAlg.finite_functions]
firstn_seq [in LangAlg.to_lang_witness]
fold_right_incl_smaller [in LangAlg.expr]
forall_existsb [in LangAlg.tools]
fst_𝐒𝐏_variables [in LangAlg.sp_terms]
funky_alg_𝐄 [in LangAlg.algebra]
funky_𝐄 [in LangAlg.algebra]
funky_is_lang_alg [in LangAlg.algebra]

G

get_finite_support_function [in LangAlg.finite_functions]
good_for_par_𝕲 [in LangAlg.sp_terms_graphs]
good_for_seq_𝕲 [in LangAlg.sp_terms_graphs]
good_par_graph_union [in LangAlg.graph]
good_seq_graph_union [in LangAlg.graph]
graphs_equivb_correct [in LangAlg.expr_graphs]
graphs_smallerb_correct [in LangAlg.expr_graphs]
graph_output [in LangAlg.sp_terms_graphs]
graph_input [in LangAlg.sp_terms_graphs]
graph_variables [in LangAlg.sp_terms_graphs]
graph_map_injective_good [in LangAlg.graph]
graph_map_injective_acyclic [in LangAlg.graph]
graph_union_assoc [in LangAlg.graph]
graph_map_union [in LangAlg.graph]
graph_map_injective_connected [in LangAlg.graph]
graph_map_path [in LangAlg.graph]
graph_map_morphism [in LangAlg.graph]
graph_vertices_map [in LangAlg.graph]
graph_map_ext_in [in LangAlg.graph]
graph_map_id [in LangAlg.graph]
graph_map_map [in LangAlg.graph]

H

hom_order_incl [in LangAlg.graph]

I

inb_dec [in LangAlg.tools]
inb_false [in LangAlg.tools]
inb_spec [in LangAlg.tools]
inclb_correct [in LangAlg.tools]
incl_𝐒𝐏_inf [in LangAlg.sp_terms]
incl_app_split [in LangAlg.tools]
incl_app_or [in LangAlg.tools]
incl_nil [in LangAlg.tools]
inf_ax_inter_r [in LangAlg.expr]
inf_ax_inter_l [in LangAlg.expr]
injective_par_map_right [in LangAlg.sp_terms_graphs]
injective_par_map_left [in LangAlg.sp_terms_graphs]
injective_morphism_connected [in LangAlg.graph]
injective_map_hom_eq [in LangAlg.graph]
injective_graph_map_path [in LangAlg.graph]
injective_add_left [in LangAlg.tools]
injective_replace [in LangAlg.tools]
injective_compose [in LangAlg.tools]
input_filter_graph [in LangAlg.graph]
input_graph_union [in LangAlg.graph]
input_graph_map [in LangAlg.graph]
internal_map_b_spec [in LangAlg.graph]
internal_map_graph_map [in LangAlg.graph]
inter_distr [in LangAlg.expr]
inter_oner [in LangAlg.expr]
inter_onel [in LangAlg.expr]
inter_1_abs [in LangAlg.expr]
inter_plus [in LangAlg.expr]
inter_subst [in LangAlg.algebra]
inverse_par_map_right [in LangAlg.sp_terms_graphs]
inverse_par_map_left [in LangAlg.sp_terms_graphs]
inverse_graph_map_morphism [in LangAlg.graph]
inverse_add_left [in LangAlg.tools]
inverse_replace [in LangAlg.tools]
inverse_composition [in LangAlg.tools]
inv_eqLang [in LangAlg.algebra]
In_vertices [in LangAlg.sp_terms_graphs]
in_graph_vertices [in LangAlg.graph]
in_map [in LangAlg.graph]
in_bimap [in LangAlg.tools]
in_rm [in LangAlg.tools]
in_split_strict [in LangAlg.tools]
In_dec [in LangAlg.tools]
ispathb_ispath [in LangAlg.graph]
ispath_app [in LangAlg.graph]
ispath_path [in LangAlg.graph]
is_term_comb [in LangAlg.expr]
is_balanced_𝐒𝐏'_variables [in LangAlg.sp_terms]
is_morph_𝐒𝐏_inf [in LangAlg.sp_terms_graphs]
is_morph_𝐒𝐏_ax [in LangAlg.sp_terms_graphs]
is_morphism_vertices [in LangAlg.sp_terms_graphs]
is_morphismb_correct [in LangAlg.graph]
is_morphism_finite_function [in LangAlg.graph]
is_morphism_compose_weak [in LangAlg.graph]
is_morphism_compose [in LangAlg.graph]
is_morphism_id [in LangAlg.graph]
is_morphism_incl [in LangAlg.graph]
is_premorphism_compose_weak [in LangAlg.graph]
is_premorphism_incl [in LangAlg.graph]
is_premorphism_compose [in LangAlg.graph]
is_lang_alg_𝐄 [in LangAlg.algebra]
is_lang_alg_languages [in LangAlg.algebra]
is_lang_alg_equiv [in LangAlg.algebra]
is_lang_alg_axiom [in LangAlg.algebra]
is_free_lang_alg_spec [in LangAlg.algebra]
is_lang_alg_ax [in LangAlg.algebra]
is_balanced_𝐖'_variables [in LangAlg.w_terms]
is_balanced_app [in LangAlg.tools]

J

join_eqLang [in LangAlg.algebra]

L

lang_σΞ_even [in LangAlg.to_lang_witness]
lang_ω_morph [in LangAlg.to_lang_witness]
lang_nil [in LangAlg.to_lang_witness]
lang_even [in LangAlg.to_lang_witness]
lang_alg_is_funky_alg [in LangAlg.algebra]
lang_alg_is_funky_alg_sig [in LangAlg.algebra]
length_rm_not_in [in LangAlg.tools]
length_app [in LangAlg.tools]
ln_pref_split_point [in LangAlg.sp_terms_graphs]
ln_non_zero [in LangAlg.sp_terms_graphs]
ln_smaller_size [in LangAlg.sp_terms_graphs]

M

map_app [in LangAlg.graph]
map_map [in LangAlg.graph]
map_id [in LangAlg.graph]
map_bimap [in LangAlg.tools]
meet_eqLang [in LangAlg.algebra]
mirror_nil [in LangAlg.language]
morphism_seq_step [in LangAlg.sp_terms_graphs]
morphism_seq_split [in LangAlg.sp_terms_graphs]
morphism_is_order_preserving [in LangAlg.graph]
morphism_ext_vertices [in LangAlg.graph]
morph_var [in LangAlg.sp_terms_graphs]

N

neighbour_spec [in LangAlg.graph]
NoDup_length [in LangAlg.tools]
NoDup_remove_3 [in LangAlg.tools]
not_incl_witness_Ξ [in LangAlg.to_lang_witness]
not_incl_witness [in LangAlg.to_lang_witness]
nth_NoDup [in LangAlg.to_lang_witness]
N_non_zero [in LangAlg.to_lang_witness]

O

orb_prop_iff [in LangAlg.tools]
output_filter_graph [in LangAlg.graph]
output_graph_union [in LangAlg.graph]
output_graph_map [in LangAlg.graph]

P

par_morphism_graph_union_right [in LangAlg.graph]
par_morphism_graph_union_left [in LangAlg.graph]
par_hom_order [in LangAlg.graph]
par_smaller_hom_order [in LangAlg.graph]
par_hom_order_weak_right [in LangAlg.graph]
par_hom_order_weak_left [in LangAlg.graph]
par_par_morphism_graph_union [in LangAlg.graph]
par_morphism_graph_union [in LangAlg.graph]
par_internal_graph_union [in LangAlg.graph]
par_graph_union_connected [in LangAlg.graph]
par_graph_union_decomp_right [in LangAlg.graph]
par_graph_union_decomp_left [in LangAlg.graph]
par_graph_union_decomp [in LangAlg.graph]
par_vertices_graph_union [in LangAlg.graph]
path_par_right [in LangAlg.sp_terms_graphs]
path_par_left [in LangAlg.sp_terms_graphs]
path_par_cross [in LangAlg.sp_terms_graphs]
path_par [in LangAlg.sp_terms_graphs]
path_seq_right [in LangAlg.sp_terms_graphs]
path_seq_left [in LangAlg.sp_terms_graphs]
path_vertices [in LangAlg.sp_terms_graphs]
path_𝕲 [in LangAlg.sp_terms_graphs]
path_is_vertices [in LangAlg.graph]
path_ispath_short [in LangAlg.graph]
path_ispath [in LangAlg.graph]
path_seq [in LangAlg.graph]
path_graph_union [in LangAlg.graph]
path_par_union_right [in LangAlg.graph]
path_par_union_left [in LangAlg.graph]
path_par_union_cross [in LangAlg.graph]
path_par_union [in LangAlg.graph]
path_graph_vertices [in LangAlg.graph]
path_in_vertices [in LangAlg.graph]
path_non_trivial_only_for_vertices [in LangAlg.graph]
powermon_lang_alg [in LangAlg.algebra]
powermon_lang_sig [in LangAlg.algebra]
premorphism_ω [in LangAlg.to_lang_witness]
prod_eqLang [in LangAlg.algebra]
prod_subst [in LangAlg.algebra]
proper_morphism_diff [in LangAlg.graph]

R

rev_seq [in LangAlg.to_lang_witness]
rm_length_in [in LangAlg.tools]
rm_length [in LangAlg.tools]
rm_app [in LangAlg.tools]
rm_notin [in LangAlg.tools]

S

seq_distr [in LangAlg.expr]
seq_lang_prod [in LangAlg.to_lang_witness]
seq_lang_vertices [in LangAlg.to_lang_witness]
seq_last [in LangAlg.to_lang_witness]
seq_app [in LangAlg.to_lang_witness]
seq_morphism_graph_union_left [in LangAlg.graph]
seq_hom_order [in LangAlg.graph]
seq_morphism_graph_union [in LangAlg.graph]
seq_internal_graph_union [in LangAlg.graph]
seq_graph_union_connected [in LangAlg.graph]
seq_vertices_connected_graph_union [in LangAlg.graph]
seq_graph_union_decomp [in LangAlg.graph]
seq_morph_equivalent [in LangAlg.tools]
seq_morph_not_in [in LangAlg.tools]
seq_morph_in [in LangAlg.tools]
short_path [in LangAlg.graph]
size_ln [in LangAlg.sp_terms_graphs]
size_𝐖'_to_𝐓 [in LangAlg.terms_w_terms]
size_term_to_𝐖' [in LangAlg.terms_w_terms]
size_𝐒𝐏_to_𝐓 [in LangAlg.terms_w_terms]
skipn_seq [in LangAlg.to_lang_witness]
smaller_equiv_iff_inter [in LangAlg.expr]
smaller_conv_iff [in LangAlg.expr]
smaller_equiv_iff_plus [in LangAlg.expr]
smaller_equiv [in LangAlg.expr]
smaller_𝕲e [in LangAlg.expr_graphs]
smaller_par_hom_order [in LangAlg.graph]
split_list [in LangAlg.expr]
split_one [in LangAlg.expr]
split_point_in_moustache [in LangAlg.sp_terms_graphs]
split_moustache_inf [in LangAlg.sp_terms_graphs]
split_moustache [in LangAlg.sp_terms_graphs]
split_path [in LangAlg.graph]
sub_identity_par_one [in LangAlg.w_terms]
sum_lang [in LangAlg.expr]
sum_app [in LangAlg.expr]
supid_hom_order [in LangAlg.sp_terms_graphs]

T

test_compatible_app [in LangAlg.language]
test_compatible_nil [in LangAlg.sp_terms]
test_compatible_Ξ [in LangAlg.w_terms]
test_compatible_𝐓_to_test_not_empty [in LangAlg.terms]
test_compatible_𝐓_to_test_false [in LangAlg.terms]
test_compatible_𝐓_to_test_true [in LangAlg.terms]
test_compatible_𝐓_to_test [in LangAlg.terms]
to_lang_𝐄_interpretation [in LangAlg.algebra]

U

union_subst [in LangAlg.algebra]
unit_subst [in LangAlg.algebra]

V

variables_graph_union [in LangAlg.graph]
variables_hom_eq [in LangAlg.graph]
variables_hom_order [in LangAlg.graph]
variables_morphism [in LangAlg.graph]
variables_premorphism [in LangAlg.graph]
variables_graph_map [in LangAlg.graph]
variables_𝐖'_seq [in LangAlg.w_terms]
variables_𝐖'_par [in LangAlg.w_terms]
variables_𝐖_seq [in LangAlg.w_terms]
variables_𝐖_par [in LangAlg.w_terms]
variables_𝐒𝐏_to_𝐓 [in LangAlg.terms_w_terms]
variables_𝐓_to_𝐖' [in LangAlg.terms_w_terms]
vertex_0 [in LangAlg.sp_terms_graphs]
vertex_ln [in LangAlg.sp_terms_graphs]
vertices_graph_vertices [in LangAlg.sp_terms_graphs]
vertices_bounded [in LangAlg.sp_terms_graphs]
vertices_graph_union [in LangAlg.graph]
Vert_vertices [in LangAlg.to_lang_witness]
Vert_NoDup [in LangAlg.to_lang_witness]
visible_moustache [in LangAlg.sp_terms_graphs]

W

weak_graph_infb_correct [in LangAlg.w_terms_graphs]
witness_Ξ [in LangAlg.to_lang_witness]
word_of_term_correct [in LangAlg.to_lang_witness]

X

X_dec [in LangAlg.tools]

other

Ξ_σΞ_nil [in LangAlg.to_lang_witness]
γN [in LangAlg.to_lang_witness]
γ_path [in LangAlg.to_lang_witness]
γ_le [in LangAlg.to_lang_witness]
γ_bij [in LangAlg.to_lang_witness]
γ_inj [in LangAlg.to_lang_witness]
γ0 [in LangAlg.to_lang_witness]
μ_morph [in LangAlg.sp_terms_graphs]
μ_internal [in LangAlg.sp_terms_graphs]
μ_k [in LangAlg.sp_terms_graphs]
μ_ln [in LangAlg.sp_terms_graphs]
μ_0 [in LangAlg.sp_terms_graphs]
σ_spec [in LangAlg.to_lang_witness]
σ_nil [in LangAlg.to_lang_witness]
σ'_nil [in LangAlg.to_lang_witness]
σΞ_σ_subword [in LangAlg.to_lang_witness]
σΞ_nil [in LangAlg.to_lang_witness]
ω_seq [in LangAlg.to_lang_witness]
ω_nil [in LangAlg.to_lang_witness]
ω_word [in LangAlg.to_lang_witness]
𝐄_to_𝐓s_lang [in LangAlg.expr_terms]
𝐄_to_𝐓_lang [in LangAlg.expr_terms]
𝐄_to_𝐓s_inf_iff [in LangAlg.expr_terms]
𝐄_to_𝐓s_inf [in LangAlg.expr_terms]
𝐄_to_𝐓_comb [in LangAlg.expr_terms]
𝐄_to_𝐓_to_𝐄 [in LangAlg.expr_terms]
𝐄_inf_incl_lang [in LangAlg.expr]
𝐄_eq_equiv_lang [in LangAlg.expr]
𝐄_empty [in LangAlg.expr]
𝐄_unit [in LangAlg.expr]
𝐄_variable [in LangAlg.expr]
𝐄_mirror [in LangAlg.expr]
𝐄_intersection [in LangAlg.expr]
𝐄_prod [in LangAlg.expr]
𝐄_union [in LangAlg.expr]
𝐄_size_conv [in LangAlg.expr]
𝐄_size_plus [in LangAlg.expr]
𝐄_size_inter [in LangAlg.expr]
𝐄_size_seq [in LangAlg.expr]
𝐄_size_var [in LangAlg.expr]
𝐄_size_zero [in LangAlg.expr]
𝐄_size_one [in LangAlg.expr]
𝐄_neq_𝐓s_neq [in LangAlg.expr_graphs]
𝐒𝐏_variable [in LangAlg.sp_terms]
𝐒𝐏_intersection [in LangAlg.sp_terms]
𝐒𝐏_prod [in LangAlg.sp_terms]
𝐒𝐏_size_𝐒𝐏'_variables [in LangAlg.sp_terms]
𝐒𝐏_variables_𝐒𝐏'_variables_iff [in LangAlg.sp_terms]
𝐒𝐏_variables_𝐒𝐏'_variables [in LangAlg.sp_terms]
𝐒𝐏_inf_variables [in LangAlg.sp_terms]
𝐒𝐏_size_𝐒𝐏_variables_eq [in LangAlg.sp_terms]
𝐒𝐏_size_𝐒𝐏_variables [in LangAlg.sp_terms]
𝐒𝐏_size_par [in LangAlg.sp_terms]
𝐒𝐏_size_seq [in LangAlg.sp_terms]
𝐒𝐏_size_var [in LangAlg.sp_terms]
𝐒𝐏_variables_par [in LangAlg.sp_terms]
𝐒𝐏_variables_seq [in LangAlg.sp_terms]
𝐒𝐏_variables_var [in LangAlg.sp_terms]
𝐒𝐏_inf_is_morph_iff [in LangAlg.sp_terms_graphs]
𝐒𝐏_inf_is_morph [in LangAlg.sp_terms_graphs]
𝐒𝐏_inf_moustache [in LangAlg.sp_terms_graphs]
𝐒𝐏_inf_pref_suf [in LangAlg.sp_terms_graphs]
𝐒𝐏_to_𝐓_lang [in LangAlg.terms_w_terms]
𝐓_inf_incl_lang [in LangAlg.expr_terms]
𝐓_to_𝐄_lang [in LangAlg.expr_terms]
𝐓_to_𝐄_inf [in LangAlg.expr_terms]
𝐓_to_𝐄_to_𝐓 [in LangAlg.expr_terms]
𝐓_incl_lang_inf [in LangAlg.completeness]
𝐓_inf_is_weak_graph_inf [in LangAlg.terms_graphs]
𝐓_unit [in LangAlg.terms]
𝐓_variable [in LangAlg.terms]
𝐓_mirror [in LangAlg.terms]
𝐓_intersection [in LangAlg.terms]
𝐓_prod [in LangAlg.terms]
𝐓_conv_one [in LangAlg.terms]
𝐓_conv_idem [in LangAlg.terms]
𝐓_weak_par [in LangAlg.terms]
𝐓_weak_seq [in LangAlg.terms]
𝐓_to_test_distr [in LangAlg.terms]
𝐓_to_test_distr2 [in LangAlg.terms]
𝐓_to_test_distr1 [in LangAlg.terms]
𝐓_to_test_dupl [in LangAlg.terms]
𝐓_to_test_comm [in LangAlg.terms]
𝐓_to_test_is_par_one [in LangAlg.terms]
𝐓_to_test_incl_inf [in LangAlg.terms]
𝐓_to_test_in [in LangAlg.terms]
𝐓_to_test_app [in LangAlg.terms]
𝐓_to_test_one [in LangAlg.terms]
𝐓_size_to_test [in LangAlg.terms]
𝐓_variables_to_test [in LangAlg.terms]
𝐓_inf_variables_incl [in LangAlg.terms]
𝐓_var_inter [in LangAlg.terms]
𝐓_var_seq [in LangAlg.terms]
𝐓_var_cvar [in LangAlg.terms]
𝐓_var_var [in LangAlg.terms]
𝐓_var_1 [in LangAlg.terms]
𝐓_size_inter [in LangAlg.terms]
𝐓_size_seq [in LangAlg.terms]
𝐓_size_var [in LangAlg.terms]
𝐓_size_cvar [in LangAlg.terms]
𝐓_size_1 [in LangAlg.terms]
𝐓_inf_one_prod_is_inter [in LangAlg.terms]
𝐓_inter_oner [in LangAlg.terms]
𝐓_inter_onel [in LangAlg.terms]
𝐓_inter_one_abs [in LangAlg.terms]
𝐓_inf_eq_inter [in LangAlg.terms]
𝐓_eq_inf [in LangAlg.terms]
𝐓_inter_intro [in LangAlg.terms]
𝐓_inter_elim [in LangAlg.terms]
𝐓_exchange [in LangAlg.terms]
𝐓_inter_one_inter [in LangAlg.terms]
𝐓_inter_one_comm_seq [in LangAlg.terms]
𝐓_inter_one_conv [in LangAlg.terms]
𝐓_inter_one_seq [in LangAlg.terms]
𝐓_inter_idem [in LangAlg.terms]
𝐓_inter_comm [in LangAlg.terms]
𝐓_inter_assoc [in LangAlg.terms]
𝐓_seq_one_right [in LangAlg.terms]
𝐓_seq_one_left [in LangAlg.terms]
𝐓_seq_assoc [in LangAlg.terms]
𝐓_to_𝐖'_lang [in LangAlg.terms_w_terms]
𝐓_to_𝐖'_inf_iff [in LangAlg.terms_w_terms]
𝐓_to_𝐖'_to_𝐓 [in LangAlg.terms_w_terms]
𝐓_to_𝐖'_to_test [in LangAlg.terms_w_terms]
𝐓_to_𝐖'_inf [in LangAlg.terms_w_terms]
𝐖_intersection_semantics [in LangAlg.w_terms]
𝐖_prod_semantics [in LangAlg.w_terms]
𝐖_size_𝐖_seq [in LangAlg.w_terms]
𝐖_size_𝐖_par [in LangAlg.w_terms]
𝐖_par_one_par [in LangAlg.w_terms]
𝐖_par_one_seq [in LangAlg.w_terms]
𝐖_par_one_seq_par_one [in LangAlg.w_terms]
𝐖_par_one_seq_par [in LangAlg.w_terms]
𝐖_par_one_r [in LangAlg.w_terms]
𝐖_par_one_l [in LangAlg.w_terms]
𝐖_par_inf [in LangAlg.w_terms]
𝐖_seq_one_r [in LangAlg.w_terms]
𝐖_seq_one_l [in LangAlg.w_terms]
𝐖_par_assoc [in LangAlg.w_terms]
𝐖_seq_assoc [in LangAlg.w_terms]
𝐖_par_idem [in LangAlg.w_terms]
𝐖_par_comm [in LangAlg.w_terms]
𝐖_variables_Some [in LangAlg.w_terms]
𝐖_variables_None [in LangAlg.w_terms]
𝐖_size_Some [in LangAlg.w_terms]
𝐖_size_None [in LangAlg.w_terms]
𝐖_equiv_inf [in LangAlg.w_terms]
𝐖_inf_Some_Some [in LangAlg.w_terms]
𝐖_inf_None_Some [in LangAlg.w_terms]
𝐖_inf_Some_None [in LangAlg.w_terms]
𝐖_inf_None_None [in LangAlg.w_terms]
𝐖_par_Some_Some [in LangAlg.w_terms]
𝐖_par_Some_None [in LangAlg.w_terms]
𝐖_par_None_Some [in LangAlg.w_terms]
𝐖_par_None_None [in LangAlg.w_terms]
𝐖_seq_Some_Some [in LangAlg.w_terms]
𝐖_seq_s_None [in LangAlg.w_terms]
𝐖_seq_None_s [in LangAlg.w_terms]
𝐖_inf_is_weak_graph_inf [in LangAlg.w_terms_graphs]
𝐖'_size_𝐖'_seq [in LangAlg.w_terms]
𝐖'_size_𝐖'_par [in LangAlg.w_terms]
𝐖'_par_one_par [in LangAlg.w_terms]
𝐖'_par_one_seq [in LangAlg.w_terms]
𝐖'_par_one_seq_par_one [in LangAlg.w_terms]
𝐖'_par_one_seq_par [in LangAlg.w_terms]
𝐖'_par_one_r [in LangAlg.w_terms]
𝐖'_par_one_l [in LangAlg.w_terms]
𝐖'_par_inf [in LangAlg.w_terms]
𝐖'_seq_one_r [in LangAlg.w_terms]
𝐖'_seq_one_l [in LangAlg.w_terms]
𝐖'_par_assoc [in LangAlg.w_terms]
𝐖'_seq_assoc [in LangAlg.w_terms]
𝐖'_par_idem [in LangAlg.w_terms]
𝐖'_par_comm [in LangAlg.w_terms]
𝐖'_size_simpl [in LangAlg.w_terms]
𝐖'_to_𝐓_lang [in LangAlg.terms_w_terms]
𝐖'_to_𝐓_inf_iff [in LangAlg.terms_w_terms]
𝐖'_to_𝐓_inf [in LangAlg.terms_w_terms]
𝐖'_to_𝐓_to_𝐖' [in LangAlg.terms_w_terms]
𝕲_connected [in LangAlg.sp_terms_graphs]
𝕲_good [in LangAlg.sp_terms_graphs]
𝕲_acyclic [in LangAlg.sp_terms_graphs]
𝕲_bounded [in LangAlg.sp_terms_graphs]

---

Constructor Index

A

ax_inter_1_inter [in LangAlg.expr]
ax_inter_1_comm_seq [in LangAlg.expr]
ax_inter_1_conv [in LangAlg.expr]
ax_inter_1_seq [in LangAlg.expr]
ax_conv_inter [in LangAlg.expr]
ax_conv_seq [in LangAlg.expr]
ax_conv_plus [in LangAlg.expr]
ax_conv_0 [in LangAlg.expr]
ax_conv_1 [in LangAlg.expr]
ax_conv_conv [in LangAlg.expr]
ax_inter_0 [in LangAlg.expr]
ax_inter_plus [in LangAlg.expr]
ax_plus_inter [in LangAlg.expr]
ax_inter_idem [in LangAlg.expr]
ax_inter_comm [in LangAlg.expr]
ax_inter_assoc [in LangAlg.expr]
ax_seq_plus [in LangAlg.expr]
ax_plus_seq [in LangAlg.expr]
ax_0_seq [in LangAlg.expr]
ax_seq_0 [in LangAlg.expr]
ax_plus_0 [in LangAlg.expr]
ax_plus_ass [in LangAlg.expr]
ax_plus_idem [in LangAlg.expr]
ax_plus_com [in LangAlg.expr]
ax_1_seq [in LangAlg.expr]
ax_seq_1 [in LangAlg.expr]
ax_seq_assoc [in LangAlg.expr]

C

concat_In [in LangAlg.algebra]

E

equiv [in LangAlg.tools]
eq_ax [in LangAlg.expr]
eq_conv [in LangAlg.expr]
eq_inter [in LangAlg.expr]
eq_seq [in LangAlg.expr]
eq_plus [in LangAlg.expr]
eq_sym [in LangAlg.expr]
eq_trans [in LangAlg.expr]
eq_refl [in LangAlg.expr]

I

inf_zero [in LangAlg.expr]
inf_ax [in LangAlg.expr]
inf_conv [in LangAlg.expr]
inf_inter [in LangAlg.expr]
inf_seq [in LangAlg.expr]
inf_plus [in LangAlg.expr]
inf_trans [in LangAlg.expr]
inf_refl [in LangAlg.expr]
interprete [in LangAlg.tools]
inverse_In [in LangAlg.algebra]

P

path_edge [in LangAlg.graph]
path_trans [in LangAlg.graph]
path_re [in LangAlg.graph]

S

sequiv [in LangAlg.tools]
size [in LangAlg.tools]
smaller [in LangAlg.tools]
ssmaller [in LangAlg.tools]
support [in LangAlg.tools]

V

variables [in LangAlg.tools]

other

𝐄_conv [in LangAlg.expr]
𝐄_plus [in LangAlg.expr]
𝐄_inter [in LangAlg.expr]
𝐄_seq [in LangAlg.expr]
𝐄_var [in LangAlg.expr]
𝐄_zero [in LangAlg.expr]
𝐄_one [in LangAlg.expr]
𝐒𝐏_inf_par [in LangAlg.sp_terms]
𝐒𝐏_inf_seq [in LangAlg.sp_terms]
𝐒𝐏_inf_axinf [in LangAlg.sp_terms]
𝐒𝐏_inf_ax [in LangAlg.sp_terms]
𝐒𝐏_inf_trans [in LangAlg.sp_terms]
𝐒𝐏_inf_re [in LangAlg.sp_terms]
𝐒𝐏_axinf_1_seqr [in LangAlg.sp_terms]
𝐒𝐏_axinf_1_seql [in LangAlg.sp_terms]
𝐒𝐏_axinf_weak [in LangAlg.sp_terms]
𝐒𝐏_par_idem [in LangAlg.sp_terms]
𝐒𝐏_par_comm [in LangAlg.sp_terms]
𝐒𝐏_par_assoc [in LangAlg.sp_terms]
𝐒𝐏_seq_assoc [in LangAlg.sp_terms]
𝐒𝐏_par [in LangAlg.sp_terms]
𝐒𝐏_seq [in LangAlg.sp_terms]
𝐒𝐏_var [in LangAlg.sp_terms]
𝐓_eq_ax [in LangAlg.terms]
𝐓_eq_inter [in LangAlg.terms]
𝐓_eq_seq [in LangAlg.terms]
𝐓_eq_sym [in LangAlg.terms]
𝐓_eq_trans [in LangAlg.terms]
𝐓_eq_refl [in LangAlg.terms]
𝐓_inf_inter [in LangAlg.terms]
𝐓_inf_seq [in LangAlg.terms]
𝐓_inf_ax [in LangAlg.terms]
𝐓_inf_axinf [in LangAlg.terms]
𝐓_inf_trans [in LangAlg.terms]
𝐓_inf_refl [in LangAlg.terms]
𝐓_ax_exchange [in LangAlg.terms]
𝐓_inter_inf [in LangAlg.terms]
𝐓_ax_inter_one_inter [in LangAlg.terms]
𝐓_ax_inter_one_comm_seq [in LangAlg.terms]
𝐓_ax_inter_one_conv [in LangAlg.terms]
𝐓_ax_inter_one_seq [in LangAlg.terms]
𝐓_ax_inter_idem [in LangAlg.terms]
𝐓_ax_inter_comm [in LangAlg.terms]
𝐓_ax_inter_assoc [in LangAlg.terms]
𝐓_ax_seq_one_right [in LangAlg.terms]
𝐓_ax_seq_one_left [in LangAlg.terms]
𝐓_ax_seq_assoc [in LangAlg.terms]
𝐓_inter [in LangAlg.terms]
𝐓_seq [in LangAlg.terms]
𝐓_cvar [in LangAlg.terms]
𝐓_var [in LangAlg.terms]
𝐓_one [in LangAlg.terms]

---

Inductive Index

A

Alphabet [in LangAlg.tools]
ax [in LangAlg.expr]

C

concat [in LangAlg.algebra]

E

Equiv [in LangAlg.tools]

I

inverse [in LangAlg.algebra]

P

path [in LangAlg.graph]

S

semantics [in LangAlg.tools]
SemEquiv [in LangAlg.tools]
SemSmaller [in LangAlg.tools]
Size [in LangAlg.tools]
Smaller [in LangAlg.tools]
Support [in LangAlg.tools]

other

𝐄 [in LangAlg.expr]
𝐄_inf [in LangAlg.expr]
𝐄_eq [in LangAlg.expr]
𝐒𝐏 [in LangAlg.sp_terms]
𝐒𝐏_inf [in LangAlg.sp_terms]
𝐒𝐏_axinf [in LangAlg.sp_terms]
𝐒𝐏_ax [in LangAlg.sp_terms]
𝐓 [in LangAlg.terms]
𝐓_eq [in LangAlg.terms]
𝐓_inf [in LangAlg.terms]
𝐓_axeq [in LangAlg.terms]
𝐓_axinf [in LangAlg.terms]
𝐓_ax [in LangAlg.terms]

---

Projection Index

A

axiom_inter_1_inter [in LangAlg.algebra]
axiom_inter_1_comm_fois [in LangAlg.algebra]
axiom_inter_1_conv [in LangAlg.algebra]
axiom_inter_1_fois [in LangAlg.algebra]
axiom_inter_idem [in LangAlg.algebra]
axiom_inter_comm [in LangAlg.algebra]
axiom_inter_assoc [in LangAlg.algebra]
axiom_1_fois [in LangAlg.algebra]
axiom_fois_1 [in LangAlg.algebra]
axiom_fois_assoc [in LangAlg.algebra]
axiom_inter_plus [in LangAlg.algebra]
axiom_plus_inter [in LangAlg.algebra]
axiom_inter_0 [in LangAlg.algebra]
axiom_fois_plus [in LangAlg.algebra]
axiom_plus_fois [in LangAlg.algebra]
axiom_0_fois [in LangAlg.algebra]
axiom_fois_0 [in LangAlg.algebra]
axiom_plus_0 [in LangAlg.algebra]
axiom_plus_ass [in LangAlg.algebra]
axiom_plus_idem [in LangAlg.algebra]
axiom_plus_com [in LangAlg.algebra]
axiom_conv_conv [in LangAlg.algebra]
axiom_conv_inter [in LangAlg.algebra]
axiom_conv_fois [in LangAlg.algebra]
axiom_conv_plus [in LangAlg.algebra]
axiom_conv_0 [in LangAlg.algebra]
axiom_conv_1 [in LangAlg.algebra]

E

eqA_Equivalence [in LangAlg.algebra]
eqB_Equivalence [in LangAlg.algebra]
equiv [in LangAlg.tools]
eqX [in LangAlg.tools]
eqX_eq [in LangAlg.tools]

F

funky_ax_ρ_prod_meet [in LangAlg.algebra]
funky_ax_ρ_prod [in LangAlg.algebra]
funky_ax_inter_idem [in LangAlg.algebra]
funky_ax_inter_comm [in LangAlg.algebra]
funky_ax_inter_assoc [in LangAlg.algebra]
funky_ax_1_fois [in LangAlg.algebra]
funky_ax_fois_1 [in LangAlg.algebra]
funky_ax_fois_assoc [in LangAlg.algebra]
funky_ax_inter_plus [in LangAlg.algebra]
funky_ax_plus_inter [in LangAlg.algebra]
funky_ax_inter_0 [in LangAlg.algebra]
funky_ax_fois_plus [in LangAlg.algebra]
funky_ax_plus_fois [in LangAlg.algebra]
funky_ax_0_fois [in LangAlg.algebra]
funky_ax_fois_0 [in LangAlg.algebra]
funky_ax_plus_0 [in LangAlg.algebra]
funky_ax_plus_ass [in LangAlg.algebra]
funky_ax_plus_idem [in LangAlg.algebra]
funky_ax_plus_com [in LangAlg.algebra]
funky_ax_conv_conv [in LangAlg.algebra]
funky_ax_conv_inter [in LangAlg.algebra]
funky_ax_conv_fois [in LangAlg.algebra]
funky_ax_conv_plus [in LangAlg.algebra]
funky_ax_conv_0 [in LangAlg.algebra]
funky_ax_conv_1 [in LangAlg.algebra]
funky_lang_sig [in LangAlg.algebra]

I

interprete [in LangAlg.tools]
inv_eqA [in LangAlg.algebra]

J

join_eqA [in LangAlg.algebra]

M

meet_eqA [in LangAlg.algebra]

P

prod_eqA [in LangAlg.algebra]

S

sequiv [in LangAlg.tools]
size [in LangAlg.tools]
smaller [in LangAlg.tools]
ssmaller [in LangAlg.tools]
support [in LangAlg.tools]

V

variables [in LangAlg.tools]

other

π_inv [in LangAlg.algebra]
π_prod [in LangAlg.algebra]
ρ_morph [in LangAlg.algebra]
ρπ [in LangAlg.algebra]

---

Instance Index

B

bimap_equiv [in LangAlg.tools]
Boolean [in LangAlg.tools]

C

conv_smaller [in LangAlg.expr]
conv_equiv [in LangAlg.expr]

D

decidable_edges [in LangAlg.graph]
dec_X' [in LangAlg.tools]
dec_list [in LangAlg.tools]

E

eqf [in LangAlg.finite_functions]
eqf_Equivalence [in LangAlg.finite_functions]
equivalent_cons_Proper [in LangAlg.tools]
equivalent_app_Proper [in LangAlg.tools]
equivalent_Equivalence [in LangAlg.tools]
equiv_Equivalence [in LangAlg.expr]

F

filter_equivalent_Proper [in LangAlg.tools]
filter_incl_Proper [in LangAlg.tools]

G

graphs_equiv [in LangAlg.expr_graphs]
graphs_smaller [in LangAlg.expr_graphs]
graph_vertices [in LangAlg.graph]

H

hom_eq_Equivalence [in LangAlg.graph]
hom_order_PreOrder [in LangAlg.graph]

I

incl_cons_Proper [in LangAlg.tools]
incl_app_Proper [in LangAlg.tools]
incl_PartialOrder [in LangAlg.tools]
incl_PreOrder [in LangAlg.tools]
intersection_lang_eq [in LangAlg.language]
intersection_lang_incl [in LangAlg.language]
inter_smaller [in LangAlg.expr]
inter_equiv [in LangAlg.expr]
In_equivalent_Proper [in LangAlg.tools]
In_incl_Proper [in LangAlg.tools]

L

labels [in LangAlg.graph]
lang_incl_PartialOrder [in LangAlg.language]
lang_incl_PreOrder [in LangAlg.language]
lang_eq_Equivalence [in LangAlg.language]
lang_incl [in LangAlg.language]
lang_eq [in LangAlg.language]

M

map_equivalent_Proper [in LangAlg.tools]
map_incl_Proper [in LangAlg.tools]
mirror_lang_eq [in LangAlg.language]
mirror_lang_incl [in LangAlg.language]

N

NatNum [in LangAlg.tools]

P

par_𝐒𝐏_inf [in LangAlg.sp_terms]
path_PreOrder [in LangAlg.graph]
plus_smaller [in LangAlg.expr]
plus_equiv [in LangAlg.expr]
prod_lang_eq [in LangAlg.language]
prod_lang_incl [in LangAlg.language]

R

rm_equivalent_Proper [in LangAlg.tools]
rm_incl_Proper [in LangAlg.tools]

S

semantic_containment_PartialOrder [in LangAlg.tools]
semantic_containment_PreOrder [in LangAlg.tools]
semantic_equality_Equivalence [in LangAlg.tools]
semEquiv_𝐄 [in LangAlg.expr]
semEquiv_𝐒𝐏 [in LangAlg.sp_terms]
semEquiv_𝐖 [in LangAlg.w_terms]
semEquiv_𝐓 [in LangAlg.terms]
semSmaller_𝐄 [in LangAlg.expr]
semSmaller_𝐒𝐏 [in LangAlg.sp_terms]
semSmaller_𝐖 [in LangAlg.w_terms]
semSmaller_𝐓 [in LangAlg.terms]
sem_eq_𝐄_conv [in LangAlg.expr]
sem_eq_𝐄_inter [in LangAlg.expr]
sem_eq_𝐄_seq [in LangAlg.expr]
sem_eq_𝐄_plus [in LangAlg.expr]
sem_incl_𝐄_conv [in LangAlg.expr]
sem_incl_𝐄_inter [in LangAlg.expr]
sem_incl_𝐄_fois [in LangAlg.expr]
sem_incl_𝐄_plus [in LangAlg.expr]
sem_eq_op [in LangAlg.language]
sem_eq_𝐒𝐏_inter [in LangAlg.sp_terms]
sem_eq_𝐒𝐏_seq [in LangAlg.sp_terms]
sem_incl_𝐒𝐏_inter [in LangAlg.sp_terms]
sem_incl_𝐒𝐏_seq [in LangAlg.sp_terms]
sem_eq_𝐖_inter [in LangAlg.w_terms]
sem_eq_𝐖_seq [in LangAlg.w_terms]
sem_incl_𝐖_inter [in LangAlg.w_terms]
sem_incl_𝐖_seq [in LangAlg.w_terms]
sem_eq_𝐓_inter [in LangAlg.terms]
sem_eq_𝐓_seq [in LangAlg.terms]
sem_incl_𝐓_inter [in LangAlg.terms]
sem_incl_𝐓_seq [in LangAlg.terms]
seq_smaller [in LangAlg.expr]
seq_equiv [in LangAlg.expr]
seq_𝐒𝐏_inf [in LangAlg.sp_terms]
size_𝐄 [in LangAlg.expr]
smaller_PartialOrder [in LangAlg.expr]
smaller_PreOrder [in LangAlg.expr]
suppT [in LangAlg.terms]

T

to_lang_𝐄 [in LangAlg.expr]
to_lang_𝐒𝐏 [in LangAlg.sp_terms]
to_lang_𝐖 [in LangAlg.w_terms]
to_lang_𝐓 [in LangAlg.terms]
to_test_equivalent [in LangAlg.terms]
to_test_inf_flip [in LangAlg.terms]
to_test_inf [in LangAlg.terms]

U

union_lang_eq [in LangAlg.language]
union_lang_incl [in LangAlg.language]

W

weak_graph_inf [in LangAlg.w_terms_graphs]

other

𝐄_sem_PartialOrder [in LangAlg.expr]
𝐄_sem_PreOrder [in LangAlg.expr]
𝐄_sem_equiv [in LangAlg.expr]
𝐄_Smaller [in LangAlg.expr]
𝐄_Equiv [in LangAlg.expr]
𝐄_decidable_set [in LangAlg.expr]
𝐒𝐏_sem_PartialOrder [in LangAlg.sp_terms]
𝐒𝐏_sem_equiv [in LangAlg.sp_terms]
𝐒𝐏_sem_PreOrder [in LangAlg.sp_terms]
𝐒𝐏_inf_PreOrder [in LangAlg.sp_terms]
𝐒𝐏_size [in LangAlg.sp_terms]
𝐒𝐏_variables [in LangAlg.sp_terms]
𝐓s_eq [in LangAlg.expr_terms]
𝐓s_inf [in LangAlg.expr_terms]
𝐓_sem_PartialOrder [in LangAlg.terms]
𝐓_sem_PreOrder [in LangAlg.terms]
𝐓_sem_equiv [in LangAlg.terms]
𝐓_conv_inf [in LangAlg.terms]
𝐓_conv_equiv [in LangAlg.terms]
𝐓_size [in LangAlg.terms]
𝐓_inf_PartialOrder [in LangAlg.terms]
𝐓_seq_smaller [in LangAlg.terms]
𝐓_inter_smaller [in LangAlg.terms]
𝐓_seq_equiv [in LangAlg.terms]
𝐓_inter_equiv [in LangAlg.terms]
𝐓_inf_PreOrder [in LangAlg.terms]
𝐓_eq_Equivalence [in LangAlg.terms]
𝐓_Equiv [in LangAlg.terms]
𝐓_Smaller [in LangAlg.terms]
𝐖_sem_PartialOrder [in LangAlg.w_terms]
𝐖_sem_PreOrder [in LangAlg.w_terms]
𝐖_sem_equiv [in LangAlg.w_terms]
𝐖_par_𝐖_equiv [in LangAlg.w_terms]
𝐖_par_𝐖_inf [in LangAlg.w_terms]
𝐖_seq_𝐖_equiv [in LangAlg.w_terms]
𝐖_seq_𝐖_inf [in LangAlg.w_terms]
𝐖_variables [in LangAlg.w_terms]
𝐖_size [in LangAlg.w_terms]
𝐖_inf_PartialOrder [in LangAlg.w_terms]
𝐖_equiv_Equivalence [in LangAlg.w_terms]
𝐖_equiv [in LangAlg.w_terms]
𝐖_inf_PreOrder [in LangAlg.w_terms]
𝐖_inf [in LangAlg.w_terms]
𝐖'_seq_𝐖'_equiv [in LangAlg.w_terms]
𝐖'_par_𝐖'_equiv [in LangAlg.w_terms]
𝐖'_seq_𝐖'_inf [in LangAlg.w_terms]
𝐖'_par_𝐖'_inf [in LangAlg.w_terms]
𝐖'_inf_PartialOrder [in LangAlg.w_terms]
𝐖'_equiv_Equivalence [in LangAlg.w_terms]
𝐖'_inf_PreOrder [in LangAlg.w_terms]
𝐖'_equiv [in LangAlg.w_terms]
𝐖'_inf [in LangAlg.w_terms]
𝐖'_size [in LangAlg.w_terms]

---

Section Index

D

decidable [in LangAlg.tools]
dec_hom [in LangAlg.graph]
dec_g [in LangAlg.graph]
dec_list [in LangAlg.tools]
def [in LangAlg.terms]
defs [in LangAlg.language]

F

funky_alg [in LangAlg.algebra]

G

g [in LangAlg.graph]

L

language [in LangAlg.expr]
language [in LangAlg.sp_terms]
language [in LangAlg.w_terms]
language [in LangAlg.terms]
languages [in LangAlg.algebra]
language_algebra [in LangAlg.algebra]
language.invert [in LangAlg.sp_terms]
language.invert [in LangAlg.terms]
language.rsimpl [in LangAlg.expr]
language.Ξ [in LangAlg.w_terms]
lang_to_funky [in LangAlg.algebra]

P

p [in LangAlg.graph]
powermonoid [in LangAlg.algebra]
primed [in LangAlg.sp_terms]
primed [in LangAlg.w_terms]
primed [in LangAlg.tools]

S

s [in LangAlg.expr_terms]
s [in LangAlg.expr]
s [in LangAlg.sp_terms]
s [in LangAlg.to_lang_witness]
s [in LangAlg.sp_terms_graphs]
s [in LangAlg.expr_graphs]
s [in LangAlg.w_terms]
s [in LangAlg.finite_functions]
s [in LangAlg.w_terms_graphs]
s [in LangAlg.terms]
s [in LangAlg.terms_w_terms]
s.seq [in LangAlg.sp_terms_graphs]
s0 [in LangAlg.sp_terms]
s0 [in LangAlg.w_terms]

T

t [in LangAlg.to_lang_witness]
t [in LangAlg.completeness]

W

w [in LangAlg.to_lang_witness]

---

Abbreviation Index

E

edg [in LangAlg.sp_terms_graphs]

G

grph [in LangAlg.sp_terms_graphs]
grph [in LangAlg.graph]

H

hom [in LangAlg.finite_functions]

I

interpr [in LangAlg.algebra]

---

Definition Index

A

acyclic [in LangAlg.graph]
assignment [in LangAlg.language]

B

bimap [in LangAlg.tools]

C

comb [in LangAlg.expr]
connected [in LangAlg.graph]
co_nth [in LangAlg.to_lang_witness]

D

decr [in LangAlg.tools]
domain [in LangAlg.finite_functions]

E

edge [in LangAlg.graph]
edges [in LangAlg.graph]
empty [in LangAlg.language]
eqb [in LangAlg.expr]
eqLang [in LangAlg.algebra]
equal_list [in LangAlg.tools]
equivalent [in LangAlg.tools]
eqX' [in LangAlg.tools]
exists_path [in LangAlg.graph]
ex_is_morphismb [in LangAlg.graph]
ex_path [in LangAlg.graph]

F

filter_graph [in LangAlg.graph]
finite_support_functions [in LangAlg.finite_functions]
finite_support [in LangAlg.finite_functions]
finite_functions [in LangAlg.finite_functions]
finite_function [in LangAlg.finite_functions]

G

good [in LangAlg.graph]
good_for_par [in LangAlg.graph]
good_for_seq [in LangAlg.graph]
graph [in LangAlg.graph]
graphs_smallerb [in LangAlg.expr_graphs]
graph_union [in LangAlg.graph]
graph_map [in LangAlg.graph]

H

hom_eq [in LangAlg.graph]
hom_order [in LangAlg.graph]

I

inb [in LangAlg.tools]
inclb [in LangAlg.tools]
incr [in LangAlg.tools]
injective [in LangAlg.tools]
input [in LangAlg.graph]
internal_map_b [in LangAlg.graph]
internal_map [in LangAlg.graph]
interpretation [in LangAlg.algebra]
intersection [in LangAlg.language]
inverse [in LangAlg.tools]
ispath [in LangAlg.graph]
ispathb [in LangAlg.graph]
is_term [in LangAlg.expr]
is_morphismb [in LangAlg.graph]
is_morphism [in LangAlg.graph]
is_premorphism [in LangAlg.graph]
is_free_lang_alg [in LangAlg.algebra]
is_lang_alg [in LangAlg.algebra]
is_balanced [in LangAlg.tools]

L

language [in LangAlg.language]
ln [in LangAlg.sp_terms_graphs]

M

make_total [in LangAlg.finite_functions]
map [in LangAlg.graph]
mirror [in LangAlg.language]
moustache [in LangAlg.sp_terms_graphs]

N

N [in LangAlg.to_lang_witness]
neighbour [in LangAlg.graph]

O

option_bimap [in LangAlg.tools]
output [in LangAlg.graph]

P

pref [in LangAlg.sp_terms_graphs]
prod [in LangAlg.language]

R

range [in LangAlg.finite_functions]
replace [in LangAlg.tools]
restriction [in LangAlg.finite_functions]
rm [in LangAlg.tools]

S

semantic_containment [in LangAlg.tools]
semantic_equality [in LangAlg.tools]
seq_morph [in LangAlg.tools]
split_point [in LangAlg.sp_terms_graphs]
suf [in LangAlg.sp_terms_graphs]
sum [in LangAlg.expr]
swap [in LangAlg.graph]

T

T [in LangAlg.w_terms]
test_compatible [in LangAlg.language]
to_test [in LangAlg.terms]

U

union [in LangAlg.language]
unit [in LangAlg.language]

V

Vert [in LangAlg.to_lang_witness]
vertices [in LangAlg.sp_terms_graphs]
visible [in LangAlg.graph]

W

weak_graph_infb [in LangAlg.w_terms_graphs]
weak_graph [in LangAlg.w_terms_graphs]
word [in LangAlg.to_lang_witness]
w_u [in LangAlg.to_lang_witness]

X

X' [in LangAlg.tools]

other

ø [in LangAlg.algebra]
Ξ [in LangAlg.w_terms]
γ [in LangAlg.to_lang_witness]
ε [in LangAlg.algebra]
μ [in LangAlg.sp_terms_graphs]
σ [in LangAlg.to_lang_witness]
σ' [in LangAlg.to_lang_witness]
σΞ [in LangAlg.to_lang_witness]
ω [in LangAlg.to_lang_witness]
𝐄_to_𝐓s [in LangAlg.expr_terms]
𝐄_to_𝐓 [in LangAlg.expr_terms]
𝐒𝐏_to_𝐓 [in LangAlg.terms_w_terms]
𝐒𝐏'_variables [in LangAlg.sp_terms]
𝐓_to_𝐄 [in LangAlg.expr_terms]
𝐓_conv [in LangAlg.terms]
𝐓_to_𝐖' [in LangAlg.terms_w_terms]
𝐖 [in LangAlg.w_terms]
𝐖_par [in LangAlg.w_terms]
𝐖_seq [in LangAlg.w_terms]
𝐖_one [in LangAlg.w_terms]
𝐖' [in LangAlg.w_terms]
𝐖'_par [in LangAlg.w_terms]
𝐖'_seq [in LangAlg.w_terms]
𝐖'_variables [in LangAlg.w_terms]
𝐖'_one [in LangAlg.w_terms]
𝐖'_to_𝐓 [in LangAlg.terms_w_terms]
𝕲 [in LangAlg.sp_terms_graphs]
𝕲e [in LangAlg.expr_graphs]
𝕲t [in LangAlg.terms_graphs]
𝕲w [in LangAlg.w_terms_graphs]

---

Record Index

A

Alphabet [in LangAlg.tools]

D

decidable_set [in LangAlg.tools]

E

Equiv [in LangAlg.tools]

F

funky_alg [in LangAlg.algebra]
funky_alg_sig [in LangAlg.algebra]

L

lang_alg [in LangAlg.algebra]
lang_sig [in LangAlg.algebra]

S

semantics [in LangAlg.tools]
SemEquiv [in LangAlg.tools]
SemSmaller [in LangAlg.tools]
Size [in LangAlg.tools]
Smaller [in LangAlg.tools]
Support [in LangAlg.tools]

---

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

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

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

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

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

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

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

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

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

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

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

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

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

(13 entries)

---

This page has been generated by coqdoc