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

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

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

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

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

(881 entries)

Axiom Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

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

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

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

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

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

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

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

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

(37 entries)

---

Global Index

A

absent [definition, in RIS.stacks]
absentb [definition, in RIS.stacks]
absentb_equivalent [instance, in RIS.stacks]
absentb_app [lemma, in RIS.stacks]
absentb_cons [lemma, in RIS.stacks]
absentb_false [lemma, in RIS.stacks]
absentb_correct [lemma, in RIS.stacks]
absent_equivalent [instance, in RIS.stacks]
absent_perm [lemma, in RIS.stacks]
absent_mix [lemma, in RIS.stacks]
absent_flip [lemma, in RIS.stacks]
absent_cons [lemma, in RIS.stacks]
absent_app [lemma, in RIS.stacks]
absent_alt_def [lemma, in RIS.stacks]
absent_subword [lemma, in RIS.aeq_facts]
Absorbing [record, in RIS.algebra]
Abs1 [lemma, in RIS.algebra]
Abs2 [lemma, in RIS.algebra]
Accepting_path_Tr [lemma, in RIS.traces]
Accepting_rmfst [lemma, in RIS.stacks]
Accepting_app [lemma, in RIS.stacks]
Accepting_cons_refl [lemma, in RIS.stacks]
Accepting_cons [lemma, in RIS.stacks]
Accepting_nil [lemma, in RIS.stacks]
Accepting_combine [lemma, in RIS.stacks]
Accepting_refl [lemma, in RIS.stacks]
Accepting_equiv_stacks [lemma, in RIS.equiv_stacks]
ACI0 [inductive, in RIS.regexp]
ACI0_prod_one [constructor, in RIS.regexp]
ACI0_add_zero [constructor, in RIS.regexp]
ACI0_add_idem [constructor, in RIS.regexp]
ACI0_add_comm [constructor, in RIS.regexp]
ACI0_add_assoc [constructor, in RIS.regexp]
ACI0_prod_assoc [constructor, in RIS.regexp]
act [projection, in RIS.atoms]
act [constructor, in RIS.atoms]
Action [record, in RIS.atoms]
Action [inductive, in RIS.atoms]
ActionSetoid [record, in RIS.nominalsetoid]
ActionSetoid [inductive, in RIS.nominalsetoid]
ActionSetoid_ext_In [lemma, in RIS.nominalsetoid]
Action_sum [instance, in RIS.atoms]
Action_option [instance, in RIS.atoms]
action_nat [instance, in RIS.atoms]
action_compose [projection, in RIS.atoms]
action_invariant [projection, in RIS.atoms]
action_letter [instance, in RIS.words]
action_X [projection, in RIS.words]
action_compose_eq [projection, in RIS.nominalsetoid]
action_invariant_eq [projection, in RIS.nominalsetoid]
actoid [projection, in RIS.nominalsetoid]
actoid [constructor, in RIS.nominalsetoid]
actoid_lists_length [lemma, in RIS.nominalsetoid]
actoid_lists_cons [lemma, in RIS.nominalsetoid]
actoid_lists_app [lemma, in RIS.nominalsetoid]
actoid_lists [instance, in RIS.nominalsetoid]
actoid_p_pinv [lemma, in RIS.nominalsetoid]
actoid_pinv_p [lemma, in RIS.nominalsetoid]
ActOrb [instance, in RIS.representative]
actReg [instance, in RIS.alpha_regexp]
ActRepr [instance, in RIS.representative]
act_lang [lemma, in RIS.alpha_regexp]
act_eq_equivalent [lemma, in RIS.atoms]
act_cons_a_a [lemma, in RIS.atoms]
act_bij [lemma, in RIS.atoms]
act_pinv_p [lemma, in RIS.atoms]
act_p_pinv [lemma, in RIS.atoms]
act_nil [lemma, in RIS.atoms]
act_pair [instance, in RIS.atoms]
act_lists_length [lemma, in RIS.atoms]
act_lists_cons [lemma, in RIS.atoms]
act_lists_app [lemma, in RIS.atoms]
act_lists [instance, in RIS.atoms]
act_cons [lemma, in RIS.atoms]
act_comp_app [lemma, in RIS.atoms]
act_atom_nil [lemma, in RIS.atoms]
act_atom [instance, in RIS.atoms]
act_bound [lemma, in RIS.representative]
act_free [lemma, in RIS.representative]
act_pointer [instance, in RIS.representative]
act_make_perm [lemma, in RIS.representative]
act_star [lemma, in RIS.alphaKA]
act_join [lemma, in RIS.alphaKA]
act_prod [lemma, in RIS.alphaKA]
aeq_first_letter [lemma, in RIS.aeq_facts]
aeq_first_letter_open [lemma, in RIS.aeq_facts]
aeq_facts [library]
algebra [section, in RIS.algebra]
algebra [library]
_ ⋆ [notation, in RIS.algebra]
_ ∪ _ [notation, in RIS.algebra]
_ · _ [notation, in RIS.algebra]
_ ⩵ _ [notation, in RIS.algebra]
_ ≦ _ [notation, in RIS.algebra]
𝟬 [notation, in RIS.algebra]
𝟭 [notation, in RIS.algebra]
all_subsets_nodup [lemma, in RIS.tools]
Alphabet [record, in RIS.words]
alphaKA [library]
alpha_regexp [library]
alternate_validity [lemma, in RIS.normalise]
alternate_eq [library]
andb_prop_iff [lemma, in RIS.tools]
Antimirov [section, in RIS.regexp]
Antimirov_sys [lemma, in RIS.systems]
Antimirov_fundamental_theorem [lemma, in RIS.systems]
Antimirov_inf [lemma, in RIS.systems]
Antimirov_lang [lemma, in RIS.regexp]
app_comm [lemma, in RIS.tools]
app_idem [lemma, in RIS.tools]
app_eq_app_length [lemma, in RIS.tools]
app_dyn_equiv [lemma, in RIS.normalise]
app_dyn_equiv_app [lemma, in RIS.normalise]
app_dyn_dynamic_sequence [lemma, in RIS.normalise]
app_dyn [definition, in RIS.normalise]
app_sequiv [instance, in RIS.nominalsetoid]
associative [projection, in RIS.algebra]
Associative [record, in RIS.algebra]
associative [constructor, in RIS.algebra]
Associative [inductive, in RIS.algebra]
Ass1 [lemma, in RIS.algebra]
Ass2 [lemma, in RIS.algebra]
Atom [record, in RIS.atoms]
atomic [constructor, in RIS.regexp]
atoms [library]
automata [section, in RIS.automata]
automata [library]
automata_system [section, in RIS.systems]
automata.def [section, in RIS.automata]
ax_inf_lang_incl [lemma, in RIS.regexp]
ax_eq_inf [lemma, in RIS.regexp]
ax_inf_PartialOrder [instance, in RIS.regexp]
ax_inf_PreOrder [instance, in RIS.regexp]
ax_eq_Equivalence [instance, in RIS.regexp]
ax_inf [definition, in RIS.regexp]
ax_eq_ax' [constructor, in RIS.regexp]
ax_eq_ax [constructor, in RIS.regexp]
ax_eq_star [constructor, in RIS.regexp]
ax_eq_add [constructor, in RIS.regexp]
ax_eq_prod [constructor, in RIS.regexp]
ax_eq_trans [constructor, in RIS.regexp]
ax_eq_sym [constructor, in RIS.regexp]
ax_eq_refl [constructor, in RIS.regexp]
ax_eq [inductive, in RIS.regexp]
A'_reachable [axiom, in RIS.systems]
A1 [lemma, in RIS.algebra]
A2 [lemma, in RIS.algebra]

B

balanced [definition, in RIS.words]
balanced_open_close [lemma, in RIS.words]
balanced_perm [lemma, in RIS.words]
balanced_alt [lemma, in RIS.alphaKA]
balExpr [definition, in RIS.alphaKA]
balExprB [definition, in RIS.alphaKA]
balExprB_balExpr [lemma, in RIS.alphaKA]
balExpr_bindFin [lemma, in RIS.alphaKA]
ba_neg_disj [projection, in RIS.algebra]
ba_neg_conj [projection, in RIS.algebra]
ba_disj_conj [projection, in RIS.algebra]
ba_conj_disj [projection, in RIS.algebra]
ba_false [projection, in RIS.algebra]
ba_true [projection, in RIS.algebra]
ba_disj_comm [projection, in RIS.algebra]
ba_conj_comm [projection, in RIS.algebra]
bijection [section, in RIS.bijection]
bijection [library]
bijection_iff_perm [lemma, in RIS.bijection]
_ >> _ [notation, in RIS.bijection]
bindFind_weight_weightExpr [lemma, in RIS.binding_finite]
bindFinList [definition, in RIS.binding_finite]
bindFinList_incl [lemma, in RIS.binding_finite]
bindFin_inf [lemma, in RIS.binding_finite]
bindings [definition, in RIS.binding_finite]
bindings_act [lemma, in RIS.binding_finite]
bindings_bindPref [lemma, in RIS.binding_finite]
bindings_prefixes_support [lemma, in RIS.binding_finite]
bindings_finite_prefixes [lemma, in RIS.binding_finite]
bindings_ε [lemma, in RIS.binding_finite]
bindings_fresh [lemma, in RIS.binding_finite]
bindings_Σ [lemma, in RIS.binding_finite]
bindings_witness [lemma, in RIS.binding_finite]
binding_finite_Σ [lemma, in RIS.binding_finite]
binding_finite_sqExpr_star [lemma, in RIS.binding_finite]
binding_finite_memory_bindPref [lemma, in RIS.binding_finite]
binding_finite_spec [lemma, in RIS.binding_finite]
binding_finite_true [lemma, in RIS.binding_finite]
binding_finite_false [lemma, in RIS.binding_finite]
binding_finite [definition, in RIS.binding_finite]
binding_finite [library]
bindPref [definition, in RIS.binding_finite]
bindPref_get_witness [lemma, in RIS.binding_finite]
bindPref_prefixes_support [lemma, in RIS.binding_finite]
bindPref_binding_finite [lemma, in RIS.binding_finite]
bindPref_prefixes [lemma, in RIS.binding_finite]
bindPref_ε [lemma, in RIS.binding_finite]
Bindupto [definition, in RIS.factors]
Bindupto_spec [lemma, in RIS.factors]
bind_fin_ind [lemma, in RIS.binding_finite]
bissim [inductive, in RIS.automata]
bissimilar [inductive, in RIS.equiv_stacks]
bissimilar_eq_sem [lemma, in RIS.equiv_stacks]
bissimilar_similar [lemma, in RIS.equiv_stacks]
bissimilar_w [lemma, in RIS.equiv_stacks]
bissimilar_accepting [lemma, in RIS.equiv_stacks]
bissimilar_alt [lemma, in RIS.equiv_stacks]
bissimilar_path [lemma, in RIS.equiv_stacks]
bissimilar_equivalence [instance, in RIS.equiv_stacks]
bissim_equiv [instance, in RIS.automata]
bissim_lang [lemma, in RIS.automata]
Bnd1 [lemma, in RIS.algebra]
Bnd2 [lemma, in RIS.algebra]
Boolean [instance, in RIS.tools]
booleanAlgebra [section, in RIS.algebra]
BooleanAlgebra [record, in RIS.algebra]
BooleanAlgebra_Semiring [instance, in RIS.algebra]
BooleanAlgebra_Join_Monoid [instance, in RIS.algebra]
BooleanAlgebra_Meet_Monoid [instance, in RIS.algebra]
BooleanAlgebra_Meet_Semilattice [instance, in RIS.algebra]
BooleanAlgebra_Join_Semilattice [instance, in RIS.algebra]
BooleanAlgebra_Join_Lattice [instance, in RIS.algebra]
_ ∨ _ [notation, in RIS.algebra]
_ ∧ _ [notation, in RIS.algebra]
_ ⩵ _ [notation, in RIS.algebra]
_ ≦ _ [notation, in RIS.algebra]
⊤ [notation, in RIS.algebra]
⊥ [notation, in RIS.algebra]
¬ [notation, in RIS.algebra]
bound [constructor, in RIS.representative]
bounded_diff [lemma, in RIS.systems]
bounded_stack [definition, in RIS.closed_automaton]
bounded_weightExpr [lemma, in RIS.binding_finite]
B1 [lemma, in RIS.algebra]
B2 [lemma, in RIS.algebra]

C

case_remove_defect [lemma, in RIS.normalise]
case_defect [lemma, in RIS.normalise]
close [constructor, in RIS.words]
closed_automaton [definition, in RIS.closed_automaton]
closed_automaton [library]
closed_languages [library]
close_balanced_no_close [lemma, in RIS.words]
close_balanced_perm [lemma, in RIS.words]
close_balanced_prefix [lemma, in RIS.words]
close_balanced [definition, in RIS.words]
cl_α_star [lemma, in RIS.closed_languages]
cl_α_prod [lemma, in RIS.closed_languages]
cl_α_αeq [instance, in RIS.closed_languages]
cl_α_inf_lang [instance, in RIS.closed_languages]
cl_α_eq_lang [instance, in RIS.closed_languages]
cl_α_nil [lemma, in RIS.closed_languages]
cl_α_join [lemma, in RIS.closed_languages]
cl_α_inf [lemma, in RIS.closed_languages]
cl_α_closed_idem [lemma, in RIS.closed_languages]
cl_α_incr [lemma, in RIS.closed_languages]
cl_α_idem [lemma, in RIS.closed_languages]
cl_α_closed [lemma, in RIS.closed_languages]
cl_α [definition, in RIS.closed_languages]
cl_α_Σ [lemma, in RIS.alphaKA]
coherent_support [axiom, in RIS.representative]
combine [section, in RIS.tools]
combine_act [lemma, in RIS.atoms]
combine_split [lemma, in RIS.tools]
combine_app [lemma, in RIS.tools]
combine_snd [lemma, in RIS.tools]
combine_fst [lemma, in RIS.tools]
combine.same_length [variable, in RIS.tools]
_ ⊗ _ [notation, in RIS.tools]
commutative [projection, in RIS.algebra]
Commutative [record, in RIS.algebra]
commutative [constructor, in RIS.algebra]
Commutative [inductive, in RIS.algebra]
compatible [definition, in RIS.transducer]
compatible_flip [lemma, in RIS.transducer]
compatible_app_Accepting [lemma, in RIS.transducer]
compatible_app [lemma, in RIS.transducer]
compatible_false [lemma, in RIS.transducer]
completeness [lemma, in RIS.transducer]
CompletenessKA [lemma, in RIS.systems]
CompletenessKA [lemma, in RIS.completenessKA]
completenessKA [library]
CompletenessKA_inf [lemma, in RIS.systems]
CompletenessKA_sigma [lemma, in RIS.completenessKA]
cons_sequiv [instance, in RIS.nominalsetoid]
cst [definition, in RIS.systems]
cst_spec [lemma, in RIS.systems]
cst_leq [definition, in RIS.systems]
c_binding_prod [lemma, in RIS.words]
c_binding [definition, in RIS.words]
C1 [lemma, in RIS.algebra]
C2 [lemma, in RIS.algebra]

D

decidable [section, in RIS.tools]
decidable_set [record, in RIS.tools]
decidable_regexp [instance, in RIS.regexp]
decompose_app [lemma, in RIS.tools]
decompose_app [lemma, in RIS.aeq_facts]
decomposition [lemma, in RIS.tools]
decomp_unambiguous [lemma, in RIS.tools]
decomp_unique [lemma, in RIS.tools]
dec_sigma [instance, in RIS.completenessKA]
dec_perm [instance, in RIS.atoms]
dec_atom [projection, in RIS.atoms]
_ ⊖ _ [notation, in RIS.tools]
_ ∖ _ [notation, in RIS.tools]
{{ _ }} [notation, in RIS.tools]
dec_list [instance, in RIS.tools]
dec_list [section, in RIS.tools]
dec_option [instance, in RIS.tools]
dec_sum [instance, in RIS.tools]
dec_prod [instance, in RIS.tools]
dec_letter [instance, in RIS.words]
dec_X [projection, in RIS.words]
defect_count_remove_defect [lemma, in RIS.normalise]
defect_count_spec [lemma, in RIS.normalise]
defect_count_disj [lemma, in RIS.normalise]
defect_count [definition, in RIS.normalise]
determinise [definition, in RIS.automata]
determinise_Reachables [lemma, in RIS.automata]
determinise_lang [lemma, in RIS.automata]
DFA [definition, in RIS.automata]
divide_by_open_spec [lemma, in RIS.factors]
divide_by_open [definition, in RIS.factors]
DMg1 [lemma, in RIS.algebra]
DMg2 [lemma, in RIS.algebra]
DNg [lemma, in RIS.algebra]
Dyn [definition, in RIS.normalise]
dynamic_sequence [definition, in RIS.normalise]
Dyn_eq [lemma, in RIS.normalise]
d_binding_simpl [lemma, in RIS.words]
d_binding_prod [lemma, in RIS.words]
d_binding [definition, in RIS.words]
D1 [lemma, in RIS.algebra]
D2 [lemma, in RIS.algebra]

E

E [abbreviation, in RIS.completenessKA]
E [abbreviation, in RIS.regexp]
elements [definition, in RIS.atoms]
elements_act_lists [lemma, in RIS.atoms]
elements_inv_act [lemma, in RIS.atoms]
elements_inv_eq [lemma, in RIS.atoms]
elements_app [lemma, in RIS.atoms]
elements_inv_act_atom [lemma, in RIS.atoms]
elim_var_solutions [lemma, in RIS.systems]
elim_var [definition, in RIS.systems]
Empt [definition, in RIS.regexp]
eqRel [instance, in RIS.tools]
eqRel_Equivalence [instance, in RIS.tools]
eqRepr [instance, in RIS.representative]
eqReprb [definition, in RIS.representative]
eqReprb_spec [lemma, in RIS.representative]
equal_list_spec [lemma, in RIS.tools]
equal_list [definition, in RIS.tools]
equate [definition, in RIS.systems]
equiv [projection, in RIS.tools]
Equiv [record, in RIS.tools]
equiv [constructor, in RIS.tools]
Equiv [inductive, in RIS.tools]
equivalent [definition, in RIS.tools]
equivalentb [definition, in RIS.tools]
equivalentb_spec [lemma, in RIS.tools]
equivalent_act [instance, in RIS.atoms]
equivalent_lift_prod_Proper [instance, in RIS.tools]
equivalent_flat_map_Proper [instance, in RIS.tools]
equivalent_rev_Proper [instance, in RIS.tools]
equivalent_cons_Proper [instance, in RIS.tools]
equivalent_app_Proper [instance, in RIS.tools]
equivalent_Equivalence [instance, in RIS.tools]
equivariant [projection, in RIS.atoms]
Equivariant [record, in RIS.atoms]
equivariant [constructor, in RIS.atoms]
Equivariant [inductive, in RIS.atoms]
equiv_alt [lemma, in RIS.alternate_eq]
equiv_id [lemma, in RIS.completenessKA]
equiv_perm_act [instance, in RIS.atoms]
equiv_perm_spec [instance, in RIS.atoms]
equiv_perm_app [instance, in RIS.atoms]
equiv_perm_inverse [instance, in RIS.atoms]
equiv_perm_Equivalence [instance, in RIS.atoms]
equiv_perm_trans [lemma, in RIS.atoms]
equiv_perm_sym [lemma, in RIS.atoms]
equiv_perm_refl [lemma, in RIS.atoms]
equiv_perm [instance, in RIS.atoms]
equiv_orbitsb_spec [lemma, in RIS.representative]
equiv_orbitsb_eq_shuffle [lemma, in RIS.representative]
equiv_orbitsb [definition, in RIS.representative]
equiv_orbits_Equivalence [instance, in RIS.representative]
equiv_orbits [instance, in RIS.representative]
equiv_dynamic_sequence_eq [lemma, in RIS.normalise]
equiv_stacks_bissimilar [lemma, in RIS.equiv_stacks]
equiv_stacks_compatible [instance, in RIS.equiv_stacks]
equiv_stacks_δt [instance, in RIS.equiv_stacks]
equiv_stacks_var_perm [instance, in RIS.equiv_stacks]
equiv_stacks_image [instance, in RIS.equiv_stacks]
equiv_stacks_cons [instance, in RIS.equiv_stacks]
equiv_stacks_equivalence [instance, in RIS.equiv_stacks]
equiv_stacks_Transitive [lemma, in RIS.equiv_stacks]
equiv_stacks_rmfst [instance, in RIS.equiv_stacks]
equiv_stacks_Symmetric [lemma, in RIS.equiv_stacks]
equiv_stacks_Accepting [lemma, in RIS.equiv_stacks]
equiv_stacks_pairedb [instance, in RIS.equiv_stacks]
equiv_stacks_paired_bis [instance, in RIS.equiv_stacks]
equiv_stacks_paired [lemma, in RIS.equiv_stacks]
equiv_stacks_Reflexive [lemma, in RIS.equiv_stacks]
equiv_stacksb_spec [lemma, in RIS.equiv_stacks]
equiv_stacksb [definition, in RIS.equiv_stacks]
equiv_stacks [definition, in RIS.equiv_stacks]
equiv_stacks [library]
eqX [definition, in RIS.systems]
eqX [projection, in RIS.tools]
eqX_eq [instance, in RIS.systems]
eqX_refl [lemma, in RIS.tools]
eqX_false [lemma, in RIS.tools]
eqX_correct [lemma, in RIS.tools]
eqX_eq [projection, in RIS.tools]
eq_lang_equiv [instance, in RIS.language]
eq_lang [instance, in RIS.language]
eq_lists_orbitX [lemma, in RIS.representative]
eq_lists_symmetric [instance, in RIS.representative]
eq_lists_trans [instance, in RIS.representative]
eq_lists_refl [lemma, in RIS.representative]
eq_lists_fst [lemma, in RIS.representative]
eq_lists_shuffle [lemma, in RIS.representative]
eq_listsb_spec [lemma, in RIS.representative]
eq_listsb [definition, in RIS.representative]
eq_lists [definition, in RIS.representative]
eq_shuffles [lemma, in RIS.tools]
eq_letter_correct [lemma, in RIS.words]
eq_letter [definition, in RIS.words]
eq_lang_incl_sem [lemma, in RIS.equiv_stacks]
eq_sem_equivalence [instance, in RIS.equiv_stacks]
eq_sem [instance, in RIS.equiv_stacks]
eq_act [instance, in RIS.nominalsetoid]
eq_act_proper [projection, in RIS.nominalsetoid]
eq_support [projection, in RIS.nominalsetoid]
eq_equivalence [projection, in RIS.nominalsetoid]
eq_regexp [definition, in RIS.regexp]
eq_regexp [definition, in RIS.regexp]
eta [section, in RIS.representative]
⦅ _ ⦆ [notation, in RIS.representative]
exact_solution_ext [lemma, in RIS.systems]
exact_solution_is_weak_solution [lemma, in RIS.systems]
exact_solution [definition, in RIS.systems]
exists_fresh [projection, in RIS.atoms]
exists_var_binding [lemma, in RIS.aeq_facts]
explore [definition, in RIS.systems]
explore_spec [lemma, in RIS.systems]
explore_Some [lemma, in RIS.systems]
explore_None [lemma, in RIS.systems]
ExprVar [definition, in RIS.systems]
ExprVar_ext [lemma, in RIS.systems]
extensional_equality2 [instance, in RIS.tools]
extensional_equality [instance, in RIS.tools]
ext_eq_fold_right [instance, in RIS.tools]
ext_eq_fold_left [instance, in RIS.tools]
ext_eq_filter [instance, in RIS.tools]
ext_eq_sum [instance, in RIS.tools]
ext_eq_map [instance, in RIS.tools]
ext_eq2_Equiv [instance, in RIS.tools]
ext_eq_Equiv [instance, in RIS.tools]
e_star [constructor, in RIS.regexp]
e_prod [constructor, in RIS.regexp]
e_add [constructor, in RIS.regexp]
e_un [constructor, in RIS.regexp]
e_zero [constructor, in RIS.regexp]
E1 [lemma, in RIS.algebra]
E2 [lemma, in RIS.algebra]

