Global Index

G

J

K

W

X

Y

Z

_

other

(205 entries)

Variable Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

U

V

W

X

Y

Z

_

other

(1 entry)

Library Index

A

B

C

D

E

F

G

H

J

K

M

O

P

Q

R

S

U

V

W

X

Y

Z

_

other

(5 entries)

Constructor Index

A

B

G

H

J

K

M

P

Q

W

X

Y

Z

_

other

(50 entries)

Lemma Index

B

G

J

K

M

O

U

W

X

Y

Z

_

other

(85 entries)

Inductive Index

A

B

F

G

J

K

M

N

P

V

W

X

Y

Z

_

other

(23 entries)

Section Index

A

B

C

D

F

G

H

I

J

K

L

M

O

P

Q

R

S

U

V

W

X

Y

Z

_

other

(3 entries)

Definition Index

E

G

J

K

N

W

X

Y

Z

_

other

(38 entries)

Global Index

A

Appv [definition, in FOUnify.listv_is_in_lv]
arity [definition, in FOUnify.nat_term_eq_quasiterm]
At_last_OK [lemma, in FOUnify.nat_term_eq_quasiterm]
At_last [definition, in FOUnify.nat_term_eq_quasiterm]

B

BC [definition, in FOUnify.nat_term_eq_quasiterm]
BConsArg [definition, in FOUnify.nat_term_eq_quasiterm]
BConsv [definition, in FOUnify.listv_is_in_lv]
BNilv [definition, in FOUnify.listv_is_in_lv]
BRoot [definition, in FOUnify.nat_term_eq_quasiterm]
BV [definition, in FOUnify.nat_term_eq_quasiterm]

C

C [constructor, in FOUnify.nat_term_eq_quasiterm]
clos [inductive, in FOUnify.term_unif]
clos_init [constructor, in FOUnify.term_unif]
ConsArg [constructor, in FOUnify.nat_term_eq_quasiterm]
ConsArg_diff_ConsArg [lemma, in FOUnify.nat_term_eq_quasiterm]
Constr_f_OK [lemma, in FOUnify.nat_term_eq_quasiterm]
Constr_f [definition, in FOUnify.nat_term_eq_quasiterm]
Consv [constructor, in FOUnify.listv_is_in_lv]
cons_nat [constructor, in FOUnify.nat_term_eq_quasiterm]
C_diff_C [lemma, in FOUnify.nat_term_eq_quasiterm]

D

Destrfun [definition, in FOUnify.nat_term_eq_quasiterm]
Destrvar [definition, in FOUnify.nat_term_eq_quasiterm]
Destr1 [definition, in FOUnify.nat_term_eq_quasiterm]
Destr2 [definition, in FOUnify.nat_term_eq_quasiterm]
Diff [lemma, in FOUnify.nat_complements]
DIFFELNB [definition, in FOUnify.term_unif]
diffelnb [inductive, in FOUnify.term_unif]
DIFFELNBor [lemma, in FOUnify.term_unif]
DIFFELNB_st_inclv_le_S [lemma, in FOUnify.term_unif]
DIFFELNB_Consv_n_O [lemma, in FOUnify.term_unif]
DIFFELNB_O [lemma, in FOUnify.term_unif]
DIFFELNB_diffelnb [lemma, in FOUnify.term_unif]
diffelnb_DIFFELNB [lemma, in FOUnify.term_unif]
diffelnb_Consv_n_in [constructor, in FOUnify.term_unif]
diffelnb_Consv_in [constructor, in FOUnify.term_unif]
diffelnb_init [constructor, in FOUnify.term_unif]
dom [definition, in FOUnify.term_unif]

E

elem_subst_init [constructor, in FOUnify.term_unif]
elem_subst [inductive, in FOUnify.term_unif]
eq_quasiterm [section, in FOUnify.nat_term_eq_quasiterm]
eq_restriction_t_s [lemma, in FOUnify.is_in_quasiterm_term_subst]
eq_restriction_s_t [lemma, in FOUnify.is_in_quasiterm_term_subst]
exi_REMOVE [lemma, in FOUnify.term_unif]

