Global Index

B

F

G

H

K

M

O

P

Q

V

X

Y

Z

_

(139 entries)

Lemma Index

B

D

F

G

H

J

K

M

O

P

Q

V

W

X

Y

Z

_

(58 entries)

Constructor Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

T

U

V

W

X

Y

Z

_

(15 entries)

Inductive Index

A

B

C

D

E

F

G

H

J

K

L

M

N

O

P

Q

S

T

U

V

W

X

Y

Z

_

(6 entries)

Definition Index

B

F

G

H

K

M

O

P

Q

V

X

Y

Z

_

(58 entries)

Library Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

S

T

U

V

W

X

Y

Z

_

(2 entries)

Global Index

A

antisymmetric [definition, in rewriting_with_some_implicits_rules]
antisymmetric [definition, in rewriting]
aux [lemma, in rewriting]
aux2 [lemma, in rewriting]

C

cases_union [lemma, in rewriting_with_some_implicits_rules]
cases_union [lemma, in rewriting]
church_rosser [definition, in rewriting]
church_rosser_confluence [lemma, in rewriting]
commutation [definition, in rewriting_with_some_implicits_rules]
commutation [definition, in rewriting]
commutation_bis [definition, in rewriting_with_some_implicits_rules]
commutation_union_aux [lemma, in rewriting_with_some_implicits_rules]
commutation_union_simple [lemma, in rewriting]
composition [definition, in rewriting]
composition [definition, in rewriting_with_some_implicits_rules]
confluence [definition, in rewriting]
confluence [definition, in rewriting_with_some_implicits_rules]
confluence_church_rosser [lemma, in rewriting]
confluence_in [definition, in rewriting]
confluence_in [definition, in rewriting_with_some_implicits_rules]
confluence_normal_form_unicity [lemma, in rewriting]
confluence_normal_form_1 [lemma, in rewriting]
confluence_normal_form_2 [lemma, in rewriting]
confluence_semi_confluence [lemma, in rewriting]
confluence_star_eq_confluence [lemma, in rewriting]
convergent [definition, in rewriting]

D

diamond_property [definition, in rewriting]
diamond_property [definition, in rewriting_with_some_implicits_rules]
diamond_property_in [definition, in rewriting]
diamond_property_in [definition, in rewriting_with_some_implicits_rules]

E

equiv [definition, in rewriting_with_some_implicits_rules]
equiv [definition, in rewriting]
example1 [lemma, in rewriting_with_some_implicits_rules]
example1 [lemma, in rewriting]

I

inclusion_start_eq [lemma, in rewriting]
isNF [definition, in rewriting]
isSN [inductive, in rewriting]
isWN [definition, in rewriting]

J

joinable [definition, in rewriting_with_some_implicits_rules]
joinable [definition, in rewriting]

L

local_confluence [definition, in rewriting]
local_confluence [definition, in rewriting_with_some_implicits_rules]
local_confluence_in [definition, in rewriting]
local_confluence_in [definition, in rewriting_with_some_implicits_rules]
l3 [lemma, in rewriting_with_some_implicits_rules]
l4 [lemma, in rewriting_with_some_implicits_rules]

N

newman [lemma, in rewriting]
newman [lemma, in rewriting_with_some_implicits_rules]
newman_shorter [lemma, in rewriting]
noetherian [definition, in rewriting_with_some_implicits_rules]
noetherian [definition, in rewriting]

R

reduces_to_normal_form [definition, in rewriting]
reflexive [definition, in rewriting_with_some_implicits_rules]
reflexive [definition, in rewriting]
relation [definition, in rewriting_with_some_implicits_rules]
relation [definition, in rewriting]
rewriting [library]
rewriting_with_some_implicits_rules [library]
Rlr [definition, in rewriting_with_some_implicits_rules]
Rlr [definition, in rewriting]
Rlrstar [inductive, in rewriting]
Rlrstar [definition, in rewriting_with_some_implicits_rules]
Rlrstar_cont_eq [constructor, in rewriting]
Rlrstar_cont_R [constructor, in rewriting]
Rlrstar_cont_Rstar [lemma, in rewriting]
Rlrstar_cont_R_rev [constructor, in rewriting]
Rlrstar_induction [constructor, in rewriting]
Rlrstar_symmetry [lemma, in rewriting]
Rn [inductive, in rewriting]
Rn_induction [constructor, in rewriting]
Rn_0 [constructor, in rewriting]
Rn_1 [constructor, in rewriting]
Roreq [definition, in rewriting]
Roreq [definition, in rewriting_with_some_implicits_rules]
Roreq_cases [lemma, in rewriting]
Roreq_cases [lemma, in rewriting_with_some_implicits_rules]
Rplus [inductive, in rewriting]
Rplus_cases [lemma, in rewriting]
Rplus_cont_R [constructor, in rewriting]
Rplus_finite_path_non_null [lemma, in rewriting]
Rplus_induction [constructor, in rewriting]
Rplus_Rstar_Rplus [lemma, in rewriting]
Rplus_R_Rplus [lemma, in rewriting]
Rplus_transitivity [lemma, in rewriting]
Rstar [inductive, in rewriting]
Rstar [inductive, in rewriting_with_some_implicits_rules]
Rstar_cases [lemma, in rewriting_with_some_implicits_rules]
Rstar_cases [lemma, in rewriting]
Rstar_cases_2 [lemma, in rewriting]
Rstar_cont_eq [constructor, in rewriting_with_some_implicits_rules]
Rstar_cont_eq [constructor, in rewriting]
Rstar_cont_ind [constructor, in rewriting_with_some_implicits_rules]
Rstar_cont_R [lemma, in rewriting_with_some_implicits_rules]
Rstar_cont_R [lemma, in rewriting]
Rstar_cont_Rplus [lemma, in rewriting]
Rstar_equality [lemma, in rewriting_with_some_implicits_rules]
Rstar_finite_path [lemma, in rewriting]
Rstar_induction [constructor, in rewriting]
Rstar_R_Rstar [lemma, in rewriting]
Rstar_transitivity [lemma, in rewriting_with_some_implicits_rules]
Rstar_transitivity [lemma, in rewriting]
R_Rstar_Rplus [lemma, in rewriting]
R_R_Rlrstar [lemma, in rewriting]