F

factors [definition, in RIS.factors]
Factors [definition, in RIS.factors]
factors [library]
factors_open_balanced [lemma, in RIS.factors]
factors_size [lemma, in RIS.factors]
factors_In [lemma, in RIS.factors]
factors_prod [lemma, in RIS.factors]
Factors_spec [lemma, in RIS.factors]
factor_perm [lemma, in RIS.atoms]
filter_equivalent_Proper [instance, in RIS.tools]
filter_incl_Proper [instance, in RIS.tools]
filter_nil [lemma, in RIS.tools]
filter_NoDup [lemma, in RIS.tools]
filter_true [lemma, in RIS.tools]
filter_ext [lemma, in RIS.tools]
filter_ext_In [lemma, in RIS.tools]
filter_map [lemma, in RIS.tools]
filter_length_eq [lemma, in RIS.tools]
filter_length [lemma, in RIS.tools]
filter_app [lemma, in RIS.tools]
find_matching_close [lemma, in RIS.aeq_facts]
first_defect_Sn [lemma, in RIS.normalise]
first_defect [definition, in RIS.normalise]
flip [definition, in RIS.tools]
flip [section, in RIS.tools]
flip_proj2 [lemma, in RIS.tools]
flip_proj1 [lemma, in RIS.tools]
flip_app [lemma, in RIS.tools]
flip_involutive [lemma, in RIS.tools]
_ ` [notation, in RIS.tools]
fold_star_prodList [lemma, in RIS.regexp]
forallb_ext [lemma, in RIS.tools]
forallb_ext_In [lemma, in RIS.tools]
forallb_false_exists [lemma, in RIS.tools]
forall_existsb [lemma, in RIS.tools]
free [constructor, in RIS.representative]
free_relational_interpretation [lemma, in RIS.normalise]
freshExpr [definition, in RIS.alphaKA]
freshExprB [definition, in RIS.alphaKA]
freshExprB_freshExpr [lemma, in RIS.alphaKA]
freshExpr_bindFin [lemma, in RIS.alphaKA]
fresh_lang [lemma, in RIS.alpha_regexp]
fresh__α [definition, in RIS.words]
fundamental_theorem [lemma, in RIS.regexp]
F1 [lemma, in RIS.algebra]
F2 [lemma, in RIS.algebra]

G

get_terms [lemma, in RIS.completenessKA]
goodACI0 [instance, in RIS.regexp]
GoodEnoughAxiom [record, in RIS.regexp]
goodKA [instance, in RIS.regexp]
goodαKA [instance, in RIS.alphaKA]
groupAct_nat [instance, in RIS.atoms]
groupAct_pointer [instance, in RIS.representative]
group_by_fst_act [lemma, in RIS.atoms]
group_by_fst_map_In [lemma, in RIS.tools]
group_by_fst_map_supp [lemma, in RIS.tools]
group_by_fst_In [lemma, in RIS.tools]
group_by_fst_length [lemma, in RIS.tools]
group_by_fst [definition, in RIS.tools]
group_by_fst [section, in RIS.tools]
group_action_letter [instance, in RIS.words]
G1 [lemma, in RIS.algebra]
G2 [lemma, in RIS.algebra]

H

has_support_perm [instance, in RIS.atoms]
has_support_ext_eq [instance, in RIS.tools]
has_support_supported [lemma, in RIS.tools]
has_support [record, in RIS.tools]
hide [definition, in RIS.normalise]
hide_close [lemma, in RIS.normalise]
homogeneous [definition, in RIS.binding_finite]
homogeneous_𝐇 [lemma, in RIS.binding_finite]
homogeneous_prod [lemma, in RIS.binding_finite]
homogeneous_alt [lemma, in RIS.binding_finite]
homogeneous_is_binding_finite [lemma, in RIS.binding_finite]
H1 [lemma, in RIS.algebra]
H2 [lemma, in RIS.algebra]

I

idempotent [projection, in RIS.algebra]
Idempotent [record, in RIS.algebra]
idempotent [constructor, in RIS.algebra]
Idempotent [inductive, in RIS.algebra]
IdemSemiRing_Semilattice [instance, in RIS.algebra]
idem_fold_star [lemma, in RIS.regexp]
Idm1 [lemma, in RIS.algebra]
Idm2 [lemma, in RIS.algebra]
image [definition, in RIS.stacks]
image_app_Accepting [lemma, in RIS.transducer]
image_spec [lemma, in RIS.stacks]
inb [definition, in RIS.tools]
inb_dec [lemma, in RIS.tools]
inb_false [lemma, in RIS.tools]
inb_spec [lemma, in RIS.tools]
inclb [definition, in RIS.tools]
inclb_correct [lemma, in RIS.tools]
incl_cons_disj' [lemma, in RIS.tools]
incl_cons_disj [lemma, in RIS.tools]
incl_split [lemma, in RIS.tools]
incl_app_split [lemma, in RIS.tools]
incl_app_or [lemma, in RIS.tools]
incl_nil [lemma, in RIS.tools]
incl_lift_prod_Proper [instance, in RIS.tools]
incl_flat_map_Proper [instance, in RIS.tools]
incl_rev_Proper [instance, in RIS.tools]
incl_cons_Proper [instance, in RIS.tools]
incl_app_Proper [instance, in RIS.tools]
incl_PartialOrder [instance, in RIS.tools]
incl_PreOrder [instance, in RIS.tools]
incl_map [lemma, in RIS.tools]
incl_sem_w [lemma, in RIS.equiv_stacks]
index [abbreviation, in RIS.representative]
index [abbreviation, in RIS.representative]
infRel [instance, in RIS.tools]
infRel_PartialOrder [instance, in RIS.tools]
infRel_PreOrder [instance, in RIS.tools]
inf_system [lemma, in RIS.systems]
inf_system [section, in RIS.systems]
inf_join_inf [definition, in RIS.systems]
inf_cup_right [definition, in RIS.systems]
inf_cup_left [definition, in RIS.systems]
inf_lang_iter_lang [instance, in RIS.language]
inf_lang_PartialOrder [instance, in RIS.language]
inf_lang_preorder [instance, in RIS.language]
inf_lang [instance, in RIS.language]
inf_lang_cl_α [instance, in RIS.closed_languages]
inf_join_inf [lemma, in RIS.algebra]
inf_cup_right [lemma, in RIS.algebra]
inf_cup_left [lemma, in RIS.algebra]
inf_sem_partialorder [instance, in RIS.equiv_stacks]
inf_sem_preorder [instance, in RIS.equiv_stacks]
inf_sem [instance, in RIS.equiv_stacks]
inject [definition, in RIS.completenessKA]
inject [definition, in RIS.representative]
injective [record, in RIS.tools]
injective_perm [instance, in RIS.atoms]
injective_free [instance, in RIS.representative]
injective_ext_eq [instance, in RIS.tools]
injective_support_closed [lemma, in RIS.tools]
inject_regexp_to_expr [lemma, in RIS.completenessKA]
inject_equiv [lemma, in RIS.representative]
inject_equivariant [lemma, in RIS.representative]
inject_support [lemma, in RIS.representative]
inject_injection [lemma, in RIS.representative]
inject_orbitb [lemma, in RIS.representative]
inject_orbit [lemma, in RIS.representative]
inject_aux [definition, in RIS.representative]
insert [definition, in RIS.tools]
insert_map [lemma, in RIS.tools]
insert_spec [lemma, in RIS.tools]
intersect [definition, in RIS.systems]
intersect [section, in RIS.systems]
intersect_univ [lemma, in RIS.systems]
intersect_right [lemma, in RIS.systems]
intersect_left [lemma, in RIS.systems]
inverse [definition, in RIS.atoms]
inverse_app [lemma, in RIS.atoms]
inverse_comp_r [lemma, in RIS.atoms]
inverse_comp_l [lemma, in RIS.atoms]
inverse_inv [lemma, in RIS.atoms]
In_support_list [lemma, in RIS.atoms]
In_act_lists [lemma, in RIS.atoms]
In_Tr_not_open_balanced [lemma, in RIS.traces]
In_shuffles [lemma, in RIS.tools]
in_cons_iff [lemma, in RIS.tools]
In_undup [lemma, in RIS.tools]
In_dec [lemma, in RIS.tools]
In_equivalent_Proper [instance, in RIS.tools]
In_incl_Proper [instance, in RIS.tools]
In_flip [lemma, in RIS.tools]
in_concat [lemma, in RIS.tools]
In_OpenVar [lemma, in RIS.alphaKA]
In_δA_stateSpace_incl [lemma, in RIS.regexp]
is_square [definition, in RIS.factors]
is_orbitb_orbitX [lemma, in RIS.representative]
is_orbit_orbitX [lemma, in RIS.representative]
is_orbitb_act [lemma, in RIS.representative]
is_orbit_act [lemma, in RIS.representative]
is_orbitb_spec [lemma, in RIS.representative]
is_orbitb [definition, in RIS.representative]
is_orbit [definition, in RIS.representative]
is_supported [projection, in RIS.tools]
is_support [projection, in RIS.tools]
is_surjective [projection, in RIS.tools]
is_injective [projection, in RIS.tools]
is_binding_finite_act [lemma, in RIS.binding_finite]
is_binding_finite_Σ [lemma, in RIS.binding_finite]
is_binding_finite_memory_bound [lemma, in RIS.binding_finite]
is_binding_finite_memory_finite [lemma, in RIS.binding_finite]
is_binding_finite_bindings [lemma, in RIS.binding_finite]
is_binding_finite [definition, in RIS.binding_finite]
is_valid_close [lemma, in RIS.normalise]
is_valid_var [lemma, in RIS.normalise]
is_valid_open [lemma, in RIS.normalise]
is_binding_finite_ax_inf [lemma, in RIS.alphaKA]
is_binding_finite_ax_eq [lemma, in RIS.alphaKA]
iter [definition, in RIS.normalise]
iter_lang_last [lemma, in RIS.language]
iter_lang [definition, in RIS.language]
iter_auto [definition, in RIS.automata]
I1 [lemma, in RIS.algebra]
I2 [lemma, in RIS.algebra]

J

Join [definition, in RIS.systems]
join [projection, in RIS.algebra]
Join [record, in RIS.algebra]
join [constructor, in RIS.algebra]
Join [inductive, in RIS.algebra]
joinLang [instance, in RIS.language]
JoinOrder [record, in RIS.algebra]
JoinOrder [inductive, in RIS.algebra]
joinOrderLang [instance, in RIS.language]
joinOrder_ax [instance, in RIS.regexp]
joinSemiLattice [section, in RIS.algebra]
_ ⩵ _ [notation, in RIS.algebra]
_ ≦ _ [notation, in RIS.algebra]
join_semilattice [instance, in RIS.systems]
join_semilattice_Lang [instance, in RIS.language]
join_semilattice [instance, in RIS.algebra]
join_is_order [projection, in RIS.algebra]
join_is_order [constructor, in RIS.algebra]
join_list_zero [lemma, in RIS.regexp]
join_list_equivalent_ACI0 [lemma, in RIS.regexp]
join_list_equivalent [lemma, in RIS.regexp]
join_list_right_distr [lemma, in RIS.regexp]
join_list_left_distr [lemma, in RIS.regexp]
join_list_add [lemma, in RIS.regexp]
join_list_monotone [lemma, in RIS.regexp]
join_list_app [lemma, in RIS.regexp]
join_list [definition, in RIS.regexp]
join_comm [projection, in RIS.regexp]
join_assoc [projection, in RIS.regexp]
join_idem [projection, in RIS.regexp]
join_ax_eq [instance, in RIS.regexp]
J1 [lemma, in RIS.algebra]
J2 [lemma, in RIS.algebra]

K

KA [inductive, in RIS.regexp]
kaX [instance, in RIS.systems]
KA_act [lemma, in RIS.alpha_regexp]
KA_regexp_to_expr [lemma, in RIS.completenessKA]
ka_zero_star [lemma, in RIS.algebra]
ka_star_mid_split [lemma, in RIS.algebra]
ka_star_unfold_right [lemma, in RIS.algebra]
ka_star_star [lemma, in RIS.algebra]
ka_star_dup [lemma, in RIS.algebra]
ka_star_unfold_eq [lemma, in RIS.algebra]
_ ⩵ _ [notation, in RIS.algebra]
_ ≦ _ [notation, in RIS.algebra]
ka_facts [section, in RIS.algebra]
ka_star_right_ind [projection, in RIS.algebra]
ka_star_left_ind [projection, in RIS.algebra]
ka_star_unfold [projection, in RIS.algebra]
ka_joinOrder [projection, in RIS.algebra]
ka_idem [projection, in RIS.algebra]
ka_semiring [projection, in RIS.algebra]
KA_αKA_inf [lemma, in RIS.alphaKA]
KA_αKA [lemma, in RIS.alphaKA]
KA_ACI0 [lemma, in RIS.regexp]
KA_regexp [instance, in RIS.regexp]
KA_star_right_ind [constructor, in RIS.regexp]
KA_star_left_ind [constructor, in RIS.regexp]
KA_star_unfold [constructor, in RIS.regexp]
KA_idem [constructor, in RIS.regexp]
KA_right_zero [constructor, in RIS.regexp]
KA_left_zero [constructor, in RIS.regexp]
KA_un_right [constructor, in RIS.regexp]
KA_un_left [constructor, in RIS.regexp]
KA_zero [constructor, in RIS.regexp]
KA_right_distr [constructor, in RIS.regexp]
KA_left_distr [constructor, in RIS.regexp]
KA_add_comm [constructor, in RIS.regexp]
KA_add_assoc [constructor, in RIS.regexp]
KA_prod_assoc [constructor, in RIS.regexp]
KA' [inductive, in RIS.regexp]
KleeneAlgebra [record, in RIS.algebra]
KleeneTheorem [lemma, in RIS.automata]
kleeneTheorem [section, in RIS.automata]
K1 [lemma, in RIS.algebra]
K2 [lemma, in RIS.algebra]

L

lang [section, in RIS.language]
lang [definition, in RIS.equiv_stacks]
langDFA [definition, in RIS.automata]
langNFA [definition, in RIS.automata]
langSys [definition, in RIS.systems]
langSys_inf_sol [lemma, in RIS.systems]
language [definition, in RIS.language]
language [library]
lang_KA [instance, in RIS.language]
lang_Semiring [instance, in RIS.language]
lang_close_automaton [lemma, in RIS.closed_automaton]
_ ^{ _ } [notation, in RIS.language]
Lattice [record, in RIS.algebra]
lat_ops [definition, in RIS.completenessKA]
lat_meet_join [projection, in RIS.algebra]
lat_join_meet [projection, in RIS.algebra]
lat_join_comm [projection, in RIS.algebra]
lat_join_assoc [projection, in RIS.algebra]
lat_meet_comm [projection, in RIS.algebra]
lat_meet_assoc [projection, in RIS.algebra]
lat_idem [projection, in RIS.algebra]
lat_comm [projection, in RIS.algebra]
lat_assoc [projection, in RIS.algebra]
least_solution_Antimirov [lemma, in RIS.systems]
least_solution_exists [lemma, in RIS.systems]
least_solution_is_exact [lemma, in RIS.systems]
least_solution_ext [lemma, in RIS.systems]
least_solution [definition, in RIS.systems]
left_absorbing [projection, in RIS.algebra]
left_unit [projection, in RIS.algebra]
left_distr [projection, in RIS.regexp]
length_sum_filter [lemma, in RIS.tools]
length_app_tail [lemma, in RIS.tools]
length_app [lemma, in RIS.tools]
length_sequiv [instance, in RIS.nominalsetoid]
len_rev_induction [lemma, in RIS.tools]
len_induction [lemma, in RIS.tools]
leqX [definition, in RIS.systems]
leqX_po [instance, in RIS.systems]
leqX_o [instance, in RIS.systems]
letter [inductive, in RIS.words]
letter_map [definition, in RIS.words]
Levi [lemma, in RIS.tools]
Levi_strict [lemma, in RIS.tools]
le_plus_Proper [instance, in RIS.tools]
lift [definition, in RIS.representative]
lift_perm_invisible [lemma, in RIS.representative]
lift_perm_inverse [lemma, in RIS.representative]
lift_equiv [instance, in RIS.representative]
lift_f [lemma, in RIS.representative]
lift_prod_spec [lemma, in RIS.tools]
lift_prod [definition, in RIS.tools]
list [section, in RIS.nominalsetoid]
lists_of_length_spec [lemma, in RIS.tools]
lists_of_length [definition, in RIS.tools]
loop [definition, in RIS.systems]
loop_spec [lemma, in RIS.systems]
lower_bound_zero [lemma, in RIS.systems]
lower_bound_ext [lemma, in RIS.systems]
lower_bound [definition, in RIS.systems]
lower_squares_size [lemma, in RIS.factors]
lower_squares_prod [lemma, in RIS.factors]
lower_squares_alt [lemma, in RIS.factors]
lower_squares_spec [lemma, in RIS.factors]
lower_squares [definition, in RIS.factors]
lt_plus_Proper [instance, in RIS.tools]
L1 [lemma, in RIS.algebra]
L2 [lemma, in RIS.algebra]

M

make_perm_id [lemma, in RIS.bijection]
make_bij [lemma, in RIS.bijection]
make_perm_spec [lemma, in RIS.bijection]
make_perm [definition, in RIS.bijection]
mapRel [definition, in RIS.tools]
mapRel_add [lemma, in RIS.tools]
mapRel_unique [lemma, in RIS.tools]
mapRel_app [lemma, in RIS.tools]
mapRel_nil [lemma, in RIS.tools]
map_expr_ax_eq [lemma, in RIS.completenessKA]
map_expr [definition, in RIS.completenessKA]
map_injective_injective [lemma, in RIS.tools]
map_undup_inj [lemma, in RIS.tools]
map_undup_id [lemma, in RIS.tools]
map_eq_equivalent [lemma, in RIS.tools]
map_ext_in_iff [lemma, in RIS.tools]
map_bij [lemma, in RIS.tools]
map_eq_id [lemma, in RIS.tools]
map_equivalent_Proper [instance, in RIS.tools]
map_incl_Proper [instance, in RIS.tools]
map_app_inverse [lemma, in RIS.tools]
match_defect_first_defect [lemma, in RIS.normalise]
match_defect_at_Sn [lemma, in RIS.normalise]
match_defect_at_n_spec [lemma, in RIS.normalise]
match_defect_at_n [definition, in RIS.normalise]
match_defect_match_defectb [lemma, in RIS.normalise]
match_defectb_spec [lemma, in RIS.normalise]
match_defectb [definition, in RIS.normalise]
match_defect [definition, in RIS.normalise]
maxBind [definition, in RIS.factors]
MaxBind [definition, in RIS.binding_finite]
maxBind_lists [lemma, in RIS.factors]
maxBind_square [lemma, in RIS.factors]
maxBind_square_disj [lemma, in RIS.factors]
maxBind_idem [lemma, in RIS.factors]
maxBind_comm [lemma, in RIS.factors]
maxBind_assoc [lemma, in RIS.factors]
maxBind_neutral [lemma, in RIS.factors]
MaxBind_lift_prod [lemma, in RIS.binding_finite]
MaxBind_In [lemma, in RIS.binding_finite]
MaxBind_sizeAt [lemma, in RIS.binding_finite]
MaxBind_fresh_Pref [lemma, in RIS.binding_finite]
MaxBind_le [lemma, in RIS.binding_finite]
MaxBind_lub [lemma, in RIS.binding_finite]
MaxBind_equiv [instance, in RIS.binding_finite]
MaxBind_cons [lemma, in RIS.binding_finite]
MaxBind_filter [lemma, in RIS.binding_finite]
MaxBind_fresh [lemma, in RIS.binding_finite]
MaxBind_app [lemma, in RIS.binding_finite]
memory_bound [lemma, in RIS.binding_finite]
memory_bound_aux [lemma, in RIS.binding_finite]
minimal_support [lemma, in RIS.atoms]
minimal_cl_α [lemma, in RIS.closed_languages]
minimal_support_eq [lemma, in RIS.nominalsetoid]
min_occ_app [lemma, in RIS.transducer]
min_occ [definition, in RIS.transducer]
mix [definition, in RIS.tools]
mix [section, in RIS.tools]
mixp [definition, in RIS.transducer]
mixp_absent [lemma, in RIS.transducer]
mixp_app [lemma, in RIS.transducer]
mixp_cons [lemma, in RIS.transducer]
mixp_snd_bis [lemma, in RIS.transducer]
mixp_snd [lemma, in RIS.transducer]
mixp_fst [lemma, in RIS.transducer]
mix_app [lemma, in RIS.tools]
mix_snd [lemma, in RIS.tools]
mix_fst [lemma, in RIS.tools]
mix.same_length [variable, in RIS.tools]
_ ⋈ _ [notation, in RIS.tools]
Monoid [record, in RIS.algebra]
mon_neg [definition, in RIS.completenessKA]
mon_itr [definition, in RIS.completenessKA]
mon_star [definition, in RIS.completenessKA]
mon_un [definition, in RIS.completenessKA]
mon_prod [definition, in RIS.completenessKA]
mon_unit [projection, in RIS.algebra]
mon_assoc [projection, in RIS.algebra]

N

NatNum [instance, in RIS.tools]
nb [abbreviation, in RIS.tools]
nb [abbreviation, in RIS.tools]
nb_act [lemma, in RIS.atoms]
nb_map [lemma, in RIS.tools]
nb_cons_eq [lemma, in RIS.tools]
nb_cons_neq [lemma, in RIS.tools]
nb_inv_nil [lemma, in RIS.tools]
nb_not_In [lemma, in RIS.tools]
nb_In [lemma, in RIS.tools]
nb_nil [lemma, in RIS.tools]
nb_count_occ [lemma, in RIS.tools]
NFA [definition, in RIS.automata]
NFA_of_regexp_spec [lemma, in RIS.automata]
NFA_of_regexp_langNFA [lemma, in RIS.automata]
NFA_of_regexp [definition, in RIS.automata]
nf_supp_inj [lemma, in RIS.representative]
nf_supp_action [lemma, in RIS.representative]
nf_supp_nodup [lemma, in RIS.representative]
nf_supp_support [lemma, in RIS.representative]
nf_supp_shuffle_support [axiom, in RIS.representative]
nf_supp [axiom, in RIS.representative]
nil_or_last [lemma, in RIS.tools]
nil_prod_lang [lemma, in RIS.regexp]
NoDupb [definition, in RIS.tools]
NoDupb_NoDup [lemma, in RIS.tools]
NoDup_act [lemma, in RIS.atoms]
NoDup_shuffles [lemma, in RIS.tools]
NoDup_map_injective [lemma, in RIS.tools]
NoDup_nb' [lemma, in RIS.tools]
NoDup_nb [lemma, in RIS.tools]
NoDup_length [lemma, in RIS.tools]
NoDup_rev [lemma, in RIS.tools]
NoDup_undup_eq [lemma, in RIS.tools]
NoDup_undup [lemma, in RIS.tools]
NoDup_app [lemma, in RIS.tools]
NoDup_app_inv [lemma, in RIS.tools]
NoDup_remove_3 [lemma, in RIS.tools]
Nominal [record, in RIS.atoms]
nominalReg [instance, in RIS.alpha_regexp]
NominalSetoid [record, in RIS.nominalsetoid]
nominalsetoid [library]
NominalSetoid_list [instance, in RIS.nominalsetoid]
Nominal_sum [instance, in RIS.atoms]
Nominal_option [instance, in RIS.atoms]
Nominal_Pair [instance, in RIS.atoms]
Nominal_list [instance, in RIS.atoms]
Nominal_Atom [instance, in RIS.atoms]
Nominal_orbit_base [instance, in RIS.representative]
NomOrbit [instance, in RIS.representative]
NomSetRepr [instance, in RIS.representative]
nom_δt [lemma, in RIS.transducer]
nom_compatible [lemma, in RIS.transducer]
nom_path [lemma, in RIS.transducer]
nom_step [lemma, in RIS.transducer]
nom_X [projection, in RIS.words]
normalise [definition, in RIS.normalise]
normalise [library]
normalise_spec [lemma, in RIS.normalise]
normal_form [lemma, in RIS.normalise]
not_nil_add [lemma, in RIS.tools]
no_var_no_fun [lemma, in RIS.completenessKA]

O

one_inf_star [lemma, in RIS.algebra]
open [constructor, in RIS.words]
OpenVar [definition, in RIS.alphaKA]
open_balanced_no_open [lemma, in RIS.words]
open_balanced_perm [lemma, in RIS.words]
open_balanced_suffix [lemma, in RIS.words]
open_balanced [definition, in RIS.words]
orbit [definition, in RIS.representative]
orbits [section, in RIS.representative]
_ ={ _ }= _ [notation, in RIS.representative]
orbitX [definition, in RIS.representative]
orbitX [section, in RIS.representative]
orbitX_perm [lemma, in RIS.representative]
orbitX_inj [lemma, in RIS.representative]
orbitX_aux [definition, in RIS.representative]
⦃ _ ⦄ [notation, in RIS.representative]
orbit_eq [lemma, in RIS.representative]
orbit_base [definition, in RIS.representative]
orb_prop_iff [lemma, in RIS.tools]

P

pad [definition, in RIS.tools]
pad_contents [lemma, in RIS.tools]
paired [definition, in RIS.stacks]
pairedb [definition, in RIS.stacks]
pairedb_app_Accepting [lemma, in RIS.transducer]
pairedb_spec [lemma, in RIS.stacks]
paired_perm [lemma, in RIS.stacks]
paired_inj [lemma, in RIS.stacks]
paired_rmfst [lemma, in RIS.stacks]
paired_cons [lemma, in RIS.stacks]
paired_mix [lemma, in RIS.stacks]
paired_flip [lemma, in RIS.stacks]
paired_app [lemma, in RIS.stacks]
paired_Accepting [lemma, in RIS.stacks]
pairs [definition, in RIS.tools]
pairs_spec [lemma, in RIS.tools]
partition [definition, in RIS.representative]
partitionb [definition, in RIS.representative]
partitionb_spec [lemma, in RIS.representative]
partition_act [lemma, in RIS.representative]
path [inductive, in RIS.transducer]
pathl [constructor, in RIS.transducer]
pathNFA [definition, in RIS.automata]
pathNFA_stateSpace [lemma, in RIS.automata]
pathNFA_last [lemma, in RIS.automata]
pathNFA_app [lemma, in RIS.automata]
pathRestr [definition, in RIS.automata]
pathRestr_split [lemma, in RIS.automata]
pathRestr_incl [lemma, in RIS.automata]
pathRestr_app [lemma, in RIS.automata]
pathRestr_pathNFA [lemma, in RIS.automata]
pathSys [definition, in RIS.systems]
path_αequiv [lemma, in RIS.transducer]
path_stack_decompose [lemma, in RIS.transducer]
path_stack_decompose_aux [lemma, in RIS.transducer]
path_app [lemma, in RIS.transducer]
path_det [lemma, in RIS.transducer]
path_mix [lemma, in RIS.transducer]
path_sym [lemma, in RIS.transducer]
path_app_Accepting [lemma, in RIS.transducer]
path_letter [lemma, in RIS.transducer]
path_decompose_app [lemma, in RIS.transducer]
path_length_word [lemma, in RIS.transducer]
path_id [lemma, in RIS.transducer]
path_id_compatible [lemma, in RIS.transducer]
path_id_Accepting [lemma, in RIS.transducer]
path_single_letter [lemma, in RIS.transducer]
path_support [lemma, in RIS.closed_automaton]
path_Tr [lemma, in RIS.traces]
path_init_refl_pair [lemma, in RIS.aeq_facts]
path_init_pair [lemma, in RIS.aeq_facts]
pathϵ [constructor, in RIS.transducer]
perm [definition, in RIS.atoms]
perm [section, in RIS.atoms]
permutations [definition, in RIS.bijection]
permutations_elements [lemma, in RIS.bijection]
permutations_image [lemma, in RIS.bijection]
permutations_spec [lemma, in RIS.bijection]
perm_path_mixp [lemma, in RIS.transducer]
perm_p_pinv_eq_nil [lemma, in RIS.atoms]
perm_pinv_p_eq_nil [lemma, in RIS.atoms]
perm_a_a_eq_nil [lemma, in RIS.atoms]
perm_bij [lemma, in RIS.atoms]
perm_inj [lemma, in RIS.atoms]
perm_comm_pair [lemma, in RIS.alphaKA]
perm.group [section, in RIS.atoms]
_ # _ [notation, in RIS.atoms]
_ ∗ [notation, in RIS.atoms]
_ ∙ _ [notation, in RIS.atoms]
⌊ _ ⌋ [notation, in RIS.atoms]
pointer [inductive, in RIS.representative]
pointers [section, in RIS.representative]
_ ? [notation, in RIS.representative]
_ ! [notation, in RIS.representative]
⦅ _ ⦆ [notation, in RIS.representative]
positive [definition, in RIS.positive_regexp]
positive_act [lemma, in RIS.alpha_regexp]
positive_star [lemma, in RIS.positive_regexp]
positive_inf [lemma, in RIS.positive_regexp]
positive_KA_inf [lemma, in RIS.positive_regexp]
positive_KA [lemma, in RIS.positive_regexp]
positive_lang [lemma, in RIS.positive_regexp]
positive_αKA_inf [lemma, in RIS.alphaKA]
positive_αKA [lemma, in RIS.alphaKA]
positive_regexp [library]
prefixes [definition, in RIS.regexp]
prefixes_support [lemma, in RIS.alpha_regexp]
prefixes_spec [lemma, in RIS.regexp]
prj1 [abbreviation, in RIS.tools]
prj2 [abbreviation, in RIS.tools]
prod [projection, in RIS.algebra]
prod [constructor, in RIS.algebra]
prodLang [instance, in RIS.language]
product [definition, in RIS.tools]
Product [record, in RIS.algebra]
Product [inductive, in RIS.algebra]
product_square_close_balanced [lemma, in RIS.factors]
product_Δ [lemma, in RIS.tools]
product_assoc [lemma, in RIS.tools]
product_infRel [instance, in RIS.tools]
product_eqRel [instance, in RIS.tools]
prod_binding_maxBind [lemma, in RIS.factors]
prod_assoc [lemma, in RIS.words]
prod_unit_l [lemma, in RIS.words]
prod_unit_r [lemma, in RIS.words]
prod_binding [definition, in RIS.words]
prod_ax_inf [instance, in RIS.regexp]
prod_ax_eq [instance, in RIS.regexp]
prog [constructor, in RIS.equiv_stacks]
prog2 [constructor, in RIS.equiv_stacks]
proj_length [lemma, in RIS.tools]
proj1_act [lemma, in RIS.atoms]
proj2_act [lemma, in RIS.atoms]
proof [section, in RIS.completenessKA]
proper_join_inf [definition, in RIS.systems]
proper_starLang [instance, in RIS.language]
proper_prodLang [instance, in RIS.language]
proper_joinLang [instance, in RIS.language]
proper_star_inf [instance, in RIS.algebra]
proper_prod_inf [instance, in RIS.algebra]
proper_join_eq [instance, in RIS.algebra]
proper_join_inf [instance, in RIS.algebra]
proper_n [projection, in RIS.algebra]
proper_d [projection, in RIS.algebra]
proper_c [projection, in RIS.algebra]
proper_star [projection, in RIS.algebra]
proper_join [projection, in RIS.algebra]
proper_prod [projection, in RIS.algebra]

R

R [axiom, in RIS.normalise]
rational [definition, in RIS.automata]
Reachables [definition, in RIS.automata]
Reachables_spec [lemma, in RIS.automata]
red_def_equiv [lemma, in RIS.normalise]
red_def_defect_count [lemma, in RIS.normalise]
red_def_valid [lemma, in RIS.normalise]
red_def [inductive, in RIS.normalise]
refactor [lemma, in RIS.algebra]
reform [lemma, in RIS.atoms]
regexp [section, in RIS.systems]
Regexp [abbreviation, in RIS.closed_automaton]
Regexp [abbreviation, in RIS.positive_regexp]
Regexp [abbreviation, in RIS.alphaKA]
regexp [inductive, in RIS.regexp]
regexp [section, in RIS.regexp]
regexp [library]
regexpPath [lemma, in RIS.automata]
regexp_laws [instance, in RIS.completenessKA]
regexp_tt [constructor, in RIS.completenessKA]
regexp_unit [inductive, in RIS.completenessKA]
regexp_to_regex'_lang [lemma, in RIS.completenessKA]
regexp_to_regex'_id [lemma, in RIS.completenessKA]
regexp_to_expr [definition, in RIS.completenessKA]
regexp_to_regex' [definition, in RIS.completenessKA]
regexp.gen_proofs [section, in RIS.regexp]
_ ≦0 _ [notation, in RIS.regexp]
_ ≡0 _ [notation, in RIS.regexp]
_ <=KA _ [notation, in RIS.regexp]
_ =KA _ [notation, in RIS.regexp]
{| _ , _ |} ⊢ _ =<= _ [notation, in RIS.regexp]
{| _ , _ |} ⊢ _ == _ [notation, in RIS.regexp]
⟦ _ ⟧ [notation, in RIS.regexp]
⟪ _ ⟫ [notation, in RIS.regexp]
Σ_{ _ } _ [notation, in RIS.regexp]
δ⋆ [notation, in RIS.regexp]
regex'_to_regexp_lang [lemma, in RIS.completenessKA]
regex'_to_regexp_id [lemma, in RIS.completenessKA]
regex'_to_regexp [definition, in RIS.completenessKA]
regJoin [instance, in RIS.regexp]
regProduct [instance, in RIS.regexp]
regStar [instance, in RIS.regexp]
regular [definition, in RIS.automata]
regUn [instance, in RIS.regexp]
regZero [instance, in RIS.regexp]
reg_lang [definition, in RIS.regexp]
rel [abbreviation, in RIS.representative]
rel [abbreviation, in RIS.representative]
relations [section, in RIS.tools]
_ ⨾ _ [notation, in RIS.tools]
relseq [instance, in RIS.normalise]
remove_defect_equiv [lemma, in RIS.normalise]
remove_defect_valid [lemma, in RIS.normalise]
remove_defect [definition, in RIS.normalise]
remove_defect_aux [definition, in RIS.normalise]
Repr [definition, in RIS.representative]
representative [library]
repr_word_equiv [lemma, in RIS.normalise]
repr_word_binding [lemma, in RIS.normalise]
repr_word_support [lemma, in RIS.normalise]
repr_word_perm [lemma, in RIS.normalise]
repr_word_injective [lemma, in RIS.normalise]
repr_letter_binding [lemma, in RIS.normalise]
repr_letter_support [lemma, in RIS.normalise]
repr_letter_equivariant [lemma, in RIS.normalise]
repr_letter_injective [lemma, in RIS.normalise]
repr_letter [definition, in RIS.normalise]
restrict [definition, in RIS.closed_languages]
restrict_eq [lemma, in RIS.closed_languages]
restrict_inf_bis [lemma, in RIS.closed_languages]
restrict_inf [lemma, in RIS.closed_languages]
restrict_inclLists [instance, in RIS.closed_languages]
restrict_eqLists [instance, in RIS.closed_languages]
rev_equivalent [lemma, in RIS.tools]
rev_induction [lemma, in RIS.tools]
right_absorbing [projection, in RIS.algebra]
right_unit [projection, in RIS.algebra]
right_distr [projection, in RIS.regexp]
rm [definition, in RIS.tools]
rmfst [definition, in RIS.tools]
rmfstn [definition, in RIS.traces]
rmfstn_decr [lemma, in RIS.traces]
rmfstn_rmfst [lemma, in RIS.traces]
rmfstn_in [lemma, in RIS.traces]
rmfstn_notin [lemma, in RIS.traces]
rmfst_perm [lemma, in RIS.atoms]
rmfst_app_dec_stacks [lemma, in RIS.stacks]
rmfst_paired [lemma, in RIS.stacks]
rmfst_present [lemma, in RIS.stacks]
rmfst_absent [lemma, in RIS.stacks]
rmfst_flip [lemma, in RIS.tools]
rmfst_app_dec [lemma, in RIS.tools]
rmfst_comm [lemma, in RIS.tools]
rmfst_decr [lemma, in RIS.tools]
rmfst_in [lemma, in RIS.tools]
rmfst_notin [lemma, in RIS.tools]
rm_notin [lemma, in RIS.tools]
rm_incl_Proper [instance, in RIS.tools]
rm_equivalent_Proper [instance, in RIS.tools]
rm_equiv [lemma, in RIS.tools]
rm_In [lemma, in RIS.tools]

S

s [section, in RIS.alpha_regexp]
s [section, in RIS.alternate_eq]
s [section, in RIS.transducer]
s [section, in RIS.closed_automaton]
s [section, in RIS.traces]
s [section, in RIS.closed_languages]
s [section, in RIS.stacks]
s [section, in RIS.representative]
s [section, in RIS.binding_finite]
s [section, in RIS.positive_regexp]
s [section, in RIS.aeq_facts]
s [section, in RIS.words]
s [section, in RIS.normalise]
s [section, in RIS.equiv_stacks]
s [section, in RIS.alphaKA]
s [section, in RIS.nominalsetoid]
same_orbitb_spec [lemma, in RIS.representative]
same_orbitb [definition, in RIS.representative]
same_orbit_get_perm [lemma, in RIS.representative]
same_orbit_Equivalence [instance, in RIS.representative]
same_orbit [definition, in RIS.representative]
scope_binding [lemma, in RIS.aeq_facts]
select [definition, in RIS.traces]
select_spec [lemma, in RIS.traces]
semantics [definition, in RIS.equiv_stacks]
SemEquiv [record, in RIS.tools]
SemEquiv [inductive, in RIS.tools]
SemEquiv_listS [instance, in RIS.nominalsetoid]
semeq_list [definition, in RIS.nominalsetoid]
Semilattice [record, in RIS.algebra]
Semilattice_KA [instance, in RIS.regexp]
Semilattice_ax [instance, in RIS.regexp]
SemiRing [record, in RIS.algebra]
semiring_right_distr [projection, in RIS.algebra]
semiring_left_distr [projection, in RIS.algebra]
semiring_zero [projection, in RIS.algebra]
semiring_comm [projection, in RIS.algebra]
semiring_add [projection, in RIS.algebra]
semiring_prod [projection, in RIS.algebra]
SemSmaller [record, in RIS.tools]
SemSmaller [inductive, in RIS.tools]
sequiv [projection, in RIS.tools]
sequiv [constructor, in RIS.tools]
Shift [definition, in RIS.normalise]
shift [definition, in RIS.normalise]
Shift_bound [lemma, in RIS.normalise]
Shift_bound_lt [lemma, in RIS.normalise]
Shift_free [lemma, in RIS.normalise]
shift_bound_lt [lemma, in RIS.normalise]
shift_bound_gt [lemma, in RIS.normalise]
shift_bound_n [lemma, in RIS.normalise]
shift_free [lemma, in RIS.normalise]
shuffle [section, in RIS.tools]
shuffles [definition, in RIS.tools]
shuffles_map [lemma, in RIS.tools]
shuffles_length [lemma, in RIS.tools]
shuffles_nodup [lemma, in RIS.tools]
shuffles_equiv [lemma, in RIS.tools]
shuffles_spec [lemma, in RIS.tools]
shuffles_act [lemma, in RIS.bijection]
similar [inductive, in RIS.equiv_stacks]
similar [inductive, in RIS.regexp]
similar_equiv_stacks [lemma, in RIS.equiv_stacks]
similar_join [lemma, in RIS.regexp]
simulation [section, in RIS.systems]
simulation_language [lemma, in RIS.regexp]
simulation_step [constructor, in RIS.regexp]
simulation_expr [section, in RIS.regexp]
size [definition, in RIS.words]
sizeAt [definition, in RIS.alpha_regexp]
sizeAt_fresh [lemma, in RIS.alpha_regexp]
sizeExpr [definition, in RIS.regexp]
sizeExpr_act [lemma, in RIS.alpha_regexp]
sizeSys [definition, in RIS.systems]
size_sizeAt [lemma, in RIS.alpha_regexp]
size_stack [lemma, in RIS.transducer]
size_prod_bound_inf_right [lemma, in RIS.words]
size_prod_bound_inf_left [lemma, in RIS.words]
size_prod_bound_sup [lemma, in RIS.words]
smaller [projection, in RIS.tools]
Smaller [record, in RIS.tools]
smaller [constructor, in RIS.tools]
Smaller [inductive, in RIS.tools]
solution_sys_spec [lemma, in RIS.systems]
solution_sys_zero [lemma, in RIS.systems]
solution_no_var [lemma, in RIS.systems]
solution_sys [definition, in RIS.systems]
soundness [lemma, in RIS.regexp]
soundness_proof [lemma, in RIS.regexp]
spines [definition, in RIS.binding_finite]
spines_homogeneous [lemma, in RIS.binding_finite]
spines_split [lemma, in RIS.binding_finite]
spines_eq [lemma, in RIS.binding_finite]
spines_support [lemma, in RIS.alphaKA]
split_app_unambiguous [lemma, in RIS.tools]
split_word [lemma, in RIS.tools]
split_fst [lemma, in RIS.tools]
split_snd [lemma, in RIS.tools]
split_star [lemma, in RIS.regexp]
sqExpr [definition, in RIS.binding_finite]
sqExpr_Σ [lemma, in RIS.binding_finite]
sqExpr_Π [lemma, in RIS.binding_finite]
sqExpr_star [lemma, in RIS.binding_finite]
sqExpr_add [lemma, in RIS.binding_finite]
sqExpr_prod [lemma, in RIS.binding_finite]
sqExpr_inf [lemma, in RIS.binding_finite]
sqExpr_bindings_finite_star [lemma, in RIS.binding_finite]
sqListExpr [definition, in RIS.binding_finite]
sqListExpr_Π_In [lemma, in RIS.binding_finite]
square [definition, in RIS.factors]
ssmaller [projection, in RIS.tools]
ssmaller [constructor, in RIS.tools]
stack [definition, in RIS.stacks]
stacks [library]
stack_binding_both [lemma, in RIS.transducer]
stack_binding [lemma, in RIS.transducer]
stack_binding_subword [lemma, in RIS.aeq_facts]
star [projection, in RIS.algebra]
Star [record, in RIS.algebra]
star [constructor, in RIS.algebra]
Star [inductive, in RIS.algebra]
starLang [instance, in RIS.language]
star_switch_side [lemma, in RIS.algebra]
star_join [lemma, in RIS.algebra]
star_incr [lemma, in RIS.algebra]
star_right_ind [lemma, in RIS.regexp]
star_left_ind [lemma, in RIS.regexp]
star_ax_eq [instance, in RIS.regexp]
statesNFA [definition, in RIS.automata]
statesNFA_path [lemma, in RIS.automata]
statesNFA_spec [lemma, in RIS.automata]
stateSpace [definition, in RIS.regexp]
stateSpace_statesNFA [lemma, in RIS.automata]
stateSpace_Var [lemma, in RIS.regexp]
stateSpace_trans [lemma, in RIS.regexp]
stateSpace_refl [lemma, in RIS.regexp]
state_space [definition, in RIS.closed_automaton]
step [definition, in RIS.transducer]
step [constructor, in RIS.normalise]
step_det [lemma, in RIS.transducer]
step_mix [lemma, in RIS.transducer]
step_sym [lemma, in RIS.transducer]
subsets [definition, in RIS.tools]
subsets_NoDup [lemma, in RIS.tools]
subsets_spec [lemma, in RIS.tools]
subsets_In [lemma, in RIS.tools]
subword [definition, in RIS.subword]
subword [section, in RIS.subword]
subword [library]
subword_cons [lemma, in RIS.subword]
subword_nil [lemma, in RIS.subword]
subword_app [instance, in RIS.subword]
subword_app_r [lemma, in RIS.subword]
subword_PartialOrder [instance, in RIS.subword]
subword_leq_length [instance, in RIS.subword]
subword_length [lemma, in RIS.subword]
subword_PreOrder [instance, in RIS.subword]
subword_cons_Proper [instance, in RIS.subword]
subword_not_In [lemma, in RIS.aeq_facts]
subword_dec_app [lemma, in RIS.aeq_facts]
subword_app [instance, in RIS.aeq_facts]
subword_map [instance, in RIS.aeq_facts]
subword_incl [lemma, in RIS.aeq_facts]
subword_filter [instance, in RIS.aeq_facts]
_ ⊑ _ [notation, in RIS.subword]
succ [definition, in RIS.systems]
succ_spec [lemma, in RIS.systems]
sum [definition, in RIS.tools]
sum_filter [lemma, in RIS.tools]
sum_incr_0_right [lemma, in RIS.tools]
sum_incr_0_left [lemma, in RIS.tools]
sum_lt [lemma, in RIS.tools]
sum_le [lemma, in RIS.tools]
sum_zero_in [lemma, in RIS.tools]
sum_add_distr [lemma, in RIS.tools]
sum_add [lemma, in RIS.tools]
sum_ext_In [lemma, in RIS.tools]
sum_ext [lemma, in RIS.tools]
sum_incr [lemma, in RIS.tools]
sum_eq_ND [lemma, in RIS.tools]
sum_incl_ND [lemma, in RIS.tools]
sum_app [lemma, in RIS.tools]
suppoid [projection, in RIS.nominalsetoid]
suppoid [constructor, in RIS.nominalsetoid]
suppoid_app [lemma, in RIS.nominalsetoid]
suppoid_cons [lemma, in RIS.nominalsetoid]
SuppOrbit [instance, in RIS.representative]
support [projection, in RIS.atoms]
Support [record, in RIS.atoms]
support [constructor, in RIS.atoms]
Support [inductive, in RIS.atoms]
SupportAtom [instance, in RIS.atoms]
supported [record, in RIS.tools]
supported_ext_eq [instance, in RIS.tools]
SupportList [instance, in RIS.atoms]
SupportPair [instance, in RIS.atoms]
SupportSetoid [record, in RIS.nominalsetoid]
SupportSetoid [inductive, in RIS.nominalsetoid]
SupportSetoidList [instance, in RIS.nominalsetoid]
support_ϵ [lemma, in RIS.alpha_regexp]
support_Var [lemma, in RIS.alpha_regexp]
support_star [lemma, in RIS.alpha_regexp]
support_prod [lemma, in RIS.alpha_regexp]
support_join [lemma, in RIS.alpha_regexp]
support_lang [lemma, in RIS.alpha_regexp]
support_image_equivariant [lemma, in RIS.atoms]
support_list_atoms [lemma, in RIS.atoms]
support_eq_action_eq [lemma, in RIS.atoms]
support_list_cons [lemma, in RIS.atoms]
support_list_app [lemma, in RIS.atoms]
Support_sum [instance, in RIS.atoms]
Support_option [instance, in RIS.atoms]
support_nat [instance, in RIS.atoms]
support_action [projection, in RIS.atoms]
support_pointer [instance, in RIS.representative]
support_letter [instance, in RIS.words]
support_X [projection, in RIS.words]
support_action_eq [projection, in RIS.nominalsetoid]
SuppRepr [instance, in RIS.representative]
supp_letter [definition, in RIS.words]
supReg [instance, in RIS.alpha_regexp]
surjective [record, in RIS.tools]
surjective_perm [instance, in RIS.atoms]
surjective_ext_eq [instance, in RIS.tools]
system [definition, in RIS.systems]
system [section, in RIS.systems]
systems [library]
system_homomorphism [definition, in RIS.systems]
system.solutions [section, in RIS.systems]
_ ⩵ _ [notation, in RIS.systems]
_ ≦ _ [notation, in RIS.systems]
sys_of_NFA_least_solution [lemma, in RIS.systems]
sys_of_NFA_lang [lemma, in RIS.systems]
sys_of_NFA_solution [lemma, in RIS.systems]
sys_of_NFA [definition, in RIS.systems]
_ =α= _ [notation, in RIS.alternate_eq]
_ ≡' _ [notation, in RIS.alternate_eq]
_ ⧓ _ [notation, in RIS.transducer]
_ ⊣ _ | _ ⤅ _ [notation, in RIS.transducer]
_ ⊣ _ | _ ↦ _ [notation, in RIS.transducer]
_ ⇂ _ [notation, in RIS.closed_languages]
_ ⊨ _ ↦ _ [notation, in RIS.stacks]
_ ✓ [notation, in RIS.stacks]
_ ? [notation, in RIS.representative]
_ ! [notation, in RIS.representative]
_ #α _ [notation, in RIS.words]
_ ⋄ _ [notation, in RIS.words]
_ ◁ _ [notation, in RIS.words]
_ ▷ _ [notation, in RIS.words]
_ ⋅ _ [notation, in RIS.words]
_ ⟩ [notation, in RIS.words]
_ +++ _ [notation, in RIS.normalise]
_ ? [notation, in RIS.normalise]
_ ≺ _ [notation, in RIS.equiv_stacks]
_ ∼ _ [notation, in RIS.equiv_stacks]
_ -- _ ---> _ [notation, in RIS.equiv_stacks]
_ -- _ -->> _ [notation, in RIS.equiv_stacks]
_ == _ [notation, in RIS.equiv_stacks]
_ <=α _ [notation, in RIS.alphaKA]
_ =α _ [notation, in RIS.alphaKA]
_ ⊙ _ [notation, in RIS.nominalsetoid]
⌈ _ ⌉ [notation, in RIS.nominalsetoid]
⟦ _ ⟧ [notation, in RIS.equiv_stacks]
⟨ _ [notation, in RIS.words]
⟪ _ ⟫ [notation, in RIS.normalise]
⦅ _ ⦆ [notation, in RIS.representative]
⦑ _ ⦒ [notation, in RIS.normalise]

T

test_dyn_seq_spec [lemma, in RIS.normalise]
test_dyn_seq [definition, in RIS.normalise]
test_valid_spec [lemma, in RIS.normalise]
test_valid_true [lemma, in RIS.normalise]
test_valid_aux_false_app [lemma, in RIS.normalise]
test_valid [definition, in RIS.normalise]
test_valid_aux [definition, in RIS.normalise]
test_var [definition, in RIS.normalise]
test0 [definition, in RIS.regexp]
test0_act [lemma, in RIS.alpha_regexp]
test0_spines [lemma, in RIS.binding_finite]
test0_𝐇 [lemma, in RIS.binding_finite]
test0_bindPref [lemma, in RIS.binding_finite]
test0_bindings [lemma, in RIS.binding_finite]
test0_αKA [lemma, in RIS.alphaKA]
test0_δA [lemma, in RIS.regexp]
test0_stateSpace [lemma, in RIS.regexp]
test0_prefixes [lemma, in RIS.regexp]
test0_δ [lemma, in RIS.regexp]
test0_test1_false [lemma, in RIS.regexp]
test0_ϵ [lemma, in RIS.regexp]
test0_KA [lemma, in RIS.regexp]
test0_Σ [lemma, in RIS.regexp]
test0_spec [lemma, in RIS.regexp]
test0_false [lemma, in RIS.regexp]
test1 [definition, in RIS.regexp]
test1_spec [lemma, in RIS.regexp]
tools [library]
to_sigma [lemma, in RIS.completenessKA]
to_nat [lemma, in RIS.completenessKA]
to_expr_id [lemma, in RIS.completenessKA]
to_perm_correct [lemma, in RIS.bijection]
Tr [definition, in RIS.traces]
traces [library]
transducer [library]
transition [constructor, in RIS.automata]
transitions_from_spec [lemma, in RIS.closed_automaton]
transitions_from [definition, in RIS.closed_automaton]
Trn [definition, in RIS.traces]
Trn_path_fst [lemma, in RIS.traces]
Trn_path_snd [lemma, in RIS.traces]
Trn_d_binding [lemma, in RIS.traces]
Trn_c_binding [lemma, in RIS.traces]
Trn_incr [lemma, in RIS.traces]
Trn_open [lemma, in RIS.traces]
Trn_In_length [lemma, in RIS.traces]
Trn_Tr [lemma, in RIS.traces]
Trn_add [lemma, in RIS.traces]
Trn_aux_Trn [lemma, in RIS.traces]
Trn_aux_fst [lemma, in RIS.traces]
Trn_aux_app [lemma, in RIS.traces]
Trn_aux_add [lemma, in RIS.traces]
Trn_aux [definition, in RIS.traces]
Tr_path [lemma, in RIS.traces]
Tr_step [lemma, in RIS.traces]
Tr_perm [lemma, in RIS.traces]
Tr_close_balanced [lemma, in RIS.traces]
Tr_support [lemma, in RIS.traces]
Tr_length_binding_atom [lemma, in RIS.traces]
Tr_add [lemma, in RIS.traces]
Tr_app [lemma, in RIS.traces]

U

UId1 [lemma, in RIS.algebra]
UId2 [lemma, in RIS.algebra]
un [projection, in RIS.algebra]
Un [record, in RIS.algebra]
un [constructor, in RIS.algebra]
Un [inductive, in RIS.algebra]
unbounded_binding [lemma, in RIS.binding_finite]
undup [definition, in RIS.tools]
undup_act [lemma, in RIS.atoms]
undup_equivalent_Proper [instance, in RIS.tools]
undup_incl_Proper [instance, in RIS.tools]
undup_equivalent [lemma, in RIS.tools]
undup_length [lemma, in RIS.tools]
UNg [lemma, in RIS.algebra]
Unit [record, in RIS.algebra]
unLang [instance, in RIS.language]
un_star [lemma, in RIS.algebra]
updTr [definition, in RIS.traces]
updTrn [definition, in RIS.traces]
updTrn_updTr [lemma, in RIS.traces]
updTr_length [lemma, in RIS.traces]

V

valid [definition, in RIS.normalise]
valid_app [lemma, in RIS.normalise]
valid_bound_αfresh [lemma, in RIS.normalise]
valid_bound_support_lt [lemma, in RIS.normalise]
valid_support_open_explicit [lemma, in RIS.normalise]
valid_support_open [lemma, in RIS.normalise]
valid_repr_word [lemma, in RIS.normalise]
valid_close [definition, in RIS.normalise]
valid_var [definition, in RIS.normalise]
valid_open [definition, in RIS.normalise]
var [constructor, in RIS.words]
Var [definition, in RIS.regexp]
vars_Antimirov [lemma, in RIS.systems]
vars_elim [lemma, in RIS.systems]
vars_system [definition, in RIS.systems]
var_leq [definition, in RIS.systems]
var_perm_app_Accepting [lemma, in RIS.transducer]
var_perm'_accepting [lemma, in RIS.stacks]
var_perm_accepting [lemma, in RIS.stacks]
var_perm_paired [lemma, in RIS.stacks]
var_perm'_spec [lemma, in RIS.stacks]
var_perm'_None [lemma, in RIS.stacks]
var_perm'_Some [lemma, in RIS.stacks]
var_perm' [definition, in RIS.stacks]
var_perm [definition, in RIS.stacks]
Var_spec [lemma, in RIS.regexp]
vector [definition, in RIS.systems]
VeryGoodAxioms [record, in RIS.regexp]
verygoodKA [instance, in RIS.regexp]
verygoodαKA [instance, in RIS.alphaKA]

W

W [abbreviation, in RIS.normalise]
weak_solution_ext [lemma, in RIS.systems]
weak_solution [definition, in RIS.systems]
weight [definition, in RIS.binding_finite]
weightExpr [definition, in RIS.binding_finite]
weightExpr_incr_sup_right [lemma, in RIS.binding_finite]
weightExpr_incr_sup_left [lemma, in RIS.binding_finite]
weight_app_right [lemma, in RIS.binding_finite]
weight_app_left [lemma, in RIS.binding_finite]
weight_app [lemma, in RIS.binding_finite]
weight_incr_sup [lemma, in RIS.binding_finite]
wequiv [instance, in RIS.words]
witness [definition, in RIS.systems]
witness_nodup [lemma, in RIS.systems]
witness_incl [lemma, in RIS.systems]
witness_dup [lemma, in RIS.systems]
witness_app [lemma, in RIS.systems]
witness_spec [lemma, in RIS.systems]
word [definition, in RIS.words]
words [library]
w_equiv_stacks [lemma, in RIS.equiv_stacks]
w_path [lemma, in RIS.equiv_stacks]
w1 [definition, in RIS.equiv_stacks]
w2 [definition, in RIS.equiv_stacks]

X

X_dec [lemma, in RIS.tools]

Z

zero [projection, in RIS.algebra]
Zero [record, in RIS.algebra]
zero [constructor, in RIS.algebra]
Zero [inductive, in RIS.algebra]
zeroLang [instance, in RIS.language]
zero_minimal [lemma, in RIS.algebra]

other

_ ⊓ _ [notation, in RIS.factors]
_ ⊣ _ | _ ⤅ _ [notation, in RIS.transducer]
_ ⊣ _ | _ ↦ _ [notation, in RIS.transducer]
_ # _ [notation, in RIS.atoms]
_ ∗ [notation, in RIS.atoms]
_ ∙ _ [notation, in RIS.atoms]
_ ⊑ _ [notation, in RIS.subword]
_ ✓ [notation, in RIS.stacks]
_ ⊨ _ ↦ _ [notation, in RIS.stacks]
_ ! [notation, in RIS.representative]
_ ={ _ }= _ [notation, in RIS.representative]
_ ⊖ _ [notation, in RIS.tools]
_ ∖ _ [notation, in RIS.tools]
_ ≈ _ [notation, in RIS.tools]
_ ` [notation, in RIS.tools]
_ ⋈ _ [notation, in RIS.tools]
_ ⊗ _ [notation, in RIS.tools]
_ :> _ [notation, in RIS.tools]
_ ∈ _ [notation, in RIS.tools]
_ ⊆ _ [notation, in RIS.tools]
_ ⨾ _ [notation, in RIS.tools]
_ =?= _ [notation, in RIS.tools]
_ ≲ _ [notation, in RIS.tools]
_ ≤ _ [notation, in RIS.tools]
_ ≃ _ [notation, in RIS.tools]
_ ≡ _ [notation, in RIS.tools]
_ ∘ _ [notation, in RIS.tools]
_ >> _ [notation, in RIS.bijection]
_ ▷ _ [notation, in RIS.words]
_ ◁ _ [notation, in RIS.words]
_ ⋄ _ [notation, in RIS.words]
_ #α _ [notation, in RIS.words]
_ ⋅ _ [notation, in RIS.words]
_ ⟩ [notation, in RIS.words]
_ ⋆ [notation, in RIS.algebra]
_ ∪ _ [notation, in RIS.algebra]
_ · _ [notation, in RIS.algebra]
_ <=α _ [notation, in RIS.alphaKA]
_ =α _ [notation, in RIS.alphaKA]
_ ⊙ _ [notation, in RIS.nominalsetoid]
_ <=KA _ [notation, in RIS.regexp]
_ =KA _ [notation, in RIS.regexp]
$ _ [notation, in RIS.tools]
{{ _ }} [notation, in RIS.tools]
{| _ , _ |} ⊢ _ =<= _ [notation, in RIS.regexp]
{| _ , _ |} ⊢ _ == _ [notation, in RIS.regexp]
⌈ _ ⌉ [notation, in RIS.nominalsetoid]
⌊ _ ⌋ [notation, in RIS.atoms]
⎢ _ ⎥ [notation, in RIS.tools]
⟦ _ ⟧ [notation, in RIS.regexp]
⟨ _ [notation, in RIS.words]
⟪ _ ⟫ [notation, in RIS.regexp]
⦅ _ ⦆ [notation, in RIS.representative]
Σ_{ _ } _ [notation, in RIS.regexp]
δ⋆ [notation, in RIS.regexp]
𝟬 [notation, in RIS.algebra]
𝟭 [notation, in RIS.algebra]
Δ [definition, in RIS.tools]
Δ_product [lemma, in RIS.tools]
Π [definition, in RIS.regexp]
Π_lang [lemma, in RIS.regexp]
Σ [definition, in RIS.algebra]
Σ_act [lemma, in RIS.alpha_regexp]
Σ_support [lemma, in RIS.alpha_regexp]
Σ_bounded [lemma, in RIS.algebra]
Σ_bigger [lemma, in RIS.algebra]
Σ_equivalent [instance, in RIS.algebra]
Σ_incl [lemma, in RIS.algebra]
Σ_app [lemma, in RIS.algebra]
Σ_distr_r [lemma, in RIS.algebra]
Σ_distr_l [lemma, in RIS.algebra]
Σ_map_app [lemma, in RIS.alphaKA]
Σ_map_equiv_α [lemma, in RIS.alphaKA]
Σ_bounded_α [lemma, in RIS.alphaKA]
Σ_map_equiv [lemma, in RIS.regexp]
Σ_map_concat [lemma, in RIS.regexp]
Σ_equivalent [instance, in RIS.regexp]
Σ_incl0 [lemma, in RIS.regexp]
Σ_app [lemma, in RIS.regexp]
Σ_lang [lemma, in RIS.regexp]
αequiv [inductive, in RIS.words]
αequiv_to_αequiv2 [lemma, in RIS.alternate_eq]
αequiv_alternate [lemma, in RIS.alternate_eq]
αequiv_αfresh_transpose [lemma, in RIS.transducer]
αequiv_path [lemma, in RIS.transducer]
αequiv_perm [lemma, in RIS.words]
αequiv_binding [lemma, in RIS.words]
αequiv_length [lemma, in RIS.words]
αequiv_app [instance, in RIS.words]
αequiv_app_right [lemma, in RIS.words]
αequiv_app_left [lemma, in RIS.words]
αequiv_equivalence [instance, in RIS.words]
αequiv' [inductive, in RIS.alternate_eq]
αequiv'_perm [lemma, in RIS.alternate_eq]
αequiv'_binding [lemma, in RIS.alternate_eq]
αequiv'_app [instance, in RIS.alternate_eq]
αequiv'_app_right [lemma, in RIS.alternate_eq]
αequiv'_app_left [lemma, in RIS.alternate_eq]
αequiv'_equivalence [instance, in RIS.alternate_eq]
αequiv2 [inductive, in RIS.alternate_eq]
αequiv2_to_αequiv [lemma, in RIS.alternate_eq]
αfresh_perm_path_nil [lemma, in RIS.transducer]
αfresh_perm_path [lemma, in RIS.transducer]
αfresh_close_split_unique [lemma, in RIS.words]
αfresh_open_split [lemma, in RIS.words]
αfresh_close_split [lemma, in RIS.words]
αfresh_support [lemma, in RIS.words]
αfresh_letter [lemma, in RIS.words]
αfresh_perm [lemma, in RIS.words]
αfresh_alt [lemma, in RIS.alphaKA]
αKA [inductive, in RIS.alphaKA]
αKA_inf_act [lemma, in RIS.alphaKA]
αKA_act [lemma, in RIS.alphaKA]
αKA_KleeneAlgebra [instance, in RIS.alphaKA]
αKA_lang_inf [lemma, in RIS.alphaKA]
αKA_lang [lemma, in RIS.alphaKA]
αKA_KA [constructor, in RIS.alphaKA]
αKA_αα [constructor, in RIS.alphaKA]
αl [constructor, in RIS.words]
αl' [constructor, in RIS.alternate_eq]
αm [constructor, in RIS.alternate_eq]
αr [constructor, in RIS.words]
αr' [constructor, in RIS.alternate_eq]
αt [constructor, in RIS.words]
αt' [constructor, in RIS.alternate_eq]
α_closed [definition, in RIS.closed_languages]
αα [constructor, in RIS.words]
αα' [constructor, in RIS.alternate_eq]
αα2 [constructor, in RIS.alternate_eq]
αε [constructor, in RIS.words]
αε' [constructor, in RIS.alternate_eq]
αε2 [constructor, in RIS.alternate_eq]
δ [definition, in RIS.regexp]
δA [definition, in RIS.regexp]
δA_proper_KA [lemma, in RIS.systems]
δA_stateSpace [lemma, in RIS.regexp]
δt [definition, in RIS.transducer]
δt_flip [lemma, in RIS.transducer]
δt_app_Accepting [lemma, in RIS.transducer]
δt_app [lemma, in RIS.transducer]
δt_path [lemma, in RIS.transducer]
δt_compatible_spec [lemma, in RIS.transducer]
δ_act [lemma, in RIS.alpha_regexp]
δ_proper_αKA_not_open_inf [lemma, in RIS.alphaKA]
δ_proper_αKA_not_open [lemma, in RIS.alphaKA]
δ_support [lemma, in RIS.alphaKA]
δ_binFin [lemma, in RIS.alphaKA]
δ_inf_e_α [lemma, in RIS.alphaKA]
δ_words_last [lemma, in RIS.regexp]
δ_words_lang [lemma, in RIS.regexp]
δ_words_add [lemma, in RIS.regexp]
δ_words_zero [lemma, in RIS.regexp]
δ_words [definition, in RIS.regexp]
δ_prod [lemma, in RIS.regexp]
δ_proper_KA_inf [lemma, in RIS.regexp]
δ_proper_KA [lemma, in RIS.regexp]
δ_Σ [lemma, in RIS.regexp]
δ_inf_e [lemma, in RIS.regexp]
δ_lang [lemma, in RIS.regexp]
ε [definition, in RIS.words]
η [definition, in RIS.representative]
η_support [lemma, in RIS.representative]
η_equivariant [lemma, in RIS.representative]
η_inj [lemma, in RIS.representative]
ρ [definition, in RIS.normalise]
ρ_spec [lemma, in RIS.normalise]
ϕ [axiom, in RIS.normalise]
ϕ_support [axiom, in RIS.normalise]
ϕ_equivariant [axiom, in RIS.normalise]
ϕ_inj [axiom, in RIS.normalise]
ϵ [definition, in RIS.regexp]
ϵ_act [lemma, in RIS.alpha_regexp]
ϵ_spines [lemma, in RIS.binding_finite]
ϵ_𝐇 [lemma, in RIS.binding_finite]
ϵ_αKA [lemma, in RIS.alphaKA]
ϵ_Σ_zero [lemma, in RIS.regexp]
ϵ_Σ_un [lemma, in RIS.regexp]
ϵ_KA [lemma, in RIS.regexp]
ϵ_idem [lemma, in RIS.regexp]
ϵ_proper_inf [instance, in RIS.regexp]
ϵ_proper [instance, in RIS.regexp]
ϵ_prod [lemma, in RIS.regexp]
ϵ_add [lemma, in RIS.regexp]
ϵ_sub_id [lemma, in RIS.regexp]
ϵ_zero [lemma, in RIS.regexp]
ϵ_ax_spec [lemma, in RIS.regexp]
ϵ_inf_e [lemma, in RIS.regexp]
ϵ_spec [lemma, in RIS.regexp]
ϵ_zero_or_un [lemma, in RIS.regexp]
𝐇 [definition, in RIS.binding_finite]
𝐇_lang [lemma, in RIS.binding_finite]
𝐇_eq [lemma, in RIS.binding_finite]
𝐇_support [lemma, in RIS.alphaKA]
𝐎 [definition, in RIS.normalise]
𝐏 [instance, in RIS.representative]
𝐰 [definition, in RIS.equiv_stacks]
𝖡 [definition, in RIS.words]
𝗙 [definition, in RIS.words]
𝗙_perm [lemma, in RIS.words]
𝗙_add [lemma, in RIS.words]
𝗙_app [lemma, in RIS.words]
𝗙_cons [lemma, in RIS.words]
𝗙_singl [lemma, in RIS.words]
𝗳 [definition, in RIS.words]
𝗳_perm [lemma, in RIS.words]