F

Fail_hd6 [constructor, in FOUnify.term_unif]
Fail_hd5 [constructor, in FOUnify.term_unif]
Fail_hd4 [constructor, in FOUnify.term_unif]
Fail_hd3 [constructor, in FOUnify.term_unif]
Fail_hd2 [constructor, in FOUnify.term_unif]
Fail_hd1 [constructor, in FOUnify.term_unif]
fun_eq_decS [lemma, in FOUnify.nat_term_eq_quasiterm]
fun_eq_decP [lemma, in FOUnify.nat_term_eq_quasiterm]
fun_ [definition, in FOUnify.nat_term_eq_quasiterm]

H

Headv [definition, in FOUnify.listv_is_in_lv]
Headv_REMOVE_Consv_Nilv [lemma, in FOUnify.term_unif]
head_diff [inductive, in FOUnify.term_unif]

I

idempotent [definition, in FOUnify.term_unif]
inclv [inductive, in FOUnify.term_unif]
inclv_le [lemma, in FOUnify.term_unif]
inclv_init [constructor, in FOUnify.term_unif]
ind_leP [lemma, in FOUnify.nat_complements]
ind_leS [lemma, in FOUnify.nat_complements]
infv [inductive, in FOUnify.term_unif]
infv_init [constructor, in FOUnify.term_unif]
IS_IN_LV_Appv_IS_IN_LV [lemma, in FOUnify.listv_is_in_lv]
IS_IN_LV_Appv2 [lemma, in FOUnify.listv_is_in_lv]
IS_IN_LV_Appv1 [lemma, in FOUnify.listv_is_in_lv]
IS_IN_LV_decP [lemma, in FOUnify.listv_is_in_lv]
IS_IN_LV_decS [lemma, in FOUnify.listv_is_in_lv]
IS_IN_LV_Consv_Nilv_eq [lemma, in FOUnify.listv_is_in_lv]
IS_IN_LV_n_eq [lemma, in FOUnify.listv_is_in_lv]
IS_IN_LV_is_in_lv [lemma, in FOUnify.listv_is_in_lv]
is_in_lv_IS_IN_LV [lemma, in FOUnify.listv_is_in_lv]
IS_IN_LV [definition, in FOUnify.listv_is_in_lv]
is_in_lv_Consv [constructor, in FOUnify.listv_is_in_lv]
is_in_lv_init [constructor, in FOUnify.listv_is_in_lv]
is_in_lv [inductive, in FOUnify.listv_is_in_lv]
IS_IN_Subst_IS_IN [lemma, in FOUnify.is_in_quasiterm_term_subst]
IS_IN_decP [lemma, in FOUnify.is_in_quasiterm_term_subst]
IS_IN_decS [lemma, in FOUnify.is_in_quasiterm_term_subst]
is_in_IS_IN [lemma, in FOUnify.is_in_quasiterm_term_subst]
IS_IN_is_in [lemma, in FOUnify.is_in_quasiterm_term_subst]
IS_IN [definition, in FOUnify.is_in_quasiterm_term_subst]
is_in_ConsArg2 [constructor, in FOUnify.is_in_quasiterm_term_subst]
is_in_ConsArg1 [constructor, in FOUnify.is_in_quasiterm_term_subst]
is_in_Root [constructor, in FOUnify.is_in_quasiterm_term_subst]
is_in_init [constructor, in FOUnify.is_in_quasiterm_term_subst]
is_in [inductive, in FOUnify.is_in_quasiterm_term_subst]
is_in_quasiterm_term_subst [library]

L