S

semi_confluence [definition, in rewriting_with_some_implicits_rules]
semi_confluence [definition, in rewriting]
semi_confluence_confluence [lemma, in rewriting]
semi_confluence_in [definition, in rewriting]
semi_confluence_in [definition, in rewriting_with_some_implicits_rules]
SN [definition, in rewriting]
SN_base [constructor, in rewriting]
SN_implies_noetherian [lemma, in rewriting]
SN_induction [constructor, in rewriting]
SN_Rplus_R [lemma, in rewriting]
strong_confluence [definition, in rewriting_with_some_implicits_rules]
strong_confluence [definition, in rewriting]
strong_confluence_confluence [lemma, in rewriting]
strong_confluence_in [definition, in rewriting]
strong_confluence_in [definition, in rewriting_with_some_implicits_rules]
strong_confluence_semi_confluence [lemma, in rewriting]
swappable [definition, in rewriting]
symmetric [definition, in rewriting_with_some_implicits_rules]
symmetric [definition, in rewriting]

T

th4 [lemma, in rewriting_with_some_implicits_rules]
transitive [definition, in rewriting_with_some_implicits_rules]
transitive [definition, in rewriting]

U

union [definition, in rewriting_with_some_implicits_rules]
union [definition, in rewriting]
union_R [lemma, in rewriting]
union_R [lemma, in rewriting_with_some_implicits_rules]
union_Rstar [lemma, in rewriting_with_some_implicits_rules]
union_Rstar [lemma, in rewriting]
union_Rstar_rev [lemma, in rewriting_with_some_implicits_rules]
union_Rstar_rev [lemma, in rewriting]
union_R_rev [lemma, in rewriting_with_some_implicits_rules]
union_R_rev [lemma, in rewriting]
union_star_star_union [lemma, in rewriting]

W

weak_commutation_in [definition, in rewriting]
weak_commutation_in [definition, in rewriting_with_some_implicits_rules]
WN [definition, in rewriting]

Lemma Index

A

aux [in rewriting]
aux2 [in rewriting]

C

cases_union [in rewriting_with_some_implicits_rules]
cases_union [in rewriting]
church_rosser_confluence [in rewriting]
commutation_union_aux [in rewriting_with_some_implicits_rules]
commutation_union_simple [in rewriting]
confluence_church_rosser [in rewriting]
confluence_normal_form_unicity [in rewriting]
confluence_normal_form_1 [in rewriting]
confluence_normal_form_2 [in rewriting]
confluence_semi_confluence [in rewriting]
confluence_star_eq_confluence [in rewriting]

E

example1 [in rewriting_with_some_implicits_rules]
example1 [in rewriting]

I

inclusion_start_eq [in rewriting]

L

l3 [in rewriting_with_some_implicits_rules]
l4 [in rewriting_with_some_implicits_rules]

N

newman [in rewriting]
newman [in rewriting_with_some_implicits_rules]
newman_shorter [in rewriting]

R

Rlrstar_cont_Rstar [in rewriting]
Rlrstar_symmetry [in rewriting]
Roreq_cases [in rewriting]
Roreq_cases [in rewriting_with_some_implicits_rules]
Rplus_cases [in rewriting]
Rplus_finite_path_non_null [in rewriting]
Rplus_Rstar_Rplus [in rewriting]
Rplus_R_Rplus [in rewriting]
Rplus_transitivity [in rewriting]
Rstar_cases [in rewriting_with_some_implicits_rules]
Rstar_cases [in rewriting]
Rstar_cases_2 [in rewriting]
Rstar_cont_R [in rewriting_with_some_implicits_rules]
Rstar_cont_R [in rewriting]
Rstar_cont_Rplus [in rewriting]
Rstar_equality [in rewriting_with_some_implicits_rules]
Rstar_finite_path [in rewriting]
Rstar_R_Rstar [in rewriting]
Rstar_transitivity [in rewriting_with_some_implicits_rules]
Rstar_transitivity [in rewriting]
R_Rstar_Rplus [in rewriting]
R_R_Rlrstar [in rewriting]