---

Notation Index

A

_ ⋆ [in RIS.algebra]
_ ∪ _ [in RIS.algebra]
_ · _ [in RIS.algebra]
_ ⩵ _ [in RIS.algebra]
_ ≦ _ [in RIS.algebra]
𝟬 [in RIS.algebra]
𝟭 [in RIS.algebra]

B

_ >> _ [in RIS.bijection]
_ ∨ _ [in RIS.algebra]
_ ∧ _ [in RIS.algebra]
_ ⩵ _ [in RIS.algebra]
_ ≦ _ [in RIS.algebra]
⊤ [in RIS.algebra]
⊥ [in RIS.algebra]
¬ [in RIS.algebra]

C

_ ⊗ _ [in RIS.tools]

D

_ ⊖ _ [in RIS.tools]
_ ∖ _ [in RIS.tools]
{{ _ }} [in RIS.tools]

E

⦅ _ ⦆ [in RIS.representative]

F

_ ` [in RIS.tools]

J

_ ⩵ _ [in RIS.algebra]
_ ≦ _ [in RIS.algebra]

K

_ ⩵ _ [in RIS.algebra]
_ ≦ _ [in RIS.algebra]

L

_ ^{ _ } [in RIS.language]

M

_ ⋈ _ [in RIS.tools]

O

_ ={ _ }= _ [in RIS.representative]
⦃ _ ⦄ [in RIS.representative]

P

_ # _ [in RIS.atoms]
_ ∗ [in RIS.atoms]
_ ∙ _ [in RIS.atoms]
⌊ _ ⌋ [in RIS.atoms]
_ ? [in RIS.representative]
_ ! [in RIS.representative]
⦅ _ ⦆ [in RIS.representative]

R

_ ≦0 _ [in RIS.regexp]
_ ≡0 _ [in RIS.regexp]
_ <=KA _ [in RIS.regexp]
_ =KA _ [in RIS.regexp]
{| _ , _ |} ⊢ _ =<= _ [in RIS.regexp]
{| _ , _ |} ⊢ _ == _ [in RIS.regexp]
⟦ _ ⟧ [in RIS.regexp]
⟪ _ ⟫ [in RIS.regexp]
Σ_{ _ } _ [in RIS.regexp]
δ⋆ [in RIS.regexp]
_ ⨾ _ [in RIS.tools]

S

_ ⊑ _ [in RIS.subword]
_ ⩵ _ [in RIS.systems]
_ ≦ _ [in RIS.systems]
_ =α= _ [in RIS.alternate_eq]
_ ≡' _ [in RIS.alternate_eq]
_ ⧓ _ [in RIS.transducer]
_ ⊣ _ | _ ⤅ _ [in RIS.transducer]
_ ⊣ _ | _ ↦ _ [in RIS.transducer]
_ ⇂ _ [in RIS.closed_languages]
_ ⊨ _ ↦ _ [in RIS.stacks]
_ ✓ [in RIS.stacks]
_ ? [in RIS.representative]
_ ! [in RIS.representative]
_ #α _ [in RIS.words]
_ ⋄ _ [in RIS.words]
_ ◁ _ [in RIS.words]
_ ▷ _ [in RIS.words]
_ ⋅ _ [in RIS.words]
_ ⟩ [in RIS.words]
_ +++ _ [in RIS.normalise]
_ ? [in RIS.normalise]
_ ≺ _ [in RIS.equiv_stacks]
_ ∼ _ [in RIS.equiv_stacks]
_ -- _ ---> _ [in RIS.equiv_stacks]
_ -- _ -->> _ [in RIS.equiv_stacks]
_ == _ [in RIS.equiv_stacks]
_ <=α _ [in RIS.alphaKA]
_ =α _ [in RIS.alphaKA]
_ ⊙ _ [in RIS.nominalsetoid]
⌈ _ ⌉ [in RIS.nominalsetoid]
⟦ _ ⟧ [in RIS.equiv_stacks]
⟨ _ [in RIS.words]
⟪ _ ⟫ [in RIS.normalise]
⦅ _ ⦆ [in RIS.representative]
⦑ _ ⦒ [in RIS.normalise]

other

_ ⊓ _ [in RIS.factors]
_ ⊣ _ | _ ⤅ _ [in RIS.transducer]
_ ⊣ _ | _ ↦ _ [in RIS.transducer]
_ # _ [in RIS.atoms]
_ ∗ [in RIS.atoms]
_ ∙ _ [in RIS.atoms]
_ ⊑ _ [in RIS.subword]
_ ✓ [in RIS.stacks]
_ ⊨ _ ↦ _ [in RIS.stacks]
_ ! [in RIS.representative]
_ ={ _ }= _ [in RIS.representative]
_ ⊖ _ [in RIS.tools]
_ ∖ _ [in RIS.tools]
_ ≈ _ [in RIS.tools]
_ ` [in RIS.tools]
_ ⋈ _ [in RIS.tools]
_ ⊗ _ [in RIS.tools]
_ :> _ [in RIS.tools]
_ ∈ _ [in RIS.tools]
_ ⊆ _ [in RIS.tools]
_ ⨾ _ [in RIS.tools]
_ =?= _ [in RIS.tools]
_ ≲ _ [in RIS.tools]
_ ≤ _ [in RIS.tools]
_ ≃ _ [in RIS.tools]
_ ≡ _ [in RIS.tools]
_ ∘ _ [in RIS.tools]
_ >> _ [in RIS.bijection]
_ ▷ _ [in RIS.words]
_ ◁ _ [in RIS.words]
_ ⋄ _ [in RIS.words]
_ #α _ [in RIS.words]
_ ⋅ _ [in RIS.words]
_ ⟩ [in RIS.words]
_ ⋆ [in RIS.algebra]
_ ∪ _ [in RIS.algebra]
_ · _ [in RIS.algebra]
_ <=α _ [in RIS.alphaKA]
_ =α _ [in RIS.alphaKA]
_ ⊙ _ [in RIS.nominalsetoid]
_ <=KA _ [in RIS.regexp]
_ =KA _ [in RIS.regexp]
$ _ [in RIS.tools]
{{ _ }} [in RIS.tools]
{| _ , _ |} ⊢ _ =<= _ [in RIS.regexp]
{| _ , _ |} ⊢ _ == _ [in RIS.regexp]
⌈ _ ⌉ [in RIS.nominalsetoid]
⌊ _ ⌋ [in RIS.atoms]
⎢ _ ⎥ [in RIS.tools]
⟦ _ ⟧ [in RIS.regexp]
⟨ _ [in RIS.words]
⟪ _ ⟫ [in RIS.regexp]
⦅ _ ⦆ [in RIS.representative]
Σ_{ _ } _ [in RIS.regexp]
δ⋆ [in RIS.regexp]
𝟬 [in RIS.algebra]
𝟭 [in RIS.algebra]