Length [definition, in FOUnify.nat_term_eq_quasiterm]
Length_SO_term [lemma, in FOUnify.nat_term_eq_quasiterm]
Length_n_O [lemma, in FOUnify.nat_term_eq_quasiterm]
less_subst_init [constructor, in FOUnify.term_unif]
less_subst [inductive, in FOUnify.term_unif]
le_S_eqP [lemma, in FOUnify.nat_complements]
le_S_eqS [lemma, in FOUnify.nat_complements]
le_decP [lemma, in FOUnify.nat_complements]
le_decS [lemma, in FOUnify.nat_complements]
listv [inductive, in FOUnify.listv_is_in_lv]
listv_is_in_lv [library]
list_var [definition, in FOUnify.term_unif]
List_queue_nat_OK [lemma, in FOUnify.nat_term_eq_quasiterm]
List_queue_nat [definition, in FOUnify.nat_term_eq_quasiterm]
list_nat [inductive, in FOUnify.nat_term_eq_quasiterm]
L_TERM_decS [lemma, in FOUnify.nat_term_eq_quasiterm]
l_term_L_TERM [lemma, in FOUnify.nat_term_eq_quasiterm]
L_TERM_l_term [lemma, in FOUnify.nat_term_eq_quasiterm]
L_TERM [definition, in FOUnify.nat_term_eq_quasiterm]
l_term_ConsArg [constructor, in FOUnify.nat_term_eq_quasiterm]
l_term_Root [constructor, in FOUnify.nat_term_eq_quasiterm]
l_term_initC [constructor, in FOUnify.nat_term_eq_quasiterm]
l_term_initV [constructor, in FOUnify.nat_term_eq_quasiterm]
l_term [inductive, in FOUnify.nat_term_eq_quasiterm]
L_TERM_term_subst [lemma, in FOUnify.is_in_quasiterm_term_subst]

M

min_unif [definition, in FOUnify.term_unif]

N

nat_caseS [lemma, in FOUnify.nat_complements]
nat_eq_decP [lemma, in FOUnify.nat_complements]
nat_eq_decS [lemma, in FOUnify.nat_complements]
nat_sequence [section, in FOUnify.nat_term_eq_quasiterm]
nat_term_eq_quasiterm [library]
nat_complements [library]
Nilv [constructor, in FOUnify.listv_is_in_lv]
nil_nat [constructor, in FOUnify.nat_term_eq_quasiterm]
n_st_inclv_l_Nilv [lemma, in FOUnify.term_unif]
n_False [lemma, in FOUnify.nat_complements]
n_SO_Length_ConsArg [lemma, in FOUnify.nat_term_eq_quasiterm]
n_IS_IN_Subst [lemma, in FOUnify.is_in_quasiterm_term_subst]

O

OK_List_queue_nat_init [constructor, in FOUnify.nat_term_eq_quasiterm]
OK_List_queue_nat [inductive, in FOUnify.nat_term_eq_quasiterm]
OK_At_last_init [constructor, in FOUnify.nat_term_eq_quasiterm]
OK_At_last [inductive, in FOUnify.nat_term_eq_quasiterm]
OK_Constr_f_init [constructor, in FOUnify.nat_term_eq_quasiterm]
OK_Constr_f [inductive, in FOUnify.nat_term_eq_quasiterm]
over [definition, in FOUnify.term_unif]

P

pred_or [lemma, in FOUnify.nat_complements]
proj_ConsArg2 [lemma, in FOUnify.nat_term_eq_quasiterm]
proj_ConsArg1 [lemma, in FOUnify.nat_term_eq_quasiterm]
proj_Root2 [lemma, in FOUnify.nat_term_eq_quasiterm]
proj_Root1 [lemma, in FOUnify.nat_term_eq_quasiterm]
proj_V [lemma, in FOUnify.nat_term_eq_quasiterm]
proj_C [lemma, in FOUnify.nat_term_eq_quasiterm]
P_S_proof2 [lemma, in FOUnify.nat_complements]
P_S_proof1 [lemma, in FOUnify.nat_complements]
P_S [definition, in FOUnify.nat_complements]