S

semi_confluence_confluence [in rewriting]
SN_implies_noetherian [in rewriting]
SN_Rplus_R [in rewriting]
strong_confluence_confluence [in rewriting]
strong_confluence_semi_confluence [in rewriting]

T

th4 [in rewriting_with_some_implicits_rules]

U

union_R [in rewriting]
union_R [in rewriting_with_some_implicits_rules]
union_Rstar [in rewriting_with_some_implicits_rules]
union_Rstar [in rewriting]
union_Rstar_rev [in rewriting_with_some_implicits_rules]
union_Rstar_rev [in rewriting]
union_R_rev [in rewriting_with_some_implicits_rules]
union_R_rev [in rewriting]
union_star_star_union [in rewriting]

Constructor Index

R

Rlrstar_cont_eq [in rewriting]
Rlrstar_cont_R [in rewriting]
Rlrstar_cont_R_rev [in rewriting]
Rlrstar_induction [in rewriting]
Rn_induction [in rewriting]
Rn_0 [in rewriting]
Rn_1 [in rewriting]
Rplus_cont_R [in rewriting]
Rplus_induction [in rewriting]
Rstar_cont_eq [in rewriting_with_some_implicits_rules]
Rstar_cont_eq [in rewriting]
Rstar_cont_ind [in rewriting_with_some_implicits_rules]
Rstar_induction [in rewriting]

S

SN_base [in rewriting]
SN_induction [in rewriting]

Inductive Index

I

isSN [in rewriting]

R

Rlrstar [in rewriting]
Rn [in rewriting]
Rplus [in rewriting]
Rstar [in rewriting]
Rstar [in rewriting_with_some_implicits_rules]

Definition Index

A

antisymmetric [in rewriting_with_some_implicits_rules]
antisymmetric [in rewriting]

C

church_rosser [in rewriting]
commutation [in rewriting_with_some_implicits_rules]
commutation [in rewriting]
commutation_bis [in rewriting_with_some_implicits_rules]
composition [in rewriting]
composition [in rewriting_with_some_implicits_rules]
confluence [in rewriting]
confluence [in rewriting_with_some_implicits_rules]
confluence_in [in rewriting]
confluence_in [in rewriting_with_some_implicits_rules]
convergent [in rewriting]

D

diamond_property [in rewriting]
diamond_property [in rewriting_with_some_implicits_rules]
diamond_property_in [in rewriting]
diamond_property_in [in rewriting_with_some_implicits_rules]

E

equiv [in rewriting_with_some_implicits_rules]
equiv [in rewriting]

I

isNF [in rewriting]
isWN [in rewriting]

J

joinable [in rewriting_with_some_implicits_rules]
joinable [in rewriting]

L

local_confluence [in rewriting]
local_confluence [in rewriting_with_some_implicits_rules]
local_confluence_in [in rewriting]
local_confluence_in [in rewriting_with_some_implicits_rules]

N

noetherian [in rewriting_with_some_implicits_rules]
noetherian [in rewriting]

R

reduces_to_normal_form [in rewriting]
reflexive [in rewriting_with_some_implicits_rules]
reflexive [in rewriting]
relation [in rewriting_with_some_implicits_rules]
relation [in rewriting]
Rlr [in rewriting_with_some_implicits_rules]
Rlr [in rewriting]
Rlrstar [in rewriting_with_some_implicits_rules]
Roreq [in rewriting]
Roreq [in rewriting_with_some_implicits_rules]

S

semi_confluence [in rewriting_with_some_implicits_rules]
semi_confluence [in rewriting]
semi_confluence_in [in rewriting]
semi_confluence_in [in rewriting_with_some_implicits_rules]
SN [in rewriting]
strong_confluence [in rewriting_with_some_implicits_rules]
strong_confluence [in rewriting]
strong_confluence_in [in rewriting]
strong_confluence_in [in rewriting_with_some_implicits_rules]
swappable [in rewriting]
symmetric [in rewriting_with_some_implicits_rules]
symmetric [in rewriting]

T

transitive [in rewriting_with_some_implicits_rules]
transitive [in rewriting]

U

union [in rewriting_with_some_implicits_rules]
union [in rewriting]

W

weak_commutation_in [in rewriting]
weak_commutation_in [in rewriting_with_some_implicits_rules]
WN [in rewriting]

Library Index

R

rewriting
rewriting_with_some_implicits_rules

Global Index

B

F

G

H

K

M

O

P

Q

V

X

Y

Z

_

(139 entries)

Lemma Index

B

D

F

G

H

J

K

M

O

P

Q

V

W

X

Y

Z

_

(58 entries)

Constructor Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

T

U

V

W

X

Y

Z

_

(15 entries)

Inductive Index

A

B

C

D

E

F

G

H

J

K

L

M

N

O

P

Q

S

T

U

V

W

X

Y

Z

_

(6 entries)

Definition Index

B

F

G

H

K

M

O

P

Q

V

X

Y

Z

_

(58 entries)

Library Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

S

T

U

V

W

X

Y

Z

_

(2 entries)

This page has been generated by coqdoc