---

Variable Index

C

combine.same_length [in RIS.tools]

M

mix.same_length [in RIS.tools]

---

Library Index

A

aeq_facts
algebra
alphaKA
alpha_regexp
alternate_eq
atoms
automata

B

bijection
binding_finite

C

closed_automaton
closed_languages
completenessKA

E

equiv_stacks

F

factors

L

language

N

nominalsetoid
normalise

P

positive_regexp

R

regexp
representative

S

stacks
subword
systems

T

tools
traces
transducer

W

words

---

Lemma Index

A

absentb_app [in RIS.stacks]
absentb_cons [in RIS.stacks]
absentb_false [in RIS.stacks]
absentb_correct [in RIS.stacks]
absent_perm [in RIS.stacks]
absent_mix [in RIS.stacks]
absent_flip [in RIS.stacks]
absent_cons [in RIS.stacks]
absent_app [in RIS.stacks]
absent_alt_def [in RIS.stacks]
absent_subword [in RIS.aeq_facts]
Abs1 [in RIS.algebra]
Abs2 [in RIS.algebra]
Accepting_path_Tr [in RIS.traces]
Accepting_rmfst [in RIS.stacks]
Accepting_app [in RIS.stacks]
Accepting_cons_refl [in RIS.stacks]
Accepting_cons [in RIS.stacks]
Accepting_nil [in RIS.stacks]
Accepting_combine [in RIS.stacks]
Accepting_refl [in RIS.stacks]
Accepting_equiv_stacks [in RIS.equiv_stacks]
ActionSetoid_ext_In [in RIS.nominalsetoid]
actoid_lists_length [in RIS.nominalsetoid]
actoid_lists_cons [in RIS.nominalsetoid]
actoid_lists_app [in RIS.nominalsetoid]
actoid_p_pinv [in RIS.nominalsetoid]
actoid_pinv_p [in RIS.nominalsetoid]
act_lang [in RIS.alpha_regexp]
act_eq_equivalent [in RIS.atoms]
act_cons_a_a [in RIS.atoms]
act_bij [in RIS.atoms]
act_pinv_p [in RIS.atoms]
act_p_pinv [in RIS.atoms]
act_nil [in RIS.atoms]
act_lists_length [in RIS.atoms]
act_lists_cons [in RIS.atoms]
act_lists_app [in RIS.atoms]
act_cons [in RIS.atoms]
act_comp_app [in RIS.atoms]
act_atom_nil [in RIS.atoms]
act_bound [in RIS.representative]
act_free [in RIS.representative]
act_make_perm [in RIS.representative]
act_star [in RIS.alphaKA]
act_join [in RIS.alphaKA]
act_prod [in RIS.alphaKA]
aeq_first_letter [in RIS.aeq_facts]
aeq_first_letter_open [in RIS.aeq_facts]
all_subsets_nodup [in RIS.tools]
alternate_validity [in RIS.normalise]
andb_prop_iff [in RIS.tools]
Antimirov_sys [in RIS.systems]
Antimirov_fundamental_theorem [in RIS.systems]
Antimirov_inf [in RIS.systems]
Antimirov_lang [in RIS.regexp]
app_comm [in RIS.tools]
app_idem [in RIS.tools]
app_eq_app_length [in RIS.tools]
app_dyn_equiv [in RIS.normalise]
app_dyn_equiv_app [in RIS.normalise]
app_dyn_dynamic_sequence [in RIS.normalise]
Ass1 [in RIS.algebra]
Ass2 [in RIS.algebra]
ax_inf_lang_incl [in RIS.regexp]
ax_eq_inf [in RIS.regexp]
A1 [in RIS.algebra]
A2 [in RIS.algebra]