Q

quasisubst [definition, in FOUnify.is_in_quasiterm_term_subst]
quasiterm [inductive, in FOUnify.nat_term_eq_quasiterm]
quasiterm_eq_decP [lemma, in FOUnify.nat_term_eq_quasiterm]
quasiterm_eq_decS [lemma, in FOUnify.nat_term_eq_quasiterm]

R

range [inductive, in FOUnify.term_unif]
range_init [constructor, in FOUnify.term_unif]
REMOVE [definition, in FOUnify.term_unif]
remove [inductive, in FOUnify.term_unif]
REMOVE_n_IS_IN_LV_DIFFELNB_pred [lemma, in FOUnify.term_unif]
REMOVE_n_eq_IS_IN_LV_IS_IN_LV [lemma, in FOUnify.term_unif]
REMOVE_IS_IN_LV_IS_IN_LV [lemma, in FOUnify.term_unif]
REMOVE_Consv_n_eq_Headv [lemma, in FOUnify.term_unif]
REMOVE_Consv_n_eq [lemma, in FOUnify.term_unif]
REMOVE_Consv_eq [lemma, in FOUnify.term_unif]
REMOVE_n_IS_IN_LV_eq [lemma, in FOUnify.term_unif]
REMOVE_remove [lemma, in FOUnify.term_unif]
remove_REMOVE [lemma, in FOUnify.term_unif]
remove_n_eq [constructor, in FOUnify.term_unif]
remove_eq [constructor, in FOUnify.term_unif]
remove_init [constructor, in FOUnify.term_unif]
Root [constructor, in FOUnify.nat_term_eq_quasiterm]
Root_diff_Root [lemma, in FOUnify.nat_term_eq_quasiterm]

S

sig_REMOVE [lemma, in FOUnify.term_unif]
SIMPLE [definition, in FOUnify.nat_term_eq_quasiterm]
SIMPLE_SO [lemma, in FOUnify.nat_term_eq_quasiterm]
SIMPLE_decS [lemma, in FOUnify.nat_term_eq_quasiterm]
SIMPLE_term_subst [lemma, in FOUnify.is_in_quasiterm_term_subst]
st_inclv_Consv_REMOVE_n_IS_IN_LV_st_inclv [lemma, in FOUnify.term_unif]
st_inclv_init [constructor, in FOUnify.term_unif]
st_inclv [inductive, in FOUnify.term_unif]
SUB [definition, in FOUnify.term_unif]
sub [inductive, in FOUnify.term_unif]
subConsArgl [constructor, in FOUnify.term_unif]
subConsArgl2 [constructor, in FOUnify.term_unif]
subConsArgr [constructor, in FOUnify.term_unif]
subConsArgr2 [constructor, in FOUnify.term_unif]
subRoot [constructor, in FOUnify.term_unif]
subRoot2 [constructor, in FOUnify.term_unif]
Subst [definition, in FOUnify.is_in_quasiterm_term_subst]
SUP [definition, in FOUnify.term_unif]

T

Tailv [definition, in FOUnify.listv_is_in_lv]
term [inductive, in FOUnify.nat_term_eq_quasiterm]
terms [section, in FOUnify.nat_term_eq_quasiterm]
terms.list_arity [variable, in FOUnify.nat_term_eq_quasiterm]
term_L_TERM_Length [lemma, in FOUnify.nat_term_eq_quasiterm]
term_decS [lemma, in FOUnify.nat_term_eq_quasiterm]
term_init [constructor, in FOUnify.nat_term_eq_quasiterm]
term_term_subst [lemma, in FOUnify.is_in_quasiterm_term_subst]
term_subst_eq_Length [lemma, in FOUnify.is_in_quasiterm_term_subst]
term_subst_init [constructor, in FOUnify.is_in_quasiterm_term_subst]
term_subst [inductive, in FOUnify.is_in_quasiterm_term_subst]
term_unif [library]

U

under [definition, in FOUnify.term_unif]
unif [definition, in FOUnify.term_unif]
Unification [inductive, in FOUnify.term_unif]
Unif_fail [constructor, in FOUnify.term_unif]
Unif_succeed [constructor, in FOUnify.term_unif]

V

V [constructor, in FOUnify.nat_term_eq_quasiterm]
var [definition, in FOUnify.nat_term_eq_quasiterm]
var_eq_decS [lemma, in FOUnify.nat_term_eq_quasiterm]
var_eq_decP [lemma, in FOUnify.nat_term_eq_quasiterm]
V_diff_V [lemma, in FOUnify.nat_term_eq_quasiterm]

Variable Index

T

terms.list_arity [in FOUnify.nat_term_eq_quasiterm]

Library Index

I

is_in_quasiterm_term_subst

L

N

nat_term_eq_quasiterm
nat_complements

T

Constructor Index

C

C [in FOUnify.nat_term_eq_quasiterm]
clos_init [in FOUnify.term_unif]
ConsArg [in FOUnify.nat_term_eq_quasiterm]
Consv [in FOUnify.listv_is_in_lv]
cons_nat [in FOUnify.nat_term_eq_quasiterm]

D

diffelnb_Consv_n_in [in FOUnify.term_unif]
diffelnb_Consv_in [in FOUnify.term_unif]
diffelnb_init [in FOUnify.term_unif]

E

elem_subst_init [in FOUnify.term_unif]

F

Fail_hd6 [in FOUnify.term_unif]
Fail_hd5 [in FOUnify.term_unif]
Fail_hd4 [in FOUnify.term_unif]
Fail_hd3 [in FOUnify.term_unif]
Fail_hd2 [in FOUnify.term_unif]
Fail_hd1 [in FOUnify.term_unif]

I

inclv_init [in FOUnify.term_unif]
infv_init [in FOUnify.term_unif]
is_in_lv_Consv [in FOUnify.listv_is_in_lv]
is_in_lv_init [in FOUnify.listv_is_in_lv]
is_in_ConsArg2 [in FOUnify.is_in_quasiterm_term_subst]
is_in_ConsArg1 [in FOUnify.is_in_quasiterm_term_subst]
is_in_Root [in FOUnify.is_in_quasiterm_term_subst]
is_in_init [in FOUnify.is_in_quasiterm_term_subst]

L

less_subst_init [in FOUnify.term_unif]
l_term_ConsArg [in FOUnify.nat_term_eq_quasiterm]
l_term_Root [in FOUnify.nat_term_eq_quasiterm]
l_term_initC [in FOUnify.nat_term_eq_quasiterm]
l_term_initV [in FOUnify.nat_term_eq_quasiterm]

N

Nilv [in FOUnify.listv_is_in_lv]
nil_nat [in FOUnify.nat_term_eq_quasiterm]

O

OK_List_queue_nat_init [in FOUnify.nat_term_eq_quasiterm]
OK_At_last_init [in FOUnify.nat_term_eq_quasiterm]
OK_Constr_f_init [in FOUnify.nat_term_eq_quasiterm]

R

range_init [in FOUnify.term_unif]
remove_n_eq [in FOUnify.term_unif]
remove_eq [in FOUnify.term_unif]
remove_init [in FOUnify.term_unif]
Root [in FOUnify.nat_term_eq_quasiterm]

S

st_inclv_init [in FOUnify.term_unif]
subConsArgl [in FOUnify.term_unif]
subConsArgl2 [in FOUnify.term_unif]
subConsArgr [in FOUnify.term_unif]
subConsArgr2 [in FOUnify.term_unif]
subRoot [in FOUnify.term_unif]
subRoot2 [in FOUnify.term_unif]