B

balanced_open_close [in RIS.words]
balanced_perm [in RIS.words]
balanced_alt [in RIS.alphaKA]
balExprB_balExpr [in RIS.alphaKA]
balExpr_bindFin [in RIS.alphaKA]
bijection_iff_perm [in RIS.bijection]
bindFind_weight_weightExpr [in RIS.binding_finite]
bindFinList_incl [in RIS.binding_finite]
bindFin_inf [in RIS.binding_finite]
bindings_act [in RIS.binding_finite]
bindings_bindPref [in RIS.binding_finite]
bindings_prefixes_support [in RIS.binding_finite]
bindings_finite_prefixes [in RIS.binding_finite]
bindings_ε [in RIS.binding_finite]
bindings_fresh [in RIS.binding_finite]
bindings_Σ [in RIS.binding_finite]
bindings_witness [in RIS.binding_finite]
binding_finite_Σ [in RIS.binding_finite]
binding_finite_sqExpr_star [in RIS.binding_finite]
binding_finite_memory_bindPref [in RIS.binding_finite]
binding_finite_spec [in RIS.binding_finite]
binding_finite_true [in RIS.binding_finite]
binding_finite_false [in RIS.binding_finite]
bindPref_get_witness [in RIS.binding_finite]
bindPref_prefixes_support [in RIS.binding_finite]
bindPref_binding_finite [in RIS.binding_finite]
bindPref_prefixes [in RIS.binding_finite]
bindPref_ε [in RIS.binding_finite]
Bindupto_spec [in RIS.factors]
bind_fin_ind [in RIS.binding_finite]
bissimilar_eq_sem [in RIS.equiv_stacks]
bissimilar_similar [in RIS.equiv_stacks]
bissimilar_w [in RIS.equiv_stacks]
bissimilar_accepting [in RIS.equiv_stacks]
bissimilar_alt [in RIS.equiv_stacks]
bissimilar_path [in RIS.equiv_stacks]
bissim_lang [in RIS.automata]
Bnd1 [in RIS.algebra]
Bnd2 [in RIS.algebra]
bounded_diff [in RIS.systems]
bounded_weightExpr [in RIS.binding_finite]
B1 [in RIS.algebra]
B2 [in RIS.algebra]

C

case_remove_defect [in RIS.normalise]
case_defect [in RIS.normalise]
close_balanced_no_close [in RIS.words]
close_balanced_perm [in RIS.words]
close_balanced_prefix [in RIS.words]
cl_α_star [in RIS.closed_languages]
cl_α_prod [in RIS.closed_languages]
cl_α_nil [in RIS.closed_languages]
cl_α_join [in RIS.closed_languages]
cl_α_inf [in RIS.closed_languages]
cl_α_closed_idem [in RIS.closed_languages]
cl_α_incr [in RIS.closed_languages]
cl_α_idem [in RIS.closed_languages]
cl_α_closed [in RIS.closed_languages]
cl_α_Σ [in RIS.alphaKA]
combine_act [in RIS.atoms]
combine_split [in RIS.tools]
combine_app [in RIS.tools]
combine_snd [in RIS.tools]
combine_fst [in RIS.tools]
compatible_flip [in RIS.transducer]
compatible_app_Accepting [in RIS.transducer]
compatible_app [in RIS.transducer]
compatible_false [in RIS.transducer]
completeness [in RIS.transducer]
CompletenessKA [in RIS.systems]
CompletenessKA [in RIS.completenessKA]
CompletenessKA_inf [in RIS.systems]
CompletenessKA_sigma [in RIS.completenessKA]
cst_spec [in RIS.systems]
c_binding_prod [in RIS.words]
C1 [in RIS.algebra]
C2 [in RIS.algebra]

D