T

term_init [in FOUnify.nat_term_eq_quasiterm]
term_subst_init [in FOUnify.is_in_quasiterm_term_subst]

U

Unif_fail [in FOUnify.term_unif]
Unif_succeed [in FOUnify.term_unif]

V

V [in FOUnify.nat_term_eq_quasiterm]

Lemma Index

A

At_last_OK [in FOUnify.nat_term_eq_quasiterm]

C

ConsArg_diff_ConsArg [in FOUnify.nat_term_eq_quasiterm]
Constr_f_OK [in FOUnify.nat_term_eq_quasiterm]
C_diff_C [in FOUnify.nat_term_eq_quasiterm]

D

Diff [in FOUnify.nat_complements]
DIFFELNBor [in FOUnify.term_unif]
DIFFELNB_st_inclv_le_S [in FOUnify.term_unif]
DIFFELNB_Consv_n_O [in FOUnify.term_unif]
DIFFELNB_O [in FOUnify.term_unif]
DIFFELNB_diffelnb [in FOUnify.term_unif]
diffelnb_DIFFELNB [in FOUnify.term_unif]

E

eq_restriction_t_s [in FOUnify.is_in_quasiterm_term_subst]
eq_restriction_s_t [in FOUnify.is_in_quasiterm_term_subst]
exi_REMOVE [in FOUnify.term_unif]

F

fun_eq_decS [in FOUnify.nat_term_eq_quasiterm]
fun_eq_decP [in FOUnify.nat_term_eq_quasiterm]

H

Headv_REMOVE_Consv_Nilv [in FOUnify.term_unif]

I

inclv_le [in FOUnify.term_unif]
ind_leP [in FOUnify.nat_complements]
ind_leS [in FOUnify.nat_complements]
IS_IN_LV_Appv_IS_IN_LV [in FOUnify.listv_is_in_lv]
IS_IN_LV_Appv2 [in FOUnify.listv_is_in_lv]
IS_IN_LV_Appv1 [in FOUnify.listv_is_in_lv]
IS_IN_LV_decP [in FOUnify.listv_is_in_lv]
IS_IN_LV_decS [in FOUnify.listv_is_in_lv]
IS_IN_LV_Consv_Nilv_eq [in FOUnify.listv_is_in_lv]
IS_IN_LV_n_eq [in FOUnify.listv_is_in_lv]
IS_IN_LV_is_in_lv [in FOUnify.listv_is_in_lv]
is_in_lv_IS_IN_LV [in FOUnify.listv_is_in_lv]
IS_IN_Subst_IS_IN [in FOUnify.is_in_quasiterm_term_subst]
IS_IN_decP [in FOUnify.is_in_quasiterm_term_subst]
IS_IN_decS [in FOUnify.is_in_quasiterm_term_subst]
is_in_IS_IN [in FOUnify.is_in_quasiterm_term_subst]
IS_IN_is_in [in FOUnify.is_in_quasiterm_term_subst]

L

Length_SO_term [in FOUnify.nat_term_eq_quasiterm]
Length_n_O [in FOUnify.nat_term_eq_quasiterm]
le_S_eqP [in FOUnify.nat_complements]
le_S_eqS [in FOUnify.nat_complements]
le_decP [in FOUnify.nat_complements]
le_decS [in FOUnify.nat_complements]
List_queue_nat_OK [in FOUnify.nat_term_eq_quasiterm]
L_TERM_decS [in FOUnify.nat_term_eq_quasiterm]
l_term_L_TERM [in FOUnify.nat_term_eq_quasiterm]
L_TERM_l_term [in FOUnify.nat_term_eq_quasiterm]
L_TERM_term_subst [in FOUnify.is_in_quasiterm_term_subst]

N

nat_caseS [in FOUnify.nat_complements]
nat_eq_decP [in FOUnify.nat_complements]
nat_eq_decS [in FOUnify.nat_complements]
n_st_inclv_l_Nilv [in FOUnify.term_unif]
n_False [in FOUnify.nat_complements]
n_SO_Length_ConsArg [in FOUnify.nat_term_eq_quasiterm]
n_IS_IN_Subst [in FOUnify.is_in_quasiterm_term_subst]

P

pred_or [in FOUnify.nat_complements]
proj_ConsArg2 [in FOUnify.nat_term_eq_quasiterm]
proj_ConsArg1 [in FOUnify.nat_term_eq_quasiterm]
proj_Root2 [in FOUnify.nat_term_eq_quasiterm]
proj_Root1 [in FOUnify.nat_term_eq_quasiterm]
proj_V [in FOUnify.nat_term_eq_quasiterm]
proj_C [in FOUnify.nat_term_eq_quasiterm]
P_S_proof2 [in FOUnify.nat_complements]
P_S_proof1 [in FOUnify.nat_complements]

Q

quasiterm_eq_decP [in FOUnify.nat_term_eq_quasiterm]
quasiterm_eq_decS [in FOUnify.nat_term_eq_quasiterm]

R

REMOVE_n_IS_IN_LV_DIFFELNB_pred [in FOUnify.term_unif]
REMOVE_n_eq_IS_IN_LV_IS_IN_LV [in FOUnify.term_unif]
REMOVE_IS_IN_LV_IS_IN_LV [in FOUnify.term_unif]
REMOVE_Consv_n_eq_Headv [in FOUnify.term_unif]
REMOVE_Consv_n_eq [in FOUnify.term_unif]
REMOVE_Consv_eq [in FOUnify.term_unif]
REMOVE_n_IS_IN_LV_eq [in FOUnify.term_unif]
REMOVE_remove [in FOUnify.term_unif]
remove_REMOVE [in FOUnify.term_unif]
Root_diff_Root [in FOUnify.nat_term_eq_quasiterm]

S

sig_REMOVE [in FOUnify.term_unif]
SIMPLE_SO [in FOUnify.nat_term_eq_quasiterm]
SIMPLE_decS [in FOUnify.nat_term_eq_quasiterm]
SIMPLE_term_subst [in FOUnify.is_in_quasiterm_term_subst]
st_inclv_Consv_REMOVE_n_IS_IN_LV_st_inclv [in FOUnify.term_unif]

T

term_L_TERM_Length [in FOUnify.nat_term_eq_quasiterm]
term_decS [in FOUnify.nat_term_eq_quasiterm]
term_term_subst [in FOUnify.is_in_quasiterm_term_subst]
term_subst_eq_Length [in FOUnify.is_in_quasiterm_term_subst]

V

var_eq_decS [in FOUnify.nat_term_eq_quasiterm]
var_eq_decP [in FOUnify.nat_term_eq_quasiterm]
V_diff_V [in FOUnify.nat_term_eq_quasiterm]

Inductive Index

C

clos [in FOUnify.term_unif]

D

diffelnb [in FOUnify.term_unif]

E

elem_subst [in FOUnify.term_unif]

H

head_diff [in FOUnify.term_unif]

I

inclv [in FOUnify.term_unif]
infv [in FOUnify.term_unif]
is_in_lv [in FOUnify.listv_is_in_lv]
is_in [in FOUnify.is_in_quasiterm_term_subst]

L

less_subst [in FOUnify.term_unif]
listv [in FOUnify.listv_is_in_lv]
list_nat [in FOUnify.nat_term_eq_quasiterm]
l_term [in FOUnify.nat_term_eq_quasiterm]

O

OK_List_queue_nat [in FOUnify.nat_term_eq_quasiterm]
OK_At_last [in FOUnify.nat_term_eq_quasiterm]
OK_Constr_f [in FOUnify.nat_term_eq_quasiterm]

Q

quasiterm [in FOUnify.nat_term_eq_quasiterm]