decompose_app [in RIS.tools]
decompose_app [in RIS.aeq_facts]
decomposition [in RIS.tools]
decomp_unambiguous [in RIS.tools]
decomp_unique [in RIS.tools]
defect_count_remove_defect [in RIS.normalise]
defect_count_spec [in RIS.normalise]
defect_count_disj [in RIS.normalise]
determinise_Reachables [in RIS.automata]
determinise_lang [in RIS.automata]
divide_by_open_spec [in RIS.factors]
DMg1 [in RIS.algebra]
DMg2 [in RIS.algebra]
DNg [in RIS.algebra]
Dyn_eq [in RIS.normalise]
d_binding_simpl [in RIS.words]
d_binding_prod [in RIS.words]
D1 [in RIS.algebra]
D2 [in RIS.algebra]

E

elements_act_lists [in RIS.atoms]
elements_inv_act [in RIS.atoms]
elements_inv_eq [in RIS.atoms]
elements_app [in RIS.atoms]
elements_inv_act_atom [in RIS.atoms]
elim_var_solutions [in RIS.systems]
eqReprb_spec [in RIS.representative]
equal_list_spec [in RIS.tools]
equivalentb_spec [in RIS.tools]
equiv_alt [in RIS.alternate_eq]
equiv_id [in RIS.completenessKA]
equiv_perm_trans [in RIS.atoms]
equiv_perm_sym [in RIS.atoms]
equiv_perm_refl [in RIS.atoms]
equiv_orbitsb_spec [in RIS.representative]
equiv_orbitsb_eq_shuffle [in RIS.representative]
equiv_dynamic_sequence_eq [in RIS.normalise]
equiv_stacks_bissimilar [in RIS.equiv_stacks]
equiv_stacks_Transitive [in RIS.equiv_stacks]
equiv_stacks_Symmetric [in RIS.equiv_stacks]
equiv_stacks_Accepting [in RIS.equiv_stacks]
equiv_stacks_paired [in RIS.equiv_stacks]
equiv_stacks_Reflexive [in RIS.equiv_stacks]
equiv_stacksb_spec [in RIS.equiv_stacks]
eqX_refl [in RIS.tools]
eqX_false [in RIS.tools]
eqX_correct [in RIS.tools]
eq_lists_orbitX [in RIS.representative]
eq_lists_refl [in RIS.representative]
eq_lists_fst [in RIS.representative]
eq_lists_shuffle [in RIS.representative]
eq_listsb_spec [in RIS.representative]
eq_shuffles [in RIS.tools]
eq_letter_correct [in RIS.words]
eq_lang_incl_sem [in RIS.equiv_stacks]
exact_solution_ext [in RIS.systems]
exact_solution_is_weak_solution [in RIS.systems]
exists_var_binding [in RIS.aeq_facts]
explore_spec [in RIS.systems]
explore_Some [in RIS.systems]
explore_None [in RIS.systems]
ExprVar_ext [in RIS.systems]
E1 [in RIS.algebra]
E2 [in RIS.algebra]

F

factors_open_balanced [in RIS.factors]
factors_size [in RIS.factors]
factors_In [in RIS.factors]
factors_prod [in RIS.factors]
Factors_spec [in RIS.factors]
factor_perm [in RIS.atoms]
filter_nil [in RIS.tools]
filter_NoDup [in RIS.tools]
filter_true [in RIS.tools]
filter_ext [in RIS.tools]
filter_ext_In [in RIS.tools]
filter_map [in RIS.tools]
filter_length_eq [in RIS.tools]
filter_length [in RIS.tools]
filter_app [in RIS.tools]
find_matching_close [in RIS.aeq_facts]
first_defect_Sn [in RIS.normalise]
flip_proj2 [in RIS.tools]
flip_proj1 [in RIS.tools]
flip_app [in RIS.tools]
flip_involutive [in RIS.tools]
fold_star_prodList [in RIS.regexp]
forallb_ext [in RIS.tools]
forallb_ext_In [in RIS.tools]
forallb_false_exists [in RIS.tools]
forall_existsb [in RIS.tools]
free_relational_interpretation [in RIS.normalise]
freshExprB_freshExpr [in RIS.alphaKA]
freshExpr_bindFin [in RIS.alphaKA]
fresh_lang [in RIS.alpha_regexp]
fundamental_theorem [in RIS.regexp]
F1 [in RIS.algebra]
F2 [in RIS.algebra]

G

get_terms [in RIS.completenessKA]
group_by_fst_act [in RIS.atoms]
group_by_fst_map_In [in RIS.tools]
group_by_fst_map_supp [in RIS.tools]
group_by_fst_In [in RIS.tools]
group_by_fst_length [in RIS.tools]
G1 [in RIS.algebra]
G2 [in RIS.algebra]

H

has_support_supported [in RIS.tools]
hide_close [in RIS.normalise]
homogeneous_𝐇 [in RIS.binding_finite]
homogeneous_prod [in RIS.binding_finite]
homogeneous_alt [in RIS.binding_finite]
homogeneous_is_binding_finite [in RIS.binding_finite]
H1 [in RIS.algebra]
H2 [in RIS.algebra]

I

idem_fold_star [in RIS.regexp]
Idm1 [in RIS.algebra]
Idm2 [in RIS.algebra]
image_app_Accepting [in RIS.transducer]
image_spec [in RIS.stacks]
inb_dec [in RIS.tools]
inb_false [in RIS.tools]
inb_spec [in RIS.tools]
inclb_correct [in RIS.tools]
incl_cons_disj' [in RIS.tools]
incl_cons_disj [in RIS.tools]
incl_split [in RIS.tools]
incl_app_split [in RIS.tools]
incl_app_or [in RIS.tools]
incl_nil [in RIS.tools]
incl_map [in RIS.tools]
incl_sem_w [in RIS.equiv_stacks]
inf_system [in RIS.systems]
inf_join_inf [in RIS.algebra]
inf_cup_right [in RIS.algebra]
inf_cup_left [in RIS.algebra]
injective_support_closed [in RIS.tools]
inject_regexp_to_expr [in RIS.completenessKA]
inject_equiv [in RIS.representative]
inject_equivariant [in RIS.representative]
inject_support [in RIS.representative]
inject_injection [in RIS.representative]
inject_orbitb [in RIS.representative]
inject_orbit [in RIS.representative]
insert_map [in RIS.tools]
insert_spec [in RIS.tools]
intersect_univ [in RIS.systems]
intersect_right [in RIS.systems]
intersect_left [in RIS.systems]
inverse_app [in RIS.atoms]
inverse_comp_r [in RIS.atoms]
inverse_comp_l [in RIS.atoms]
inverse_inv [in RIS.atoms]
In_support_list [in RIS.atoms]
In_act_lists [in RIS.atoms]
In_Tr_not_open_balanced [in RIS.traces]
In_shuffles [in RIS.tools]
in_cons_iff [in RIS.tools]
In_undup [in RIS.tools]
In_dec [in RIS.tools]
In_flip [in RIS.tools]
in_concat [in RIS.tools]
In_OpenVar [in RIS.alphaKA]
In_δA_stateSpace_incl [in RIS.regexp]
is_orbitb_orbitX [in RIS.representative]
is_orbit_orbitX [in RIS.representative]
is_orbitb_act [in RIS.representative]
is_orbit_act [in RIS.representative]
is_orbitb_spec [in RIS.representative]
is_binding_finite_act [in RIS.binding_finite]
is_binding_finite_Σ [in RIS.binding_finite]
is_binding_finite_memory_bound [in RIS.binding_finite]
is_binding_finite_memory_finite [in RIS.binding_finite]
is_binding_finite_bindings [in RIS.binding_finite]
is_valid_close [in RIS.normalise]
is_valid_var [in RIS.normalise]
is_valid_open [in RIS.normalise]
is_binding_finite_ax_inf [in RIS.alphaKA]
is_binding_finite_ax_eq [in RIS.alphaKA]
iter_lang_last [in RIS.language]
I1 [in RIS.algebra]
I2 [in RIS.algebra]

J

join_list_zero [in RIS.regexp]
join_list_equivalent_ACI0 [in RIS.regexp]
join_list_equivalent [in RIS.regexp]
join_list_right_distr [in RIS.regexp]
join_list_left_distr [in RIS.regexp]
join_list_add [in RIS.regexp]
join_list_monotone [in RIS.regexp]
join_list_app [in RIS.regexp]
J1 [in RIS.algebra]
J2 [in RIS.algebra]

K

KA_act [in RIS.alpha_regexp]
KA_regexp_to_expr [in RIS.completenessKA]
ka_zero_star [in RIS.algebra]
ka_star_mid_split [in RIS.algebra]
ka_star_unfold_right [in RIS.algebra]
ka_star_star [in RIS.algebra]
ka_star_dup [in RIS.algebra]
ka_star_unfold_eq [in RIS.algebra]
KA_αKA_inf [in RIS.alphaKA]
KA_αKA [in RIS.alphaKA]
KA_ACI0 [in RIS.regexp]
KleeneTheorem [in RIS.automata]
K1 [in RIS.algebra]
K2 [in RIS.algebra]

L

langSys_inf_sol [in RIS.systems]
lang_close_automaton [in RIS.closed_automaton]
least_solution_Antimirov [in RIS.systems]
least_solution_exists [in RIS.systems]
least_solution_is_exact [in RIS.systems]
least_solution_ext [in RIS.systems]
length_sum_filter [in RIS.tools]
length_app_tail [in RIS.tools]
length_app [in RIS.tools]
len_rev_induction [in RIS.tools]
len_induction [in RIS.tools]
Levi [in RIS.tools]
Levi_strict [in RIS.tools]
lift_perm_invisible [in RIS.representative]
lift_perm_inverse [in RIS.representative]
lift_f [in RIS.representative]
lift_prod_spec [in RIS.tools]
lists_of_length_spec [in RIS.tools]
loop_spec [in RIS.systems]
lower_bound_zero [in RIS.systems]
lower_bound_ext [in RIS.systems]
lower_squares_size [in RIS.factors]
lower_squares_prod [in RIS.factors]
lower_squares_alt [in RIS.factors]
lower_squares_spec [in RIS.factors]
L1 [in RIS.algebra]
L2 [in RIS.algebra]

M

make_perm_id [in RIS.bijection]
make_bij [in RIS.bijection]
make_perm_spec [in RIS.bijection]
mapRel_add [in RIS.tools]
mapRel_unique [in RIS.tools]
mapRel_app [in RIS.tools]
mapRel_nil [in RIS.tools]
map_expr_ax_eq [in RIS.completenessKA]
map_injective_injective [in RIS.tools]
map_undup_inj [in RIS.tools]
map_undup_id [in RIS.tools]
map_eq_equivalent [in RIS.tools]
map_ext_in_iff [in RIS.tools]
map_bij [in RIS.tools]
map_eq_id [in RIS.tools]
map_app_inverse [in RIS.tools]
match_defect_first_defect [in RIS.normalise]
match_defect_at_Sn [in RIS.normalise]
match_defect_at_n_spec [in RIS.normalise]
match_defect_match_defectb [in RIS.normalise]
match_defectb_spec [in RIS.normalise]
maxBind_lists [in RIS.factors]
maxBind_square [in RIS.factors]
maxBind_square_disj [in RIS.factors]
maxBind_idem [in RIS.factors]
maxBind_comm [in RIS.factors]
maxBind_assoc [in RIS.factors]
maxBind_neutral [in RIS.factors]
MaxBind_lift_prod [in RIS.binding_finite]
MaxBind_In [in RIS.binding_finite]
MaxBind_sizeAt [in RIS.binding_finite]
MaxBind_fresh_Pref [in RIS.binding_finite]
MaxBind_le [in RIS.binding_finite]
MaxBind_lub [in RIS.binding_finite]
MaxBind_cons [in RIS.binding_finite]
MaxBind_filter [in RIS.binding_finite]
MaxBind_fresh [in RIS.binding_finite]
MaxBind_app [in RIS.binding_finite]
memory_bound [in RIS.binding_finite]
memory_bound_aux [in RIS.binding_finite]
minimal_support [in RIS.atoms]
minimal_cl_α [in RIS.closed_languages]
minimal_support_eq [in RIS.nominalsetoid]
min_occ_app [in RIS.transducer]
mixp_absent [in RIS.transducer]
mixp_app [in RIS.transducer]
mixp_cons [in RIS.transducer]
mixp_snd_bis [in RIS.transducer]
mixp_snd [in RIS.transducer]
mixp_fst [in RIS.transducer]
mix_app [in RIS.tools]
mix_snd [in RIS.tools]
mix_fst [in RIS.tools]

N

nb_act [in RIS.atoms]
nb_map [in RIS.tools]
nb_cons_eq [in RIS.tools]
nb_cons_neq [in RIS.tools]
nb_inv_nil [in RIS.tools]
nb_not_In [in RIS.tools]
nb_In [in RIS.tools]
nb_nil [in RIS.tools]
nb_count_occ [in RIS.tools]
NFA_of_regexp_spec [in RIS.automata]
NFA_of_regexp_langNFA [in RIS.automata]
nf_supp_inj [in RIS.representative]
nf_supp_action [in RIS.representative]
nf_supp_nodup [in RIS.representative]
nf_supp_support [in RIS.representative]
nil_or_last [in RIS.tools]
nil_prod_lang [in RIS.regexp]
NoDupb_NoDup [in RIS.tools]
NoDup_act [in RIS.atoms]
NoDup_shuffles [in RIS.tools]
NoDup_map_injective [in RIS.tools]
NoDup_nb' [in RIS.tools]
NoDup_nb [in RIS.tools]
NoDup_length [in RIS.tools]
NoDup_rev [in RIS.tools]
NoDup_undup_eq [in RIS.tools]
NoDup_undup [in RIS.tools]
NoDup_app [in RIS.tools]
NoDup_app_inv [in RIS.tools]
NoDup_remove_3 [in RIS.tools]
nom_δt [in RIS.transducer]
nom_compatible [in RIS.transducer]
nom_path [in RIS.transducer]
nom_step [in RIS.transducer]
normalise_spec [in RIS.normalise]
normal_form [in RIS.normalise]
not_nil_add [in RIS.tools]
no_var_no_fun [in RIS.completenessKA]

O

one_inf_star [in RIS.algebra]
open_balanced_no_open [in RIS.words]
open_balanced_perm [in RIS.words]
open_balanced_suffix [in RIS.words]
orbitX_perm [in RIS.representative]
orbitX_inj [in RIS.representative]
orbit_eq [in RIS.representative]
orb_prop_iff [in RIS.tools]

P

pad_contents [in RIS.tools]
pairedb_app_Accepting [in RIS.transducer]
pairedb_spec [in RIS.stacks]
paired_perm [in RIS.stacks]
paired_inj [in RIS.stacks]
paired_rmfst [in RIS.stacks]
paired_cons [in RIS.stacks]
paired_mix [in RIS.stacks]
paired_flip [in RIS.stacks]
paired_app [in RIS.stacks]
paired_Accepting [in RIS.stacks]
pairs_spec [in RIS.tools]
partitionb_spec [in RIS.representative]
partition_act [in RIS.representative]
pathNFA_stateSpace [in RIS.automata]
pathNFA_last [in RIS.automata]
pathNFA_app [in RIS.automata]
pathRestr_split [in RIS.automata]
pathRestr_incl [in RIS.automata]
pathRestr_app [in RIS.automata]
pathRestr_pathNFA [in RIS.automata]
path_αequiv [in RIS.transducer]
path_stack_decompose [in RIS.transducer]
path_stack_decompose_aux [in RIS.transducer]
path_app [in RIS.transducer]
path_det [in RIS.transducer]
path_mix [in RIS.transducer]
path_sym [in RIS.transducer]
path_app_Accepting [in RIS.transducer]
path_letter [in RIS.transducer]
path_decompose_app [in RIS.transducer]
path_length_word [in RIS.transducer]
path_id [in RIS.transducer]
path_id_compatible [in RIS.transducer]
path_id_Accepting [in RIS.transducer]
path_single_letter [in RIS.transducer]
path_support [in RIS.closed_automaton]
path_Tr [in RIS.traces]
path_init_refl_pair [in RIS.aeq_facts]
path_init_pair [in RIS.aeq_facts]
permutations_elements [in RIS.bijection]
permutations_image [in RIS.bijection]
permutations_spec [in RIS.bijection]
perm_path_mixp [in RIS.transducer]
perm_p_pinv_eq_nil [in RIS.atoms]
perm_pinv_p_eq_nil [in RIS.atoms]
perm_a_a_eq_nil [in RIS.atoms]
perm_bij [in RIS.atoms]
perm_inj [in RIS.atoms]
perm_comm_pair [in RIS.alphaKA]
positive_act [in RIS.alpha_regexp]
positive_star [in RIS.positive_regexp]
positive_inf [in RIS.positive_regexp]
positive_KA_inf [in RIS.positive_regexp]
positive_KA [in RIS.positive_regexp]
positive_lang [in RIS.positive_regexp]
positive_αKA_inf [in RIS.alphaKA]
positive_αKA [in RIS.alphaKA]
prefixes_support [in RIS.alpha_regexp]
prefixes_spec [in RIS.regexp]
product_square_close_balanced [in RIS.factors]
product_Δ [in RIS.tools]
product_assoc [in RIS.tools]
prod_binding_maxBind [in RIS.factors]
prod_assoc [in RIS.words]
prod_unit_l [in RIS.words]
prod_unit_r [in RIS.words]
proj_length [in RIS.tools]
proj1_act [in RIS.atoms]
proj2_act [in RIS.atoms]

R

Reachables_spec [in RIS.automata]
red_def_equiv [in RIS.normalise]
red_def_defect_count [in RIS.normalise]
red_def_valid [in RIS.normalise]
refactor [in RIS.algebra]
reform [in RIS.atoms]
regexpPath [in RIS.automata]
regexp_to_regex'_lang [in RIS.completenessKA]
regexp_to_regex'_id [in RIS.completenessKA]
regex'_to_regexp_lang [in RIS.completenessKA]
regex'_to_regexp_id [in RIS.completenessKA]
remove_defect_equiv [in RIS.normalise]
remove_defect_valid [in RIS.normalise]
repr_word_equiv [in RIS.normalise]
repr_word_binding [in RIS.normalise]
repr_word_support [in RIS.normalise]
repr_word_perm [in RIS.normalise]
repr_word_injective [in RIS.normalise]
repr_letter_binding [in RIS.normalise]
repr_letter_support [in RIS.normalise]
repr_letter_equivariant [in RIS.normalise]
repr_letter_injective [in RIS.normalise]
restrict_eq [in RIS.closed_languages]
restrict_inf_bis [in RIS.closed_languages]
restrict_inf [in RIS.closed_languages]
rev_equivalent [in RIS.tools]
rev_induction [in RIS.tools]
rmfstn_decr [in RIS.traces]
rmfstn_rmfst [in RIS.traces]
rmfstn_in [in RIS.traces]
rmfstn_notin [in RIS.traces]
rmfst_perm [in RIS.atoms]
rmfst_app_dec_stacks [in RIS.stacks]
rmfst_paired [in RIS.stacks]
rmfst_present [in RIS.stacks]
rmfst_absent [in RIS.stacks]
rmfst_flip [in RIS.tools]
rmfst_app_dec [in RIS.tools]
rmfst_comm [in RIS.tools]
rmfst_decr [in RIS.tools]
rmfst_in [in RIS.tools]
rmfst_notin [in RIS.tools]
rm_notin [in RIS.tools]
rm_equiv [in RIS.tools]
rm_In [in RIS.tools]

S

same_orbitb_spec [in RIS.representative]
same_orbit_get_perm [in RIS.representative]
scope_binding [in RIS.aeq_facts]
select_spec [in RIS.traces]
Shift_bound [in RIS.normalise]
Shift_bound_lt [in RIS.normalise]
Shift_free [in RIS.normalise]
shift_bound_lt [in RIS.normalise]
shift_bound_gt [in RIS.normalise]
shift_bound_n [in RIS.normalise]
shift_free [in RIS.normalise]
shuffles_map [in RIS.tools]
shuffles_length [in RIS.tools]
shuffles_nodup [in RIS.tools]
shuffles_equiv [in RIS.tools]
shuffles_spec [in RIS.tools]
shuffles_act [in RIS.bijection]
similar_equiv_stacks [in RIS.equiv_stacks]
similar_join [in RIS.regexp]
simulation_language [in RIS.regexp]
sizeAt_fresh [in RIS.alpha_regexp]
sizeExpr_act [in RIS.alpha_regexp]
size_sizeAt [in RIS.alpha_regexp]
size_stack [in RIS.transducer]
size_prod_bound_inf_right [in RIS.words]
size_prod_bound_inf_left [in RIS.words]
size_prod_bound_sup [in RIS.words]
solution_sys_spec [in RIS.systems]
solution_sys_zero [in RIS.systems]
solution_no_var [in RIS.systems]
soundness [in RIS.regexp]
soundness_proof [in RIS.regexp]
spines_homogeneous [in RIS.binding_finite]
spines_split [in RIS.binding_finite]
spines_eq [in RIS.binding_finite]
spines_support [in RIS.alphaKA]
split_app_unambiguous [in RIS.tools]
split_word [in RIS.tools]
split_fst [in RIS.tools]
split_snd [in RIS.tools]
split_star [in RIS.regexp]
sqExpr_Σ [in RIS.binding_finite]
sqExpr_Π [in RIS.binding_finite]
sqExpr_star [in RIS.binding_finite]
sqExpr_add [in RIS.binding_finite]
sqExpr_prod [in RIS.binding_finite]
sqExpr_inf [in RIS.binding_finite]
sqExpr_bindings_finite_star [in RIS.binding_finite]
sqListExpr_Π_In [in RIS.binding_finite]
stack_binding_both [in RIS.transducer]
stack_binding [in RIS.transducer]
stack_binding_subword [in RIS.aeq_facts]
star_switch_side [in RIS.algebra]
star_join [in RIS.algebra]
star_incr [in RIS.algebra]
star_right_ind [in RIS.regexp]
star_left_ind [in RIS.regexp]
statesNFA_path [in RIS.automata]
statesNFA_spec [in RIS.automata]
stateSpace_statesNFA [in RIS.automata]
stateSpace_Var [in RIS.regexp]
stateSpace_trans [in RIS.regexp]
stateSpace_refl [in RIS.regexp]
step_det [in RIS.transducer]
step_mix [in RIS.transducer]
step_sym [in RIS.transducer]
subsets_NoDup [in RIS.tools]
subsets_spec [in RIS.tools]
subsets_In [in RIS.tools]
subword_cons [in RIS.subword]
subword_nil [in RIS.subword]
subword_app_r [in RIS.subword]
subword_length [in RIS.subword]
subword_not_In [in RIS.aeq_facts]
subword_dec_app [in RIS.aeq_facts]
subword_incl [in RIS.aeq_facts]
succ_spec [in RIS.systems]
sum_filter [in RIS.tools]
sum_incr_0_right [in RIS.tools]
sum_incr_0_left [in RIS.tools]
sum_lt [in RIS.tools]
sum_le [in RIS.tools]
sum_zero_in [in RIS.tools]
sum_add_distr [in RIS.tools]
sum_add [in RIS.tools]
sum_ext_In [in RIS.tools]
sum_ext [in RIS.tools]
sum_incr [in RIS.tools]
sum_eq_ND [in RIS.tools]
sum_incl_ND [in RIS.tools]
sum_app [in RIS.tools]
suppoid_app [in RIS.nominalsetoid]
suppoid_cons [in RIS.nominalsetoid]
support_ϵ [in RIS.alpha_regexp]
support_Var [in RIS.alpha_regexp]
support_star [in RIS.alpha_regexp]
support_prod [in RIS.alpha_regexp]
support_join [in RIS.alpha_regexp]
support_lang [in RIS.alpha_regexp]
support_image_equivariant [in RIS.atoms]
support_list_atoms [in RIS.atoms]
support_eq_action_eq [in RIS.atoms]
support_list_cons [in RIS.atoms]
support_list_app [in RIS.atoms]
sys_of_NFA_least_solution [in RIS.systems]
sys_of_NFA_lang [in RIS.systems]
sys_of_NFA_solution [in RIS.systems]

T

test_dyn_seq_spec [in RIS.normalise]
test_valid_spec [in RIS.normalise]
test_valid_true [in RIS.normalise]
test_valid_aux_false_app [in RIS.normalise]
test0_act [in RIS.alpha_regexp]
test0_spines [in RIS.binding_finite]
test0_𝐇 [in RIS.binding_finite]
test0_bindPref [in RIS.binding_finite]
test0_bindings [in RIS.binding_finite]
test0_αKA [in RIS.alphaKA]
test0_δA [in RIS.regexp]
test0_stateSpace [in RIS.regexp]
test0_prefixes [in RIS.regexp]
test0_δ [in RIS.regexp]
test0_test1_false [in RIS.regexp]
test0_ϵ [in RIS.regexp]
test0_KA [in RIS.regexp]
test0_Σ [in RIS.regexp]
test0_spec [in RIS.regexp]
test0_false [in RIS.regexp]
test1_spec [in RIS.regexp]
to_sigma [in RIS.completenessKA]
to_nat [in RIS.completenessKA]
to_expr_id [in RIS.completenessKA]
to_perm_correct [in RIS.bijection]
transitions_from_spec [in RIS.closed_automaton]
Trn_path_fst [in RIS.traces]
Trn_path_snd [in RIS.traces]
Trn_d_binding [in RIS.traces]
Trn_c_binding [in RIS.traces]
Trn_incr [in RIS.traces]
Trn_open [in RIS.traces]
Trn_In_length [in RIS.traces]
Trn_Tr [in RIS.traces]
Trn_add [in RIS.traces]
Trn_aux_Trn [in RIS.traces]
Trn_aux_fst [in RIS.traces]
Trn_aux_app [in RIS.traces]
Trn_aux_add [in RIS.traces]
Tr_path [in RIS.traces]
Tr_step [in RIS.traces]
Tr_perm [in RIS.traces]
Tr_close_balanced [in RIS.traces]
Tr_support [in RIS.traces]
Tr_length_binding_atom [in RIS.traces]
Tr_add [in RIS.traces]
Tr_app [in RIS.traces]

U

UId1 [in RIS.algebra]
UId2 [in RIS.algebra]
unbounded_binding [in RIS.binding_finite]
undup_act [in RIS.atoms]
undup_equivalent [in RIS.tools]
undup_length [in RIS.tools]
UNg [in RIS.algebra]
un_star [in RIS.algebra]
updTrn_updTr [in RIS.traces]
updTr_length [in RIS.traces]

V

valid_app [in RIS.normalise]
valid_bound_αfresh [in RIS.normalise]
valid_bound_support_lt [in RIS.normalise]
valid_support_open_explicit [in RIS.normalise]
valid_support_open [in RIS.normalise]
valid_repr_word [in RIS.normalise]
vars_Antimirov [in RIS.systems]
vars_elim [in RIS.systems]
var_perm_app_Accepting [in RIS.transducer]
var_perm'_accepting [in RIS.stacks]
var_perm_accepting [in RIS.stacks]
var_perm_paired [in RIS.stacks]
var_perm'_spec [in RIS.stacks]
var_perm'_None [in RIS.stacks]
var_perm'_Some [in RIS.stacks]
Var_spec [in RIS.regexp]

W

weak_solution_ext [in RIS.systems]
weightExpr_incr_sup_right [in RIS.binding_finite]
weightExpr_incr_sup_left [in RIS.binding_finite]
weight_app_right [in RIS.binding_finite]
weight_app_left [in RIS.binding_finite]
weight_app [in RIS.binding_finite]
weight_incr_sup [in RIS.binding_finite]
witness_nodup [in RIS.systems]
witness_incl [in RIS.systems]
witness_dup [in RIS.systems]
witness_app [in RIS.systems]
witness_spec [in RIS.systems]
w_equiv_stacks [in RIS.equiv_stacks]
w_path [in RIS.equiv_stacks]

X

X_dec [in RIS.tools]

Z

zero_minimal [in RIS.algebra]

other

Δ_product [in RIS.tools]
Π_lang [in RIS.regexp]
Σ_act [in RIS.alpha_regexp]
Σ_support [in RIS.alpha_regexp]
Σ_bounded [in RIS.algebra]
Σ_bigger [in RIS.algebra]
Σ_incl [in RIS.algebra]
Σ_app [in RIS.algebra]
Σ_distr_r [in RIS.algebra]
Σ_distr_l [in RIS.algebra]
Σ_map_app [in RIS.alphaKA]
Σ_map_equiv_α [in RIS.alphaKA]
Σ_bounded_α [in RIS.alphaKA]
Σ_map_equiv [in RIS.regexp]
Σ_map_concat [in RIS.regexp]
Σ_incl0 [in RIS.regexp]
Σ_app [in RIS.regexp]
Σ_lang [in RIS.regexp]
αequiv_to_αequiv2 [in RIS.alternate_eq]
αequiv_alternate [in RIS.alternate_eq]
αequiv_αfresh_transpose [in RIS.transducer]
αequiv_path [in RIS.transducer]
αequiv_perm [in RIS.words]
αequiv_binding [in RIS.words]
αequiv_length [in RIS.words]
αequiv_app_right [in RIS.words]
αequiv_app_left [in RIS.words]
αequiv'_perm [in RIS.alternate_eq]
αequiv'_binding [in RIS.alternate_eq]
αequiv'_app_right [in RIS.alternate_eq]
αequiv'_app_left [in RIS.alternate_eq]
αequiv2_to_αequiv [in RIS.alternate_eq]
αfresh_perm_path_nil [in RIS.transducer]
αfresh_perm_path [in RIS.transducer]
αfresh_close_split_unique [in RIS.words]
αfresh_open_split [in RIS.words]
αfresh_close_split [in RIS.words]
αfresh_support [in RIS.words]
αfresh_letter [in RIS.words]
αfresh_perm [in RIS.words]
αfresh_alt [in RIS.alphaKA]
αKA_inf_act [in RIS.alphaKA]
αKA_act [in RIS.alphaKA]
αKA_lang_inf [in RIS.alphaKA]
αKA_lang [in RIS.alphaKA]
δA_proper_KA [in RIS.systems]
δA_stateSpace [in RIS.regexp]
δt_flip [in RIS.transducer]
δt_app_Accepting [in RIS.transducer]
δt_app [in RIS.transducer]
δt_path [in RIS.transducer]
δt_compatible_spec [in RIS.transducer]
δ_act [in RIS.alpha_regexp]
δ_proper_αKA_not_open_inf [in RIS.alphaKA]
δ_proper_αKA_not_open [in RIS.alphaKA]
δ_support [in RIS.alphaKA]
δ_binFin [in RIS.alphaKA]
δ_inf_e_α [in RIS.alphaKA]
δ_words_last [in RIS.regexp]
δ_words_lang [in RIS.regexp]
δ_words_add [in RIS.regexp]
δ_words_zero [in RIS.regexp]
δ_prod [in RIS.regexp]
δ_proper_KA_inf [in RIS.regexp]
δ_proper_KA [in RIS.regexp]
δ_Σ [in RIS.regexp]
δ_inf_e [in RIS.regexp]
δ_lang [in RIS.regexp]
η_support [in RIS.representative]
η_equivariant [in RIS.representative]
η_inj [in RIS.representative]
ρ_spec [in RIS.normalise]
ϵ_act [in RIS.alpha_regexp]
ϵ_spines [in RIS.binding_finite]
ϵ_𝐇 [in RIS.binding_finite]
ϵ_αKA [in RIS.alphaKA]
ϵ_Σ_zero [in RIS.regexp]
ϵ_Σ_un [in RIS.regexp]
ϵ_KA [in RIS.regexp]
ϵ_idem [in RIS.regexp]
ϵ_prod [in RIS.regexp]
ϵ_add [in RIS.regexp]
ϵ_sub_id [in RIS.regexp]
ϵ_zero [in RIS.regexp]
ϵ_ax_spec [in RIS.regexp]
ϵ_inf_e [in RIS.regexp]
ϵ_spec [in RIS.regexp]
ϵ_zero_or_un [in RIS.regexp]
𝐇_lang [in RIS.binding_finite]
𝐇_eq [in RIS.binding_finite]
𝐇_support [in RIS.alphaKA]
𝗙_perm [in RIS.words]
𝗙_add [in RIS.words]
𝗙_app [in RIS.words]
𝗙_cons [in RIS.words]
𝗙_singl [in RIS.words]
𝗳_perm [in RIS.words]

---

Axiom Index

A

A'_reachable [in RIS.systems]

C

coherent_support [in RIS.representative]

N

nf_supp_shuffle_support [in RIS.representative]
nf_supp [in RIS.representative]

R

R [in RIS.normalise]

other

ϕ [in RIS.normalise]
ϕ_support [in RIS.normalise]
ϕ_equivariant [in RIS.normalise]
ϕ_inj [in RIS.normalise]

---

Constructor Index

A

ACI0_prod_one [in RIS.regexp]
ACI0_add_zero [in RIS.regexp]
ACI0_add_idem [in RIS.regexp]
ACI0_add_comm [in RIS.regexp]
ACI0_add_assoc [in RIS.regexp]
ACI0_prod_assoc [in RIS.regexp]
act [in RIS.atoms]
actoid [in RIS.nominalsetoid]
associative [in RIS.algebra]
atomic [in RIS.regexp]
ax_eq_ax' [in RIS.regexp]
ax_eq_ax [in RIS.regexp]
ax_eq_star [in RIS.regexp]
ax_eq_add [in RIS.regexp]
ax_eq_prod [in RIS.regexp]
ax_eq_trans [in RIS.regexp]
ax_eq_sym [in RIS.regexp]
ax_eq_refl [in RIS.regexp]

B

bound [in RIS.representative]

C

close [in RIS.words]
commutative [in RIS.algebra]

E

equiv [in RIS.tools]
equivariant [in RIS.atoms]
e_star [in RIS.regexp]
e_prod [in RIS.regexp]
e_add [in RIS.regexp]
e_un [in RIS.regexp]
e_zero [in RIS.regexp]

F

free [in RIS.representative]

I

idempotent [in RIS.algebra]

J

join [in RIS.algebra]
join_is_order [in RIS.algebra]

K

KA_star_right_ind [in RIS.regexp]
KA_star_left_ind [in RIS.regexp]
KA_star_unfold [in RIS.regexp]
KA_idem [in RIS.regexp]
KA_right_zero [in RIS.regexp]
KA_left_zero [in RIS.regexp]
KA_un_right [in RIS.regexp]
KA_un_left [in RIS.regexp]
KA_zero [in RIS.regexp]
KA_right_distr [in RIS.regexp]
KA_left_distr [in RIS.regexp]
KA_add_comm [in RIS.regexp]
KA_add_assoc [in RIS.regexp]
KA_prod_assoc [in RIS.regexp]

O

open [in RIS.words]

P

pathl [in RIS.transducer]
pathϵ [in RIS.transducer]
prod [in RIS.algebra]
prog [in RIS.equiv_stacks]
prog2 [in RIS.equiv_stacks]

R

regexp_tt [in RIS.completenessKA]

S

sequiv [in RIS.tools]
simulation_step [in RIS.regexp]
smaller [in RIS.tools]
ssmaller [in RIS.tools]
star [in RIS.algebra]
step [in RIS.normalise]
suppoid [in RIS.nominalsetoid]
support [in RIS.atoms]

T

transition [in RIS.automata]

U

un [in RIS.algebra]

V

var [in RIS.words]

Z

zero [in RIS.algebra]

other

αKA_KA [in RIS.alphaKA]
αKA_αα [in RIS.alphaKA]
αl [in RIS.words]
αl' [in RIS.alternate_eq]
αm [in RIS.alternate_eq]
αr [in RIS.words]
αr' [in RIS.alternate_eq]
αt [in RIS.words]
αt' [in RIS.alternate_eq]
αα [in RIS.words]
αα' [in RIS.alternate_eq]
αα2 [in RIS.alternate_eq]
αε [in RIS.words]
αε' [in RIS.alternate_eq]
αε2 [in RIS.alternate_eq]

---

Inductive Index

A

ACI0 [in RIS.regexp]
Action [in RIS.atoms]
ActionSetoid [in RIS.nominalsetoid]
Associative [in RIS.algebra]
ax_eq [in RIS.regexp]

B

bissim [in RIS.automata]
bissimilar [in RIS.equiv_stacks]

C

Commutative [in RIS.algebra]

E

Equiv [in RIS.tools]
Equivariant [in RIS.atoms]

I

Idempotent [in RIS.algebra]

J

Join [in RIS.algebra]
JoinOrder [in RIS.algebra]

K

KA [in RIS.regexp]
KA' [in RIS.regexp]

L

letter [in RIS.words]

P

path [in RIS.transducer]
pointer [in RIS.representative]
Product [in RIS.algebra]

R

red_def [in RIS.normalise]
regexp [in RIS.regexp]
regexp_unit [in RIS.completenessKA]

S

SemEquiv [in RIS.tools]
SemSmaller [in RIS.tools]
similar [in RIS.equiv_stacks]
similar [in RIS.regexp]
Smaller [in RIS.tools]
Star [in RIS.algebra]
Support [in RIS.atoms]
SupportSetoid [in RIS.nominalsetoid]

U

Un [in RIS.algebra]

Z

Zero [in RIS.algebra]

other

αequiv [in RIS.words]
αequiv' [in RIS.alternate_eq]
αequiv2 [in RIS.alternate_eq]
αKA [in RIS.alphaKA]

---

Projection Index

A

act [in RIS.atoms]
action_compose [in RIS.atoms]
action_invariant [in RIS.atoms]
action_X [in RIS.words]
action_compose_eq [in RIS.nominalsetoid]
action_invariant_eq [in RIS.nominalsetoid]
actoid [in RIS.nominalsetoid]
associative [in RIS.algebra]

B

ba_neg_disj [in RIS.algebra]
ba_neg_conj [in RIS.algebra]
ba_disj_conj [in RIS.algebra]
ba_conj_disj [in RIS.algebra]
ba_false [in RIS.algebra]
ba_true [in RIS.algebra]
ba_disj_comm [in RIS.algebra]
ba_conj_comm [in RIS.algebra]

C

commutative [in RIS.algebra]

D

dec_atom [in RIS.atoms]
dec_X [in RIS.words]

E

equiv [in RIS.tools]
equivariant [in RIS.atoms]
eqX [in RIS.tools]
eqX_eq [in RIS.tools]
eq_act_proper [in RIS.nominalsetoid]
eq_support [in RIS.nominalsetoid]
eq_equivalence [in RIS.nominalsetoid]
exists_fresh [in RIS.atoms]

I

idempotent [in RIS.algebra]
is_supported [in RIS.tools]
is_support [in RIS.tools]
is_surjective [in RIS.tools]
is_injective [in RIS.tools]

J

join [in RIS.algebra]
join_is_order [in RIS.algebra]
join_comm [in RIS.regexp]
join_assoc [in RIS.regexp]
join_idem [in RIS.regexp]

K

ka_star_right_ind [in RIS.algebra]
ka_star_left_ind [in RIS.algebra]
ka_star_unfold [in RIS.algebra]
ka_joinOrder [in RIS.algebra]
ka_idem [in RIS.algebra]
ka_semiring [in RIS.algebra]

L

lat_meet_join [in RIS.algebra]
lat_join_meet [in RIS.algebra]
lat_join_comm [in RIS.algebra]
lat_join_assoc [in RIS.algebra]
lat_meet_comm [in RIS.algebra]
lat_meet_assoc [in RIS.algebra]
lat_idem [in RIS.algebra]
lat_comm [in RIS.algebra]
lat_assoc [in RIS.algebra]
left_absorbing [in RIS.algebra]
left_unit [in RIS.algebra]
left_distr [in RIS.regexp]

M

mon_unit [in RIS.algebra]
mon_assoc [in RIS.algebra]

N

nom_X [in RIS.words]

P

prod [in RIS.algebra]
proper_n [in RIS.algebra]
proper_d [in RIS.algebra]
proper_c [in RIS.algebra]
proper_star [in RIS.algebra]
proper_join [in RIS.algebra]
proper_prod [in RIS.algebra]

R

right_absorbing [in RIS.algebra]
right_unit [in RIS.algebra]
right_distr [in RIS.regexp]

S

semiring_right_distr [in RIS.algebra]
semiring_left_distr [in RIS.algebra]
semiring_zero [in RIS.algebra]
semiring_comm [in RIS.algebra]
semiring_add [in RIS.algebra]
semiring_prod [in RIS.algebra]
sequiv [in RIS.tools]
smaller [in RIS.tools]
ssmaller [in RIS.tools]
star [in RIS.algebra]
suppoid [in RIS.nominalsetoid]
support [in RIS.atoms]
support_action [in RIS.atoms]
support_X [in RIS.words]
support_action_eq [in RIS.nominalsetoid]

U

un [in RIS.algebra]

Z

zero [in RIS.algebra]

---

Section Index

A

algebra [in RIS.algebra]
Antimirov [in RIS.regexp]
automata [in RIS.automata]
automata_system [in RIS.systems]
automata.def [in RIS.automata]

B

bijection [in RIS.bijection]
booleanAlgebra [in RIS.algebra]

C

combine [in RIS.tools]

D

decidable [in RIS.tools]
dec_list [in RIS.tools]

E

eta [in RIS.representative]

F

flip [in RIS.tools]

G

group_by_fst [in RIS.tools]

I

inf_system [in RIS.systems]
intersect [in RIS.systems]

J

joinSemiLattice [in RIS.algebra]

K

ka_facts [in RIS.algebra]
kleeneTheorem [in RIS.automata]

L

lang [in RIS.language]
list [in RIS.nominalsetoid]

M

mix [in RIS.tools]

O

orbits [in RIS.representative]
orbitX [in RIS.representative]

P

perm [in RIS.atoms]
perm.group [in RIS.atoms]
pointers [in RIS.representative]
proof [in RIS.completenessKA]

R

regexp [in RIS.systems]
regexp [in RIS.regexp]
regexp.gen_proofs [in RIS.regexp]
relations [in RIS.tools]

S