R

range [in FOUnify.term_unif]
remove [in FOUnify.term_unif]

S

st_inclv [in FOUnify.term_unif]
sub [in FOUnify.term_unif]

T

term [in FOUnify.nat_term_eq_quasiterm]
term_subst [in FOUnify.is_in_quasiterm_term_subst]

U

Unification [in FOUnify.term_unif]

Section Index

E

eq_quasiterm [in FOUnify.nat_term_eq_quasiterm]

N

nat_sequence [in FOUnify.nat_term_eq_quasiterm]

T

terms [in FOUnify.nat_term_eq_quasiterm]

Definition Index

A

Appv [in FOUnify.listv_is_in_lv]
arity [in FOUnify.nat_term_eq_quasiterm]
At_last [in FOUnify.nat_term_eq_quasiterm]

B

BC [in FOUnify.nat_term_eq_quasiterm]
BConsArg [in FOUnify.nat_term_eq_quasiterm]
BConsv [in FOUnify.listv_is_in_lv]
BNilv [in FOUnify.listv_is_in_lv]
BRoot [in FOUnify.nat_term_eq_quasiterm]
BV [in FOUnify.nat_term_eq_quasiterm]

C

Constr_f [in FOUnify.nat_term_eq_quasiterm]

D

Destrfun [in FOUnify.nat_term_eq_quasiterm]
Destrvar [in FOUnify.nat_term_eq_quasiterm]
Destr1 [in FOUnify.nat_term_eq_quasiterm]
Destr2 [in FOUnify.nat_term_eq_quasiterm]
DIFFELNB [in FOUnify.term_unif]
dom [in FOUnify.term_unif]

F

fun_ [in FOUnify.nat_term_eq_quasiterm]

H

Headv [in FOUnify.listv_is_in_lv]

I

idempotent [in FOUnify.term_unif]
IS_IN_LV [in FOUnify.listv_is_in_lv]
IS_IN [in FOUnify.is_in_quasiterm_term_subst]

L

Length [in FOUnify.nat_term_eq_quasiterm]
list_var [in FOUnify.term_unif]
List_queue_nat [in FOUnify.nat_term_eq_quasiterm]
L_TERM [in FOUnify.nat_term_eq_quasiterm]

M

min_unif [in FOUnify.term_unif]

O

over [in FOUnify.term_unif]

P

P_S [in FOUnify.nat_complements]

Q

quasisubst [in FOUnify.is_in_quasiterm_term_subst]

R

REMOVE [in FOUnify.term_unif]

S

SIMPLE [in FOUnify.nat_term_eq_quasiterm]
SUB [in FOUnify.term_unif]
Subst [in FOUnify.is_in_quasiterm_term_subst]
SUP [in FOUnify.term_unif]

T

Tailv [in FOUnify.listv_is_in_lv]

U

under [in FOUnify.term_unif]
unif [in FOUnify.term_unif]

V

var [in FOUnify.nat_term_eq_quasiterm]

Global Index

G

J

K

W

X

Y

Z

_

other

(205 entries)

Variable Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

U

V

W

X

Y

Z

_

other

(1 entry)

Library Index

A

B

C

D

E

F

G

H

J

K

M

O

P

Q

R

S

U

V

W

X

Y

Z

_

other

(5 entries)

Constructor Index

A

B

G

H

J

K

M

P

Q

W

X

Y

Z

_

other

(50 entries)

Lemma Index

B

G

J

K

M

O

U

W

X

Y

Z

_

other

(85 entries)

Inductive Index

A

B

F

G

J

K

M

N

P

V

W

X

Y

Z

_

other

(23 entries)

Section Index

A

B

C

D

F

G

H

I

J

K

L

M

O

P

Q

R

S

U

V

W

X

Y

Z

_

other

(3 entries)

Definition Index

E

G

J

K

N

W

X

Y

Z

_

other

(38 entries)