s [in RIS.alpha_regexp]
s [in RIS.alternate_eq]
s [in RIS.transducer]
s [in RIS.closed_automaton]
s [in RIS.traces]
s [in RIS.closed_languages]
s [in RIS.stacks]
s [in RIS.representative]
s [in RIS.binding_finite]
s [in RIS.positive_regexp]
s [in RIS.aeq_facts]
s [in RIS.words]
s [in RIS.normalise]
s [in RIS.equiv_stacks]
s [in RIS.alphaKA]
s [in RIS.nominalsetoid]
shuffle [in RIS.tools]
simulation [in RIS.systems]
simulation_expr [in RIS.regexp]
subword [in RIS.subword]
system [in RIS.systems]
system.solutions [in RIS.systems]

---

Instance Index

A

absentb_equivalent [in RIS.stacks]
absent_equivalent [in RIS.stacks]
Action_sum [in RIS.atoms]
Action_option [in RIS.atoms]
action_nat [in RIS.atoms]
action_letter [in RIS.words]
actoid_lists [in RIS.nominalsetoid]
ActOrb [in RIS.representative]
actReg [in RIS.alpha_regexp]
ActRepr [in RIS.representative]
act_pair [in RIS.atoms]
act_lists [in RIS.atoms]
act_atom [in RIS.atoms]
act_pointer [in RIS.representative]
app_sequiv [in RIS.nominalsetoid]
ax_inf_PartialOrder [in RIS.regexp]
ax_inf_PreOrder [in RIS.regexp]
ax_eq_Equivalence [in RIS.regexp]

B

bissimilar_equivalence [in RIS.equiv_stacks]
bissim_equiv [in RIS.automata]
Boolean [in RIS.tools]
BooleanAlgebra_Semiring [in RIS.algebra]
BooleanAlgebra_Join_Monoid [in RIS.algebra]
BooleanAlgebra_Meet_Monoid [in RIS.algebra]
BooleanAlgebra_Meet_Semilattice [in RIS.algebra]
BooleanAlgebra_Join_Semilattice [in RIS.algebra]
BooleanAlgebra_Join_Lattice [in RIS.algebra]

C

cl_α_αeq [in RIS.closed_languages]
cl_α_inf_lang [in RIS.closed_languages]
cl_α_eq_lang [in RIS.closed_languages]
cons_sequiv [in RIS.nominalsetoid]

D

decidable_regexp [in RIS.regexp]
dec_sigma [in RIS.completenessKA]
dec_perm [in RIS.atoms]
dec_list [in RIS.tools]
dec_option [in RIS.tools]
dec_sum [in RIS.tools]
dec_prod [in RIS.tools]
dec_letter [in RIS.words]

E

eqRel [in RIS.tools]
eqRel_Equivalence [in RIS.tools]
eqRepr [in RIS.representative]
equivalent_act [in RIS.atoms]
equivalent_lift_prod_Proper [in RIS.tools]
equivalent_flat_map_Proper [in RIS.tools]
equivalent_rev_Proper [in RIS.tools]
equivalent_cons_Proper [in RIS.tools]
equivalent_app_Proper [in RIS.tools]
equivalent_Equivalence [in RIS.tools]
equiv_perm_act [in RIS.atoms]
equiv_perm_spec [in RIS.atoms]
equiv_perm_app [in RIS.atoms]
equiv_perm_inverse [in RIS.atoms]
equiv_perm_Equivalence [in RIS.atoms]
equiv_perm [in RIS.atoms]
equiv_orbits_Equivalence [in RIS.representative]
equiv_orbits [in RIS.representative]
equiv_stacks_compatible [in RIS.equiv_stacks]
equiv_stacks_δt [in RIS.equiv_stacks]
equiv_stacks_var_perm [in RIS.equiv_stacks]
equiv_stacks_image [in RIS.equiv_stacks]
equiv_stacks_cons [in RIS.equiv_stacks]
equiv_stacks_equivalence [in RIS.equiv_stacks]
equiv_stacks_rmfst [in RIS.equiv_stacks]
equiv_stacks_pairedb [in RIS.equiv_stacks]
equiv_stacks_paired_bis [in RIS.equiv_stacks]
eqX_eq [in RIS.systems]
eq_lang_equiv [in RIS.language]
eq_lang [in RIS.language]
eq_lists_symmetric [in RIS.representative]
eq_lists_trans [in RIS.representative]
eq_sem_equivalence [in RIS.equiv_stacks]
eq_sem [in RIS.equiv_stacks]
eq_act [in RIS.nominalsetoid]
extensional_equality2 [in RIS.tools]
extensional_equality [in RIS.tools]
ext_eq_fold_right [in RIS.tools]
ext_eq_fold_left [in RIS.tools]
ext_eq_filter [in RIS.tools]
ext_eq_sum [in RIS.tools]
ext_eq_map [in RIS.tools]
ext_eq2_Equiv [in RIS.tools]
ext_eq_Equiv [in RIS.tools]

F

filter_equivalent_Proper [in RIS.tools]
filter_incl_Proper [in RIS.tools]

G

goodACI0 [in RIS.regexp]
goodKA [in RIS.regexp]
goodαKA [in RIS.alphaKA]
groupAct_nat [in RIS.atoms]
groupAct_pointer [in RIS.representative]
group_action_letter [in RIS.words]

H

has_support_perm [in RIS.atoms]
has_support_ext_eq [in RIS.tools]

I

IdemSemiRing_Semilattice [in RIS.algebra]
incl_lift_prod_Proper [in RIS.tools]
incl_flat_map_Proper [in RIS.tools]
incl_rev_Proper [in RIS.tools]
incl_cons_Proper [in RIS.tools]
incl_app_Proper [in RIS.tools]
incl_PartialOrder [in RIS.tools]
incl_PreOrder [in RIS.tools]
infRel [in RIS.tools]
infRel_PartialOrder [in RIS.tools]
infRel_PreOrder [in RIS.tools]
inf_lang_iter_lang [in RIS.language]
inf_lang_PartialOrder [in RIS.language]
inf_lang_preorder [in RIS.language]
inf_lang [in RIS.language]
inf_lang_cl_α [in RIS.closed_languages]
inf_sem_partialorder [in RIS.equiv_stacks]
inf_sem_preorder [in RIS.equiv_stacks]
inf_sem [in RIS.equiv_stacks]
injective_perm [in RIS.atoms]
injective_free [in RIS.representative]
injective_ext_eq [in RIS.tools]
In_equivalent_Proper [in RIS.tools]
In_incl_Proper [in RIS.tools]

J

joinLang [in RIS.language]
joinOrderLang [in RIS.language]
joinOrder_ax [in RIS.regexp]
join_semilattice [in RIS.systems]
join_semilattice_Lang [in RIS.language]
join_semilattice [in RIS.algebra]
join_ax_eq [in RIS.regexp]

K

kaX [in RIS.systems]
KA_regexp [in RIS.regexp]

L

lang_KA [in RIS.language]
lang_Semiring [in RIS.language]
length_sequiv [in RIS.nominalsetoid]
leqX_po [in RIS.systems]
leqX_o [in RIS.systems]
le_plus_Proper [in RIS.tools]
lift_equiv [in RIS.representative]
lt_plus_Proper [in RIS.tools]

M

map_equivalent_Proper [in RIS.tools]
map_incl_Proper [in RIS.tools]
MaxBind_equiv [in RIS.binding_finite]

N

NatNum [in RIS.tools]
nominalReg [in RIS.alpha_regexp]
NominalSetoid_list [in RIS.nominalsetoid]
Nominal_sum [in RIS.atoms]
Nominal_option [in RIS.atoms]
Nominal_Pair [in RIS.atoms]
Nominal_list [in RIS.atoms]
Nominal_Atom [in RIS.atoms]
Nominal_orbit_base [in RIS.representative]
NomOrbit [in RIS.representative]
NomSetRepr [in RIS.representative]

P

prodLang [in RIS.language]
product_infRel [in RIS.tools]
product_eqRel [in RIS.tools]
prod_ax_inf [in RIS.regexp]
prod_ax_eq [in RIS.regexp]
proper_starLang [in RIS.language]
proper_prodLang [in RIS.language]
proper_joinLang [in RIS.language]
proper_star_inf [in RIS.algebra]
proper_prod_inf [in RIS.algebra]
proper_join_eq [in RIS.algebra]
proper_join_inf [in RIS.algebra]

R

regexp_laws [in RIS.completenessKA]
regJoin [in RIS.regexp]
regProduct [in RIS.regexp]
regStar [in RIS.regexp]
regUn [in RIS.regexp]
regZero [in RIS.regexp]
relseq [in RIS.normalise]
restrict_inclLists [in RIS.closed_languages]
restrict_eqLists [in RIS.closed_languages]
rm_incl_Proper [in RIS.tools]
rm_equivalent_Proper [in RIS.tools]

S

same_orbit_Equivalence [in RIS.representative]
SemEquiv_listS [in RIS.nominalsetoid]
Semilattice_KA [in RIS.regexp]
Semilattice_ax [in RIS.regexp]
starLang [in RIS.language]
star_ax_eq [in RIS.regexp]
subword_app [in RIS.subword]
subword_PartialOrder [in RIS.subword]
subword_leq_length [in RIS.subword]
subword_PreOrder [in RIS.subword]
subword_cons_Proper [in RIS.subword]
subword_app [in RIS.aeq_facts]
subword_map [in RIS.aeq_facts]
subword_filter [in RIS.aeq_facts]
SuppOrbit [in RIS.representative]
SupportAtom [in RIS.atoms]
supported_ext_eq [in RIS.tools]
SupportList [in RIS.atoms]
SupportPair [in RIS.atoms]
SupportSetoidList [in RIS.nominalsetoid]
Support_sum [in RIS.atoms]
Support_option [in RIS.atoms]
support_nat [in RIS.atoms]
support_pointer [in RIS.representative]
support_letter [in RIS.words]
SuppRepr [in RIS.representative]
supReg [in RIS.alpha_regexp]
surjective_perm [in RIS.atoms]
surjective_ext_eq [in RIS.tools]

U

undup_equivalent_Proper [in RIS.tools]
undup_incl_Proper [in RIS.tools]
unLang [in RIS.language]

V

verygoodKA [in RIS.regexp]
verygoodαKA [in RIS.alphaKA]

W

wequiv [in RIS.words]

Z

zeroLang [in RIS.language]

other

Σ_equivalent [in RIS.algebra]
Σ_equivalent [in RIS.regexp]
αequiv_app [in RIS.words]
αequiv_equivalence [in RIS.words]
αequiv'_app [in RIS.alternate_eq]
αequiv'_equivalence [in RIS.alternate_eq]
αKA_KleeneAlgebra [in RIS.alphaKA]
ϵ_proper_inf [in RIS.regexp]
ϵ_proper [in RIS.regexp]
𝐏 [in RIS.representative]

---

Abbreviation Index

E

E [in RIS.completenessKA]
E [in RIS.regexp]

I

index [in RIS.representative]
index [in RIS.representative]

N

nb [in RIS.tools]
nb [in RIS.tools]

P

prj1 [in RIS.tools]
prj2 [in RIS.tools]

R

Regexp [in RIS.closed_automaton]
Regexp [in RIS.positive_regexp]
Regexp [in RIS.alphaKA]
rel [in RIS.representative]
rel [in RIS.representative]

W

W [in RIS.normalise]

---

Definition Index

A

absent [in RIS.stacks]
absentb [in RIS.stacks]
app_dyn [in RIS.normalise]
ax_inf [in RIS.regexp]

B

balanced [in RIS.words]
balExpr [in RIS.alphaKA]
balExprB [in RIS.alphaKA]
bindFinList [in RIS.binding_finite]
bindings [in RIS.binding_finite]
binding_finite [in RIS.binding_finite]
bindPref [in RIS.binding_finite]
Bindupto [in RIS.factors]
bounded_stack [in RIS.closed_automaton]

C

closed_automaton [in RIS.closed_automaton]
close_balanced [in RIS.words]
cl_α [in RIS.closed_languages]
compatible [in RIS.transducer]
cst [in RIS.systems]
cst_leq [in RIS.systems]
c_binding [in RIS.words]

D

defect_count [in RIS.normalise]
determinise [in RIS.automata]
DFA [in RIS.automata]
divide_by_open [in RIS.factors]
Dyn [in RIS.normalise]
dynamic_sequence [in RIS.normalise]
d_binding [in RIS.words]

E

elements [in RIS.atoms]
elim_var [in RIS.systems]
Empt [in RIS.regexp]
eqReprb [in RIS.representative]
equal_list [in RIS.tools]
equate [in RIS.systems]
equivalent [in RIS.tools]
equivalentb [in RIS.tools]
equiv_orbitsb [in RIS.representative]
equiv_stacksb [in RIS.equiv_stacks]
equiv_stacks [in RIS.equiv_stacks]
eqX [in RIS.systems]
eq_listsb [in RIS.representative]
eq_lists [in RIS.representative]
eq_letter [in RIS.words]
eq_regexp [in RIS.regexp]
eq_regexp [in RIS.regexp]
exact_solution [in RIS.systems]
explore [in RIS.systems]
ExprVar [in RIS.systems]

F

factors [in RIS.factors]
Factors [in RIS.factors]
first_defect [in RIS.normalise]
flip [in RIS.tools]
freshExpr [in RIS.alphaKA]
freshExprB [in RIS.alphaKA]
fresh__α [in RIS.words]

G

group_by_fst [in RIS.tools]

H

hide [in RIS.normalise]
homogeneous [in RIS.binding_finite]

I

image [in RIS.stacks]
inb [in RIS.tools]
inclb [in RIS.tools]
inf_join_inf [in RIS.systems]
inf_cup_right [in RIS.systems]
inf_cup_left [in RIS.systems]
inject [in RIS.completenessKA]
inject [in RIS.representative]
inject_aux [in RIS.representative]
insert [in RIS.tools]
intersect [in RIS.systems]
inverse [in RIS.atoms]
is_square [in RIS.factors]
is_orbitb [in RIS.representative]
is_orbit [in RIS.representative]
is_binding_finite [in RIS.binding_finite]
iter [in RIS.normalise]
iter_lang [in RIS.language]
iter_auto [in RIS.automata]

J

Join [in RIS.systems]
join_list [in RIS.regexp]

L

lang [in RIS.equiv_stacks]
langDFA [in RIS.automata]
langNFA [in RIS.automata]
langSys [in RIS.systems]
language [in RIS.language]
lat_ops [in RIS.completenessKA]
least_solution [in RIS.systems]
leqX [in RIS.systems]
letter_map [in RIS.words]
lift [in RIS.representative]
lift_prod [in RIS.tools]
lists_of_length [in RIS.tools]
loop [in RIS.systems]
lower_bound [in RIS.systems]
lower_squares [in RIS.factors]

M

make_perm [in RIS.bijection]
mapRel [in RIS.tools]
map_expr [in RIS.completenessKA]
match_defect_at_n [in RIS.normalise]
match_defectb [in RIS.normalise]
match_defect [in RIS.normalise]
maxBind [in RIS.factors]
MaxBind [in RIS.binding_finite]
min_occ [in RIS.transducer]
mix [in RIS.tools]
mixp [in RIS.transducer]
mon_neg [in RIS.completenessKA]
mon_itr [in RIS.completenessKA]
mon_star [in RIS.completenessKA]
mon_un [in RIS.completenessKA]
mon_prod [in RIS.completenessKA]

N

NFA [in RIS.automata]
NFA_of_regexp [in RIS.automata]
NoDupb [in RIS.tools]
normalise [in RIS.normalise]

O

OpenVar [in RIS.alphaKA]
open_balanced [in RIS.words]
orbit [in RIS.representative]
orbitX [in RIS.representative]
orbitX_aux [in RIS.representative]
orbit_base [in RIS.representative]

P

pad [in RIS.tools]
paired [in RIS.stacks]
pairedb [in RIS.stacks]
pairs [in RIS.tools]
partition [in RIS.representative]
partitionb [in RIS.representative]
pathNFA [in RIS.automata]
pathRestr [in RIS.automata]
pathSys [in RIS.systems]
perm [in RIS.atoms]
permutations [in RIS.bijection]
positive [in RIS.positive_regexp]
prefixes [in RIS.regexp]
product [in RIS.tools]
prod_binding [in RIS.words]
proper_join_inf [in RIS.systems]

R

rational [in RIS.automata]
Reachables [in RIS.automata]
regexp_to_expr [in RIS.completenessKA]
regexp_to_regex' [in RIS.completenessKA]
regex'_to_regexp [in RIS.completenessKA]
regular [in RIS.automata]
reg_lang [in RIS.regexp]
remove_defect [in RIS.normalise]
remove_defect_aux [in RIS.normalise]
Repr [in RIS.representative]
repr_letter [in RIS.normalise]
restrict [in RIS.closed_languages]
rm [in RIS.tools]
rmfst [in RIS.tools]
rmfstn [in RIS.traces]

S

same_orbitb [in RIS.representative]
same_orbit [in RIS.representative]
select [in RIS.traces]
semantics [in RIS.equiv_stacks]
semeq_list [in RIS.nominalsetoid]
Shift [in RIS.normalise]
shift [in RIS.normalise]
shuffles [in RIS.tools]
size [in RIS.words]
sizeAt [in RIS.alpha_regexp]
sizeExpr [in RIS.regexp]
sizeSys [in RIS.systems]
solution_sys [in RIS.systems]
spines [in RIS.binding_finite]
sqExpr [in RIS.binding_finite]
sqListExpr [in RIS.binding_finite]
square [in RIS.factors]
stack [in RIS.stacks]
statesNFA [in RIS.automata]
stateSpace [in RIS.regexp]
state_space [in RIS.closed_automaton]
step [in RIS.transducer]
subsets [in RIS.tools]
subword [in RIS.subword]
succ [in RIS.systems]
sum [in RIS.tools]
supp_letter [in RIS.words]
system [in RIS.systems]
system_homomorphism [in RIS.systems]
sys_of_NFA [in RIS.systems]

T

test_dyn_seq [in RIS.normalise]
test_valid [in RIS.normalise]
test_valid_aux [in RIS.normalise]
test_var [in RIS.normalise]
test0 [in RIS.regexp]
test1 [in RIS.regexp]
Tr [in RIS.traces]
transitions_from [in RIS.closed_automaton]
Trn [in RIS.traces]
Trn_aux [in RIS.traces]

U

undup [in RIS.tools]
updTr [in RIS.traces]
updTrn [in RIS.traces]

V

valid [in RIS.normalise]
valid_close [in RIS.normalise]
valid_var [in RIS.normalise]
valid_open [in RIS.normalise]
Var [in RIS.regexp]
vars_system [in RIS.systems]
var_leq [in RIS.systems]
var_perm' [in RIS.stacks]
var_perm [in RIS.stacks]
vector [in RIS.systems]

W

weak_solution [in RIS.systems]
weight [in RIS.binding_finite]
weightExpr [in RIS.binding_finite]
witness [in RIS.systems]
word [in RIS.words]
w1 [in RIS.equiv_stacks]
w2 [in RIS.equiv_stacks]

other

Δ [in RIS.tools]
Π [in RIS.regexp]
Σ [in RIS.algebra]
α_closed [in RIS.closed_languages]
δ [in RIS.regexp]
δA [in RIS.regexp]
δt [in RIS.transducer]
δ_words [in RIS.regexp]
ε [in RIS.words]
η [in RIS.representative]
ρ [in RIS.normalise]
ϵ [in RIS.regexp]
𝐇 [in RIS.binding_finite]
𝐎 [in RIS.normalise]
𝐰 [in RIS.equiv_stacks]
𝖡 [in RIS.words]
𝗙 [in RIS.words]
𝗳 [in RIS.words]

---

Record Index

A

Absorbing [in RIS.algebra]
Action [in RIS.atoms]
ActionSetoid [in RIS.nominalsetoid]
Alphabet [in RIS.words]
Associative [in RIS.algebra]
Atom [in RIS.atoms]

B

BooleanAlgebra [in RIS.algebra]

C

Commutative [in RIS.algebra]

D

decidable_set [in RIS.tools]

E

Equiv [in RIS.tools]
Equivariant [in RIS.atoms]

G

GoodEnoughAxiom [in RIS.regexp]

H

has_support [in RIS.tools]

I

Idempotent [in RIS.algebra]
injective [in RIS.tools]

J

Join [in RIS.algebra]
JoinOrder [in RIS.algebra]

K

KleeneAlgebra [in RIS.algebra]

L

Lattice [in RIS.algebra]

M

Monoid [in RIS.algebra]

N

Nominal [in RIS.atoms]
NominalSetoid [in RIS.nominalsetoid]

P

Product [in RIS.algebra]

S

SemEquiv [in RIS.tools]
Semilattice [in RIS.algebra]
SemiRing [in RIS.algebra]
SemSmaller [in RIS.tools]
Smaller [in RIS.tools]
Star [in RIS.algebra]
Support [in RIS.atoms]
supported [in RIS.tools]
SupportSetoid [in RIS.nominalsetoid]
surjective [in RIS.tools]

U

Un [in RIS.algebra]
Unit [in RIS.algebra]

V

VeryGoodAxioms [in RIS.regexp]

Z

Zero [in RIS.algebra]

---

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

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

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

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

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

(881 entries)

Axiom Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

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

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

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

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

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

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

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

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

(37 entries)

---

This page has been generated by coqdoc