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

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

(34 entries)

Module Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

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

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

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

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

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

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

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

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

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

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

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

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

(18 entries)

---

Global Index

A

a [inductive, in Generators]
abstraction [record, in Ergo.Ergo]
Abstractions [section, in Ergo.Ergo]
Abstractions.reifs [variable, in Ergo.Ergo]
Abstractions.ty_env [variable, in Ergo.Ergo]
Abstractions.t_env [variable, in Ergo.Ergo]
Abstractions.v [variable, in Ergo.Ergo]
Abstractions.vm [variable, in Ergo.Ergo]
Abstractions2 [section, in Ergo.Ergo]
Abstractions2.ty_env [variable, in Ergo.Ergo]
Abstractions2.t_env [variable, in Ergo.Ergo]
Abstractions2.v [variable, in Ergo.Ergo]
Abstractions2.vm [variable, in Ergo.Ergo]
Acc_inverse_image [lemma, in Ergo.Lexico]
Acc_lemma [lemma, in Ergo.Lexico]
Acc_incl [lemma, in Ergo.Lexico]
add [definition, in Ergo.Use]
add [definition, in Ergo.Uf]
addk_cancel_embed [lemma, in Ergo.TheoryArith]
add_const_as_addk [lemma, in Ergo.TheoryArith]
add_monome_as_addk [lemma, in Ergo.TheoryArith]
add_as_addk [lemma, in Ergo.TheoryArith]
add_conservative [lemma, in Ergo.Uf]
add_find [lemma, in Ergo.Uf]
add_find_2 [lemma, in Ergo.Uf]
add_find_1 [lemma, in Ergo.Uf]
add_mem_iff [lemma, in Ergo.Uf]
add_mem_3 [lemma, in Ergo.Uf]
add_mem_2 [lemma, in Ergo.Uf]
add_mem_1 [lemma, in Ergo.Uf]
ADEQUATION [module, in Ergo.Adequation]
Adequation [library]
AdequationLazy [module, in Ergo.TacticLazy]
AdequationLazy.adequation [lemma, in Ergo.TacticLazy]
AdequationLazy.Adequation [section, in Ergo.TacticLazy]
AdequationLazy.Adequation.v [variable, in Ergo.TacticLazy]
AdequationLazy.canonical_model [definition, in Ergo.TacticLazy]
AdequationLazy.interp [definition, in Ergo.TacticLazy]
ADEQUATION.adequation [axiom, in Ergo.Adequation]
ADEQUATION.canonical_model [axiom, in Ergo.Adequation]
ADEQUATION.interp [axiom, in Ergo.Adequation]
ADEQUATION.vars [axiom, in Ergo.Adequation]
ainterp [definition, in Ergo.Ergo]
ainterp_is_finterp [lemma, in Ergo.Ergo]
ainterp_eq_is_finterp [lemma, in Ergo.Ergo]
ainterp_eq [definition, in Ergo.Ergo]
all [variable, in Demo]
all [variable, in AltDemo]
allcc [variable, in Demo]
allcc [variable, in AltDemo]
allfull [variable, in Demo]
allfull [variable, in AltDemo]
AllInstances [library]
all_are_true [definition, in Generators]
all_variables_differ [definition, in Generators]
AltDemo [library]
AltErgo [library]
ant [definition, in Generators]
AnyOrderedType [section, in Ergo.Diff]
AnyOrderedType.WithSpecs [section, in Ergo.Diff]
app [constructor, in Ergo.Term]
are_diff_separate_3 [lemma, in Ergo.Diff]
are_diff_separate_2 [lemma, in Ergo.Diff]
are_diff_separate_1 [lemma, in Ergo.Diff]
are_diff_empty [lemma, in Ergo.Diff]
are_diff_m [instance, in Ergo.Diff]
are_diff [definition, in Ergo.Diff]
arithop [inductive, in Ergo.Term]
arithop_equal [definition, in Ergo.Term]
arithop_OT [definition, in Ergo.TermUtils]
arithop_UOT [instance, in Ergo.TermUtils]
arithop_eq_iff [lemma, in Ergo.TermUtils]
ArithTheory [module, in Ergo.TheoryArith]
ArithTheory.Th [definition, in Ergo.TheoryArith]
ArithTheory.ThSpecs [lemma, in Ergo.TheoryArith]
Arith_theory [instance, in Ergo.TheoryArith]
arith_domain [inductive, in Ergo.Term]
arith_domain_OT [definition, in Ergo.TermUtils]
arith_domain_UOT [instance, in Ergo.TermUtils]
arith_domain_eq_iff [lemma, in Ergo.TermUtils]
A1 [lemma, in EinsteinEasy]
A1 [lemma, in EinsteinEasy2]

B

bad_div_cancel [constructor, in Ergo.ModelsRingExt]
bad_opp_cancel [constructor, in Ergo.ModelsRingExt]
bad_1_neutral [constructor, in Ergo.ModelsRingExt]
bad_0_neutral [constructor, in Ergo.ModelsRingExt]
bad_equality [inductive, in Ergo.ModelsRingExt]
bdiscr [lemma, in Ergo.Term]
belim [lemma, in Ergo.SatCaml]
binterp [definition, in Ergo.Ergo]
binterp_is_finterp [lemma, in Ergo.Ergo]
binterp_eq_is_finterp [lemma, in Ergo.Ergo]
binterp_eq [definition, in Ergo.Ergo]
BoolasDT [module, in Ergo.Term]
BoolasDT.eq_dec [definition, in Ergo.Term]
BoolasDT.U [definition, in Ergo.Term]
BoolEqDep [module, in Ergo.Term]

C

cancel_as_addk [lemma, in Ergo.TheoryArith]
canon [projection, in Ergo.Uf]
CanonicalStructure [section, in Ergo.Term]
CanonicalStructure.v [variable, in Ergo.Term]
CanonicalStructure.vtypes [variable, in Ergo.Term]
cardinal_map_le [lemma, in Ergo.Uf]
CCA [module, in Demo]
CCA [module, in Ergo.CCX]
CCE [module, in Demo]
CCE [module, in Ergo.CCX]
CCX [module, in Ergo.CCX]
CCX [library]
CCX_SIG.Specs.query_assumed [axiom, in Ergo.CCX]
CCX_SIG.Specs.query_true [axiom, in Ergo.CCX]
CCX_SIG.Specs.assumed_inconsistent [axiom, in Ergo.CCX]
CCX_SIG.Specs.assumed_assume [axiom, in Ergo.CCX]
CCX_SIG.Specs.assumed_empty [axiom, in Ergo.CCX]
CCX_SIG.Specs [module, in Ergo.CCX]
CCX_SIG.assumed [axiom, in Ergo.CCX]
CCX_SIG.query [axiom, in Ergo.CCX]
CCX_SIG.assume [axiom, in Ergo.CCX]
CCX_SIG.empty [axiom, in Ergo.CCX]
CCX_SIG.t [axiom, in Ergo.CCX]
CCX_SIG [module, in Ergo.CCX]
CCX.assume [definition, in Ergo.CCX]
CCX.assumed [definition, in Ergo.CCX]
CCX.empty [definition, in Ergo.CCX]
CCX.mk_t [constructor, in Ergo.CCX]
CCX.query [definition, in Ergo.CCX]
CCX.RAW [module, in Ergo.CCX]
CCX.Specs [module, in Ergo.CCX]
CCX.Specs.assumed_inconsistent [lemma, in Ergo.CCX]
CCX.Specs.assumed_assume [lemma, in Ergo.CCX]
CCX.Specs.assumed_empty [lemma, in Ergo.CCX]
CCX.Specs.query_assumed [lemma, in Ergo.CCX]
CCX.Specs.query_true [lemma, in Ergo.CCX]
CCX.Specs.this_assume_inc [lemma, in Ergo.CCX]
CCX.Specs.this_assume [lemma, in Ergo.CCX]
CCX.t [definition, in Ergo.CCX]
CCX.this [projection, in Ergo.CCX]
CCX.this_wf [projection, in Ergo.CCX]
CCX.t_ [record, in Ergo.CCX]
chap10 [lemma, in Demo]
chap10 [lemma, in AltDemo]
Chap11 [module, in AltDemo]
Chap11.diamond0 [lemma, in AltDemo]
Chap11.diamond1 [lemma, in AltDemo]
Chap11.diamond2 [lemma, in AltDemo]
Chap11.diamond3 [lemma, in AltDemo]
Chap11.diamond4 [lemma, in AltDemo]
Chap11.diamond5 [lemma, in AltDemo]
Chap11.fdiamond0 [lemma, in AltDemo]
Chap11.fdiamond1 [lemma, in AltDemo]
Chap11.fdiamond2 [lemma, in AltDemo]
Chap11.fdiamond3 [lemma, in AltDemo]
Chap11.fdiamond4 [lemma, in AltDemo]
Chap11.fdiamond5 [lemma, in AltDemo]
Chap11.FiboA0 [lemma, in AltDemo]
Chap11.FiboA1 [lemma, in AltDemo]
Chap11.FiboA10 [lemma, in AltDemo]
Chap11.FiboA15 [lemma, in AltDemo]
Chap11.FiboA2 [lemma, in AltDemo]
Chap11.FiboA20 [lemma, in AltDemo]
Chap11.FiboA5 [lemma, in AltDemo]
Chap11.In_list [lemma, in AltDemo]
Chap11.peirce [lemma, in AltDemo]
Chap11.Zdiamond0 [lemma, in AltDemo]
Chap11.Zdiamond1 [lemma, in AltDemo]
Chap11.Zdiamond2 [lemma, in AltDemo]
Chap11.Zdiamond3 [lemma, in AltDemo]
Chap11.Zdiamond4 [lemma, in AltDemo]
Chap11.Zdiamond5 [lemma, in AltDemo]
Chap11.Zdiamond6 [lemma, in AltDemo]
Chap11.Zdiamond7 [lemma, in AltDemo]
cinterp [definition, in Ergo.DistrNeg]
cmp_terms_spec [lemma, in Ergo.TermUtils]
cmp_term_spec [lemma, in Ergo.TermUtils]
cmp_terms_sym [definition, in Ergo.TermUtils]
cmp_term_sym [definition, in Ergo.TermUtils]
cmp_term_terms_sym [lemma, in Ergo.TermUtils]
cmp_terms_eq [definition, in Ergo.TermUtils]
cmp_term_eq [definition, in Ergo.TermUtils]
cmp_term_terms_eq [lemma, in Ergo.TermUtils]
CNF [module, in Ergo.Cnf]
Cnf [library]
CNFLAZY [module, in Ergo.CNFLazy]
CNFLazy [library]
CNFLAZYCOMMON [module, in Ergo.CNFLazyCommon]
CNFLazyCommon [library]
CNFLAZYCOMMON.clause [abbreviation, in Ergo.CNFLazyCommon]
CNFLAZYCOMMON.clause_OT [definition, in Ergo.CNFLazyCommon]
CNFLAZYCOMMON.cset [abbreviation, in Ergo.CNFLazyCommon]
CNFLAZYCOMMON.formula [definition, in Ergo.CNFLazyCommon]
CNFLAZYCOMMON.L [module, in Ergo.CNFLazyCommon]
CNFLAZYCOMMON.lset [abbreviation, in Ergo.CNFLazyCommon]
CNFLAZYCOMMON.pick [definition, in Ergo.CNFLazyCommon]
CNFLAZYCOMMON.pick_2 [lemma, in Ergo.CNFLazyCommon]
CNFLAZYCOMMON.pick_1 [lemma, in Ergo.CNFLazyCommon]
CNFLAZYCOMMON.Sem [module, in Ergo.CNFLazyCommon]
CNFLAZYN [module, in Ergo.CNFLazyN]
CNFLazyN [library]
CNFLAZYN.and_interp [definition, in Ergo.CNFLazyN]
CNFLAZYN.cfl [definition, in Ergo.CNFLazyN]
CNFLAZYN.cfl_1 [lemma, in Ergo.CNFLazyN]
CNFLAZYN.Conversion [module, in Ergo.CNFLazyN]
CNFLAZYN.Conversion.cnf [lemma, in Ergo.CNFLazyN]
CNFLAZYN.Conversion.mk_form_equiv [lemma, in Ergo.CNFLazyN]
CNFLAZYN.Conversion.mk_or_equiv [lemma, in Ergo.CNFLazyN]
CNFLAZYN.Conversion.mk_and_equiv [lemma, in Ergo.CNFLazyN]
CNFLAZYN.Conversion.mk_not_not [lemma, in Ergo.CNFLazyN]
CNFLAZYN.Conversion.mk_form [definition, in Ergo.CNFLazyN]
CNFLAZYN.Conversion.mk_or_list [definition, in Ergo.CNFLazyN]
CNFLAZYN.Conversion.mk_and_list [definition, in Ergo.CNFLazyN]
CNFLAZYN.Conversion.not_mk_not [lemma, in Ergo.CNFLazyN]
CNFLAZYN.interp [definition, in Ergo.CNFLazyN]
CNFLAZYN.make [definition, in Ergo.CNFLazyN]
CNFLAZYN.make_1 [lemma, in Ergo.CNFLazyN]
CNFLAZYN.mk_iff [definition, in Ergo.CNFLazyN]
CNFLAZYN.mk_iff_ [definition, in Ergo.CNFLazyN]
CNFLAZYN.mk_impl [definition, in Ergo.CNFLazyN]
CNFLAZYN.mk_impl_ [definition, in Ergo.CNFLazyN]
CNFLAZYN.mk_and [definition, in Ergo.CNFLazyN]
CNFLAZYN.mk_and_ [definition, in Ergo.CNFLazyN]
CNFLAZYN.mk_or [definition, in Ergo.CNFLazyN]
CNFLAZYN.mk_or_ [definition, in Ergo.CNFLazyN]
CNFLAZYN.mk_not_size [lemma, in Ergo.CNFLazyN]
CNFLAZYN.mk_false [definition, in Ergo.CNFLazyN]
CNFLAZYN.mk_true [definition, in Ergo.CNFLazyN]
CNFLAZYN.mk_lit [definition, in Ergo.CNFLazyN]
CNFLAZYN.mk_lit_ [definition, in Ergo.CNFLazyN]
CNFLAZYN.or_interp [definition, in Ergo.CNFLazyN]
CNFLAZYN.wf_mk_iff [lemma, in Ergo.CNFLazyN]
CNFLAZYN.wf_mk_impl [lemma, in Ergo.CNFLazyN]
CNFLAZYN.wf_mk_and [lemma, in Ergo.CNFLazyN]
CNFLAZYN.wf_mk_or [lemma, in Ergo.CNFLazyN]
CNFLAZYN.wf_mk_lit [lemma, in Ergo.CNFLazyN]
CNFLAZY_INTERFACE.Conversion.cnf [axiom, in Ergo.CNFLazyCommon]
CNFLAZY_INTERFACE.Conversion.mk_form [axiom, in Ergo.CNFLazyCommon]
CNFLAZY_INTERFACE.Conversion [module, in Ergo.CNFLazyCommon]
CNFLAZY_INTERFACE.interp [definition, in Ergo.CNFLazyCommon]
CNFLAZY_INTERFACE.make_1 [axiom, in Ergo.CNFLazyCommon]
CNFLAZY_INTERFACE [module, in Ergo.CNFLazyCommon]
CNFLAZY.cfl [definition, in Ergo.CNFLazy]
CNFLAZY.cfl_1 [lemma, in Ergo.CNFLazy]
CNFLAZY.Conversion [module, in Ergo.CNFLazy]
CNFLAZY.Conversion.cnf [lemma, in Ergo.CNFLazy]
CNFLAZY.Conversion.mk_form_equiv [lemma, in Ergo.CNFLazy]
CNFLAZY.Conversion.mk_not_not [lemma, in Ergo.CNFLazy]
CNFLAZY.Conversion.mk_form [definition, in Ergo.CNFLazy]
CNFLAZY.Conversion.not_mk_not [lemma, in Ergo.CNFLazy]
CNFLAZY.interp [definition, in Ergo.CNFLazy]
CNFLAZY.make [definition, in Ergo.CNFLazy]
CNFLAZY.make_1 [lemma, in Ergo.CNFLazy]
CNFLAZY.mk_iff [definition, in Ergo.CNFLazy]
CNFLAZY.mk_impl [definition, in Ergo.CNFLazy]
CNFLAZY.mk_and [definition, in Ergo.CNFLazy]
CNFLAZY.mk_or [definition, in Ergo.CNFLazy]
CNFLAZY.mk_not_size [lemma, in Ergo.CNFLazy]
CNFLAZY.mk_false [definition, in Ergo.CNFLazy]
CNFLAZY.mk_true [definition, in Ergo.CNFLazy]
CNFLAZY.mk_lit [definition, in Ergo.CNFLazy]
CNFLAZY.wf_mk_iff [lemma, in Ergo.CNFLazy]
CNFLAZY.wf_mk_impl [lemma, in Ergo.CNFLazy]
CNFLAZY.wf_mk_and [lemma, in Ergo.CNFLazy]
CNFLAZY.wf_mk_or [lemma, in Ergo.CNFLazy]
CNFLAZY.wf_mk_lit [lemma, in Ergo.CNFLazy]
CNFRAW [module, in Ergo.CNFLazy]
CNFRAW.mk_iff [definition, in Ergo.CNFLazy]
CNFRAW.mk_impl [definition, in Ergo.CNFLazy]
CNFRAW.mk_and [definition, in Ergo.CNFLazy]
CNFRAW.mk_or [definition, in Ergo.CNFLazy]
CNFRAW.mk_false [definition, in Ergo.CNFLazy]
CNFRAW.mk_true [definition, in Ergo.CNFLazy]
CNFRAW.mk_lit [definition, in Ergo.CNFLazy]
CNF.cfl [axiom, in Ergo.Cnf]
CNF.cfl_1 [axiom, in Ergo.Cnf]
CNF.clause [abbreviation, in Ergo.Cnf]
CNF.cset [abbreviation, in Ergo.Cnf]
CNF.formula [axiom, in Ergo.Cnf]
CNF.L [module, in Ergo.Cnf]
CNF.lset [abbreviation, in Ergo.Cnf]
CNF.make [axiom, in Ergo.Cnf]
CNF.pick [axiom, in Ergo.Cnf]
CNF.pick_2 [axiom, in Ergo.Cnf]
CNF.pick_1 [axiom, in Ergo.Cnf]
CNF.Sem [module, in Ergo.Cnf]
common_denom_isZp [lemma, in Ergo.TheoryArith]
common_denom_coef [lemma, in Ergo.TheoryArith]
common_denom_nonzero [lemma, in Ergo.TheoryArith]
common_denom [definition, in Ergo.TheoryArith]
compare_list [definition, in Ergo.LLazy]
compare_cst [definition, in Ergo.TermUtils]
Compose [section, in Ergo.DistrNeg]
Compose.A [variable, in Ergo.DistrNeg]
Compose.B [variable, in Ergo.DistrNeg]
Compose.eqA [variable, in Ergo.DistrNeg]
Compose.eqA_trans [variable, in Ergo.DistrNeg]
Compose.eqA_sym [variable, in Ergo.DistrNeg]
Compose.eqA_refl [variable, in Ergo.DistrNeg]
Compose.eqB [variable, in Ergo.DistrNeg]
Compose.eqB_trans [variable, in Ergo.DistrNeg]
Compose.eqB_sym [variable, in Ergo.DistrNeg]
Compose.eqB_refl [variable, in Ergo.DistrNeg]
Compose.f [variable, in Ergo.DistrNeg]
Compose.f_commut [variable, in Ergo.DistrNeg]
Compose.negA [variable, in Ergo.DistrNeg]
Compose.negA_m [variable, in Ergo.DistrNeg]
Compose.negB [variable, in Ergo.DistrNeg]
Compose.negB_m [variable, in Ergo.DistrNeg]
congruent [definition, in Ergo.Uf]
congruent_dec [lemma, in Ergo.Uf]
congruent_false [constructor, in Ergo.Uf]
congruent_true [constructor, in Ergo.Uf]
congruent_spec [inductive, in Ergo.Uf]
CPolynoms [library]
crowded [definition, in Generators]
crowded_aux [definition, in Generators]
crowded_aux_2 [definition, in Generators]
Cst [constructor, in Ergo.Term]
cst_equal [definition, in Ergo.Term]
cst_eq_dep [lemma, in Ergo.TermUtils]

D

DBExample [section, in GeneratorsNG]
DBExample [section, in Generators]
DBExample2 [section, in Generators]
deb1 [definition, in GeneratorsNG]
deb1 [definition, in Generators]
deb1 [lemma, in AltDemo]
deb10 [definition, in GeneratorsNG]
deb10 [definition, in Generators]
deb100 [lemma, in AltDemo]
deb15 [lemma, in AltDemo]
deb2 [definition, in GeneratorsNG]
deb2 [definition, in Generators]
deb2 [lemma, in AltDemo]
deb20 [lemma, in Demo]
deb20 [lemma, in AltDemo]
deb3 [lemma, in AltDemo]
deb4 [lemma, in AltDemo]
deb5 [lemma, in AltDemo]
deb50 [definition, in GeneratorsNG]
deb50 [definition, in Generators]
deb6 [definition, in GeneratorsNG]
deb6 [definition, in Generators]
deb6 [lemma, in AltDemo]
Demo [library]
depvarmap [definition, in Ergo.Term]
de_bruijn [definition, in GeneratorsNG]
de_bruijn [definition, in Generators]
diagProd [definition, in Ergo.DiagProd]
DiagProd [library]
diagProd_subset_m [instance, in Ergo.DiagProd]
diagProd_m [instance, in Ergo.DiagProd]
diagProd_iff [lemma, in Ergo.DiagProd]
diagProd_aux_inv [lemma, in Ergo.DiagProd]
diagProd_aux [definition, in Ergo.DiagProd]
diamond [definition, in GeneratorsEq]
diamond_Zequations [definition, in GeneratorsEq]
diamond_equations [definition, in GeneratorsEq]
Diff [library]
differs [definition, in Generators]
Disequation [constructor, in Ergo.CCX]
DistrNeg [section, in Ergo.DistrNeg]
DistrNeg [library]
DistrNeg.A [variable, in Ergo.DistrNeg]
DistrNeg.neg [variable, in Ergo.DistrNeg]
distr_neg_f [lemma, in Ergo.DistrNeg]
distr_neg_m [lemma, in Ergo.DistrNeg]
distr_neg [definition, in Ergo.DistrNeg]
Div [constructor, in Ergo.Term]
dnc [lemma, in Ergo.DoubleNegUtils]
dnc_or [lemma, in Ergo.DoubleNegUtils]
dnc_and [lemma, in Ergo.DoubleNegUtils]
dom [definition, in Ergo.Term]
DomainDT [module, in Ergo.TermUtils]
DomainDT.eq_dec [lemma, in Ergo.TermUtils]
DomainDT.U [definition, in Ergo.TermUtils]
DomainEqDep [module, in Ergo.TermUtils]
DomainN [constructor, in Ergo.Term]
DomainNat [constructor, in Ergo.Term]
DomainPos [constructor, in Ergo.Term]
DomainQ [constructor, in Ergo.Term]
DomainZ [constructor, in Ergo.Term]
dom_equal [definition, in Ergo.Term]
dom_interp [definition, in Ergo.Term]
DoubleNegUtils [library]
double_not [lemma, in Ergo.DoubleNegUtils]
DPLL [module, in Ergo.Dpll]
Dpll [library]
DPLL.dpll [axiom, in Ergo.Dpll]
DPLL.dpll_correct [axiom, in Ergo.Dpll]
DPLL.E [module, in Ergo.Dpll]
DPLL.Res [inductive, in Ergo.Dpll]
DPLL.Sat [constructor, in Ergo.Dpll]
DPLL.Unsat [constructor, in Ergo.Dpll]
dummy [inductive, in Ergo.Term]

E

E [module, in Ergo.AllInstances]
E [module, in Ergo.AltErgo]
Einstein [section, in EinsteinEasy]
Einstein [section, in EinsteinEasy2]
EinsteinEasy [library]
EinsteinEasy2 [library]
Einstein.Blue [variable, in EinsteinEasy]
Einstein.Blue [variable, in EinsteinEasy2]
Einstein.color [variable, in EinsteinEasy]
Einstein.color [variable, in EinsteinEasy2]
Einstein.color_is_house [variable, in EinsteinEasy]
Einstein.color_2 [variable, in EinsteinEasy]
Einstein.color_is_color [variable, in EinsteinEasy]
Einstein.color_1 [variable, in EinsteinEasy]
Einstein.color_to [variable, in EinsteinEasy]
Einstein.color_of [variable, in EinsteinEasy]
Einstein.color_discr [variable, in EinsteinEasy]
Einstein.color_is_house [variable, in EinsteinEasy2]
Einstein.color_2 [variable, in EinsteinEasy2]
Einstein.color_is_color [variable, in EinsteinEasy2]
Einstein.color_1 [variable, in EinsteinEasy2]
Einstein.color_to [variable, in EinsteinEasy2]
Einstein.color_of [variable, in EinsteinEasy2]
Einstein.color_discr [variable, in EinsteinEasy2]
Einstein.Engineer [variable, in EinsteinEasy]
Einstein.Engineer [variable, in EinsteinEasy2]
Einstein.house_is_house [variable, in EinsteinEasy]
Einstein.house_owner [variable, in EinsteinEasy]
Einstein.house_of [variable, in EinsteinEasy]
Einstein.house_is_house [variable, in EinsteinEasy2]
Einstein.house_owner [variable, in EinsteinEasy2]
Einstein.house_of [variable, in EinsteinEasy2]
Einstein.H1 [variable, in EinsteinEasy]
Einstein.H1 [variable, in EinsteinEasy2]
Einstein.H2 [variable, in EinsteinEasy]
Einstein.H2 [variable, in EinsteinEasy2]
Einstein.H3 [variable, in EinsteinEasy]
Einstein.H3 [variable, in EinsteinEasy2]
Einstein.H4 [variable, in EinsteinEasy]
Einstein.H4 [variable, in EinsteinEasy2]
Einstein.H5 [variable, in EinsteinEasy]
Einstein.H5 [variable, in EinsteinEasy2]
Einstein.MacOS [variable, in EinsteinEasy]
Einstein.MacOS [variable, in EinsteinEasy2]
Einstein.owner_is_person [variable, in EinsteinEasy]
Einstein.owner_house [variable, in EinsteinEasy]
Einstein.owner_of [variable, in EinsteinEasy]
Einstein.owner_is_person [variable, in EinsteinEasy2]
Einstein.owner_house [variable, in EinsteinEasy2]
Einstein.owner_of [variable, in EinsteinEasy2]
Einstein.person [variable, in EinsteinEasy]
Einstein.person [variable, in EinsteinEasy2]
Einstein.person_discr [variable, in EinsteinEasy]
Einstein.person_discr [variable, in EinsteinEasy2]
Einstein.Professor [variable, in EinsteinEasy]
Einstein.Professor [variable, in EinsteinEasy2]
Einstein.Red [variable, in EinsteinEasy]
Einstein.Red [variable, in EinsteinEasy2]
Einstein.Scientist [variable, in EinsteinEasy]
Einstein.Scientist [variable, in EinsteinEasy2]
Einstein.Suse [variable, in EinsteinEasy]
Einstein.Suse [variable, in EinsteinEasy2]
Einstein.system [variable, in EinsteinEasy]
Einstein.system [variable, in EinsteinEasy2]
Einstein.system_is_system [variable, in EinsteinEasy]
Einstein.system_user [variable, in EinsteinEasy]
Einstein.system_of [variable, in EinsteinEasy]
Einstein.system_discr [variable, in EinsteinEasy]
Einstein.system_is_system [variable, in EinsteinEasy2]
Einstein.system_user [variable, in EinsteinEasy2]
Einstein.system_of [variable, in EinsteinEasy2]
Einstein.system_discr [variable, in EinsteinEasy2]
Einstein.Ubuntu [variable, in EinsteinEasy]
Einstein.Ubuntu [variable, in EinsteinEasy2]
Einstein.user_is_user [variable, in EinsteinEasy]
Einstein.user_system [variable, in EinsteinEasy]
Einstein.user_of [variable, in EinsteinEasy]
Einstein.user_is_user [variable, in EinsteinEasy2]
Einstein.user_system [variable, in EinsteinEasy2]
Einstein.user_of [variable, in EinsteinEasy2]
Einstein.White [variable, in EinsteinEasy]
Einstein.White [variable, in EinsteinEasy2]
empty [definition, in Ergo.Use]
empty [definition, in Ergo.Uf]
empty [definition, in Ergo.Diff]
EmptyTheory [module, in Ergo.Theory]
EmptyTheory.Empty_theory_specs [instance, in Ergo.Theory]
EmptyTheory.Empty_theory_implyX [instance, in Ergo.Theory]
EmptyTheory.Empty_theory [instance, in Ergo.Theory]
EmptyTheory.implyX_m [lemma, in Ergo.Theory]
EmptyTheory.Th [definition, in Ergo.Theory]
EmptyTheory.ThSpecs [definition, in Ergo.Theory]
empty_find [lemma, in Ergo.Use]
empty_maps [definition, in Ergo.Ergo]
empty_find [lemma, in Ergo.Uf]
empty_mem [lemma, in Ergo.Uf]
EN [module, in Ergo.AllInstances]
EN [module, in Ergo.AltErgo]
ENV [module, in Ergo.Env]
Env [library]
EnvCC [module, in Demo]
EnvCC [module, in Ergo.AltErgo]
EnvCCA [module, in Demo]
EnvCCA [module, in Ergo.AltErgo]
EnvCCAN [module, in Ergo.AltErgo]
EnvCCN [module, in Ergo.AltErgo]
EnvFacts [module, in Ergo.Env]
EnvFacts.assumed_singleton [lemma, in Ergo.Env]
EnvFacts.query_assume [lemma, in Ergo.Env]
EnvFacts.query_m [lemma, in Ergo.Env]
ENVLAZY [module, in Ergo.EnvLazy]
EnvLazy [library]
ENVLAZY.assume [definition, in Ergo.EnvLazy]
ENVLAZY.assumed [definition, in Ergo.EnvLazy]
ENVLAZY.assumed_inconsistent [lemma, in Ergo.EnvLazy]
ENVLAZY.assumed_assume [lemma, in Ergo.EnvLazy]
ENVLAZY.assumed_oapply [lemma, in Ergo.EnvLazy]
ENVLAZY.assumed_empty [lemma, in Ergo.EnvLazy]
ENVLAZY.Build_t [constructor, in Ergo.EnvLazy]
ENVLAZY.cc [projection, in Ergo.EnvLazy]
ENVLAZY.empty [definition, in Ergo.EnvLazy]
ENVLAZY.env [projection, in Ergo.EnvLazy]
ENVLAZY.filter_elim [lemma, in Ergo.EnvLazy]
ENVLAZY.input_to_lit_lift [lemma, in Ergo.EnvLazy]
ENVLAZY.in_cc_is_no_prop [lemma, in Ergo.EnvLazy]
ENVLAZY.is_prop_m [instance, in Ergo.EnvLazy]
ENVLAZY.is_prop [definition, in Ergo.EnvLazy]
ENVLAZY.lit_to_input_lift [lemma, in Ergo.EnvLazy]
ENVLAZY.oapply [definition, in Ergo.EnvLazy]
ENVLAZY.query [definition, in Ergo.EnvLazy]
ENVLAZY.query_expand [lemma, in Ergo.EnvLazy]
ENVLAZY.query_monotonic [axiom, in Ergo.EnvLazy]
ENVLAZY.query_assumed [lemma, in Ergo.EnvLazy]
ENVLAZY.query_true [lemma, in Ergo.EnvLazy]
ENVLAZY.query_m [lemma, in Ergo.EnvLazy]
ENVLAZY.submodel_eq_submodel [lemma, in Ergo.EnvLazy]
ENVLAZY.t [definition, in Ergo.EnvLazy]
ENVLAZY.t_ [record, in Ergo.EnvLazy]
_ |= _ [notation, in Ergo.EnvLazy]
dom _ [notation, in Ergo.EnvLazy]
EnvSat [module, in Demo]
ENV_INTERFACE.query_expand [axiom, in Ergo.Env]
ENV_INTERFACE.query_monotonic [axiom, in Ergo.Env]
ENV_INTERFACE.query_assumed [axiom, in Ergo.Env]
ENV_INTERFACE.query_true [axiom, in Ergo.Env]
ENV_INTERFACE.query_m [instance, in Ergo.Env]
ENV_INTERFACE.assumed_inconsistent [axiom, in Ergo.Env]
ENV_INTERFACE.assumed_assume [axiom, in Ergo.Env]
ENV_INTERFACE.assumed_empty [axiom, in Ergo.Env]
dom _ [notation, in Ergo.Env]
ENV_INTERFACE.assumed [axiom, in Ergo.Env]
_ |= _ [notation, in Ergo.Env]
ENV_INTERFACE.query [axiom, in Ergo.Env]
ENV_INTERFACE.assume [axiom, in Ergo.Env]
ENV_INTERFACE.empty [axiom, in Ergo.Env]
ENV_INTERFACE.t [axiom, in Ergo.Env]
ENV_INTERFACE [module, in Ergo.Env]
ENV.assume [definition, in Ergo.Env]
ENV.assumed [definition, in Ergo.Env]
ENV.assumed_inconsistent [lemma, in Ergo.Env]
ENV.assumed_assume [lemma, in Ergo.Env]
ENV.assumed_empty [lemma, in Ergo.Env]
ENV.Build_t [constructor, in Ergo.Env]
ENV.empty [definition, in Ergo.Env]
ENV.query [definition, in Ergo.Env]
ENV.query_expand [lemma, in Ergo.Env]
ENV.query_monotonic [lemma, in Ergo.Env]
ENV.query_assumed [lemma, in Ergo.Env]
ENV.query_true [lemma, in Ergo.Env]
ENV.query_m [instance, in Ergo.Env]
ENV.SemF [module, in Ergo.Env]
ENV.t [definition, in Ergo.Env]
ENV.this [projection, in Ergo.Env]
ENV.t_ [record, in Ergo.Env]
ENV.wf [projection, in Ergo.Env]
ENV.wf_add [lemma, in Ergo.Env]
ENV.wf_empty [lemma, in Ergo.Env]
EProps [module, in Ergo.Sat]
EProps [module, in Ergo.FoldProps]
eq [definition, in Ergo.ModelsRingExt]
eq [definition, in Ergo.Term]
equals [definition, in GeneratorsNG]
equals [definition, in Generators]
Equation [constructor, in Ergo.CCX]
EquivExample [section, in Generators]
equivn [definition, in Generators]
equiv_M [lemma, in Ergo.TheoryArith]
equiv1 [definition, in Generators]
equiv10 [definition, in Generators]
equiv2 [definition, in Generators]
equiv30 [definition, in Generators]
eq_integral [lemma, in Ergo.ModelsRingExt]
eq_ring [lemma, in Ergo.ModelsRingExt]
eq_wt_iff [axiom, in Ergo.ModelsRingExt]
eq_congr [definition, in Ergo.ModelsRingExt]
eq_trans [definition, in Ergo.ModelsRingExt]
eq_sym [definition, in Ergo.ModelsRingExt]
eq_refl [definition, in Ergo.ModelsRingExt]
eq_congr [lemma, in Ergo.Term]
eq_terms_trans [lemma, in Ergo.Term]
eq_terms_sym [lemma, in Ergo.Term]
eq_terms_refl [lemma, in Ergo.Term]
eq_terms_cons [constructor, in Ergo.Term]
eq_terms_nil [constructor, in Ergo.Term]
eq_terms [inductive, in Ergo.Term]
eq_trans [lemma, in Ergo.Term]
eq_sym [lemma, in Ergo.Term]
eq_refl [lemma, in Ergo.Term]
Ergo [library]
ErgoCC [module, in Demo]
ErgoCC [module, in Ergo.AltErgo]
ErgoCCA [module, in Demo]
ErgoCCA [module, in Ergo.AltErgo]
ErgoCCAN [module, in Ergo.AltErgo]
ErgoCCN [module, in Ergo.AltErgo]
ErgoE [module, in Ergo.AltErgo]
ErgoEN [module, in Ergo.AltErgo]
ErgoSat [module, in Demo]
everyone_happy [definition, in GeneratorsNG]
everyone_happy_aux [definition, in GeneratorsNG]
everyone_home [definition, in GeneratorsNG]
everyone_home_aux [definition, in GeneratorsNG]
everyone_happy [definition, in Generators]
everyone_happy_aux [definition, in Generators]
everyone_home [definition, in Generators]
everyone_home_aux [definition, in Generators]
Example [section, in GeneratorsNG]
Example [section, in Generators]
Exception [inductive, in Ergo.Env]

F

FAnd [constructor, in Ergo.Ergo]
fdiamond [definition, in GeneratorsEq]
fdiamond_equations [definition, in GeneratorsEq]
FEq [constructor, in Ergo.Ergo]
FExample [section, in Generators]
FFalse [constructor, in Ergo.Ergo]
fform [inductive, in Ergo.Ergo]
fibo [definition, in GeneratorsEq]
fibo_arith [definition, in GeneratorsEq]
fibo_defs [definition, in GeneratorsEq]
FIff [constructor, in Ergo.Ergo]
FImp [constructor, in Ergo.Ergo]
find [definition, in Ergo.Use]
find [definition, in Ergo.Uf]
find_multiple_poly [lemma, in Ergo.TheoryArith]
finterp [definition, in Ergo.Ergo]
FInterp [section, in Ergo.Ergo]
FInterp.ty_env [variable, in Ergo.Ergo]
FInterp.t_env [variable, in Ergo.Ergo]
FInterp.v [variable, in Ergo.Ergo]
FInterp.vm [variable, in Ergo.Ergo]
Fn [definition, in Generators]
FNot [constructor, in Ergo.Ergo]
FoldProps [library]
FOr [constructor, in Ergo.Ergo]
form [inductive, in Ergo.Ergo]
FormSize [section, in Ergo.CNFLazyN]
FormSize.P [variable, in Ergo.CNFLazyN]
form_size_induction [lemma, in Ergo.CNFLazyN]
form_size_pos [lemma, in Ergo.CNFLazyN]
form_size [definition, in Ergo.CNFLazyN]
FP [definition, in AltDemo]
FP13_2_1 [lemma, in AltDemo]
FP13_12_1 [lemma, in AltDemo]
FP13_5_1 [lemma, in AltDemo]
FP13_5_2 [lemma, in AltDemo]
FP13_5_3 [lemma, in AltDemo]
FP13_5_8 [lemma, in AltDemo]
FP25_24_24 [lemma, in AltDemo]
FP25_15_5 [lemma, in AltDemo]
FP25_13_1 [lemma, in AltDemo]
FP25_11_1 [lemma, in AltDemo]
FP25_2_1 [lemma, in AltDemo]
FP5_3_1 [lemma, in AltDemo]
FP9_4_1 [lemma, in AltDemo]
FTrue [constructor, in Ergo.Ergo]
FULL [module, in Ergo.CPolynoms]
FULL.add [definition, in Ergo.CPolynoms]
FULL.addk [definition, in Ergo.CPolynoms]
FULL.addk_co [lemma, in Ergo.CPolynoms]
FULL.addk_equiv [instance, in Ergo.CPolynoms]
FULL.addk_dec [lemma, in Ergo.CPolynoms]
FULL.addk_spec_intro [constructor, in Ergo.CPolynoms]
FULL.addk_spec [inductive, in Ergo.CPolynoms]
FULL.add_co [lemma, in Ergo.CPolynoms]
FULL.add_monome_co [lemma, in Ergo.CPolynoms]
FULL.add_const_co [lemma, in Ergo.CPolynoms]
FULL.add_equiv [instance, in Ergo.CPolynoms]
FULL.add_monome_equiv [instance, in Ergo.CPolynoms]
FULL.add_const_equiv [instance, in Ergo.CPolynoms]
FULL.add_dec [lemma, in Ergo.CPolynoms]
FULL.add_spec_intro [constructor, in Ergo.CPolynoms]
FULL.add_spec [inductive, in Ergo.CPolynoms]
FULL.add_monome_dec [lemma, in Ergo.CPolynoms]
FULL.add_monome_spec_intro [constructor, in Ergo.CPolynoms]
FULL.add_monome_spec [inductive, in Ergo.CPolynoms]
FULL.add_const_dec [lemma, in Ergo.CPolynoms]
FULL.add_const_spec_intro [constructor, in Ergo.CPolynoms]
FULL.add_const_spec [inductive, in Ergo.CPolynoms]
FULL.add_monome [definition, in Ergo.CPolynoms]
FULL.add_const [definition, in Ergo.CPolynoms]
FULL.cancel [definition, in Ergo.CPolynoms]
FULL.cancel_co [lemma, in Ergo.CPolynoms]
FULL.cancel_equiv [instance, in Ergo.CPolynoms]
FULL.cancel_dec [lemma, in Ergo.CPolynoms]
FULL.cancel_spec_intro [constructor, in Ergo.CPolynoms]
FULL.cancel_spec [inductive, in Ergo.CPolynoms]
FULL.choose [definition, in Ergo.CPolynoms]
FULL.choose_dec [lemma, in Ergo.CPolynoms]
FULL.choose_spec_Some [constructor, in Ergo.CPolynoms]
FULL.choose_spec_None [constructor, in Ergo.CPolynoms]
FULL.choose_spec [inductive, in Ergo.CPolynoms]
FULL.choose_equiv [instance, in Ergo.CPolynoms]
FULL.coef_of_equiv [instance, in Ergo.CPolynoms]
FULL.coef_of [definition, in Ergo.CPolynoms]
FULL.div [definition, in Ergo.CPolynoms]
FULL.div_co [lemma, in Ergo.CPolynoms]
FULL.div_equiv [instance, in Ergo.CPolynoms]
FULL.div_dec [lemma, in Ergo.CPolynoms]
FULL.embed [definition, in Ergo.CPolynoms]
FULL.embed_co [lemma, in Ergo.CPolynoms]
FULL.embed_dec [lemma, in Ergo.CPolynoms]
FULL.embed_spec_intro [constructor, in Ergo.CPolynoms]
FULL.embed_spec [inductive, in Ergo.CPolynoms]
FULL.equiv [definition, in Ergo.CPolynoms]
FULL.equiv_Equivalence [instance, in Ergo.CPolynoms]
FULL.extract [definition, in Ergo.CPolynoms]
FULL.extract_embed [lemma, in Ergo.CPolynoms]
FULL.extract_dec [lemma, in Ergo.CPolynoms]
FULL.extract_spec_Some [constructor, in Ergo.CPolynoms]
FULL.extract_spec_None [constructor, in Ergo.CPolynoms]
FULL.extract_spec [inductive, in Ergo.CPolynoms]
FULL.extract_equiv [instance, in Ergo.CPolynoms]
FULL.is_const_dec [lemma, in Ergo.CPolynoms]
FULL.is_const_spec_false [constructor, in Ergo.CPolynoms]
FULL.is_const_spec_true [constructor, in Ergo.CPolynoms]
FULL.is_const_spec [inductive, in Ergo.CPolynoms]
FULL.is_const_equiv [instance, in Ergo.CPolynoms]
FULL.is_const [definition, in Ergo.CPolynoms]
FULL.leaves [definition, in Ergo.CPolynoms]
FULL.leaves_iff [lemma, in Ergo.CPolynoms]
FULL.leaves_equiv [instance, in Ergo.CPolynoms]
FULL.mk_poly [constructor, in Ergo.CPolynoms]
FULL.mult [definition, in Ergo.CPolynoms]
FULL.mult_co [lemma, in Ergo.CPolynoms]
FULL.mult_equiv [instance, in Ergo.CPolynoms]
FULL.mult_dec [lemma, in Ergo.CPolynoms]
FULL.mult_spec_intro [constructor, in Ergo.CPolynoms]
FULL.mult_spec [inductive, in Ergo.CPolynoms]
FULL.poly [record, in Ergo.CPolynoms]
FULL.poly_OT [instance, in Ergo.CPolynoms]
FULL.poly_SOT [instance, in Ergo.CPolynoms]
FULL.Pq [definition, in Ergo.CPolynoms]
FULL.Pq_co [lemma, in Ergo.CPolynoms]
FULL.Pz [definition, in Ergo.CPolynoms]
FULL.Pz_co [lemma, in Ergo.CPolynoms]
FULL.P0 [definition, in Ergo.CPolynoms]
FULL.P0_co [lemma, in Ergo.CPolynoms]
FULL.P1 [definition, in Ergo.CPolynoms]
FULL.P1_co [lemma, in Ergo.CPolynoms]
FULL.reminder [definition, in Ergo.CPolynoms]
FULL.sub [definition, in Ergo.CPolynoms]
FULL.sub_co [lemma, in Ergo.CPolynoms]
FULL.sub_equiv [instance, in Ergo.CPolynoms]
FULL.sub_dec [lemma, in Ergo.CPolynoms]
FULL.sub_spec_intro [constructor, in Ergo.CPolynoms]
FULL.sub_spec [inductive, in Ergo.CPolynoms]
FULL.wf_this [projection, in Ergo.CPolynoms]
FULL.WithVars [section, in Ergo.CPolynoms]
FULL.WithVars.vars [variable, in Ergo.CPolynoms]
FULL._this [projection, in Ergo.CPolynoms]
FVar [constructor, in Ergo.Ergo]
f_m [instance, in Ergo.TheoryArith]
f_idx2 [abbreviation, in Ergo.TheoryArith]
f_idx1 [abbreviation, in Ergo.TheoryArith]
f1 [definition, in Generators]
f10 [definition, in Generators]
f2 [definition, in Generators]
f30 [definition, in Generators]

G

Generators [library]
GeneratorsEq [library]
GeneratorsNG [library]
GenericCongrClosure [module, in Ergo.ModelsRingExt]
GenericCongrClosure.app_rev_fold [lemma, in Ergo.ModelsRingExt]
GenericCongrClosure.collect_paths [lemma, in Ergo.ModelsRingExt]
GenericCongrClosure.Congruence [definition, in Ergo.ModelsRingExt]
GenericCongrClosure.forall2 [definition, in Ergo.ModelsRingExt]
GenericCongrClosure.forall3 [definition, in Ergo.ModelsRingExt]
GenericCongrClosure.linked [definition, in Ergo.ModelsRingExt]
GenericCongrClosure.linked_congr [lemma, in Ergo.ModelsRingExt]
GenericCongrClosure.linked_trans [lemma, in Ergo.ModelsRingExt]
GenericCongrClosure.linked_sym [lemma, in Ergo.ModelsRingExt]
GenericCongrClosure.linked_refl [lemma, in Ergo.ModelsRingExt]
GenericCongrClosure.mext [inductive, in Ergo.ModelsRingExt]
GenericCongrClosure.mext_iff [lemma, in Ergo.ModelsRingExt]
GenericCongrClosure.mext_cons [constructor, in Ergo.ModelsRingExt]
GenericCongrClosure.mext_nil [constructor, in Ergo.ModelsRingExt]
GenericCongrClosure.mext_terms [inductive, in Ergo.ModelsRingExt]
GenericCongrClosure.mext_congr [constructor, in Ergo.ModelsRingExt]
GenericCongrClosure.mext_trans [constructor, in Ergo.ModelsRingExt]
GenericCongrClosure.mext_sym [constructor, in Ergo.ModelsRingExt]
GenericCongrClosure.mext_refl [constructor, in Ergo.ModelsRingExt]
GenericCongrClosure.mext_rule [constructor, in Ergo.ModelsRingExt]
GenericCongrClosure.path [definition, in Ergo.ModelsRingExt]
GenericCongrClosure.plunge_and_flatten_linked [lemma, in Ergo.ModelsRingExt]
GenericCongrClosure.plunge_rel_chain [lemma, in Ergo.ModelsRingExt]
GenericCongrClosure.plunge_and_flatten [definition, in Ergo.ModelsRingExt]
GenericCongrClosure.rel_at_terms_pre [lemma, in Ergo.ModelsRingExt]
GenericCongrClosure.rel_at_sym [lemma, in Ergo.ModelsRingExt]
GenericCongrClosure.rel_chain_singl [lemma, in Ergo.ModelsRingExt]
GenericCongrClosure.rel_chain_app [lemma, in Ergo.ModelsRingExt]
GenericCongrClosure.rel_chain_cons [constructor, in Ergo.ModelsRingExt]
GenericCongrClosure.rel_chain_nil [constructor, in Ergo.ModelsRingExt]
GenericCongrClosure.rel_chain [inductive, in Ergo.ModelsRingExt]
GenericCongrClosure.rel_at_terms_S [constructor, in Ergo.ModelsRingExt]
GenericCongrClosure.rel_at_terms_0 [constructor, in Ergo.ModelsRingExt]
GenericCongrClosure.rel_at_terms [inductive, in Ergo.ModelsRingExt]
GenericCongrClosure.rel_at_next [constructor, in Ergo.ModelsRingExt]
GenericCongrClosure.rel_at_here [constructor, in Ergo.ModelsRingExt]
GenericCongrClosure.rel_at [inductive, in Ergo.ModelsRingExt]
GenericCongrClosure.smallest_closure [lemma, in Ergo.ModelsRingExt]
GenericCongrClosure.WithRelation [section, in Ergo.ModelsRingExt]
GenericCongrClosure.WithRelation.Closure [section, in Ergo.ModelsRingExt]
GenericCongrClosure.WithRelation.Closure.C [variable, in Ergo.ModelsRingExt]
GenericCongrClosure.WithRelation.Closure.C_R [variable, in Ergo.ModelsRingExt]
GenericCongrClosure.WithRelation.Closure.C_congr [variable, in Ergo.ModelsRingExt]
GenericCongrClosure.WithRelation.Closure.C_trans [variable, in Ergo.ModelsRingExt]
GenericCongrClosure.WithRelation.Closure.C_sym [variable, in Ergo.ModelsRingExt]
GenericCongrClosure.WithRelation.Closure.C_refl [variable, in Ergo.ModelsRingExt]
GenericCongrClosure.WithRelation.R [variable, in Ergo.ModelsRingExt]
GenericCongrClosure.WithRelation.R_sym [variable, in Ergo.ModelsRingExt]
g_idx2 [abbreviation, in Ergo.TheoryArith]
g_idx1 [abbreviation, in Ergo.TheoryArith]

H

Ha [projection, in Ergo.Ergo]
has_type_irrelevant [lemma, in Ergo.Term]
has_type_type_of_congr [lemma, in Ergo.Term]
has_type_congr [lemma, in Ergo.Term]
has_type_is_type_of [lemma, in Ergo.Term]
has_type_iff [lemma, in Ergo.Term]
has_type_2 [lemma, in Ergo.Term]
has_type_1 [lemma, in Ergo.Term]
has_type_unfold [lemma, in Ergo.Term]
has_type [definition, in Ergo.Term]
have_type_congr [lemma, in Ergo.Term]
have_type [definition, in Ergo.Term]
Hb [projection, in Ergo.Ergo]
hole [definition, in GeneratorsNG]
hole [definition, in Generators]
HoleWithListVars [section, in GeneratorsNG]
HoleWithListVars.N [variable, in GeneratorsNG]
HoleWithListVars.vars [variable, in GeneratorsNG]
hole1 [definition, in GeneratorsNG]
hole1 [definition, in Generators]
hole10 [definition, in GeneratorsNG]
hole10 [definition, in Generators]
hole2 [lemma, in Demo]
hole2 [definition, in GeneratorsNG]
hole2 [definition, in Generators]
hole2 [lemma, in AltDemo]
hole2_tauto [lemma, in Demo]
hole2_tauto [lemma, in AltDemo]
hole3 [lemma, in AltDemo]
hole4 [lemma, in Demo]
hole4 [lemma, in AltDemo]
hole5 [lemma, in AltDemo]
hole6 [definition, in GeneratorsNG]
hole6 [definition, in Generators]

I

iff_def2 [lemma, in Ergo.DoubleNegUtils]
iff_def [lemma, in Ergo.DoubleNegUtils]
IllTypedEqualities [section, in Ergo.ModelsRingExt]
IllTypedEqualities.M [variable, in Ergo.ModelsRingExt]
ill_typed_ZRing_2 [lemma, in Ergo.ModelsRingExt]
ill_typed_ZRing_1 [lemma, in Ergo.ModelsRingExt]
implyX [definition, in Ergo.Theory]
implyX_entails [lemma, in Ergo.TheoryArith]
implyX_specs [lemma, in Ergo.TheoryArith]
implyX_weaken [lemma, in Ergo.Theory]
implyX_Ax [lemma, in Ergo.Theory]
implyX_impl [lemma, in Ergo.Theory]
implyX_Trans [instance, in Ergo.Theory]
implyX_Sym [instance, in Ergo.Theory]
implyX_Refl [instance, in Ergo.Theory]
implyX_m [instance, in Ergo.Theory]
implyX_entails [projection, in Ergo.Theory]
implyX_dec [projection, in Ergo.Theory]
implyX_Solve [projection, in Ergo.Theory]
implyX_Subst [projection, in Ergo.Theory]
implyX_Specs [record, in Ergo.Theory]
imp_def [lemma, in Ergo.DoubleNegUtils]
InA_in_list [lemma, in Ergo.Use]
Inconsistent [constructor, in Ergo.Env]
INDEX [module, in Ergo.Index]
Index [library]
INDEX.compare_3 [lemma, in Ergo.Index]
INDEX.compare_2 [lemma, in Ergo.Index]
INDEX.compare_1 [lemma, in Ergo.Index]
INDEX.compare_ [definition, in Ergo.Index]
INDEX.eq [definition, in Ergo.Index]
INDEX.eq_trans [lemma, in Ergo.Index]
INDEX.eq_sym [lemma, in Ergo.Index]
INDEX.eq_refl [lemma, in Ergo.Index]
INDEX.lt [definition, in Ergo.Index]
INDEX.lt_not_eq [lemma, in Ergo.Index]
INDEX.lt_trans [lemma, in Ergo.Index]
INDEX.t [definition, in Ergo.Index]
INDEX.t_OT [definition, in Ergo.Index]
INDEX.t_UOT [instance, in Ergo.Index]
inj_cst_2 [lemma, in Ergo.TermUtils]
input [inductive, in Ergo.CCX]
input_to_lit [definition, in Ergo.CCX]
insert_neq_o [lemma, in Ergo.Use]
insert_eq_o [lemma, in Ergo.Use]
insert_neq_o [lemma, in Ergo.Diff]
insert_eq_o [lemma, in Ergo.Diff]
int [definition, in Ergo.Term]
interp [definition, in Ergo.Ergo]
Interp [section, in Ergo.Ergo]
interp [definition, in Ergo.Term]
Interp [section, in Ergo.Term]
Interp [section, in Ergo.DistrNeg]
interps [definition, in Ergo.Term]
interps_ [definition, in Ergo.Term]
interp_irrelevant [lemma, in Ergo.Term]
interp_congr [lemma, in Ergo.Term]
interp_unfold [lemma, in Ergo.Term]
interp_op [definition, in Ergo.Term]
interp_m [lemma, in Ergo.DistrNeg]
interp' [definition, in Ergo.Term]
Interp.A [variable, in Ergo.DistrNeg]
Interp.Interps [section, in Ergo.Term]
Interp.Interps.interp [variable, in Ergo.Term]
Interp.v [variable, in Ergo.Ergo]
Interp.v [variable, in Ergo.Term]
Interp.vtypes [variable, in Ergo.Term]
[| _ |] [notation, in Ergo.Term]
introduce_vars [definition, in GeneratorsNG]
Inverse_Image.Rof [variable, in Ergo.Lexico]
Inverse_Image.f [variable, in Ergo.Lexico]
Inverse_Image.R [variable, in Ergo.Lexico]
Inverse_Image.B [variable, in Ergo.Lexico]
Inverse_Image.A [variable, in Ergo.Lexico]
Inverse_Image [section, in Ergo.Lexico]
in_list_rev_iff [lemma, in Ergo.Use]
in_list [definition, in Ergo.Use]
isM [definition, in Ergo.TheoryArith]
isMpoly [definition, in Ergo.TheoryArith]
isMpoly_m [instance, in Ergo.TheoryArith]
isMp_iter [lemma, in Ergo.TheoryArith]
isMp_make [lemma, in Ergo.TheoryArith]
isMp_mk_term [lemma, in Ergo.TheoryArith]
isMp_add_monome [lemma, in Ergo.TheoryArith]
isMp_embed [lemma, in Ergo.TheoryArith]
isMp_add_const [lemma, in Ergo.TheoryArith]
isMp_sub [lemma, in Ergo.TheoryArith]
isMp_add [lemma, in Ergo.TheoryArith]
isMp_addk [lemma, in Ergo.TheoryArith]
isMp_mult [lemma, in Ergo.TheoryArith]
isMp_P1 [lemma, in Ergo.TheoryArith]
isMp_P0 [lemma, in Ergo.TheoryArith]
isM_not_is_const [lemma, in Ergo.TheoryArith]
isM_make_embed [lemma, in Ergo.TheoryArith]
isZ [inductive, in Ergo.TheoryArith]
isZpoly [definition, in Ergo.TheoryArith]
isZpoly_m [instance, in Ergo.TheoryArith]
isZp_subst [lemma, in Ergo.TheoryArith]
isZp_isZ [lemma, in Ergo.TheoryArith]
isZp_make [lemma, in Ergo.TheoryArith]
isZp_mk_term [lemma, in Ergo.TheoryArith]
isZp_add_const [lemma, in Ergo.TheoryArith]
isZp_add_monome [lemma, in Ergo.TheoryArith]
isZp_cancel [lemma, in Ergo.TheoryArith]
isZp_mult [lemma, in Ergo.TheoryArith]
isZp_opp [lemma, in Ergo.TheoryArith]
isZp_sub [lemma, in Ergo.TheoryArith]
isZp_add [lemma, in Ergo.TheoryArith]
isZp_addk [lemma, in Ergo.TheoryArith]
isZp_embed [lemma, in Ergo.TheoryArith]
isZp_Pz [lemma, in Ergo.TheoryArith]
isZp_P1 [lemma, in Ergo.TheoryArith]
isZp_R0 [lemma, in Ergo.TheoryArith]
isZ_mult [lemma, in Ergo.TheoryArith]
isZ_opp [lemma, in Ergo.TheoryArith]
isZ_minus [lemma, in Ergo.TheoryArith]
isZ_plus [lemma, in Ergo.TheoryArith]
isZ_z [lemma, in Ergo.TheoryArith]
isZ_m [instance, in Ergo.TheoryArith]
isZ_intro [constructor, in Ergo.TheoryArith]
is_eq_sym [lemma, in Ergo.ModelsRingExt]
is_eq_refl [lemma, in Ergo.ModelsRingExt]
is_system [abbreviation, in EinsteinEasy]
is_person [abbreviation, in EinsteinEasy]
is_color [abbreviation, in EinsteinEasy]
is_house [abbreviation, in EinsteinEasy]
is_const_const [lemma, in Ergo.TheoryArith]
is_home [definition, in GeneratorsNG]
is_home [definition, in Generators]
is_wf [projection, in Ergo.Uf]
is_system [abbreviation, in EinsteinEasy2]
is_person [abbreviation, in EinsteinEasy2]
is_color [abbreviation, in EinsteinEasy2]
is_house [abbreviation, in EinsteinEasy2]
is_wf [projection, in Ergo.Diff]
iter [definition, in Ergo.Theory]
IterOps [section, in Ergo.TheoryArith]
IterOps.E [variable, in Ergo.TheoryArith]
IterOps.f [variable, in Ergo.TheoryArith]
IterOps.Hf [variable, in Ergo.TheoryArith]
IterOps.Ilin [variable, in Ergo.TheoryArith]
iter_idem [lemma, in Ergo.TheoryArith]
iter_idem_2' [lemma, in Ergo.TheoryArith]
iter_idem_2 [lemma, in Ergo.TheoryArith]
iter_unsolvable_None [lemma, in Ergo.TheoryArith]
iter_preserves_unsolvable [lemma, in Ergo.TheoryArith]
iter_cancel [lemma, in Ergo.TheoryArith]
iter_sub [lemma, in Ergo.TheoryArith]
iter_add [lemma, in Ergo.TheoryArith]
iter_mult [lemma, in Ergo.TheoryArith]
iter_Pq [lemma, in Ergo.TheoryArith]
iter_Pz [lemma, in Ergo.TheoryArith]
iter_P0 [lemma, in Ergo.TheoryArith]
iter_linear [lemma, in Ergo.TheoryArith]
iter_m [lemma, in Ergo.TheoryArith]
iter_as_list [lemma, in Ergo.TheoryArith]
iter_m [lemma, in Ergo.Theory]

K

K [module, in Ergo.AllInstances]
K.classic [definition, in Ergo.AllInstances]

L

leaves [definition, in Ergo.TheoryArith]
leaves [projection, in Ergo.Theory]
leaves_not_empty [lemma, in Ergo.TheoryArith]
leaves_m [instance, in Ergo.TheoryArith]
leaves_not_empty [projection, in Ergo.Theory]
leaves_m [projection, in Ergo.Theory]
Lexico [library]
lex2 [definition, in Ergo.Lexico]
LITERAL [module, in Ergo.Literal]
Literal [library]
LITERALBASE [module, in Ergo.LLazy]
LITERALBASE.interp [axiom, in Ergo.LLazy]
LITERALBASE.interp_mk_not [axiom, in Ergo.LLazy]
LITERALBASE.lfalse [axiom, in Ergo.LLazy]
LITERALBASE.ltrue [axiom, in Ergo.LLazy]
LITERALBASE.mk_not_fix [axiom, in Ergo.LLazy]
LITERALBASE.mk_not_invol [axiom, in Ergo.LLazy]
LITERALBASE.mk_not_compat [axiom, in Ergo.LLazy]
LITERALBASE.mk_not_tf [axiom, in Ergo.LLazy]
LITERALBASE.mk_not [axiom, in Ergo.LLazy]
LITERALBASE.t [axiom, in Ergo.LLazy]
LITERALBASE.t_OT [instance, in Ergo.LLazy]
LITERAL.clause [abbreviation, in Ergo.Literal]
LITERAL.clause_OT [definition, in Ergo.Literal]
LITERAL.cset [abbreviation, in Ergo.Literal]
LITERAL.expand [axiom, in Ergo.Literal]
LITERAL.ExpandNot [section, in Ergo.Literal]
LITERAL.ExpandNot.f [variable, in Ergo.Literal]
LITERAL.ExpandNot.fl [variable, in Ergo.Literal]
LITERAL.ExpandNot.fll [variable, in Ergo.Literal]
LITERAL.expand_mk_not [axiom, in Ergo.Literal]
LITERAL.expand_compat [axiom, in Ergo.Literal]
LITERAL.interp [axiom, in Ergo.Literal]
LITERAL.interp_mk_not [axiom, in Ergo.Literal]
LITERAL.is_proxy_true [axiom, in Ergo.Literal]
LITERAL.is_proxy_nil [axiom, in Ergo.Literal]
LITERAL.is_proxy_m [instance, in Ergo.Literal]
LITERAL.is_proxy_mk_not [axiom, in Ergo.Literal]
LITERAL.is_proxy [axiom, in Ergo.Literal]
LITERAL.lfalse [axiom, in Ergo.Literal]
LITERAL.llsize [definition, in Ergo.Literal]
LITERAL.lset [abbreviation, in Ergo.Literal]
LITERAL.lsize [definition, in Ergo.Literal]
LITERAL.ltrue [axiom, in Ergo.Literal]
LITERAL.mk_not_fix [axiom, in Ergo.Literal]
LITERAL.mk_not_invol [axiom, in Ergo.Literal]
LITERAL.mk_not_compat [axiom, in Ergo.Literal]
LITERAL.mk_not_m [instance, in Ergo.Literal]
LITERAL.mk_not_tf [axiom, in Ergo.Literal]
LITERAL.mk_not [axiom, in Ergo.Literal]
LITERAL.size [axiom, in Ergo.Literal]
LITERAL.size_expand [axiom, in Ergo.Literal]
LITERAL.size_mk_not [axiom, in Ergo.Literal]
LITERAL.size_pos [axiom, in Ergo.Literal]
LITERAL.size_m [instance, in Ergo.Literal]
LITERAL.t [axiom, in Ergo.Literal]
LITERAL.t_OT [instance, in Ergo.Literal]
LITINDEX [module, in Ergo.LLazy]
LITINDEX.Atom [constructor, in Ergo.LLazy]
LITINDEX.atom [inductive, in Ergo.LLazy]
LITINDEX.AtomOrderedType [section, in Ergo.LLazy]
LITINDEX.atom_UOT [instance, in Ergo.LLazy]
LITINDEX.atom_eq_iff [lemma, in Ergo.LLazy]
LITINDEX.Equation [constructor, in Ergo.LLazy]
LITINDEX.interp [definition, in Ergo.LLazy]
LITINDEX.interp_mk_not [lemma, in Ergo.LLazy]
LITINDEX.interp_atom [definition, in Ergo.LLazy]
LITINDEX.lfalse [definition, in Ergo.LLazy]
LITINDEX.lookup [definition, in Ergo.LLazy]
LITINDEX.ltrue [definition, in Ergo.LLazy]
LITINDEX.mk_not_fix [lemma, in Ergo.LLazy]
LITINDEX.mk_not_invol [lemma, in Ergo.LLazy]
LITINDEX.mk_not_compat [lemma, in Ergo.LLazy]
LITINDEX.mk_not_tf [lemma, in Ergo.LLazy]
LITINDEX.mk_not [definition, in Ergo.LLazy]
LITINDEX.t [definition, in Ergo.LLazy]
LITINDEX.t_OT [instance, in Ergo.LLazy]
LLAZY [module, in Ergo.LLazy]
LLazy [library]
LLAZYFY [module, in Ergo.LLazy]
LLAZYFY.clause [abbreviation, in Ergo.LLazy]
LLAZYFY.clause_OT [definition, in Ergo.LLazy]
LLAZYFY.compare_3 [lemma, in Ergo.LLazy]
LLAZYFY.compare_2 [lemma, in Ergo.LLazy]
LLAZYFY.compare_list_1 [lemma, in Ergo.LLazy]
LLAZYFY.compare_1 [lemma, in Ergo.LLazy]
LLAZYFY.cset [abbreviation, in Ergo.LLazy]
LLAZYFY.eq [definition, in Ergo.LLazy]
LLAZYFY.eqlist_to_raw [lemma, in Ergo.LLazy]
LLAZYFY.eqlist_trans [lemma, in Ergo.LLazy]
LLAZYFY.eqlist_sym [lemma, in Ergo.LLazy]
LLAZYFY.eqlist2_to_raw [lemma, in Ergo.LLazy]
LLAZYFY.eq_trans [lemma, in Ergo.LLazy]
LLAZYFY.eq_sym [lemma, in Ergo.LLazy]
LLAZYFY.eq_refl [lemma, in Ergo.LLazy]
LLAZYFY.expand [definition, in Ergo.LLazy]
LLAZYFY.ExpandNot [section, in Ergo.LLazy]
LLAZYFY.ExpandNot.f [variable, in Ergo.LLazy]
LLAZYFY.ExpandNot.fl [variable, in Ergo.LLazy]
LLAZYFY.ExpandNot.fll [variable, in Ergo.LLazy]
LLAZYFY.ExpandNot.f_m [variable, in Ergo.LLazy]
LLAZYFY.expand_mk_not [lemma, in Ergo.LLazy]
LLAZYFY.expand_map_map [lemma, in Ergo.LLazy]
LLAZYFY.expand_compat [lemma, in Ergo.LLazy]
LLAZYFY.interp [definition, in Ergo.LLazy]
LLAZYFY.interp_mk_not [definition, in Ergo.LLazy]
LLAZYFY.is_proxy_true [lemma, in Ergo.LLazy]
LLAZYFY.is_proxy_nil [lemma, in Ergo.LLazy]
LLAZYFY.is_proxy_m [instance, in Ergo.LLazy]
LLAZYFY.is_proxy_mk_not [lemma, in Ergo.LLazy]
LLAZYFY.is_proxy [definition, in Ergo.LLazy]
LLAZYFY.lfalse [definition, in Ergo.LLazy]
LLAZYFY.lllt [abbreviation, in Ergo.LLazy]
LLAZYFY.llsize [definition, in Ergo.LLazy]
LLAZYFY.llsize_llsize [lemma, in Ergo.LLazy]
LLAZYFY.llt [abbreviation, in Ergo.LLazy]
LLAZYFY.lset [abbreviation, in Ergo.LLazy]
LLAZYFY.lsize [definition, in Ergo.LLazy]
LLAZYFY.lt [definition, in Ergo.LLazy]
LLAZYFY.ltrue [definition, in Ergo.LLazy]
LLAZYFY.lt_not_eq [lemma, in Ergo.LLazy]
LLAZYFY.lt_trans [lemma, in Ergo.LLazy]
LLAZYFY.mk_not_fix [lemma, in Ergo.LLazy]
LLAZYFY.mk_not_invol [lemma, in Ergo.LLazy]
LLAZYFY.mk_not_m [instance, in Ergo.LLazy]
LLAZYFY.mk_not_compat [lemma, in Ergo.LLazy]
LLAZYFY.mk_not_tf [lemma, in Ergo.LLazy]
LLAZYFY.mk_not_interp [lemma, in Ergo.LLazy]
LLAZYFY.mk_not [definition, in Ergo.LLazy]
LLAZYFY.mk_literal [constructor, in Ergo.LLazy]
LLAZYFY.negate_expand [lemma, in Ergo.LLazy]
LLAZYFY.negation [definition, in Ergo.LLazy]
LLAZYFY.negation_interp [lemma, in Ergo.LLazy]
LLAZYFY.RAW [module, in Ergo.LLazy]
LLAZYFY.size [definition, in Ergo.LLazy]
LLAZYFY.size_expand [lemma, in Ergo.LLazy]
LLAZYFY.size_mk_not [lemma, in Ergo.LLazy]
LLAZYFY.size_pos [lemma, in Ergo.LLazy]
LLAZYFY.size_m [instance, in Ergo.LLazy]
LLAZYFY.t [definition, in Ergo.LLazy]
LLAZYFY.this [projection, in Ergo.LLazy]
LLAZYFY.t_OT [instance, in Ergo.LLazy]
LLAZYFY.t_ [record, in Ergo.LLazy]
LLAZYFY.wf [projection, in Ergo.LLazy]
LLAZYFY.wf_expand [lemma, in Ergo.LLazy]
LLAZYFY.wf_mk_not [lemma, in Ergo.LLazy]
LLAZYFY.wf_negation [lemma, in Ergo.LLazy]
LLAZYFY.wf_lit_2_weak [lemma, in Ergo.LLazy]
LLAZYFY.wf_lit_wk_proxy [constructor, in Ergo.LLazy]
LLAZYFY.wf_lit_wk_lit [constructor, in Ergo.LLazy]
LLAZYFY.wf_lit_weak [inductive, in Ergo.LLazy]
LLAZYFY.wf_lit_proxy [constructor, in Ergo.LLazy]
LLAZYFY.wf_lit_lit [constructor, in Ergo.LLazy]
LLAZYFY.wf_lit [inductive, in Ergo.LLazy]
ll_interp [definition, in Ergo.DistrNeg]
Ln [definition, in Generators]
LoadTactic [module, in Ergo.TacticLazy]
LoadTactic.AD [module, in Ergo.TacticLazy]
LoadTactic.Deprecated [module, in Ergo.TacticLazy]
LoadTactic.dpll [definition, in Ergo.TacticLazy]
LoadTactic.dpll' [definition, in Ergo.TacticLazy]
LoadTactic.L [module, in Ergo.TacticLazy]
LoadTactic.Res [inductive, in Ergo.TacticLazy]
LoadTactic.Sat [constructor, in Ergo.TacticLazy]
LoadTactic.Unsat [constructor, in Ergo.TacticLazy]
LoadTactic.validity [lemma, in Ergo.TacticLazy]
LoadTactic.validity' [lemma, in Ergo.TacticLazy]
lookup [definition, in Ergo.Term]
lookup_type [definition, in Ergo.Term]
LtList [section, in Ergo.LLazy]
LtList.A [variable, in Ergo.LLazy]
LtList.compareA [variable, in Ergo.LLazy]
LtList.ltA [variable, in Ergo.LLazy]
lt_list [definition, in Ergo.LLazy]
l_interp [definition, in Ergo.DistrNeg]

M

make [definition, in Ergo.TheoryArith]
make [projection, in Ergo.Theory]
MakeErgo [module, in Demo]
MakeErgo [module, in Ergo.AltErgo]
MakeErgo.DPLL [module, in Demo]
MakeErgo.DPLL [module, in Ergo.AltErgo]
MakeErgo.DPLL.E [module, in Demo]
MakeErgo.DPLL.E [module, in Ergo.AltErgo]
make_term_of_R [lemma, in Ergo.TheoryArith]
make_entails [lemma, in Ergo.TheoryArith]
make_correct [lemma, in Ergo.TheoryArith]
make_tmult_3 [lemma, in Ergo.TheoryArith]
make_tmult_2 [lemma, in Ergo.TheoryArith]
make_tmult_1 [lemma, in Ergo.TheoryArith]
make_topp [lemma, in Ergo.TheoryArith]
make_tminus [lemma, in Ergo.TheoryArith]
make_tplus [lemma, in Ergo.TheoryArith]
make_z [lemma, in Ergo.TheoryArith]
make_sound [lemma, in Ergo.Theory]
melange_cc_sat [lemma, in Demo]
melange_cc_sat [lemma, in AltDemo]
mem [definition, in Ergo.Uf]
merge [definition, in Ergo.Use]
merge [definition, in Ergo.Uf]
merge_find [lemma, in Ergo.Use]
merge_touched_find [lemma, in Ergo.Uf]
merge_touched_spec_2 [definition, in Ergo.Uf]
merge_touched_mem [lemma, in Ergo.Uf]
merge_touched_spec [definition, in Ergo.Uf]
merge_find [lemma, in Ergo.Uf]
merge_mem [lemma, in Ergo.Uf]
merge_touched [definition, in Ergo.Uf]
merge' [definition, in Ergo.Uf]
merge'_touched_spec [lemma, in Ergo.Uf]
merge'_find [lemma, in Ergo.Uf]
merge'_mem [lemma, in Ergo.Uf]
mext [inductive, in Ergo.ModelsRingExt]
mext_cons [constructor, in Ergo.ModelsRingExt]
mext_nil [constructor, in Ergo.ModelsRingExt]
mext_terms [inductive, in Ergo.ModelsRingExt]
mext_rule [constructor, in Ergo.ModelsRingExt]
mext_congr [constructor, in Ergo.ModelsRingExt]
mext_trans [constructor, in Ergo.ModelsRingExt]
mext_sym [constructor, in Ergo.ModelsRingExt]
mext_refl [constructor, in Ergo.ModelsRingExt]
mext_wt [constructor, in Ergo.ModelsRingExt]
mi [definition, in Ergo.TheoryArith]
Minus [constructor, in Ergo.Term]
mk_varmaps [constructor, in Ergo.Ergo]
mk_term_of_R [lemma, in Ergo.TheoryArith]
mk_term_correct [lemma, in Ergo.TheoryArith]
mk_term_make [lemma, in Ergo.TheoryArith]
mk_term_acc [lemma, in Ergo.TheoryArith]
mk_term [definition, in Ergo.TheoryArith]
mk_depvmap [definition, in Ergo.Term]
mk_symbol [definition, in Ergo.Term]
mk_dummy [constructor, in Ergo.Term]
mk_a [constructor, in Generators]
mk_x [constructor, in Generators]
mk_occ [constructor, in Generators]
mk_t [constructor, in Ergo.Uf]
mk_z [constructor, in GeneratorsEq]
mk_y [constructor, in GeneratorsEq]
mk_x [constructor, in GeneratorsEq]
ModelsAsRing [module, in Ergo.TheoryArith]
ModelsAsRing.implyX_entails [lemma, in Ergo.TheoryArith]
ModelsRingExt [library]
models_integral' [lemma, in Ergo.TheoryArith]
models_neq_cst_iff [lemma, in Ergo.TheoryArith]
models_eq_cst_iff [lemma, in Ergo.TheoryArith]
models_eq_Trans [instance, in Ergo.TheoryArith]
models_eq_Sym [instance, in Ergo.TheoryArith]
models_eq_Refl [instance, in Ergo.TheoryArith]
Morphisms [section, in Ergo.DistrNeg]
Morphisms.A [variable, in Ergo.DistrNeg]
Morphisms.eq [variable, in Ergo.DistrNeg]
Morphisms.eq_trans [variable, in Ergo.DistrNeg]
Morphisms.eq_sym [variable, in Ergo.DistrNeg]
Morphisms.eq_refl [variable, in Ergo.DistrNeg]
Morphisms.f [variable, in Ergo.DistrNeg]
Morphisms.f_m [variable, in Ergo.DistrNeg]
Morphisms.neg [variable, in Ergo.DistrNeg]
Morphisms.neg_m [variable, in Ergo.DistrNeg]
Morphisms2 [section, in Ergo.DistrNeg]
Morphisms2.A [variable, in Ergo.DistrNeg]
Morphisms2.eq [variable, in Ergo.DistrNeg]
Morphisms2.eq_trans [variable, in Ergo.DistrNeg]
Morphisms2.eq_sym [variable, in Ergo.DistrNeg]
Morphisms2.eq_refl [variable, in Ergo.DistrNeg]
Morphisms2.H [variable, in Ergo.DistrNeg]
Morphisms2.neg [variable, in Ergo.DistrNeg]
Morphisms2.neg' [variable, in Ergo.DistrNeg]
Mult [constructor, in Ergo.Term]
mult_as_addk [lemma, in Ergo.TheoryArith]
myType [definition, in Ergo.CCX]
M1 [lemma, in EinsteinEasy]
M1 [lemma, in EinsteinEasy2]
M2 [lemma, in EinsteinEasy]
M2 [lemma, in EinsteinEasy2]
M3 [lemma, in EinsteinEasy]
M3 [lemma, in EinsteinEasy2]
M4 [lemma, in EinsteinEasy2]
M5 [lemma, in EinsteinEasy2]

N

negation_compose [lemma, in Ergo.DistrNeg]
negation_interp [lemma, in Ergo.DistrNeg]
neqs [definition, in Ergo.Diff]
neqs_separate_3 [lemma, in Ergo.Diff]
neqs_separate_2 [lemma, in Ergo.Diff]
neqs_separate_1 [lemma, in Ergo.Diff]
neqs_empty [lemma, in Ergo.Diff]
neqs_sym [lemma, in Ergo.Diff]
neqs_m [instance, in Ergo.Diff]
neqs_not_iff [lemma, in Ergo.Diff]
neqs_iff [lemma, in Ergo.Diff]
niff_def2 [lemma, in Ergo.DoubleNegUtils]
niff_def [lemma, in Ergo.DoubleNegUtils]
nimp_def [lemma, in Ergo.DoubleNegUtils]
Normal [constructor, in Ergo.Env]
not_or_and_not [lemma, in Ergo.DoubleNegUtils]
not_and_or_not [lemma, in Ergo.DoubleNegUtils]
num_classes_merge'_lt [lemma, in Ergo.Uf]
num_classes_merge' [lemma, in Ergo.Uf]
num_classes_add [lemma, in Ergo.Uf]
num_classes_empty [lemma, in Ergo.Uf]
num_classes [definition, in Ergo.Uf]

O

occ [definition, in GeneratorsNG]
occ [inductive, in Generators]
one [definition, in Ergo.TheoryArith]
one [projection, in Ergo.Theory]
one_is_false [definition, in Generators]
one_is_crowded [definition, in Generators]
one_is_crowded_aux [definition, in Generators]
Op [constructor, in Ergo.Term]
Opp [constructor, in Ergo.Term]
orderAB [definition, in Ergo.Lexico]
or_and_distr [lemma, in Ergo.DoubleNegUtils]
or_distr_and [lemma, in Ergo.DoubleNegUtils]

P

partage [definition, in Generators]
partage2 [definition, in Generators]
peirce_or_is_it [lemma, in Demo]
peirce_or_is_it [lemma, in AltDemo]
pgcd_fix_Z [lemma, in Demo]
pgcd_fix_sat [lemma, in Demo]
pgcd_fix_congruence [lemma, in Demo]
pgcd_fix [lemma, in Demo]
pgcd_fix_Z [lemma, in AltDemo]
pgcd_fix_sat [lemma, in AltDemo]
pgcd_fix_congruence [lemma, in AltDemo]
pgcd_fix [lemma, in AltDemo]
pinterp [definition, in Ergo.DistrNeg]
pl [definition, in Ergo.TheoryArith]
Plus [constructor, in Ergo.Term]
power [definition, in Demo]
power [definition, in AltDemo]
power [definition, in GeneratorsEq]
powerZ [definition, in Demo]
powerZ [definition, in AltDemo]
Props [module, in Ergo.Sat]
Props [module, in Ergo.FoldProps]
Props [section, in Ergo.DistrNeg]
Props.A [variable, in Ergo.DistrNeg]
Props.f [variable, in Ergo.DistrNeg]
Props.mk_not [variable, in Ergo.DistrNeg]
Props.negation [variable, in Ergo.DistrNeg]
push_minus [lemma, in Ergo.TheoryArith]
push_mult [lemma, in Ergo.TheoryArith]
push_addk [lemma, in Ergo.TheoryArith]
push_tminus_tmult [lemma, in Ergo.TheoryArith]
push_right_eq [lemma, in Ergo.TheoryArith]

Q

QasDT [module, in Ergo.Rational]
QasDT.eq_dec [lemma, in Ergo.Rational]
QasDT.U [definition, in Ergo.Rational]
QEqDep [module, in Ergo.Rational]
Qfloor_isZ [lemma, in Ergo.TheoryArith]
Qfloor_opp [lemma, in Ergo.TheoryArith]
Qfloor_mult [lemma, in Ergo.TheoryArith]
Qfloor_addk [lemma, in Ergo.TheoryArith]
Q_neq [lemma, in Ergo.TheoryArith]
Q_cancel [lemma, in Ergo.TheoryArith]
Q2Qc_m [instance, in Ergo.TheoryArith]

R

R [definition, in Ergo.TheoryArith]
R [projection, in Ergo.Theory]
ra [projection, in Ergo.Ergo]
range [definition, in Ergo.Uf]
range_merge' [lemma, in Ergo.Uf]
range_merge [lemma, in Ergo.Uf]
range_add [lemma, in Ergo.Uf]
range_empty [lemma, in Ergo.Uf]
range_mem [lemma, in Ergo.Uf]
Rational [library]
rational_OT [definition, in Ergo.Rational]
rational_UOT [instance, in Ergo.Rational]
RAW [module, in Ergo.LLazy]
RAW [module, in Ergo.CPolynoms]
RAWCCA [module, in Ergo.CCX]
RAWCCE [module, in Ergo.CCX]
RAWCCX [module, in Ergo.CCX]
RAWCCX.are_diff [definition, in Ergo.CCX]
RAWCCX.are_equal [definition, in Ergo.CCX]
RAWCCX.assume [definition, in Ergo.CCX]
RAWCCX.assumed [definition, in Ergo.CCX]
RAWCCX.CleanUp [section, in Ergo.CCX]
RAWCCX.D [projection, in Ergo.CCX]
RAWCCX.diff [definition, in Ergo.CCX]
RAWCCX.empty [definition, in Ergo.CCX]
RAWCCX.F [projection, in Ergo.CCX]
RAWCCX.filter_subset_gen [lemma, in Ergo.CCX]
RAWCCX.find_congr_equations_terms [lemma, in Ergo.CCX]
RAWCCX.find_congr_equations2_terms [lemma, in Ergo.CCX]
RAWCCX.find_congr_equations1_terms [lemma, in Ergo.CCX]
RAWCCX.find_add_equations [definition, in Ergo.CCX]
RAWCCX.find_congr_equations [definition, in Ergo.CCX]
RAWCCX.find_congr_equations2 [definition, in Ergo.CCX]
RAWCCX.find_congr_equations1 [definition, in Ergo.CCX]
RAWCCX.G [projection, in Ergo.CCX]
RAWCCX.guard [definition, in Ergo.CCX]
RAWCCX.guarded_wf_lt [definition, in Ergo.CCX]
RAWCCX.I [projection, in Ergo.CCX]
RAWCCX.incoherent [definition, in Ergo.CCX]
RAWCCX.inter_leaves_terms [lemma, in Ergo.CCX]
RAWCCX.inter_leaves [definition, in Ergo.CCX]
RAWCCX.lcongr [definition, in Ergo.CCX]
RAWCCX.lexists [definition, in Ergo.CCX]
RAWCCX.lleaves [definition, in Ergo.CCX]
RAWCCX.merge [definition, in Ergo.CCX]
RAWCCX.merge_decreases [lemma, in Ergo.CCX]
RAWCCX.mk_env [constructor, in Ergo.CCX]
RAWCCX.N [projection, in Ergo.CCX]
RAWCCX.num_pending_wf [lemma, in Ergo.CCX]
RAWCCX.num_distincts_wf [lemma, in Ergo.CCX]
RAWCCX.num_distinct_pairs_le [lemma, in Ergo.CCX]
RAWCCX.num_pending [definition, in Ergo.CCX]
RAWCCX.num_distinct_pairs [definition, in Ergo.CCX]
RAWCCX.query [definition, in Ergo.CCX]
RAWCCX.Specs [module, in Ergo.CCX]
RAWCCX.Specs.add_terms_dec [definition, in Ergo.CCX]
RAWCCX.Specs.add_term_dec [definition, in Ergo.CCX]
RAWCCX.Specs.add_term_terms_dec [lemma, in Ergo.CCX]
RAWCCX.Specs.add_terms_spec_Normal [constructor, in Ergo.CCX]
RAWCCX.Specs.add_terms_spec [inductive, in Ergo.CCX]
RAWCCX.Specs.add_term_spec_Normal [constructor, in Ergo.CCX]
RAWCCX.Specs.add_term_spec [inductive, in Ergo.CCX]
RAWCCX.Specs.are_diff_dec [lemma, in Ergo.CCX]
RAWCCX.Specs.are_diff_spec_false [constructor, in Ergo.CCX]
RAWCCX.Specs.are_diff_spec_true [constructor, in Ergo.CCX]
RAWCCX.Specs.are_diff_spec [inductive, in Ergo.CCX]
RAWCCX.Specs.are_equal_dec [lemma, in Ergo.CCX]
RAWCCX.Specs.are_equal_spec_false [constructor, in Ergo.CCX]
RAWCCX.Specs.are_equal_spec_true [constructor, in Ergo.CCX]
RAWCCX.Specs.are_equal_spec [inductive, in Ergo.CCX]
RAWCCX.Specs.assumed_inconsistent [lemma, in Ergo.CCX]
RAWCCX.Specs.assumed_assume [lemma, in Ergo.CCX]
RAWCCX.Specs.assumed_empty [lemma, in Ergo.CCX]
RAWCCX.Specs.assume_dec [lemma, in Ergo.CCX]
RAWCCX.Specs.assume_spec_Inconsistent [constructor, in Ergo.CCX]
RAWCCX.Specs.assume_spec_Input [constructor, in Ergo.CCX]
RAWCCX.Specs.assume_spec [inductive, in Ergo.CCX]
RAWCCX.Specs.clean_up_dec [lemma, in Ergo.CCX]
RAWCCX.Specs.clean_up_Normal [constructor, in Ergo.CCX]
RAWCCX.Specs.clean_up_Inconsistent [constructor, in Ergo.CCX]
RAWCCX.Specs.clean_up_spec [inductive, in Ergo.CCX]
RAWCCX.Specs.coherence [projection, in Ergo.CCX]
RAWCCX.Specs.coherent [definition, in Ergo.CCX]
RAWCCX.Specs.coherent_diff [lemma, in Ergo.CCX]
RAWCCX.Specs.coherent_merge [lemma, in Ergo.CCX]
RAWCCX.Specs.coherent_add [lemma, in Ergo.CCX]
RAWCCX.Specs.coincides [inductive, in Ergo.CCX]
RAWCCX.Specs.coincides_weaken [lemma, in Ergo.CCX]
RAWCCX.Specs.coincides_merge [lemma, in Ergo.CCX]
RAWCCX.Specs.coincides_add [lemma, in Ergo.CCX]
RAWCCX.Specs.coincides_inputs [lemma, in Ergo.CCX]
RAWCCX.Specs.coincides_submodel [lemma, in Ergo.CCX]
RAWCCX.Specs.coincides'_merge [lemma, in Ergo.CCX]
RAWCCX.Specs.Dcorrect [projection, in Ergo.CCX]
RAWCCX.Specs.diff_dec [lemma, in Ergo.CCX]
RAWCCX.Specs.diff_spec_Normal [constructor, in Ergo.CCX]
RAWCCX.Specs.diff_spec_Inconsistent [constructor, in Ergo.CCX]
RAWCCX.Specs.diff_spec [inductive, in Ergo.CCX]
RAWCCX.Specs.Dwf [projection, in Ergo.CCX]
RAWCCX.Specs.eqns_of [definition, in Ergo.CCX]
RAWCCX.Specs.Fcorrect [projection, in Ergo.CCX]
RAWCCX.Specs.find_congr_equations_extend [lemma, in Ergo.CCX]
RAWCCX.Specs.find_congr_equations_correct [lemma, in Ergo.CCX]
RAWCCX.Specs.find_congr_equations2_extend [lemma, in Ergo.CCX]
RAWCCX.Specs.find_congr_equations2_correct [lemma, in Ergo.CCX]
RAWCCX.Specs.find_congr_equations1_extend [lemma, in Ergo.CCX]
RAWCCX.Specs.find_congr_equations1_correct [lemma, in Ergo.CCX]
RAWCCX.Specs.find_add_equations_extend [lemma, in Ergo.CCX]
RAWCCX.Specs.find_add_equations_correct [lemma, in Ergo.CCX]
RAWCCX.Specs.incoherent_true [lemma, in Ergo.CCX]
RAWCCX.Specs.incoherent_false [lemma, in Ergo.CCX]
RAWCCX.Specs.input_range [definition, in Ergo.CCX]
RAWCCX.Specs.input_assume [definition, in Ergo.CCX]
RAWCCX.Specs.iter [definition, in Ergo.CCX]
RAWCCX.Specs.iter_correct [lemma, in Ergo.CCX]
RAWCCX.Specs.justify [inductive, in Ergo.CCX]
RAWCCX.Specs.justify_merge [lemma, in Ergo.CCX]
RAWCCX.Specs.justify_add [lemma, in Ergo.CCX]
RAWCCX.Specs.justify_coincides [lemma, in Ergo.CCX]
RAWCCX.Specs.justify_cons [constructor, in Ergo.CCX]
RAWCCX.Specs.justify_nil [constructor, in Ergo.CCX]
RAWCCX.Specs.lcongr_merge [lemma, in Ergo.CCX]
RAWCCX.Specs.lcongr_add [lemma, in Ergo.CCX]
RAWCCX.Specs.merge_dec [lemma, in Ergo.CCX]
RAWCCX.Specs.merge_spec_Normal [constructor, in Ergo.CCX]
RAWCCX.Specs.merge_spec_Inconsistent [constructor, in Ergo.CCX]
RAWCCX.Specs.merge_spec [inductive, in Ergo.CCX]
RAWCCX.Specs.mk_coincides [constructor, in Ergo.CCX]
RAWCCX.Specs.Ncoincides [definition, in Ergo.CCX]
RAWCCX.Specs.Ncoincides_separate [lemma, in Ergo.CCX]
RAWCCX.Specs.Ncoincides_weaken [lemma, in Ergo.CCX]
RAWCCX.Specs.Ncoincides_inputs [lemma, in Ergo.CCX]
RAWCCX.Specs.Ncoincides_submodel [lemma, in Ergo.CCX]
RAWCCX.Specs.Ncorrect [projection, in Ergo.CCX]
RAWCCX.Specs.no_trivial_model [lemma, in Ergo.CCX]
RAWCCX.Specs.Nwf [projection, in Ergo.CCX]
RAWCCX.Specs.pack [definition, in Ergo.CCX]
RAWCCX.Specs.query_true [lemma, in Ergo.CCX]
RAWCCX.Specs.query_assumed [lemma, in Ergo.CCX]
RAWCCX.Specs.query_dec [lemma, in Ergo.CCX]
RAWCCX.Specs.query_spec_false [constructor, in Ergo.CCX]
RAWCCX.Specs.query_spec_true [constructor, in Ergo.CCX]
RAWCCX.Specs.query_spec [inductive, in Ergo.CCX]
RAWCCX.Specs.submodel_eq_models_list [lemma, in Ergo.CCX]
RAWCCX.Specs.theory_iter_correct [lemma, in Ergo.CCX]
RAWCCX.Specs.Wf [record, in Ergo.CCX]
RAWCCX.Specs.Wf_assume [lemma, in Ergo.CCX]
RAWCCX.Specs.Wf_diff [lemma, in Ergo.CCX]
RAWCCX.Specs.Wf_clean_up [lemma, in Ergo.CCX]
RAWCCX.Specs.Wf_merge' [lemma, in Ergo.CCX]
RAWCCX.Specs.Wf_merge [lemma, in Ergo.CCX]
RAWCCX.Specs.Wf_add_terms [instance, in Ergo.CCX]
RAWCCX.Specs.Wf_add_term [instance, in Ergo.CCX]
RAWCCX.Specs.Wf_add_term_terms [lemma, in Ergo.CCX]
RAWCCX.Specs.Wf_empty [instance, in Ergo.CCX]
RAWCCX.t [definition, in Ergo.CCX]
RAWCCX.terms_of [definition, in Ergo.CCX]
RAWCCX.terms_of_list [definition, in Ergo.CCX]
RAWCCX.t_lt_wf [lemma, in Ergo.CCX]
RAWCCX.t_lt_2 [constructor, in Ergo.CCX]
RAWCCX.t_lt_1 [constructor, in Ergo.CCX]
RAWCCX.t_lt [inductive, in Ergo.CCX]
RAWCCX.t_ [record, in Ergo.CCX]
RAWCCX.uncongr [definition, in Ergo.CCX]
RAWCCX.uncongr_gen [lemma, in Ergo.CCX]
RAWCCX.uncongr_m [instance, in Ergo.CCX]
RAW.add [definition, in Ergo.CPolynoms]
RAW.addk [definition, in Ergo.CPolynoms]
RAW.addk_dec' [lemma, in Ergo.CPolynoms]
RAW.addk_spec'_intro [constructor, in Ergo.CPolynoms]
RAW.addk_spec' [inductive, in Ergo.CPolynoms]
RAW.addk_dec [lemma, in Ergo.CPolynoms]
RAW.addk_spec_intro [constructor, in Ergo.CPolynoms]
RAW.addk_spec_0 [constructor, in Ergo.CPolynoms]
RAW.addk_spec [inductive, in Ergo.CPolynoms]
RAW.addk_m_dec [lemma, in Ergo.CPolynoms]
RAW.addk_m_spec_intro [constructor, in Ergo.CPolynoms]
RAW.addk_m_spec [inductive, in Ergo.CPolynoms]
RAW.addk_morphism [instance, in Ergo.CPolynoms]
RAW.addk_m_m [instance, in Ergo.CPolynoms]
RAW.addk_m [definition, in Ergo.CPolynoms]
RAW.add_equiv [instance, in Ergo.CPolynoms]
RAW.add_monome_equiv [instance, in Ergo.CPolynoms]
RAW.add_const_equiv [instance, in Ergo.CPolynoms]
RAW.add_dec' [lemma, in Ergo.CPolynoms]
RAW.add_spec'_intro [constructor, in Ergo.CPolynoms]
RAW.add_spec' [inductive, in Ergo.CPolynoms]
RAW.add_monome_dec' [lemma, in Ergo.CPolynoms]
RAW.add_monome_spec'_intro [constructor, in Ergo.CPolynoms]
RAW.add_monome_spec' [inductive, in Ergo.CPolynoms]
RAW.add_const_dec' [lemma, in Ergo.CPolynoms]
RAW.add_const_spec'_intro [constructor, in Ergo.CPolynoms]
RAW.add_const_spec' [inductive, in Ergo.CPolynoms]
RAW.add_dec [lemma, in Ergo.CPolynoms]
RAW.add_spec_intro [constructor, in Ergo.CPolynoms]
RAW.add_spec [inductive, in Ergo.CPolynoms]
RAW.add_monome_dec [lemma, in Ergo.CPolynoms]
RAW.add_monome_spec_intro [constructor, in Ergo.CPolynoms]
RAW.add_monome_spec_0 [constructor, in Ergo.CPolynoms]
RAW.add_monome_spec [inductive, in Ergo.CPolynoms]
RAW.add_monome_m [instance, in Ergo.CPolynoms]
RAW.add_const_m [instance, in Ergo.CPolynoms]
RAW.add_m [instance, in Ergo.CPolynoms]
RAW.add_monome [definition, in Ergo.CPolynoms]
RAW.add_const [definition, in Ergo.CPolynoms]
RAW.cancel [definition, in Ergo.CPolynoms]
RAW.cancel_equiv [instance, in Ergo.CPolynoms]
RAW.cancel_dec' [lemma, in Ergo.CPolynoms]
RAW.cancel_spec'_intro [constructor, in Ergo.CPolynoms]
RAW.cancel_spec' [inductive, in Ergo.CPolynoms]
RAW.cancel_m [instance, in Ergo.CPolynoms]
RAW.cardinal_m [instance, in Ergo.CPolynoms]
RAW.choose [definition, in Ergo.CPolynoms]
RAW.choose_dec [lemma, in Ergo.CPolynoms]
RAW.choose_spec_Some [constructor, in Ergo.CPolynoms]
RAW.choose_spec_None [constructor, in Ergo.CPolynoms]
RAW.choose_spec [inductive, in Ergo.CPolynoms]
RAW.choose_m [instance, in Ergo.CPolynoms]
RAW.cinterp [definition, in Ergo.LLazy]
RAW.coef_of_m [instance, in Ergo.CPolynoms]
RAW.coef_of_equiv [instance, in Ergo.CPolynoms]
RAW.coef_of [definition, in Ergo.CPolynoms]
RAW.compare_ [definition, in Ergo.LLazy]
RAW.div [definition, in Ergo.CPolynoms]
RAW.div_equiv [instance, in Ergo.CPolynoms]
RAW.div_dec' [lemma, in Ergo.CPolynoms]
RAW.div_dec [lemma, in Ergo.CPolynoms]
RAW.div_m [instance, in Ergo.CPolynoms]
RAW.elements_m [instance, in Ergo.CPolynoms]
RAW.embed [definition, in Ergo.CPolynoms]
RAW.embed_m [instance, in Ergo.CPolynoms]
RAW.eq [definition, in Ergo.LLazy]
RAW.equiv [definition, in Ergo.CPolynoms]
RAW.equiv_Transitive [instance, in Ergo.CPolynoms]
RAW.equiv_Symmetric [instance, in Ergo.CPolynoms]
RAW.equiv_Reflexive [instance, in Ergo.CPolynoms]
RAW.eq_equiv [instance, in Ergo.CPolynoms]
RAW.expand [definition, in Ergo.LLazy]
RAW.expand_compat [lemma, in Ergo.LLazy]
RAW.extract [definition, in Ergo.CPolynoms]
RAW.extract_embed [lemma, in Ergo.CPolynoms]
RAW.extract_dec [lemma, in Ergo.CPolynoms]
RAW.extract_spec_Some [constructor, in Ergo.CPolynoms]
RAW.extract_spec_None [constructor, in Ergo.CPolynoms]
RAW.extract_spec [inductive, in Ergo.CPolynoms]
RAW.extract_m [instance, in Ergo.CPolynoms]
RAW.find_m [instance, in Ergo.CPolynoms]
RAW.fold_coefs_m [instance, in Ergo.CPolynoms]
RAW.fold_coefs [definition, in Ergo.CPolynoms]
RAW.fold_m [instance, in Ergo.CPolynoms]
RAW.interp [definition, in Ergo.LLazy]
RAW.Interp [section, in Ergo.LLazy]
RAW.Interp.v [variable, in Ergo.LLazy]
RAW.In_m [instance, in Ergo.CPolynoms]
RAW.is_const_dec [lemma, in Ergo.CPolynoms]
RAW.is_const_spec_false [constructor, in Ergo.CPolynoms]
RAW.is_const_spec_true [constructor, in Ergo.CPolynoms]
RAW.is_const_spec [inductive, in Ergo.CPolynoms]
RAW.is_const [definition, in Ergo.CPolynoms]
RAW.is_add_monome_add [constructor, in Ergo.CPolynoms]
RAW.is_add_monome_diff [constructor, in Ergo.CPolynoms]
RAW.is_add_monome_adjust [constructor, in Ergo.CPolynoms]
RAW.is_add_monome_of [inductive, in Ergo.CPolynoms]
RAW.is_addk_of_2 [constructor, in Ergo.CPolynoms]
RAW.is_addk_of_1 [constructor, in Ergo.CPolynoms]
RAW.is_addk_of_both [constructor, in Ergo.CPolynoms]
RAW.is_addk_of [inductive, in Ergo.CPolynoms]
RAW.is_mult_intro [constructor, in Ergo.CPolynoms]
RAW.is_mult_of [inductive, in Ergo.CPolynoms]
RAW.is_compare_m [instance, in Ergo.CPolynoms]
RAW.leaves [definition, in Ergo.CPolynoms]
RAW.leaves_m [instance, in Ergo.CPolynoms]
RAW.lfalse [definition, in Ergo.LLazy]
RAW.ListSize [section, in Ergo.LLazy]
RAW.ListSize.A [variable, in Ergo.LLazy]
RAW.ListSize.sz [variable, in Ergo.LLazy]
RAW.Lit [constructor, in Ergo.LLazy]
RAW.LiteralInduction [section, in Ergo.LLazy]
RAW.LiteralInductionDefault [section, in Ergo.LLazy]
RAW.LiteralInductionDefault.Hlit [variable, in Ergo.LLazy]
RAW.LiteralInductionDefault.Hview [variable, in Ergo.LLazy]
RAW.LiteralInductionDefault.P [variable, in Ergo.LLazy]
RAW.LiteralInductionDefault.Pl [variable, in Ergo.LLazy]
RAW.LiteralInductionDefault.Pp [variable, in Ergo.LLazy]
RAW.LiteralInduction.Hcons [variable, in Ergo.LLazy]
RAW.LiteralInduction.Hlcons [variable, in Ergo.LLazy]
RAW.LiteralInduction.Hlit [variable, in Ergo.LLazy]
RAW.LiteralInduction.Hlnil [variable, in Ergo.LLazy]
RAW.LiteralInduction.Hnil [variable, in Ergo.LLazy]
RAW.LiteralInduction.Hview [variable, in Ergo.LLazy]
RAW.LiteralInduction.P [variable, in Ergo.LLazy]
RAW.LiteralInduction.Pl [variable, in Ergo.LLazy]
RAW.LiteralInduction.Pp [variable, in Ergo.LLazy]
RAW.literal_ind [lemma, in Ergo.LLazy]
RAW.literal_ind2 [definition, in Ergo.LLazy]
RAW.lllt [abbreviation, in Ergo.LLazy]
RAW.llsize [definition, in Ergo.LLazy]
RAW.llt [abbreviation, in Ergo.LLazy]
RAW.lsize [definition, in Ergo.LLazy]
RAW.lt [definition, in Ergo.LLazy]
RAW.ltrue [definition, in Ergo.LLazy]
RAW.lt_trans [lemma, in Ergo.LLazy]
RAW.lt_not_eq [lemma, in Ergo.LLazy]
RAW.MapQ_OT [definition, in Ergo.CPolynoms]
RAW.map2_m [instance, in Ergo.CPolynoms]
RAW.mk_not_invol [lemma, in Ergo.LLazy]
RAW.mk_not [definition, in Ergo.LLazy]
RAW.mult [definition, in Ergo.CPolynoms]
RAW.mult_equiv [instance, in Ergo.CPolynoms]
RAW.mult_dec' [lemma, in Ergo.CPolynoms]
RAW.mult_spec'_intro [constructor, in Ergo.CPolynoms]
RAW.mult_spec' [inductive, in Ergo.CPolynoms]
RAW.mult_dec [lemma, in Ergo.CPolynoms]
RAW.mult_spec_intro [constructor, in Ergo.CPolynoms]
RAW.mult_spec [inductive, in Ergo.CPolynoms]
RAW.mult_m [instance, in Ergo.CPolynoms]
RAW.OrderedType [section, in Ergo.LLazy]
RAW.padd_m [instance, in Ergo.CPolynoms]
RAW.pinterp [definition, in Ergo.LLazy]
RAW.poly [definition, in Ergo.CPolynoms]
RAW.poly_OT [definition, in Ergo.CPolynoms]
RAW.Pq [definition, in Ergo.CPolynoms]
RAW.proxy [variable, in Ergo.LLazy]
RAW.Proxy [constructor, in Ergo.LLazy]
RAW.Pz [definition, in Ergo.CPolynoms]
RAW.P0 [definition, in Ergo.CPolynoms]
RAW.P1 [definition, in Ergo.CPolynoms]
RAW.remove_m [instance, in Ergo.CPolynoms]
RAW.size [definition, in Ergo.LLazy]
RAW.Size [section, in Ergo.LLazy]
RAW.size_expand [lemma, in Ergo.LLazy]
RAW.size_pos [lemma, in Ergo.LLazy]
RAW.size_m [lemma, in Ergo.LLazy]
RAW.sub [definition, in Ergo.CPolynoms]
RAW.sub_equiv [instance, in Ergo.CPolynoms]
RAW.sub_dec' [lemma, in Ergo.CPolynoms]
RAW.sub_spec'_intro [constructor, in Ergo.CPolynoms]
RAW.sub_spec' [inductive, in Ergo.CPolynoms]
RAW.sub_dec [lemma, in Ergo.CPolynoms]
RAW.sub_spec_intro [constructor, in Ergo.CPolynoms]
RAW.sub_spec [inductive, in Ergo.CPolynoms]
RAW.sub_m [instance, in Ergo.CPolynoms]
RAW.t [definition, in Ergo.LLazy]
RAW.t_ [inductive, in Ergo.LLazy]
RAW.vars_of [definition, in Ergo.CPolynoms]
RAW.Wf [record, in Ergo.CPolynoms]
RAW.wf_equiv_iff [lemma, in Ergo.CPolynoms]
RAW.Wf_div [instance, in Ergo.CPolynoms]
RAW.Wf_sub [instance, in Ergo.CPolynoms]
RAW.Wf_add [instance, in Ergo.CPolynoms]
RAW.Wf_add_monome [instance, in Ergo.CPolynoms]
RAW.Wf_addk [instance, in Ergo.CPolynoms]
RAW.Wf_addk_m [lemma, in Ergo.CPolynoms]
RAW.Wf_cancel [instance, in Ergo.CPolynoms]
RAW.Wf_add_const [instance, in Ergo.CPolynoms]
RAW.Wf_mult [instance, in Ergo.CPolynoms]
RAW.Wf_embed [instance, in Ergo.CPolynoms]
RAW.Wf_Pq [instance, in Ergo.CPolynoms]
RAW.Wf_Pz [instance, in Ergo.CPolynoms]
RAW.Wf_P1 [instance, in Ergo.CPolynoms]
RAW.Wf_P0 [instance, in Ergo.CPolynoms]
RAW.Wf_p [projection, in Ergo.CPolynoms]
RAW.WithVars [section, in Ergo.CPolynoms]
RAW.WithVars.vars [variable, in Ergo.CPolynoms]
rb [projection, in Ergo.Ergo]
replace [lemma, in Ergo.Term]
replace' [lemma, in Ergo.Term]
reprs [definition, in Ergo.Uf]
reprs_merge' [lemma, in Ergo.Uf]
reprs_merge [lemma, in Ergo.Uf]
reprs_add_2 [lemma, in Ergo.Uf]
reprs_add_1 [lemma, in Ergo.Uf]
reprs_empty [lemma, in Ergo.Uf]
reprs_mem [lemma, in Ergo.Uf]
Reverse_Induction.A [variable, in Ergo.FoldProps]
Reverse_Induction [section, in Ergo.FoldProps]
rev_rec [lemma, in Ergo.FoldProps]
rev_list_rec [lemma, in Ergo.FoldProps]
Rn [definition, in Generators]
room_mate [definition, in Generators]
rowProd_inv [lemma, in Ergo.DiagProd]
Rz [definition, in Ergo.TheoryArith]
R_OT [definition, in Ergo.TheoryArith]
R_OT [projection, in Ergo.Theory]
R0 [definition, in Ergo.TheoryArith]
r1 [abbreviation, in Ergo.TheoryArith]
R1 [definition, in Ergo.TheoryArith]
r2 [abbreviation, in Ergo.TheoryArith]

S

S [module, in Ergo.AllInstances]
safe [definition, in GeneratorsNG]
safe [definition, in Generators]
sane [definition, in GeneratorsNG]
sane [definition, in Generators]
sane_aux [definition, in GeneratorsNG]
sane_aux_2 [definition, in GeneratorsNG]
sane_aux [definition, in Generators]
sane_aux_2 [definition, in Generators]
SAT [module, in Ergo.Sat]
Sat [library]
SATCAML [module, in Ergo.SatCaml]
SatCaml [library]
SATCAML.bcp [definition, in Ergo.SatCaml]
SATCAML.BCP [section, in Ergo.SatCaml]
SATCAML.bcpNone [constructor, in Ergo.SatCaml]
SATCAML.bcpRes [inductive, in Ergo.SatCaml]
SATCAML.bcpSome [constructor, in Ergo.SatCaml]
SATCAML.bcp_complete [lemma, in Ergo.SatCaml]
SATCAML.bcp_monotonic_env [lemma, in Ergo.SatCaml]
SATCAML.bcp_consistent [lemma, in Ergo.SatCaml]
SATCAML.bcp_progress [lemma, in Ergo.SatCaml]
SATCAML.bcp_unsat [lemma, in Ergo.SatCaml]
SATCAML.bcp_correct [lemma, in Ergo.SatCaml]
SATCAML.compatible_e [definition, in Ergo.SatCaml]
SATCAML.dpll [definition, in Ergo.SatCaml]
SATCAML.dpll_correct [lemma, in Ergo.SatCaml]
SATCAML.expand_nonrec_2 [lemma, in Ergo.SatCaml]
SATCAML.expand_nonrec [lemma, in Ergo.SatCaml]
SATCAML.extend [definition, in Ergo.SatCaml]
SATCAML.llsize_app [lemma, in Ergo.SatCaml]
SATCAML.ll2s [definition, in Ergo.SatCaml]
SATCAML.ll2s_map_elements [lemma, in Ergo.SatCaml]
SATCAML.ll2s_expand [lemma, in Ergo.SatCaml]
SATCAML.ll2s_cfl [lemma, in Ergo.SatCaml]
SATCAML.ll2s_app [lemma, in Ergo.SatCaml]
SATCAML.lsize_pos [lemma, in Ergo.SatCaml]
SATCAML.l2s [definition, in Ergo.SatCaml]
SATCAML.l2s_elements [lemma, in Ergo.SatCaml]
SATCAML.l2s_Subset [lemma, in Ergo.SatCaml]
SATCAML.l2s_iff [lemma, in Ergo.SatCaml]
SATCAML.proof_search_sat [lemma, in Ergo.SatCaml]
SATCAML.proof_search_unsat [lemma, in Ergo.SatCaml]
SATCAML.proof_search [definition, in Ergo.SatCaml]
SATCAML.redNone [constructor, in Ergo.SatCaml]
SATCAML.redRes [inductive, in Ergo.SatCaml]
SATCAML.redSome [constructor, in Ergo.SatCaml]
SATCAML.reduce [definition, in Ergo.SatCaml]
SATCAML.Reduce [section, in Ergo.SatCaml]
SATCAML.reduce_complete [lemma, in Ergo.SatCaml]
SATCAML.reduce_correct [lemma, in Ergo.SatCaml]
SATCAML.reduce_spec [lemma, in Ergo.SatCaml]
SATCAML.reduce_redNone [constructor, in Ergo.SatCaml]
SATCAML.reduce_redSome [constructor, in Ergo.SatCaml]
SATCAML.reduce_spec_ [inductive, in Ergo.SatCaml]
SATCAML.Reduce.D [variable, in Ergo.SatCaml]
SATCAML.Reduce.G [variable, in Ergo.SatCaml]
SATCAML.remove_union [lemma, in Ergo.SatCaml]
SATCAML.remove_transpose [lemma, in Ergo.SatCaml]
SATCAML.Res [inductive, in Ergo.SatCaml]
SATCAML.S [module, in Ergo.SatCaml]
SATCAML.Sat [constructor, in Ergo.SatCaml]
SATCAML.SemF [module, in Ergo.SatCaml]
SATCAML.submodel_e [definition, in Ergo.SatCaml]
SATCAML.union_remove [lemma, in Ergo.SatCaml]
SATCAML.Unsat [constructor, in Ergo.SatCaml]
SATCAML.weak_assume [lemma, in Ergo.SatCaml]
_ |- _ [notation, in Ergo.SatCaml]
SAT.AAssume [constructor, in Ergo.Sat]
SAT.AConflict [constructor, in Ergo.Sat]
SAT.AElim [constructor, in Ergo.Sat]
SAT.ARed [constructor, in Ergo.Sat]
SAT.AStrongRed [lemma, in Ergo.Sat]
SAT.AUnsat [constructor, in Ergo.Sat]
SAT.cfl_expand_m [lemma, in Ergo.Sat]
SAT.compat_unitary [instance, in Ergo.Sat]
SAT.compat_red [instance, in Ergo.Sat]
SAT.compat_mem2 [instance, in Ergo.Sat]
SAT.compat_elim [instance, in Ergo.Sat]
SAT.compat_mem [instance, in Ergo.Sat]
SAT.csize [definition, in Ergo.Sat]
SAT.csize_in [lemma, in Ergo.Sat]
SAT.csize_acc_ge [lemma, in Ergo.Sat]
SAT.csize_lt_compat [lemma, in Ergo.Sat]
SAT.csize_monotonic [lemma, in Ergo.Sat]
SAT.csize_acc [lemma, in Ergo.Sat]
SAT.C_csize [instance, in Ergo.Sat]
SAT.C_lsize [instance, in Ergo.Sat]
SAT.D [projection, in Ergo.Sat]
SAT.derivable [inductive, in Ergo.Sat]
SAT.derivable_morphism [instance, in Ergo.Sat]
SAT.derivable_m [lemma, in Ergo.Sat]
SAT.dpll [definition, in Ergo.Sat]
SAT.dpll_correct [lemma, in Ergo.Sat]
SAT.eliminable [definition, in Ergo.Sat]
SAT.EnvF [module, in Ergo.Sat]
SAT.eq_Seq_m [instance, in Ergo.Sat]
SAT.eq_Seq_Equivalence [instance, in Ergo.Sat]
SAT.eq_Seq [definition, in Ergo.Sat]
SAT.expand_models [lemma, in Ergo.Sat]
SAT.Filtering [section, in Ergo.Sat]
SAT.Filtering.D [variable, in Ergo.Sat]
SAT.Filtering.Finding [section, in Ergo.Sat]
SAT.Filtering.Finding.compatf [variable, in Ergo.Sat]
SAT.Filtering.Finding.f [variable, in Ergo.Sat]
SAT.Filtering.G [variable, in Ergo.Sat]
SAT.find [definition, in Ergo.Sat]
SAT.find_3 [lemma, in Ergo.Sat]
SAT.find_2 [lemma, in Ergo.Sat]
SAT.find_1 [lemma, in Ergo.Sat]
SAT.G [projection, in Ergo.Sat]
SAT.incompatible [definition, in Ergo.Sat]
SAT.lsize [definition, in Ergo.Sat]
SAT.lsize_acc [lemma, in Ergo.Sat]
SAT.lsize_lt_compat [lemma, in Ergo.Sat]
SAT.lsize_monotonic [lemma, in Ergo.Sat]
SAT.Measure [section, in Ergo.Sat]
SAT.mk_sequent [constructor, in Ergo.Sat]
SAT.model_expand [definition, in Ergo.Sat]
SAT.proof_search_sat [lemma, in Ergo.Sat]
SAT.proof_search_unsat [lemma, in Ergo.Sat]
SAT.proof_search [definition, in Ergo.Sat]
SAT.reducible [definition, in Ergo.Sat]
SAT.Res [inductive, in Ergo.Sat]
SAT.Sat [constructor, in Ergo.Sat]
SAT.sat_goal_e [definition, in Ergo.Sat]
SAT.sat_clause_e [definition, in Ergo.Sat]
SAT.select [definition, in Ergo.Sat]
SAT.SemF [module, in Ergo.Sat]
SAT.sequent [record, in Ergo.Sat]
SAT.size [definition, in Ergo.Sat]
SAT.size_right_unsat_dec [lemma, in Ergo.Sat]
SAT.size_left_unsat_dec [lemma, in Ergo.Sat]
SAT.size_assume_dec [lemma, in Ergo.Sat]
SAT.size_expand [lemma, in Ergo.Sat]
SAT.size_union [lemma, in Ergo.Sat]
SAT.size_red_dec [lemma, in Ergo.Sat]
SAT.size_elim_dec [lemma, in Ergo.Sat]
SAT.size_add [lemma, in Ergo.Sat]
SAT.size_in [lemma, in Ergo.Sat]
SAT.size_m [lemma, in Ergo.Sat]
SAT.soundness [lemma, in Ergo.Sat]
SAT.submodel_add [lemma, in Ergo.Sat]
SAT.sub_sequent [definition, in Ergo.Sat]
SAT.T_csize [lemma, in Ergo.Sat]
SAT.T_lsize [lemma, in Ergo.Sat]
SAT.unitary [definition, in Ergo.Sat]
SAT.unitary_singl [lemma, in Ergo.Sat]
SAT.Unsat [constructor, in Ergo.Sat]
SAT.weakening [lemma, in Ergo.Sat]
SAT.Weakening [section, in Ergo.Sat]
SAT.wf_expand [definition, in Ergo.Sat]
SAT.wf_context [definition, in Ergo.Sat]
_ |- _ [notation, in Ergo.Sat]
SCaml [module, in Ergo.AllInstances]
SCamlN [module, in Ergo.AllInstances]
SCamlN.E [module, in Ergo.AllInstances]
SCaml.E [module, in Ergo.AllInstances]
schwicht [definition, in Generators]
SEMANTICS [module, in Ergo.Semantics]
Semantics [library]
SEMANTICS.consistent [definition, in Ergo.Semantics]
SEMANTICS.Creation [section, in Ergo.Semantics]
SEMANTICS.Creation.Hconsistent [variable, in Ergo.Semantics]
SEMANTICS.Creation.Hexpand [variable, in Ergo.Semantics]
SEMANTICS.Creation.Hfull [variable, in Ergo.Semantics]
SEMANTICS.Creation.Hmorphism [variable, in Ergo.Semantics]
SEMANTICS.Creation.Htrue [variable, in Ergo.Semantics]
SEMANTICS.Creation.m [variable, in Ergo.Semantics]
SEMANTICS.full [definition, in Ergo.Semantics]
SEMANTICS.incompatible [definition, in Ergo.Semantics]
SEMANTICS.mk_model [constructor, in Ergo.Semantics]
SEMANTICS.model [definition, in Ergo.Semantics]
SEMANTICS.model_as_model_of [lemma, in Ergo.Semantics]
SEMANTICS.model_of [definition, in Ergo.Semantics]
SEMANTICS.model_as_fun [definition, in Ergo.Semantics]
SEMANTICS.model_with_props [record, in Ergo.Semantics]
SEMANTICS.model_ [definition, in Ergo.Semantics]
SEMANTICS.morphism [definition, in Ergo.Semantics]
SEMANTICS.sat_goal_p [definition, in Ergo.Semantics]
SEMANTICS.sat_clause_p [definition, in Ergo.Semantics]
SEMANTICS.sat_goal [definition, in Ergo.Semantics]
SEMANTICS.sat_clause [definition, in Ergo.Semantics]
SEMANTICS.submodel [definition, in Ergo.Semantics]
SEMANTICS.this [projection, in Ergo.Semantics]
SEMANTICS.this_expand [projection, in Ergo.Semantics]
SEMANTICS.this_true [projection, in Ergo.Semantics]
SEMANTICS.this_m [projection, in Ergo.Semantics]
SEMANTICS.this_wf [projection, in Ergo.Semantics]
SEMANTICS.this_full [projection, in Ergo.Semantics]
SEMANTICS.WF [module, in Ergo.Semantics]
SEMANTICS.wf_expand [definition, in Ergo.Semantics]
SEMANTICS.wf_true [definition, in Ergo.Semantics]
SEMANTICS.WF.consistent [definition, in Ergo.Semantics]
SEMANTICS.WF.full [definition, in Ergo.Semantics]
SEMANTICS.WF.morphism [definition, in Ergo.Semantics]
SEMANTICS.WF.wf_expand [definition, in Ergo.Semantics]
SEMANTICS.WF.wf_true [definition, in Ergo.Semantics]
SemFacts [module, in Ergo.Semantics]
SemFacts.model_expand [lemma, in Ergo.Semantics]
SemFacts.model_true [lemma, in Ergo.Semantics]
SemFacts.model_full [lemma, in Ergo.Semantics]
SemFacts.model_em [lemma, in Ergo.Semantics]
SemFacts.model_m [lemma, in Ergo.Semantics]
SemFacts.submodel_empty [lemma, in Ergo.Semantics]
SEMLAZY [module, in Ergo.SemLazy]
SemLazy [library]
SEMLAZY.consistent [lemma, in Ergo.SemLazy]
SEMLAZY.disequation [definition, in Ergo.SemLazy]
SEMLAZY.entails [definition, in Ergo.SemLazy]
SEMLAZY.equation [definition, in Ergo.SemLazy]
SEMLAZY.full [lemma, in Ergo.SemLazy]
SEMLAZY.incompatible [definition, in Ergo.SemLazy]
SEMLAZY.model [definition, in Ergo.SemLazy]
SEMLAZY.models_eq_congr [lemma, in Ergo.SemLazy]
SEMLAZY.models_list_in [lemma, in Ergo.SemLazy]
SEMLAZY.models_list_iff [definition, in Ergo.SemLazy]
SEMLAZY.models_list_cons [constructor, in Ergo.SemLazy]
SEMLAZY.models_list_nil [constructor, in Ergo.SemLazy]
SEMLAZY.models_list [inductive, in Ergo.SemLazy]
SEMLAZY.models_neq_sym [lemma, in Ergo.SemLazy]
SEMLAZY.models_neq_irrefl [lemma, in Ergo.SemLazy]
SEMLAZY.models_eq_trans [lemma, in Ergo.SemLazy]
SEMLAZY.models_eq_sym [lemma, in Ergo.SemLazy]
SEMLAZY.models_eq_refl [lemma, in Ergo.SemLazy]
SEMLAZY.models_neq_iff [lemma, in Ergo.SemLazy]
SEMLAZY.models_eq_iff [lemma, in Ergo.SemLazy]
SEMLAZY.models_neq [definition, in Ergo.SemLazy]
SEMLAZY.models_eq [definition, in Ergo.SemLazy]
SEMLAZY.model_as_fun [definition, in Ergo.SemLazy]
SEMLAZY.model_as_fun_l [definition, in Ergo.SemLazy]
SEMLAZY.morphism [lemma, in Ergo.SemLazy]
SEMLAZY.sat_goal_p [definition, in Ergo.SemLazy]
SEMLAZY.sat_clause_p [definition, in Ergo.SemLazy]
SEMLAZY.sat_goal [definition, in Ergo.SemLazy]
SEMLAZY.sat_clause [definition, in Ergo.SemLazy]
SEMLAZY.submodel [definition, in Ergo.SemLazy]
SEMLAZY.wf_expand [lemma, in Ergo.SemLazy]
SEMLAZY.wf_expand_lift [lemma, in Ergo.SemLazy]
SEMLAZY.wf_expand_ [lemma, in Ergo.SemLazy]
SEMLAZY.wf_true [lemma, in Ergo.SemLazy]
_ |- _ = _ (sem_scope) [notation, in Ergo.SemLazy]
_ |= _ <> _ (sem_scope) [notation, in Ergo.SemLazy]
_ |= _ = _ (sem_scope) [notation, in Ergo.SemLazy]
_ :> _ [notation, in Ergo.SemLazy]
_ [ _ ] [notation, in Ergo.SemLazy]
SEM_INTERFACE.sat_goal_p [definition, in Ergo.Semantics]
SEM_INTERFACE.sat_clause_p [definition, in Ergo.Semantics]
SEM_INTERFACE.incompatible [definition, in Ergo.Semantics]
SEM_INTERFACE.submodel [definition, in Ergo.Semantics]
SEM_INTERFACE.sat_goal [definition, in Ergo.Semantics]
SEM_INTERFACE.sat_clause [definition, in Ergo.Semantics]
SEM_INTERFACE.wf_expand [axiom, in Ergo.Semantics]
SEM_INTERFACE.wf_true [axiom, in Ergo.Semantics]
SEM_INTERFACE.morphism [axiom, in Ergo.Semantics]
SEM_INTERFACE.consistent [axiom, in Ergo.Semantics]
SEM_INTERFACE.full [axiom, in Ergo.Semantics]
SEM_INTERFACE.WF.M [variable, in Ergo.Semantics]
SEM_INTERFACE.WF [section, in Ergo.Semantics]
SEM_INTERFACE.model_as_fun [axiom, in Ergo.Semantics]
SEM_INTERFACE.model [axiom, in Ergo.Semantics]
SEM_INTERFACE [module, in Ergo.Semantics]
separate [definition, in Ergo.Diff]
separate_conservative [lemma, in Ergo.Diff]
SetFoldInd [module, in Ergo.FoldProps]
SetFoldInd.fold_rel [lemma, in Ergo.FoldProps]
SetFoldInd.fold_relation.Hstep [variable, in Ergo.FoldProps]
SetFoldInd.fold_relation.Hi [variable, in Ergo.FoldProps]
SetFoldInd.fold_relation.s [variable, in Ergo.FoldProps]
SetFoldInd.fold_relation.i2 [variable, in Ergo.FoldProps]
SetFoldInd.fold_relation.i1 [variable, in Ergo.FoldProps]
SetFoldInd.fold_relation.f2 [variable, in Ergo.FoldProps]
SetFoldInd.fold_relation.f1 [variable, in Ergo.FoldProps]
SetFoldInd.fold_relation.R [variable, in Ergo.FoldProps]
SetFoldInd.fold_relation.Acc2 [variable, in Ergo.FoldProps]
SetFoldInd.fold_relation.Acc1 [variable, in Ergo.FoldProps]
SetFoldInd.fold_relation.A [variable, in Ergo.FoldProps]
SetFoldInd.fold_relation [section, in Ergo.FoldProps]
SetFoldInd.fold_ind2 [lemma, in Ergo.FoldProps]
SetFoldInd.fold_ind [lemma, in Ergo.FoldProps]
SetFoldInd.fold_ind_aux [lemma, in Ergo.FoldProps]
SetFoldInd.fold_induction.Hstep [variable, in Ergo.FoldProps]
SetFoldInd.fold_induction.Hi [variable, in Ergo.FoldProps]
SetFoldInd.fold_induction.P_m [variable, in Ergo.FoldProps]
SetFoldInd.fold_induction.s [variable, in Ergo.FoldProps]
SetFoldInd.fold_induction.i [variable, in Ergo.FoldProps]
SetFoldInd.fold_induction.f [variable, in Ergo.FoldProps]
SetFoldInd.fold_induction.P [variable, in Ergo.FoldProps]
SetFoldInd.fold_induction.A [variable, in Ergo.FoldProps]
SetFoldInd.fold_induction [section, in Ergo.FoldProps]
SetFoldInd.Hli [lemma, in Ergo.FoldProps]
SetFoldInd.Pl [definition, in Ergo.FoldProps]
SetFoldInd.set_of_list [definition, in Ergo.FoldProps]
SetFoldInd.sofl_1 [lemma, in Ergo.FoldProps]
SExample [section, in Generators]
shankar_01 [lemma, in Demo]
shankar_01 [lemma, in AltDemo]
simple_congr_congruence [lemma, in Demo]
simple_congr [lemma, in Demo]
simple_congr_congruence [lemma, in AltDemo]
simple_congr [lemma, in AltDemo]
size [definition, in Ergo.CNFLazyN]
SN [module, in Ergo.AllInstances]
SN.E [module, in Ergo.AllInstances]
Solution [inductive, in Ergo.Theory]
solution_eq_Equiv [instance, in Ergo.Theory]
solution_eq_trans [lemma, in Ergo.Theory]
solution_eq_sym [lemma, in Ergo.Theory]
solution_eq_refl [lemma, in Ergo.Theory]
solution_eq_Subst [constructor, in Ergo.Theory]
solution_eq_Unsolvable [constructor, in Ergo.Theory]
solution_eq_Solved [constructor, in Ergo.Theory]
solution_eq [inductive, in Ergo.Theory]
Solution_OT [section, in Ergo.Theory]
solve [definition, in Ergo.TheoryArith]
solve [projection, in Ergo.Theory]
Solved [constructor, in Ergo.Theory]
solved_iff [lemma, in Ergo.TheoryArith]
solve_dec [lemma, in Ergo.TheoryArith]
solve_basic_dec [lemma, in Ergo.TheoryArith]
solve_basic_Subst [constructor, in Ergo.TheoryArith]
solve_basic_Unsolvable [constructor, in Ergo.TheoryArith]
solve_basic_Solved [constructor, in Ergo.TheoryArith]
solve_basic_spec [inductive, in Ergo.TheoryArith]
solve_m [instance, in Ergo.TheoryArith]
solve_trivial [lemma, in Ergo.Theory]
solve_dec [projection, in Ergo.Theory]
solve_m [projection, in Ergo.Theory]
solve_specs_Subst [constructor, in Ergo.Theory]
solve_specs_Unsolvable [constructor, in Ergo.Theory]
solve_specs_Solved [constructor, in Ergo.Theory]
solve_specs [inductive, in Ergo.Theory]
some_are_equal [definition, in GeneratorsNG]
some_are_equal [definition, in Generators]
stripR [definition, in Ergo.TheoryArith]
submodel_eq_In [lemma, in Ergo.CCX]
submodel_cons_neq [constructor, in Ergo.CCX]
submodel_cons_eq [constructor, in Ergo.CCX]
submodel_nil [constructor, in Ergo.CCX]
submodel_eq [inductive, in Ergo.CCX]
subst [definition, in Ergo.TheoryArith]
subst [projection, in Ergo.Theory]
Subst [constructor, in Ergo.Theory]
subst_idem [lemma, in Ergo.TheoryArith]
subst_idem_2 [lemma, in Ergo.TheoryArith]
subst_idem_1 [lemma, in Ergo.TheoryArith]
subst_as_addk [lemma, in Ergo.TheoryArith]
subst_linear [lemma, in Ergo.TheoryArith]
subst_full_dec [lemma, in Ergo.TheoryArith]
subst_spec_other [constructor, in Ergo.TheoryArith]
subst_spec_normal [constructor, in Ergo.TheoryArith]
subst_full_spec [inductive, in Ergo.TheoryArith]
subst_dec [lemma, in Ergo.TheoryArith]
subst_spec_intro [constructor, in Ergo.TheoryArith]
subst_spec [inductive, in Ergo.TheoryArith]
subst_m [instance, in Ergo.TheoryArith]
subst_m [projection, in Ergo.Theory]
sub_as_addk [lemma, in Ergo.TheoryArith]
symbol [inductive, in Ergo.Term]
symbol_equal [definition, in Ergo.Term]
symbol_OT [definition, in Ergo.TermUtils]
symbol_UOT [instance, in Ergo.TermUtils]
symbol_cmp_spec [lemma, in Ergo.TermUtils]
symbol_cmp [definition, in Ergo.TermUtils]
symbol_StrictOrder [definition, in Ergo.TermUtils]
symbol_lt_irrefl [lemma, in Ergo.TermUtils]
symbol_lt_trans [lemma, in Ergo.TermUtils]
symbol_lt_Op_2 [constructor, in Ergo.TermUtils]
symbol_lt_Op_1 [constructor, in Ergo.TermUtils]
symbol_lt_Cst_Op [constructor, in Ergo.TermUtils]
symbol_lt_Q_1 [constructor, in Ergo.TermUtils]
symbol_lt_Z_Q [constructor, in Ergo.TermUtils]
symbol_lt_Z_1 [constructor, in Ergo.TermUtils]
symbol_lt_Pos_Q [constructor, in Ergo.TermUtils]
symbol_lt_Pos_Z [constructor, in Ergo.TermUtils]
symbol_lt_Pos_1 [constructor, in Ergo.TermUtils]
symbol_lt_N_Q [constructor, in Ergo.TermUtils]
symbol_lt_N_Z [constructor, in Ergo.TermUtils]
symbol_lt_N_Pos [constructor, in Ergo.TermUtils]
symbol_lt_N_1 [constructor, in Ergo.TermUtils]
symbol_lt_Nat_Q [constructor, in Ergo.TermUtils]
symbol_lt_Nat_Z [constructor, in Ergo.TermUtils]
symbol_lt_Nat_Pos [constructor, in Ergo.TermUtils]
symbol_lt_Nat_N [constructor, in Ergo.TermUtils]
symbol_lt_Nat_1 [constructor, in Ergo.TermUtils]
symbol_lt_Unint_Op [constructor, in Ergo.TermUtils]
symbol_lt_Unint_Cst [constructor, in Ergo.TermUtils]
symbol_lt_Unint_2 [constructor, in Ergo.TermUtils]
symbol_lt_Unint_1 [constructor, in Ergo.TermUtils]
symbol_lt [inductive, in Ergo.TermUtils]
Symbol_as_UOT.Arithop_as_UOT [section, in Ergo.TermUtils]
Symbol_as_UOT.ArithDomain_as_UOT [section, in Ergo.TermUtils]
Symbol_as_UOT [section, in Ergo.TermUtils]
S.E [module, in Ergo.AllInstances]
s1 [definition, in Generators]
s10 [definition, in Generators]
s2 [definition, in Generators]
s30 [definition, in Generators]

T

t [definition, in Ergo.Use]
t [abbreviation, in Ergo.TheoryArith]
t [definition, in Ergo.Uf]
t [definition, in Ergo.Diff]
Tac [module, in Ergo.AllInstances]
TacCaml [module, in Ergo.AllInstances]
TacCamlN [module, in Ergo.AllInstances]
TacN [module, in Ergo.AllInstances]
TacticLazy [library]
TAnd [constructor, in Ergo.Ergo]
tcons [abbreviation, in Ergo.Term]
tdiv [definition, in Ergo.ModelsRingExt]
tequal [definition, in Ergo.Term]
tequal_iff [lemma, in Ergo.Term]
tequal_2 [lemma, in Ergo.Term]
tequal_1 [lemma, in Ergo.Term]
term [inductive, in Ergo.Term]
Term [library]
TermInduction [section, in Ergo.Term]
TermInduction.Hcons [variable, in Ergo.Term]
TermInduction.Hlift [variable, in Ergo.Term]
TermInduction.Hnil [variable, in Ergo.Term]
TermInduction.P [variable, in Ergo.Term]
TermInduction.P0 [variable, in Ergo.Term]
TermMutualInduction [section, in Ergo.TermUtils]
TermMutualInduction.Happ [variable, in Ergo.TermUtils]
TermMutualInduction.Hcons [variable, in Ergo.TermUtils]
TermMutualInduction.Hnil [variable, in Ergo.TermUtils]
TermMutualInduction.P [variable, in Ergo.TermUtils]
TermMutualInduction.Pl [variable, in Ergo.TermUtils]
terms [abbreviation, in Ergo.Term]
terms_of_merge [lemma, in Ergo.Use]
terms_of_find [lemma, in Ergo.Use]
terms_of_empty [lemma, in Ergo.Use]
terms_of_iff [lemma, in Ergo.Use]
terms_of [definition, in Ergo.Use]
terms_OT [definition, in Ergo.TermUtils]
terms_UOT [instance, in Ergo.TermUtils]
terms_lt_trans [definition, in Ergo.TermUtils]
terms_lt_not_eq [lemma, in Ergo.TermUtils]
terms_lt [definition, in Ergo.TermUtils]
TermUtils [library]
term_of_R_add_const [lemma, in Ergo.TheoryArith]
term_of_R_add_monome [lemma, in Ergo.TheoryArith]
term_of_R_cancel [lemma, in Ergo.TheoryArith]
term_of_R_sub [lemma, in Ergo.TheoryArith]
term_of_R_add [lemma, in Ergo.TheoryArith]
term_of_R_mult [lemma, in Ergo.TheoryArith]
term_of_R_addk [lemma, in Ergo.TheoryArith]
term_of_R_embed [lemma, in Ergo.TheoryArith]
term_of_R_Pq [lemma, in Ergo.TheoryArith]
term_of_R_P1 [lemma, in Ergo.TheoryArith]
term_of_R_P0 [lemma, in Ergo.TheoryArith]
term_of_R_m [instance, in Ergo.TheoryArith]
term_of_R [definition, in Ergo.TheoryArith]
term_env [definition, in Ergo.Term]
term_equal_2 [axiom, in Ergo.Term]
term_equal_1 [axiom, in Ergo.Term]
term_equal [definition, in Ergo.Term]
term_terms_rect [definition, in Ergo.Term]
term_OT [definition, in Ergo.TermUtils]
term_UOT [instance, in Ergo.TermUtils]
term_lt_trans [definition, in Ergo.TermUtils]
term_terms_lt_trans [lemma, in Ergo.TermUtils]
term_lt_not_eq [lemma, in Ergo.TermUtils]
term_lt [definition, in Ergo.TermUtils]
term_terms_rect_default [definition, in Ergo.TermUtils]
term_mutual_ind [lemma, in Ergo.TermUtils]
Test [section, in Ergo.TheoryArith]
Test [module, in Ergo.Term]
TestErgo [library]
TestsDeCCXA [module, in Ergo.CCX]
TestsDeCCXA.a [abbreviation, in Ergo.CCX]
TestsDeCCXA.b [abbreviation, in Ergo.CCX]
TestsDeCCXA.bottom [abbreviation, in Ergo.CCX]
TestsDeCCXA.c [abbreviation, in Ergo.CCX]
TestsDeCCXA.e [definition, in Ergo.CCX]
TestsDeCCXA.ea1 [definition, in Ergo.CCX]
TestsDeCCXA.ea2 [definition, in Ergo.CCX]
TestsDeCCXA.ea2' [definition, in Ergo.CCX]
TestsDeCCXA.ea2'' [definition, in Ergo.CCX]
TestsDeCCXA.ea2''' [definition, in Ergo.CCX]
TestsDeCCXA.ea2'''' [definition, in Ergo.CCX]
TestsDeCCXA.ea2''''' [definition, in Ergo.CCX]
TestsDeCCXA.error [axiom, in Ergo.CCX]
TestsDeCCXA.e1 [definition, in Ergo.CCX]
TestsDeCCXA.e1' [definition, in Ergo.CCX]
TestsDeCCXA.e1'' [definition, in Ergo.CCX]
TestsDeCCXA.e2 [definition, in Ergo.CCX]
TestsDeCCXA.e3 [definition, in Ergo.CCX]
TestsDeCCXA.f [abbreviation, in Ergo.CCX]
TestsDeCCXA.fa [abbreviation, in Ergo.CCX]
TestsDeCCXA.fb [abbreviation, in Ergo.CCX]
TestsDeCCXA.fc [abbreviation, in Ergo.CCX]
TestsDeCCXA.f2a [abbreviation, in Ergo.CCX]
TestsDeCCXA.f3a [abbreviation, in Ergo.CCX]
TestsDeCCXA.f4a [abbreviation, in Ergo.CCX]
TestsDeCCXA.f5a [abbreviation, in Ergo.CCX]
TestsDeCCXA.g [abbreviation, in Ergo.CCX]
TestsDeCCXA.ga [abbreviation, in Ergo.CCX]
TestsDeCCXA.gb [abbreviation, in Ergo.CCX]
TestsDeCCXA.gc [abbreviation, in Ergo.CCX]
TestsDeCCXA.one [abbreviation, in Ergo.CCX]
TestsDeCCXA.strip [definition, in Ergo.CCX]
TestsDeCCXA.stripR [definition, in Ergo.CCX]
TestsDeCCXA.ta [abbreviation, in Ergo.CCX]
TestsDeCCXA.tb [abbreviation, in Ergo.CCX]
TestsDeCCXA.tc [abbreviation, in Ergo.CCX]
TestsDeCCXA.TestNewUse [module, in Ergo.CCX]
TestsDeCCXA.TestNewUse.e1 [definition, in Ergo.CCX]
TestsDeCCXA.TestNewUse.e2 [definition, in Ergo.CCX]
TestsDeCCXA.tfx [abbreviation, in Ergo.CCX]
TestsDeCCXA.tfxzero [abbreviation, in Ergo.CCX]
TestsDeCCXA.tf1 [abbreviation, in Ergo.CCX]
TestsDeCCXA.tone [abbreviation, in Ergo.CCX]
TestsDeCCXA.tx [abbreviation, in Ergo.CCX]
TestsDeCCXA.txzero [abbreviation, in Ergo.CCX]
TestsDeCCXA.tzero [abbreviation, in Ergo.CCX]
TestsDeCCXA.x [abbreviation, in Ergo.CCX]
TestsDeCCXA.zero [abbreviation, in Ergo.CCX]
do _ [notation, in Ergo.CCX]
monome _ [notation, in Ergo.CCX]
TestsDeCCXE [module, in Ergo.CCX]
TestsDeCCXE.a [abbreviation, in Ergo.CCX]
TestsDeCCXE.b [abbreviation, in Ergo.CCX]
TestsDeCCXE.c [abbreviation, in Ergo.CCX]
TestsDeCCXE.e [definition, in Ergo.CCX]
TestsDeCCXE.error [axiom, in Ergo.CCX]
TestsDeCCXE.e1 [definition, in Ergo.CCX]
TestsDeCCXE.e1' [definition, in Ergo.CCX]
TestsDeCCXE.e1'' [definition, in Ergo.CCX]
TestsDeCCXE.e2 [definition, in Ergo.CCX]
TestsDeCCXE.e3 [definition, in Ergo.CCX]
TestsDeCCXE.f [abbreviation, in Ergo.CCX]
TestsDeCCXE.fa [abbreviation, in Ergo.CCX]
TestsDeCCXE.fb [abbreviation, in Ergo.CCX]
TestsDeCCXE.fc [abbreviation, in Ergo.CCX]
TestsDeCCXE.f2a [abbreviation, in Ergo.CCX]
TestsDeCCXE.f3a [abbreviation, in Ergo.CCX]
TestsDeCCXE.f4a [abbreviation, in Ergo.CCX]
TestsDeCCXE.f5a [abbreviation, in Ergo.CCX]
TestsDeCCXE.g [abbreviation, in Ergo.CCX]
TestsDeCCXE.ga [abbreviation, in Ergo.CCX]
TestsDeCCXE.gb [abbreviation, in Ergo.CCX]
TestsDeCCXE.gc [abbreviation, in Ergo.CCX]
TestsDeCCXE.strip [definition, in Ergo.CCX]
TestsDeCCXE.ta [abbreviation, in Ergo.CCX]
TestsDeCCXE.tb [abbreviation, in Ergo.CCX]
TestsDeCCXE.tc [abbreviation, in Ergo.CCX]
TestsDeCCXE.TestNewUse [module, in Ergo.CCX]
TestsDeCCXE.TestNewUse.e1 [definition, in Ergo.CCX]
TestsDeCCXE.TestNewUse.e2 [definition, in Ergo.CCX]
TestsDeCCXE.TestNewUse.e3 [definition, in Ergo.CCX]
do _ [notation, in Ergo.CCX]
TestWithNat [module, in Ergo.Term]
TestWithNat.a [definition, in Ergo.Term]
TestWithNat.anatbool [definition, in Ergo.Term]
TestWithNat.anatbool_x [definition, in Ergo.Term]
TestWithNat.anatnat [definition, in Ergo.Term]
TestWithNat.b [definition, in Ergo.Term]
TestWithNat.bfalse [definition, in Ergo.Term]
TestWithNat.bfalse2 [definition, in Ergo.Term]
TestWithNat.boolx [variable, in Ergo.Term]
TestWithNat.bool_varmap [definition, in Ergo.Term]
TestWithNat.bool_idx [definition, in Ergo.Term]
TestWithNat.btrue [definition, in Ergo.Term]
TestWithNat.bx [definition, in Ergo.Term]
TestWithNat.fx [definition, in Ergo.Term]
TestWithNat.f3x [definition, in Ergo.Term]
TestWithNat.f5x [definition, in Ergo.Term]
TestWithNat.ia [definition, in Ergo.Term]
TestWithNat.ib [definition, in Ergo.Term]
TestWithNat.inbx [definition, in Ergo.Term]
TestWithNat.interp [definition, in Ergo.Term]
TestWithNat.itwo [definition, in Ergo.Term]
TestWithNat.ix [definition, in Ergo.Term]
TestWithNat.izero [definition, in Ergo.Term]
TestWithNat.natbool [variable, in Ergo.Term]
TestWithNat.natnat [variable, in Ergo.Term]
TestWithNat.natx [variable, in Ergo.Term]
TestWithNat.nat_arrow_nat_varmap [definition, in Ergo.Term]
TestWithNat.nat_arrow_bool_varmap [definition, in Ergo.Term]
TestWithNat.nat_varmap [definition, in Ergo.Term]
TestWithNat.nat_arrow_nat_idx [definition, in Ergo.Term]
TestWithNat.nat_arrow_bool_idx [definition, in Ergo.Term]
TestWithNat.nat_idx [definition, in Ergo.Term]
TestWithNat.nx [definition, in Ergo.Term]
TestWithNat.n0 [definition, in Ergo.Term]
TestWithNat.n1 [definition, in Ergo.Term]
TestWithNat.n2 [definition, in Ergo.Term]
TestWithNat.power [definition, in Ergo.Term]
TestWithNat.succ [definition, in Ergo.Term]
TestWithNat.tbool [definition, in Ergo.Term]
TestWithNat.test0 [definition, in Ergo.Term]
TestWithNat.tnat [definition, in Ergo.Term]
TestWithNat.tnat_arrow_nat [definition, in Ergo.Term]
TestWithNat.tnat_arrow_bool [definition, in Ergo.Term]
TestWithNat.two [definition, in Ergo.Term]
TestWithNat.variables [definition, in Ergo.Term]
TestWithNat.vtypes [definition, in Ergo.Term]
TestWithNat.x [definition, in Ergo.Term]
TestWithNat.zero [definition, in Ergo.Term]
[| _ |] [notation, in Ergo.Term]
test_arith_nat_sat [lemma, in Demo]
test_arithZ [lemma, in Demo]
test_arith_nat_sat [lemma, in AltDemo]
test_arithZ [lemma, in AltDemo]
Test.a [definition, in Ergo.Term]
Test.anatbool [definition, in Ergo.Term]
Test.anatbool_x [definition, in Ergo.Term]
Test.anatnat [definition, in Ergo.Term]
Test.b [definition, in Ergo.Term]
Test.bfalse [definition, in Ergo.Term]
Test.bfalse2 [definition, in Ergo.Term]
Test.boolx [variable, in Ergo.Term]
Test.bool_varmap [definition, in Ergo.Term]
Test.bool_idx [definition, in Ergo.Term]
Test.btrue [definition, in Ergo.Term]
Test.bx [definition, in Ergo.Term]
Test.fx [definition, in Ergo.Term]
Test.f3x [definition, in Ergo.Term]
Test.f5x [definition, in Ergo.Term]
Test.ia [definition, in Ergo.Term]
Test.ib [definition, in Ergo.Term]
Test.inbx [definition, in Ergo.Term]
Test.interp [definition, in Ergo.Term]
Test.itwo [definition, in Ergo.Term]
Test.ix [definition, in Ergo.Term]
Test.izero [definition, in Ergo.Term]
Test.natbool [variable, in Ergo.Term]
Test.natnat [variable, in Ergo.Term]
Test.natx [variable, in Ergo.Term]
Test.nat_arrow_nat_varmap [definition, in Ergo.Term]
Test.nat_arrow_bool_varmap [definition, in Ergo.Term]
Test.nat_varmap [definition, in Ergo.Term]
Test.nat_arrow_nat_idx [definition, in Ergo.Term]
Test.nat_arrow_bool_idx [definition, in Ergo.Term]
Test.nat_idx [definition, in Ergo.Term]
Test.nx [definition, in Ergo.Term]
Test.n0 [definition, in Ergo.Term]
Test.n1 [definition, in Ergo.Term]
Test.n2 [definition, in Ergo.Term]
Test.power [definition, in Ergo.Term]
Test.succ [definition, in Ergo.Term]
Test.tbool [definition, in Ergo.Term]
Test.test0 [definition, in Ergo.Term]
Test.tnat [definition, in Ergo.Term]
Test.tnat_arrow_nat [definition, in Ergo.Term]
Test.tnat_arrow_bool [definition, in Ergo.Term]
Test.two [definition, in Ergo.Term]
Test.variables [definition, in Ergo.Term]
Test.vtypes [definition, in Ergo.Term]
Test.x [definition, in Ergo.Term]
Test.zero [definition, in Ergo.Term]
[| _ |] [notation, in Ergo.Term]
TFalse [constructor, in Ergo.Ergo]
THEORY [module, in Ergo.CCX]
Theory [record, in Ergo.Theory]
Theory [library]
TheoryArith [library]
TheorySpecs [record, in Ergo.Theory]
TheorySpecs [section, in Ergo.Theory]
THEORY.Th [instance, in Ergo.CCX]
THEORY.ThSpecs [instance, in Ergo.CCX]
this [projection, in Ergo.Uf]
TIff [constructor, in Ergo.Ergo]
TImp [constructor, in Ergo.Ergo]
tinterp [definition, in Ergo.Term]
TInterp [section, in Ergo.Term]
TInterp.vtypes [variable, in Ergo.Term]
tminus [definition, in Ergo.ModelsRingExt]
tminus [definition, in Ergo.TheoryArith]
tminus_m [instance, in Ergo.TheoryArith]
tmult [definition, in Ergo.ModelsRingExt]
tmult [definition, in Ergo.TheoryArith]
tmult_0_equal [lemma, in Ergo.TheoryArith]
tmult_m [instance, in Ergo.TheoryArith]
tnil [abbreviation, in Ergo.Term]
TNot [constructor, in Ergo.Ergo]
topp [definition, in Ergo.ModelsRingExt]
topp [definition, in Ergo.TheoryArith]
topp_const [lemma, in Ergo.TheoryArith]
topp_m [instance, in Ergo.TheoryArith]
TOr [constructor, in Ergo.Ergo]
touched_spec [lemma, in Ergo.Uf]
tplus [definition, in Ergo.ModelsRingExt]
tplus [definition, in Ergo.TheoryArith]
tplus_0_equal [lemma, in Ergo.TheoryArith]
tplus_m [instance, in Ergo.TheoryArith]
tr1 [abbreviation, in Ergo.TheoryArith]
tr2 [abbreviation, in Ergo.TheoryArith]
TTrue [constructor, in Ergo.Ergo]
TVar [constructor, in Ergo.Ergo]
ty [projection, in Ergo.Ergo]
type [inductive, in Ergo.Term]
typeArith [constructor, in Ergo.Term]
typeArrow [constructor, in Ergo.Term]
TypeasDT [module, in Ergo.Term]
TypeasDT.eq_dec [definition, in Ergo.Term]
TypeasDT.U [definition, in Ergo.Term]
typeBinop [definition, in Ergo.Term]
typeCst [constructor, in Ergo.Term]
typeDefault [constructor, in Ergo.Term]
TypeEqDep [module, in Ergo.Term]
types_of_congr [lemma, in Ergo.Term]
types_of [definition, in Ergo.Term]
typeUnop [definition, in Ergo.Term]
typeZ [definition, in Ergo.ModelsRingExt]
type_of_congr [lemma, in Ergo.Term]
type_of [definition, in Ergo.Term]
type_dec [lemma, in Ergo.Term]
type_env [definition, in Ergo.Term]
t_ [record, in Ergo.Uf]
t0 [abbreviation, in Ergo.TheoryArith]
t1 [abbreviation, in Ergo.TheoryArith]

U

u [abbreviation, in Ergo.TheoryArith]
udeb1 [definition, in Generators]
udeb10 [definition, in Generators]
udeb2 [definition, in Generators]
udeb50 [definition, in Generators]
udeb6 [definition, in Generators]
ude_bruijn [definition, in Generators]
Uf [library]
Unint [constructor, in Ergo.Term]
Unsolvable [constructor, in Ergo.Theory]
unsolvable_iff [lemma, in Ergo.TheoryArith]
Use [library]
using_all [definition, in Ergo.Use]

V

varmaps [record, in Ergo.Ergo]
varmaps_vsy [projection, in Ergo.Ergo]
varmaps_vty [projection, in Ergo.Ergo]
varmaps_lits [projection, in Ergo.Ergo]
VExample [section, in Generators]
vhole [definition, in Generators]
vhole1 [definition, in Generators]
vhole10 [definition, in Generators]
vhole2 [definition, in Generators]
vhole6 [definition, in Generators]

W

well_typed_formula_iff_binterp [lemma, in Ergo.Ergo]
well_typed_formula [inductive, in Ergo.Ergo]
well_typed_dec [lemma, in Ergo.Term]
well_typed_terms [inductive, in Ergo.Term]
well_typed [inductive, in Ergo.Term]
Wf [record, in Ergo.Uf]
Wf [record, in Ergo.Diff]
WfInclusion [section, in Ergo.Lexico]
WfInclusion.A [variable, in Ergo.Lexico]
WfInclusion.R1 [variable, in Ergo.Lexico]
WfInclusion.R2 [variable, in Ergo.Lexico]
wf_tcons [constructor, in Ergo.Term]
wf_tnil [constructor, in Ergo.Term]
wf_lt_lexico [lemma, in Ergo.Lexico]
Wf_lt_lexic.measB [variable, in Ergo.Lexico]
Wf_lt_lexic.measA [variable, in Ergo.Lexico]
Wf_lt_lexic.B [variable, in Ergo.Lexico]
Wf_lt_lexic.A [variable, in Ergo.Lexico]
Wf_lt_lexic [section, in Ergo.Lexico]
wf_inverse_image [lemma, in Ergo.Lexico]
wf_incl [lemma, in Ergo.Lexico]
Wf_merge' [instance, in Ergo.Uf]
Wf_merge [instance, in Ergo.Uf]
Wf_add [instance, in Ergo.Uf]
Wf_empty [instance, in Ergo.Uf]
Wf_separate [instance, in Ergo.Diff]
Wf_empty [instance, in Ergo.Diff]
what_if_its_not_valid [lemma, in Demo]
what_if_its_not_valid [lemma, in AltDemo]
WithClassic [module, in Demo]
WithClassic.vhole2 [lemma, in Demo]
WithListVars [section, in GeneratorsNG]
WithListVars.variables [variable, in GeneratorsNG]
WithModelsAndR [section, in Ergo.ModelsRingExt]
WithModelsAndR.M [variable, in Ergo.ModelsRingExt]
WithModelsAndR.R [variable, in Ergo.ModelsRingExt]
WithModelsAndR.vsy [variable, in Ergo.ModelsRingExt]
WithModelsAndR.vty [variable, in Ergo.ModelsRingExt]
_ :/> _ [notation, in Ergo.ModelsRingExt]
_ :> _ [notation, in Ergo.ModelsRingExt]
WithOT [section, in Ergo.DiagProd]
WithTheory [section, in Ergo.Use]
WithTheory [section, in Ergo.Uf]
WithTheorySpecs [section, in Ergo.Use]
WithTheorySpecs [section, in Ergo.Uf]
WithTheorySpecs [section, in Ergo.Theory]
wt_FIff [constructor, in Ergo.Ergo]
wt_FImp [constructor, in Ergo.Ergo]
wt_FNot [constructor, in Ergo.Ergo]
wt_FOr [constructor, in Ergo.Ergo]
wt_FAnd [constructor, in Ergo.Ergo]
wt_FFalse [constructor, in Ergo.Ergo]
wt_FTrue [constructor, in Ergo.Ergo]
wt_FEq [constructor, in Ergo.Ergo]
wt_FVar [constructor, in Ergo.Ergo]
wt_app [constructor, in Ergo.Term]

X

x [definition, in GeneratorsNG]
x [inductive, in Generators]
x [inductive, in GeneratorsEq]

Y

y [inductive, in GeneratorsEq]

Z

z [inductive, in GeneratorsEq]
Zdiamond [definition, in GeneratorsEq]
ZEntailment [section, in Ergo.TheoryArith]
ZEntailment.M [variable, in Ergo.TheoryArith]
ZEntailment.MakeOps [section, in Ergo.TheoryArith]
ZEntailment.models_integral [variable, in Ergo.TheoryArith]
ZEntailment.models_ring [variable, in Ergo.TheoryArith]
ZEntailment.vsy [variable, in Ergo.TheoryArith]
ZEntailment.vty [variable, in Ergo.TheoryArith]
_ [*] _ [notation, in Ergo.TheoryArith]
_ [-] _ [notation, in Ergo.TheoryArith]
_ [+] _ [notation, in Ergo.TheoryArith]
[ _ ] [notation, in Ergo.TheoryArith]
Zify_Q [lemma, in Ergo.TheoryArith]
ZRing [inductive, in Ergo.ModelsRingExt]
ZRing_well_type_eq [lemma, in Ergo.ModelsRingExt]
ZRing_well_type_2 [lemma, in Ergo.ModelsRingExt]
ZRing_well_type_1 [lemma, in Ergo.ModelsRingExt]
ZRing_div_cancel [constructor, in Ergo.ModelsRingExt]
ZRing_opp_def [constructor, in Ergo.ModelsRingExt]
ZRing_sub_def [constructor, in Ergo.ModelsRingExt]
ZRing_distr_l [constructor, in Ergo.ModelsRingExt]
ZRing_mul_assoc [constructor, in Ergo.ModelsRingExt]
ZRing_mul_comm [constructor, in Ergo.ModelsRingExt]
ZRing_mul_1_l [constructor, in Ergo.ModelsRingExt]
ZRing_add_assoc [constructor, in Ergo.ModelsRingExt]
ZRing_add_comm [constructor, in Ergo.ModelsRingExt]
ZRing_add_0_l [constructor, in Ergo.ModelsRingExt]
zx [axiom, in GeneratorsEq]
zy [axiom, in GeneratorsEq]
zz [axiom, in GeneratorsEq]
Z_idx [abbreviation, in Ergo.TheoryArith]

other

_ [/] _ [notation, in Ergo.ModelsRingExt]
_ [*] _ [notation, in Ergo.ModelsRingExt]
_ [-] _ [notation, in Ergo.ModelsRingExt]
_ [+] _ [notation, in Ergo.ModelsRingExt]
_ ^Z _ [notation, in Demo]
_ ^ _ [notation, in Demo]
_ ^Z _ [notation, in AltDemo]
_ ^ _ [notation, in AltDemo]
type of _ in _ [notation, in Ergo.ModelsRingExt]
wt _ in _ [notation, in Ergo.ModelsRingExt]
[ _ ] [notation, in Ergo.ModelsRingExt]

---

Notation Index

E

_ |= _ [in Ergo.EnvLazy]
dom _ [in Ergo.EnvLazy]
dom _ [in Ergo.Env]
_ |= _ [in Ergo.Env]

I

[| _ |] [in Ergo.Term]

S

_ |- _ [in Ergo.SatCaml]
_ |- _ [in Ergo.Sat]
_ |- _ = _ (sem_scope) [in Ergo.SemLazy]
_ |= _ <> _ (sem_scope) [in Ergo.SemLazy]
_ |= _ = _ (sem_scope) [in Ergo.SemLazy]
_ :> _ [in Ergo.SemLazy]
_ [ _ ] [in Ergo.SemLazy]

T

do _ [in Ergo.CCX]
monome _ [in Ergo.CCX]
do _ [in Ergo.CCX]
[| _ |] [in Ergo.Term]
[| _ |] [in Ergo.Term]

W

_ :/> _ [in Ergo.ModelsRingExt]
_ :> _ [in Ergo.ModelsRingExt]

Z

_ [*] _ [in Ergo.TheoryArith]
_ [-] _ [in Ergo.TheoryArith]
_ [+] _ [in Ergo.TheoryArith]
[ _ ] [in Ergo.TheoryArith]

other

_ [/] _ [in Ergo.ModelsRingExt]
_ [*] _ [in Ergo.ModelsRingExt]
_ [-] _ [in Ergo.ModelsRingExt]
_ [+] _ [in Ergo.ModelsRingExt]
_ ^Z _ [in Demo]
_ ^ _ [in Demo]
_ ^Z _ [in AltDemo]
_ ^ _ [in AltDemo]
type of _ in _ [in Ergo.ModelsRingExt]
wt _ in _ [in Ergo.ModelsRingExt]
[ _ ] [in Ergo.ModelsRingExt]

---

Module Index

A

ADEQUATION [in Ergo.Adequation]
AdequationLazy [in Ergo.TacticLazy]
ArithTheory [in Ergo.TheoryArith]

B

BoolasDT [in Ergo.Term]
BoolEqDep [in Ergo.Term]

C

CCA [in Demo]
CCA [in Ergo.CCX]
CCE [in Demo]
CCE [in Ergo.CCX]
CCX [in Ergo.CCX]
CCX_SIG.Specs [in Ergo.CCX]
CCX_SIG [in Ergo.CCX]
CCX.RAW [in Ergo.CCX]
CCX.Specs [in Ergo.CCX]
Chap11 [in AltDemo]
CNF [in Ergo.Cnf]
CNFLAZY [in Ergo.CNFLazy]
CNFLAZYCOMMON [in Ergo.CNFLazyCommon]
CNFLAZYCOMMON.L [in Ergo.CNFLazyCommon]
CNFLAZYCOMMON.Sem [in Ergo.CNFLazyCommon]
CNFLAZYN [in Ergo.CNFLazyN]
CNFLAZYN.Conversion [in Ergo.CNFLazyN]
CNFLAZY_INTERFACE.Conversion [in Ergo.CNFLazyCommon]
CNFLAZY_INTERFACE [in Ergo.CNFLazyCommon]
CNFLAZY.Conversion [in Ergo.CNFLazy]
CNFRAW [in Ergo.CNFLazy]
CNF.L [in Ergo.Cnf]
CNF.Sem [in Ergo.Cnf]

D

DomainDT [in Ergo.TermUtils]
DomainEqDep [in Ergo.TermUtils]
DPLL [in Ergo.Dpll]
DPLL.E [in Ergo.Dpll]

E

E [in Ergo.AllInstances]
E [in Ergo.AltErgo]
EmptyTheory [in Ergo.Theory]
EN [in Ergo.AllInstances]
EN [in Ergo.AltErgo]
ENV [in Ergo.Env]
EnvCC [in Demo]
EnvCC [in Ergo.AltErgo]
EnvCCA [in Demo]
EnvCCA [in Ergo.AltErgo]
EnvCCAN [in Ergo.AltErgo]
EnvCCN [in Ergo.AltErgo]
EnvFacts [in Ergo.Env]
ENVLAZY [in Ergo.EnvLazy]
EnvSat [in Demo]
ENV_INTERFACE [in Ergo.Env]
ENV.SemF [in Ergo.Env]
EProps [in Ergo.Sat]
EProps [in Ergo.FoldProps]
ErgoCC [in Demo]
ErgoCC [in Ergo.AltErgo]
ErgoCCA [in Demo]
ErgoCCA [in Ergo.AltErgo]
ErgoCCAN [in Ergo.AltErgo]
ErgoCCN [in Ergo.AltErgo]
ErgoE [in Ergo.AltErgo]
ErgoEN [in Ergo.AltErgo]
ErgoSat [in Demo]

F

FULL [in Ergo.CPolynoms]

G

GenericCongrClosure [in Ergo.ModelsRingExt]

I

INDEX [in Ergo.Index]

K

K [in Ergo.AllInstances]

L

LITERAL [in Ergo.Literal]
LITERALBASE [in Ergo.LLazy]
LITINDEX [in Ergo.LLazy]
LLAZY [in Ergo.LLazy]
LLAZYFY [in Ergo.LLazy]
LLAZYFY.RAW [in Ergo.LLazy]
LoadTactic [in Ergo.TacticLazy]
LoadTactic.AD [in Ergo.TacticLazy]
LoadTactic.Deprecated [in Ergo.TacticLazy]
LoadTactic.L [in Ergo.TacticLazy]

M

MakeErgo [in Demo]
MakeErgo [in Ergo.AltErgo]
MakeErgo.DPLL [in Demo]
MakeErgo.DPLL [in Ergo.AltErgo]
MakeErgo.DPLL.E [in Demo]
MakeErgo.DPLL.E [in Ergo.AltErgo]
ModelsAsRing [in Ergo.TheoryArith]

P

Props [in Ergo.Sat]
Props [in Ergo.FoldProps]

Q

QasDT [in Ergo.Rational]
QEqDep [in Ergo.Rational]

R

RAW [in Ergo.LLazy]
RAW [in Ergo.CPolynoms]
RAWCCA [in Ergo.CCX]
RAWCCE [in Ergo.CCX]
RAWCCX [in Ergo.CCX]
RAWCCX.Specs [in Ergo.CCX]

S

S [in Ergo.AllInstances]
SAT [in Ergo.Sat]
SATCAML [in Ergo.SatCaml]
SATCAML.S [in Ergo.SatCaml]
SATCAML.SemF [in Ergo.SatCaml]
SAT.EnvF [in Ergo.Sat]
SAT.SemF [in Ergo.Sat]
SCaml [in Ergo.AllInstances]
SCamlN [in Ergo.AllInstances]
SCamlN.E [in Ergo.AllInstances]
SCaml.E [in Ergo.AllInstances]
SEMANTICS [in Ergo.Semantics]
SEMANTICS.WF [in Ergo.Semantics]
SemFacts [in Ergo.Semantics]
SEMLAZY [in Ergo.SemLazy]
SEM_INTERFACE [in Ergo.Semantics]
SetFoldInd [in Ergo.FoldProps]
SN [in Ergo.AllInstances]
SN.E [in Ergo.AllInstances]
S.E [in Ergo.AllInstances]

T

Tac [in Ergo.AllInstances]
TacCaml [in Ergo.AllInstances]
TacCamlN [in Ergo.AllInstances]
TacN [in Ergo.AllInstances]
Test [in Ergo.Term]
TestsDeCCXA [in Ergo.CCX]
TestsDeCCXA.TestNewUse [in Ergo.CCX]
TestsDeCCXE [in Ergo.CCX]
TestsDeCCXE.TestNewUse [in Ergo.CCX]
TestWithNat [in Ergo.Term]
THEORY [in Ergo.CCX]
TypeasDT [in Ergo.Term]
TypeEqDep [in Ergo.Term]

W

WithClassic [in Demo]

---

Variable Index

A

Abstractions.reifs [in Ergo.Ergo]
Abstractions.ty_env [in Ergo.Ergo]
Abstractions.t_env [in Ergo.Ergo]
Abstractions.v [in Ergo.Ergo]
Abstractions.vm [in Ergo.Ergo]
Abstractions2.ty_env [in Ergo.Ergo]
Abstractions2.t_env [in Ergo.Ergo]
Abstractions2.v [in Ergo.Ergo]
Abstractions2.vm [in Ergo.Ergo]
AdequationLazy.Adequation.v [in Ergo.TacticLazy]
all [in Demo]
all [in AltDemo]
allcc [in Demo]
allcc [in AltDemo]
allfull [in Demo]
allfull [in AltDemo]

C

CanonicalStructure.v [in Ergo.Term]
CanonicalStructure.vtypes [in Ergo.Term]
Compose.A [in Ergo.DistrNeg]
Compose.B [in Ergo.DistrNeg]
Compose.eqA [in Ergo.DistrNeg]
Compose.eqA_trans [in Ergo.DistrNeg]
Compose.eqA_sym [in Ergo.DistrNeg]
Compose.eqA_refl [in Ergo.DistrNeg]
Compose.eqB [in Ergo.DistrNeg]
Compose.eqB_trans [in Ergo.DistrNeg]
Compose.eqB_sym [in Ergo.DistrNeg]
Compose.eqB_refl [in Ergo.DistrNeg]
Compose.f [in Ergo.DistrNeg]
Compose.f_commut [in Ergo.DistrNeg]
Compose.negA [in Ergo.DistrNeg]
Compose.negA_m [in Ergo.DistrNeg]
Compose.negB [in Ergo.DistrNeg]
Compose.negB_m [in Ergo.DistrNeg]

D

DistrNeg.A [in Ergo.DistrNeg]
DistrNeg.neg [in Ergo.DistrNeg]

E

Einstein.Blue [in EinsteinEasy]
Einstein.Blue [in EinsteinEasy2]
Einstein.color [in EinsteinEasy]
Einstein.color [in EinsteinEasy2]
Einstein.color_is_house [in EinsteinEasy]
Einstein.color_2 [in EinsteinEasy]
Einstein.color_is_color [in EinsteinEasy]
Einstein.color_1 [in EinsteinEasy]
Einstein.color_to [in EinsteinEasy]
Einstein.color_of [in EinsteinEasy]
Einstein.color_discr [in EinsteinEasy]
Einstein.color_is_house [in EinsteinEasy2]
Einstein.color_2 [in EinsteinEasy2]
Einstein.color_is_color [in EinsteinEasy2]
Einstein.color_1 [in EinsteinEasy2]
Einstein.color_to [in EinsteinEasy2]
Einstein.color_of [in EinsteinEasy2]
Einstein.color_discr [in EinsteinEasy2]
Einstein.Engineer [in EinsteinEasy]
Einstein.Engineer [in EinsteinEasy2]
Einstein.house_is_house [in EinsteinEasy]
Einstein.house_owner [in EinsteinEasy]
Einstein.house_of [in EinsteinEasy]
Einstein.house_is_house [in EinsteinEasy2]
Einstein.house_owner [in EinsteinEasy2]
Einstein.house_of [in EinsteinEasy2]
Einstein.H1 [in EinsteinEasy]
Einstein.H1 [in EinsteinEasy2]
Einstein.H2 [in EinsteinEasy]
Einstein.H2 [in EinsteinEasy2]
Einstein.H3 [in EinsteinEasy]
Einstein.H3 [in EinsteinEasy2]
Einstein.H4 [in EinsteinEasy]
Einstein.H4 [in EinsteinEasy2]
Einstein.H5 [in EinsteinEasy]
Einstein.H5 [in EinsteinEasy2]
Einstein.MacOS [in EinsteinEasy]
Einstein.MacOS [in EinsteinEasy2]
Einstein.owner_is_person [in EinsteinEasy]
Einstein.owner_house [in EinsteinEasy]
Einstein.owner_of [in EinsteinEasy]
Einstein.owner_is_person [in EinsteinEasy2]
Einstein.owner_house [in EinsteinEasy2]
Einstein.owner_of [in EinsteinEasy2]
Einstein.person [in EinsteinEasy]
Einstein.person [in EinsteinEasy2]
Einstein.person_discr [in EinsteinEasy]
Einstein.person_discr [in EinsteinEasy2]
Einstein.Professor [in EinsteinEasy]
Einstein.Professor [in EinsteinEasy2]
Einstein.Red [in EinsteinEasy]
Einstein.Red [in EinsteinEasy2]
Einstein.Scientist [in EinsteinEasy]
Einstein.Scientist [in EinsteinEasy2]
Einstein.Suse [in EinsteinEasy]
Einstein.Suse [in EinsteinEasy2]
Einstein.system [in EinsteinEasy]
Einstein.system [in EinsteinEasy2]
Einstein.system_is_system [in EinsteinEasy]
Einstein.system_user [in EinsteinEasy]
Einstein.system_of [in EinsteinEasy]
Einstein.system_discr [in EinsteinEasy]
Einstein.system_is_system [in EinsteinEasy2]
Einstein.system_user [in EinsteinEasy2]
Einstein.system_of [in EinsteinEasy2]
Einstein.system_discr [in EinsteinEasy2]
Einstein.Ubuntu [in EinsteinEasy]
Einstein.Ubuntu [in EinsteinEasy2]
Einstein.user_is_user [in EinsteinEasy]
Einstein.user_system [in EinsteinEasy]
Einstein.user_of [in EinsteinEasy]
Einstein.user_is_user [in EinsteinEasy2]
Einstein.user_system [in EinsteinEasy2]
Einstein.user_of [in EinsteinEasy2]
Einstein.White [in EinsteinEasy]
Einstein.White [in EinsteinEasy2]

F

FInterp.ty_env [in Ergo.Ergo]
FInterp.t_env [in Ergo.Ergo]
FInterp.v [in Ergo.Ergo]
FInterp.vm [in Ergo.Ergo]
FormSize.P [in Ergo.CNFLazyN]
FULL.WithVars.vars [in Ergo.CPolynoms]

G

GenericCongrClosure.WithRelation.Closure.C [in Ergo.ModelsRingExt]
GenericCongrClosure.WithRelation.Closure.C_R [in Ergo.ModelsRingExt]
GenericCongrClosure.WithRelation.Closure.C_congr [in Ergo.ModelsRingExt]
GenericCongrClosure.WithRelation.Closure.C_trans [in Ergo.ModelsRingExt]
GenericCongrClosure.WithRelation.Closure.C_sym [in Ergo.ModelsRingExt]
GenericCongrClosure.WithRelation.Closure.C_refl [in Ergo.ModelsRingExt]
GenericCongrClosure.WithRelation.R [in Ergo.ModelsRingExt]
GenericCongrClosure.WithRelation.R_sym [in Ergo.ModelsRingExt]

H

HoleWithListVars.N [in GeneratorsNG]
HoleWithListVars.vars [in GeneratorsNG]

I

IllTypedEqualities.M [in Ergo.ModelsRingExt]
Interp.A [in Ergo.DistrNeg]
Interp.Interps.interp [in Ergo.Term]
Interp.v [in Ergo.Ergo]
Interp.v [in Ergo.Term]
Interp.vtypes [in Ergo.Term]
Inverse_Image.Rof [in Ergo.Lexico]
Inverse_Image.f [in Ergo.Lexico]
Inverse_Image.R [in Ergo.Lexico]
Inverse_Image.B [in Ergo.Lexico]
Inverse_Image.A [in Ergo.Lexico]
IterOps.E [in Ergo.TheoryArith]
IterOps.f [in Ergo.TheoryArith]
IterOps.Hf [in Ergo.TheoryArith]
IterOps.Ilin [in Ergo.TheoryArith]

L

LITERAL.ExpandNot.f [in Ergo.Literal]
LITERAL.ExpandNot.fl [in Ergo.Literal]
LITERAL.ExpandNot.fll [in Ergo.Literal]
LLAZYFY.ExpandNot.f [in Ergo.LLazy]
LLAZYFY.ExpandNot.fl [in Ergo.LLazy]
LLAZYFY.ExpandNot.fll [in Ergo.LLazy]
LLAZYFY.ExpandNot.f_m [in Ergo.LLazy]
LtList.A [in Ergo.LLazy]
LtList.compareA [in Ergo.LLazy]
LtList.ltA [in Ergo.LLazy]

M

Morphisms.A [in Ergo.DistrNeg]
Morphisms.eq [in Ergo.DistrNeg]
Morphisms.eq_trans [in Ergo.DistrNeg]
Morphisms.eq_sym [in Ergo.DistrNeg]
Morphisms.eq_refl [in Ergo.DistrNeg]
Morphisms.f [in Ergo.DistrNeg]
Morphisms.f_m [in Ergo.DistrNeg]
Morphisms.neg [in Ergo.DistrNeg]
Morphisms.neg_m [in Ergo.DistrNeg]
Morphisms2.A [in Ergo.DistrNeg]
Morphisms2.eq [in Ergo.DistrNeg]
Morphisms2.eq_trans [in Ergo.DistrNeg]
Morphisms2.eq_sym [in Ergo.DistrNeg]
Morphisms2.eq_refl [in Ergo.DistrNeg]
Morphisms2.H [in Ergo.DistrNeg]
Morphisms2.neg [in Ergo.DistrNeg]
Morphisms2.neg' [in Ergo.DistrNeg]

P

Props.A [in Ergo.DistrNeg]
Props.f [in Ergo.DistrNeg]
Props.mk_not [in Ergo.DistrNeg]
Props.negation [in Ergo.DistrNeg]

R

RAW.Interp.v [in Ergo.LLazy]
RAW.ListSize.A [in Ergo.LLazy]
RAW.ListSize.sz [in Ergo.LLazy]
RAW.LiteralInductionDefault.Hlit [in Ergo.LLazy]
RAW.LiteralInductionDefault.Hview [in Ergo.LLazy]
RAW.LiteralInductionDefault.P [in Ergo.LLazy]
RAW.LiteralInductionDefault.Pl [in Ergo.LLazy]
RAW.LiteralInductionDefault.Pp [in Ergo.LLazy]
RAW.LiteralInduction.Hcons [in Ergo.LLazy]
RAW.LiteralInduction.Hlcons [in Ergo.LLazy]
RAW.LiteralInduction.Hlit [in Ergo.LLazy]
RAW.LiteralInduction.Hlnil [in Ergo.LLazy]
RAW.LiteralInduction.Hnil [in Ergo.LLazy]
RAW.LiteralInduction.Hview [in Ergo.LLazy]
RAW.LiteralInduction.P [in Ergo.LLazy]
RAW.LiteralInduction.Pl [in Ergo.LLazy]
RAW.LiteralInduction.Pp [in Ergo.LLazy]
RAW.proxy [in Ergo.LLazy]
RAW.WithVars.vars [in Ergo.CPolynoms]
Reverse_Induction.A [in Ergo.FoldProps]

S

SATCAML.Reduce.D [in Ergo.SatCaml]
SATCAML.Reduce.G [in Ergo.SatCaml]
SAT.Filtering.D [in Ergo.Sat]
SAT.Filtering.Finding.compatf [in Ergo.Sat]
SAT.Filtering.Finding.f [in Ergo.Sat]
SAT.Filtering.G [in Ergo.Sat]
SEMANTICS.Creation.Hconsistent [in Ergo.Semantics]
SEMANTICS.Creation.Hexpand [in Ergo.Semantics]
SEMANTICS.Creation.Hfull [in Ergo.Semantics]
SEMANTICS.Creation.Hmorphism [in Ergo.Semantics]
SEMANTICS.Creation.Htrue [in Ergo.Semantics]
SEMANTICS.Creation.m [in Ergo.Semantics]
SEM_INTERFACE.WF.M [in Ergo.Semantics]
SetFoldInd.fold_relation.Hstep [in Ergo.FoldProps]
SetFoldInd.fold_relation.Hi [in Ergo.FoldProps]
SetFoldInd.fold_relation.s [in Ergo.FoldProps]
SetFoldInd.fold_relation.i2 [in Ergo.FoldProps]
SetFoldInd.fold_relation.i1 [in Ergo.FoldProps]
SetFoldInd.fold_relation.f2 [in Ergo.FoldProps]
SetFoldInd.fold_relation.f1 [in Ergo.FoldProps]
SetFoldInd.fold_relation.R [in Ergo.FoldProps]
SetFoldInd.fold_relation.Acc2 [in Ergo.FoldProps]
SetFoldInd.fold_relation.Acc1 [in Ergo.FoldProps]
SetFoldInd.fold_relation.A [in Ergo.FoldProps]
SetFoldInd.fold_induction.Hstep [in Ergo.FoldProps]
SetFoldInd.fold_induction.Hi [in Ergo.FoldProps]
SetFoldInd.fold_induction.P_m [in Ergo.FoldProps]
SetFoldInd.fold_induction.s [in Ergo.FoldProps]
SetFoldInd.fold_induction.i [in Ergo.FoldProps]
SetFoldInd.fold_induction.f [in Ergo.FoldProps]
SetFoldInd.fold_induction.P [in Ergo.FoldProps]
SetFoldInd.fold_induction.A [in Ergo.FoldProps]

T

TermInduction.Hcons [in Ergo.Term]
TermInduction.Hlift [in Ergo.Term]
TermInduction.Hnil [in Ergo.Term]
TermInduction.P [in Ergo.Term]
TermInduction.P0 [in Ergo.Term]
TermMutualInduction.Happ [in Ergo.TermUtils]
TermMutualInduction.Hcons [in Ergo.TermUtils]
TermMutualInduction.Hnil [in Ergo.TermUtils]
TermMutualInduction.P [in Ergo.TermUtils]
TermMutualInduction.Pl [in Ergo.TermUtils]
TestWithNat.boolx [in Ergo.Term]
TestWithNat.natbool [in Ergo.Term]
TestWithNat.natnat [in Ergo.Term]
TestWithNat.natx [in Ergo.Term]
Test.boolx [in Ergo.Term]
Test.natbool [in Ergo.Term]
Test.natnat [in Ergo.Term]
Test.natx [in Ergo.Term]
TInterp.vtypes [in Ergo.Term]

W

WfInclusion.A [in Ergo.Lexico]
WfInclusion.R1 [in Ergo.Lexico]
WfInclusion.R2 [in Ergo.Lexico]
Wf_lt_lexic.measB [in Ergo.Lexico]
Wf_lt_lexic.measA [in Ergo.Lexico]
Wf_lt_lexic.B [in Ergo.Lexico]
Wf_lt_lexic.A [in Ergo.Lexico]
WithListVars.variables [in GeneratorsNG]
WithModelsAndR.M [in Ergo.ModelsRingExt]
WithModelsAndR.R [in Ergo.ModelsRingExt]
WithModelsAndR.vsy [in Ergo.ModelsRingExt]
WithModelsAndR.vty [in Ergo.ModelsRingExt]

Z

ZEntailment.M [in Ergo.TheoryArith]
ZEntailment.models_integral [in Ergo.TheoryArith]
ZEntailment.models_ring [in Ergo.TheoryArith]
ZEntailment.vsy [in Ergo.TheoryArith]
ZEntailment.vty [in Ergo.TheoryArith]

---

Library Index

A

Adequation
AllInstances
AltDemo
AltErgo

C

CCX
Cnf
CNFLazy
CNFLazyCommon
CNFLazyN
CPolynoms

D

Demo
DiagProd
Diff
DistrNeg
DoubleNegUtils
Dpll

E

EinsteinEasy
EinsteinEasy2
Env
EnvLazy
Ergo

F

FoldProps

G

Generators
GeneratorsEq
GeneratorsNG

I

Index

L

Lexico
Literal
LLazy

M

ModelsRingExt

R

Rational

S

Sat
SatCaml
Semantics
SemLazy

T

TacticLazy
Term
TermUtils
TestErgo
Theory
TheoryArith

U

Uf
Use

---

Lemma Index

A

Acc_inverse_image [in Ergo.Lexico]
Acc_lemma [in Ergo.Lexico]
Acc_incl [in Ergo.Lexico]
addk_cancel_embed [in Ergo.TheoryArith]
add_const_as_addk [in Ergo.TheoryArith]
add_monome_as_addk [in Ergo.TheoryArith]
add_as_addk [in Ergo.TheoryArith]
add_conservative [in Ergo.Uf]
add_find [in Ergo.Uf]
add_find_2 [in Ergo.Uf]
add_find_1 [in Ergo.Uf]
add_mem_iff [in Ergo.Uf]
add_mem_3 [in Ergo.Uf]
add_mem_2 [in Ergo.Uf]
add_mem_1 [in Ergo.Uf]
AdequationLazy.adequation [in Ergo.TacticLazy]
ainterp_is_finterp [in Ergo.Ergo]
ainterp_eq_is_finterp [in Ergo.Ergo]
are_diff_separate_3 [in Ergo.Diff]
are_diff_separate_2 [in Ergo.Diff]
are_diff_separate_1 [in Ergo.Diff]
are_diff_empty [in Ergo.Diff]
arithop_eq_iff [in Ergo.TermUtils]
ArithTheory.ThSpecs [in Ergo.TheoryArith]
arith_domain_eq_iff [in Ergo.TermUtils]
A1 [in EinsteinEasy]
A1 [in EinsteinEasy2]

B

bdiscr [in Ergo.Term]
belim [in Ergo.SatCaml]
binterp_is_finterp [in Ergo.Ergo]
binterp_eq_is_finterp [in Ergo.Ergo]

C

cancel_as_addk [in Ergo.TheoryArith]
cardinal_map_le [in Ergo.Uf]
CCX.Specs.assumed_inconsistent [in Ergo.CCX]
CCX.Specs.assumed_assume [in Ergo.CCX]
CCX.Specs.assumed_empty [in Ergo.CCX]
CCX.Specs.query_assumed [in Ergo.CCX]
CCX.Specs.query_true [in Ergo.CCX]
CCX.Specs.this_assume_inc [in Ergo.CCX]
CCX.Specs.this_assume [in Ergo.CCX]
chap10 [in Demo]
chap10 [in AltDemo]
Chap11.diamond0 [in AltDemo]
Chap11.diamond1 [in AltDemo]
Chap11.diamond2 [in AltDemo]
Chap11.diamond3 [in AltDemo]
Chap11.diamond4 [in AltDemo]
Chap11.diamond5 [in AltDemo]
Chap11.fdiamond0 [in AltDemo]
Chap11.fdiamond1 [in AltDemo]
Chap11.fdiamond2 [in AltDemo]
Chap11.fdiamond3 [in AltDemo]
Chap11.fdiamond4 [in AltDemo]
Chap11.fdiamond5 [in AltDemo]
Chap11.FiboA0 [in AltDemo]
Chap11.FiboA1 [in AltDemo]
Chap11.FiboA10 [in AltDemo]
Chap11.FiboA15 [in AltDemo]
Chap11.FiboA2 [in AltDemo]
Chap11.FiboA20 [in AltDemo]
Chap11.FiboA5 [in AltDemo]
Chap11.In_list [in AltDemo]
Chap11.peirce [in AltDemo]
Chap11.Zdiamond0 [in AltDemo]
Chap11.Zdiamond1 [in AltDemo]
Chap11.Zdiamond2 [in AltDemo]
Chap11.Zdiamond3 [in AltDemo]
Chap11.Zdiamond4 [in AltDemo]
Chap11.Zdiamond5 [in AltDemo]
Chap11.Zdiamond6 [in AltDemo]
Chap11.Zdiamond7 [in AltDemo]
cmp_terms_spec [in Ergo.TermUtils]
cmp_term_spec [in Ergo.TermUtils]
cmp_term_terms_sym [in Ergo.TermUtils]
cmp_term_terms_eq [in Ergo.TermUtils]
CNFLAZYCOMMON.pick_2 [in Ergo.CNFLazyCommon]
CNFLAZYCOMMON.pick_1 [in Ergo.CNFLazyCommon]
CNFLAZYN.cfl_1 [in Ergo.CNFLazyN]
CNFLAZYN.Conversion.cnf [in Ergo.CNFLazyN]
CNFLAZYN.Conversion.mk_form_equiv [in Ergo.CNFLazyN]
CNFLAZYN.Conversion.mk_or_equiv [in Ergo.CNFLazyN]
CNFLAZYN.Conversion.mk_and_equiv [in Ergo.CNFLazyN]
CNFLAZYN.Conversion.mk_not_not [in Ergo.CNFLazyN]
CNFLAZYN.Conversion.not_mk_not [in Ergo.CNFLazyN]
CNFLAZYN.make_1 [in Ergo.CNFLazyN]
CNFLAZYN.mk_not_size [in Ergo.CNFLazyN]
CNFLAZYN.wf_mk_iff [in Ergo.CNFLazyN]
CNFLAZYN.wf_mk_impl [in Ergo.CNFLazyN]
CNFLAZYN.wf_mk_and [in Ergo.CNFLazyN]
CNFLAZYN.wf_mk_or [in Ergo.CNFLazyN]
CNFLAZYN.wf_mk_lit [in Ergo.CNFLazyN]
CNFLAZY.cfl_1 [in Ergo.CNFLazy]
CNFLAZY.Conversion.cnf [in Ergo.CNFLazy]
CNFLAZY.Conversion.mk_form_equiv [in Ergo.CNFLazy]
CNFLAZY.Conversion.mk_not_not [in Ergo.CNFLazy]
CNFLAZY.Conversion.not_mk_not [in Ergo.CNFLazy]
CNFLAZY.make_1 [in Ergo.CNFLazy]
CNFLAZY.mk_not_size [in Ergo.CNFLazy]
CNFLAZY.wf_mk_iff [in Ergo.CNFLazy]
CNFLAZY.wf_mk_impl [in Ergo.CNFLazy]
CNFLAZY.wf_mk_and [in Ergo.CNFLazy]
CNFLAZY.wf_mk_or [in Ergo.CNFLazy]
CNFLAZY.wf_mk_lit [in Ergo.CNFLazy]
common_denom_isZp [in Ergo.TheoryArith]
common_denom_coef [in Ergo.TheoryArith]
common_denom_nonzero [in Ergo.TheoryArith]
congruent_dec [in Ergo.Uf]
cst_eq_dep [in Ergo.TermUtils]

D

deb1 [in AltDemo]
deb100 [in AltDemo]
deb15 [in AltDemo]
deb2 [in AltDemo]
deb20 [in Demo]
deb20 [in AltDemo]
deb3 [in AltDemo]
deb4 [in AltDemo]
deb5 [in AltDemo]
deb6 [in AltDemo]
diagProd_iff [in Ergo.DiagProd]
diagProd_aux_inv [in Ergo.DiagProd]
distr_neg_f [in Ergo.DistrNeg]
distr_neg_m [in Ergo.DistrNeg]
dnc [in Ergo.DoubleNegUtils]
dnc_or [in Ergo.DoubleNegUtils]
dnc_and [in Ergo.DoubleNegUtils]
DomainDT.eq_dec [in Ergo.TermUtils]
double_not [in Ergo.DoubleNegUtils]

E

EmptyTheory.implyX_m [in Ergo.Theory]
empty_find [in Ergo.Use]
empty_find [in Ergo.Uf]
empty_mem [in Ergo.Uf]
EnvFacts.assumed_singleton [in Ergo.Env]
EnvFacts.query_assume [in Ergo.Env]
EnvFacts.query_m [in Ergo.Env]
ENVLAZY.assumed_inconsistent [in Ergo.EnvLazy]
ENVLAZY.assumed_assume [in Ergo.EnvLazy]
ENVLAZY.assumed_oapply [in Ergo.EnvLazy]
ENVLAZY.assumed_empty [in Ergo.EnvLazy]
ENVLAZY.filter_elim [in Ergo.EnvLazy]
ENVLAZY.input_to_lit_lift [in Ergo.EnvLazy]
ENVLAZY.in_cc_is_no_prop [in Ergo.EnvLazy]
ENVLAZY.lit_to_input_lift [in Ergo.EnvLazy]
ENVLAZY.query_expand [in Ergo.EnvLazy]
ENVLAZY.query_assumed [in Ergo.EnvLazy]
ENVLAZY.query_true [in Ergo.EnvLazy]
ENVLAZY.query_m [in Ergo.EnvLazy]
ENVLAZY.submodel_eq_submodel [in Ergo.EnvLazy]
ENV.assumed_inconsistent [in Ergo.Env]
ENV.assumed_assume [in Ergo.Env]
ENV.assumed_empty [in Ergo.Env]
ENV.query_expand [in Ergo.Env]
ENV.query_monotonic [in Ergo.Env]
ENV.query_assumed [in Ergo.Env]
ENV.query_true [in Ergo.Env]
ENV.wf_add [in Ergo.Env]
ENV.wf_empty [in Ergo.Env]
equiv_M [in Ergo.TheoryArith]
eq_integral [in Ergo.ModelsRingExt]
eq_ring [in Ergo.ModelsRingExt]
eq_congr [in Ergo.Term]
eq_terms_trans [in Ergo.Term]
eq_terms_sym [in Ergo.Term]
eq_terms_refl [in Ergo.Term]
eq_trans [in Ergo.Term]
eq_sym [in Ergo.Term]
eq_refl [in Ergo.Term]

F

find_multiple_poly [in Ergo.TheoryArith]
form_size_induction [in Ergo.CNFLazyN]
form_size_pos [in Ergo.CNFLazyN]
FP13_2_1 [in AltDemo]
FP13_12_1 [in AltDemo]
FP13_5_1 [in AltDemo]
FP13_5_2 [in AltDemo]
FP13_5_3 [in AltDemo]
FP13_5_8 [in AltDemo]
FP25_24_24 [in AltDemo]
FP25_15_5 [in AltDemo]
FP25_13_1 [in AltDemo]
FP25_11_1 [in AltDemo]
FP25_2_1 [in AltDemo]
FP5_3_1 [in AltDemo]
FP9_4_1 [in AltDemo]
FULL.addk_co [in Ergo.CPolynoms]
FULL.addk_dec [in Ergo.CPolynoms]
FULL.add_co [in Ergo.CPolynoms]
FULL.add_monome_co [in Ergo.CPolynoms]
FULL.add_const_co [in Ergo.CPolynoms]
FULL.add_dec [in Ergo.CPolynoms]
FULL.add_monome_dec [in Ergo.CPolynoms]
FULL.add_const_dec [in Ergo.CPolynoms]
FULL.cancel_co [in Ergo.CPolynoms]
FULL.cancel_dec [in Ergo.CPolynoms]
FULL.choose_dec [in Ergo.CPolynoms]
FULL.div_co [in Ergo.CPolynoms]
FULL.div_dec [in Ergo.CPolynoms]
FULL.embed_co [in Ergo.CPolynoms]
FULL.embed_dec [in Ergo.CPolynoms]
FULL.extract_embed [in Ergo.CPolynoms]
FULL.extract_dec [in Ergo.CPolynoms]
FULL.is_const_dec [in Ergo.CPolynoms]
FULL.leaves_iff [in Ergo.CPolynoms]
FULL.mult_co [in Ergo.CPolynoms]
FULL.mult_dec [in Ergo.CPolynoms]
FULL.Pq_co [in Ergo.CPolynoms]
FULL.Pz_co [in Ergo.CPolynoms]
FULL.P0_co [in Ergo.CPolynoms]
FULL.P1_co [in Ergo.CPolynoms]
FULL.sub_co [in Ergo.CPolynoms]
FULL.sub_dec [in Ergo.CPolynoms]

G

GenericCongrClosure.app_rev_fold [in Ergo.ModelsRingExt]
GenericCongrClosure.collect_paths [in Ergo.ModelsRingExt]
GenericCongrClosure.linked_congr [in Ergo.ModelsRingExt]
GenericCongrClosure.linked_trans [in Ergo.ModelsRingExt]
GenericCongrClosure.linked_sym [in Ergo.ModelsRingExt]
GenericCongrClosure.linked_refl [in Ergo.ModelsRingExt]
GenericCongrClosure.mext_iff [in Ergo.ModelsRingExt]
GenericCongrClosure.plunge_and_flatten_linked [in Ergo.ModelsRingExt]
GenericCongrClosure.plunge_rel_chain [in Ergo.ModelsRingExt]
GenericCongrClosure.rel_at_terms_pre [in Ergo.ModelsRingExt]
GenericCongrClosure.rel_at_sym [in Ergo.ModelsRingExt]
GenericCongrClosure.rel_chain_singl [in Ergo.ModelsRingExt]
GenericCongrClosure.rel_chain_app [in Ergo.ModelsRingExt]
GenericCongrClosure.smallest_closure [in Ergo.ModelsRingExt]

H

has_type_irrelevant [in Ergo.Term]
has_type_type_of_congr [in Ergo.Term]
has_type_congr [in Ergo.Term]
has_type_is_type_of [in Ergo.Term]
has_type_iff [in Ergo.Term]
has_type_2 [in Ergo.Term]
has_type_1 [in Ergo.Term]
has_type_unfold [in Ergo.Term]
have_type_congr [in Ergo.Term]
hole2 [in Demo]
hole2 [in AltDemo]
hole2_tauto [in Demo]
hole2_tauto [in AltDemo]
hole3 [in AltDemo]
hole4 [in Demo]
hole4 [in AltDemo]
hole5 [in AltDemo]

I

iff_def2 [in Ergo.DoubleNegUtils]
iff_def [in Ergo.DoubleNegUtils]
ill_typed_ZRing_2 [in Ergo.ModelsRingExt]
ill_typed_ZRing_1 [in Ergo.ModelsRingExt]
implyX_entails [in Ergo.TheoryArith]
implyX_specs [in Ergo.TheoryArith]
implyX_weaken [in Ergo.Theory]
implyX_Ax [in Ergo.Theory]
implyX_impl [in Ergo.Theory]
imp_def [in Ergo.DoubleNegUtils]
InA_in_list [in Ergo.Use]
INDEX.compare_3 [in Ergo.Index]
INDEX.compare_2 [in Ergo.Index]
INDEX.compare_1 [in Ergo.Index]
INDEX.eq_trans [in Ergo.Index]
INDEX.eq_sym [in Ergo.Index]
INDEX.eq_refl [in Ergo.Index]
INDEX.lt_not_eq [in Ergo.Index]
INDEX.lt_trans [in Ergo.Index]
inj_cst_2 [in Ergo.TermUtils]
insert_neq_o [in Ergo.Use]
insert_eq_o [in Ergo.Use]
insert_neq_o [in Ergo.Diff]
insert_eq_o [in Ergo.Diff]
interp_irrelevant [in Ergo.Term]
interp_congr [in Ergo.Term]
interp_unfold [in Ergo.Term]
interp_m [in Ergo.DistrNeg]
in_list_rev_iff [in Ergo.Use]
isMp_iter [in Ergo.TheoryArith]
isMp_make [in Ergo.TheoryArith]
isMp_mk_term [in Ergo.TheoryArith]
isMp_add_monome [in Ergo.TheoryArith]
isMp_embed [in Ergo.TheoryArith]
isMp_add_const [in Ergo.TheoryArith]
isMp_sub [in Ergo.TheoryArith]
isMp_add [in Ergo.TheoryArith]
isMp_addk [in Ergo.TheoryArith]
isMp_mult [in Ergo.TheoryArith]
isMp_P1 [in Ergo.TheoryArith]
isMp_P0 [in Ergo.TheoryArith]
isM_not_is_const [in Ergo.TheoryArith]
isM_make_embed [in Ergo.TheoryArith]
isZp_subst [in Ergo.TheoryArith]
isZp_isZ [in Ergo.TheoryArith]
isZp_make [in Ergo.TheoryArith]
isZp_mk_term [in Ergo.TheoryArith]
isZp_add_const [in Ergo.TheoryArith]
isZp_add_monome [in Ergo.TheoryArith]
isZp_cancel [in Ergo.TheoryArith]
isZp_mult [in Ergo.TheoryArith]
isZp_opp [in Ergo.TheoryArith]
isZp_sub [in Ergo.TheoryArith]
isZp_add [in Ergo.TheoryArith]
isZp_addk [in Ergo.TheoryArith]
isZp_embed [in Ergo.TheoryArith]
isZp_Pz [in Ergo.TheoryArith]
isZp_P1 [in Ergo.TheoryArith]
isZp_R0 [in Ergo.TheoryArith]
isZ_mult [in Ergo.TheoryArith]
isZ_opp [in Ergo.TheoryArith]
isZ_minus [in Ergo.TheoryArith]
isZ_plus [in Ergo.TheoryArith]
isZ_z [in Ergo.TheoryArith]
is_eq_sym [in Ergo.ModelsRingExt]
is_eq_refl [in Ergo.ModelsRingExt]
is_const_const [in Ergo.TheoryArith]
iter_idem [in Ergo.TheoryArith]
iter_idem_2' [in Ergo.TheoryArith]
iter_idem_2 [in Ergo.TheoryArith]
iter_unsolvable_None [in Ergo.TheoryArith]
iter_preserves_unsolvable [in Ergo.TheoryArith]
iter_cancel [in Ergo.TheoryArith]
iter_sub [in Ergo.TheoryArith]
iter_add [in Ergo.TheoryArith]
iter_mult [in Ergo.TheoryArith]
iter_Pq [in Ergo.TheoryArith]
iter_Pz [in Ergo.TheoryArith]
iter_P0 [in Ergo.TheoryArith]
iter_linear [in Ergo.TheoryArith]
iter_m [in Ergo.TheoryArith]
iter_as_list [in Ergo.TheoryArith]
iter_m [in Ergo.Theory]

L

leaves_not_empty [in Ergo.TheoryArith]
LITINDEX.atom_eq_iff [in Ergo.LLazy]
LITINDEX.interp_mk_not [in Ergo.LLazy]
LITINDEX.mk_not_fix [in Ergo.LLazy]
LITINDEX.mk_not_invol [in Ergo.LLazy]
LITINDEX.mk_not_compat [in Ergo.LLazy]
LITINDEX.mk_not_tf [in Ergo.LLazy]
LLAZYFY.compare_3 [in Ergo.LLazy]
LLAZYFY.compare_2 [in Ergo.LLazy]
LLAZYFY.compare_list_1 [in Ergo.LLazy]
LLAZYFY.compare_1 [in Ergo.LLazy]
LLAZYFY.eqlist_to_raw [in Ergo.LLazy]
LLAZYFY.eqlist_trans [in Ergo.LLazy]
LLAZYFY.eqlist_sym [in Ergo.LLazy]
LLAZYFY.eqlist2_to_raw [in Ergo.LLazy]
LLAZYFY.eq_trans [in Ergo.LLazy]
LLAZYFY.eq_sym [in Ergo.LLazy]
LLAZYFY.eq_refl [in Ergo.LLazy]
LLAZYFY.expand_mk_not [in Ergo.LLazy]
LLAZYFY.expand_map_map [in Ergo.LLazy]
LLAZYFY.expand_compat [in Ergo.LLazy]
LLAZYFY.is_proxy_true [in Ergo.LLazy]
LLAZYFY.is_proxy_nil [in Ergo.LLazy]
LLAZYFY.is_proxy_mk_not [in Ergo.LLazy]
LLAZYFY.llsize_llsize [in Ergo.LLazy]
LLAZYFY.lt_not_eq [in Ergo.LLazy]
LLAZYFY.lt_trans [in Ergo.LLazy]
LLAZYFY.mk_not_fix [in Ergo.LLazy]
LLAZYFY.mk_not_invol [in Ergo.LLazy]
LLAZYFY.mk_not_compat [in Ergo.LLazy]
LLAZYFY.mk_not_tf [in Ergo.LLazy]
LLAZYFY.mk_not_interp [in Ergo.LLazy]
LLAZYFY.negate_expand [in Ergo.LLazy]
LLAZYFY.negation_interp [in Ergo.LLazy]
LLAZYFY.size_expand [in Ergo.LLazy]
LLAZYFY.size_mk_not [in Ergo.LLazy]
LLAZYFY.size_pos [in Ergo.LLazy]
LLAZYFY.wf_expand [in Ergo.LLazy]
LLAZYFY.wf_mk_not [in Ergo.LLazy]
LLAZYFY.wf_negation [in Ergo.LLazy]
LLAZYFY.wf_lit_2_weak [in Ergo.LLazy]
LoadTactic.validity [in Ergo.TacticLazy]
LoadTactic.validity' [in Ergo.TacticLazy]

M

make_term_of_R [in Ergo.TheoryArith]
make_entails [in Ergo.TheoryArith]
make_correct [in Ergo.TheoryArith]
make_tmult_3 [in Ergo.TheoryArith]
make_tmult_2 [in Ergo.TheoryArith]
make_tmult_1 [in Ergo.TheoryArith]
make_topp [in Ergo.TheoryArith]
make_tminus [in Ergo.TheoryArith]
make_tplus [in Ergo.TheoryArith]
make_z [in Ergo.TheoryArith]
make_sound [in Ergo.Theory]
melange_cc_sat [in Demo]
melange_cc_sat [in AltDemo]
merge_find [in Ergo.Use]
merge_touched_find [in Ergo.Uf]
merge_touched_mem [in Ergo.Uf]
merge_find [in Ergo.Uf]
merge_mem [in Ergo.Uf]
merge'_touched_spec [in Ergo.Uf]
merge'_find [in Ergo.Uf]
merge'_mem [in Ergo.Uf]
mk_term_of_R [in Ergo.TheoryArith]
mk_term_correct [in Ergo.TheoryArith]
mk_term_make [in Ergo.TheoryArith]
mk_term_acc [in Ergo.TheoryArith]
ModelsAsRing.implyX_entails [in Ergo.TheoryArith]
models_integral' [in Ergo.TheoryArith]
models_neq_cst_iff [in Ergo.TheoryArith]
models_eq_cst_iff [in Ergo.TheoryArith]
mult_as_addk [in Ergo.TheoryArith]
M1 [in EinsteinEasy]
M1 [in EinsteinEasy2]
M2 [in EinsteinEasy]
M2 [in EinsteinEasy2]
M3 [in EinsteinEasy]
M3 [in EinsteinEasy2]
M4 [in EinsteinEasy2]
M5 [in EinsteinEasy2]

N

negation_compose [in Ergo.DistrNeg]
negation_interp [in Ergo.DistrNeg]
neqs_separate_3 [in Ergo.Diff]
neqs_separate_2 [in Ergo.Diff]
neqs_separate_1 [in Ergo.Diff]
neqs_empty [in Ergo.Diff]
neqs_sym [in Ergo.Diff]
neqs_not_iff [in Ergo.Diff]
neqs_iff [in Ergo.Diff]
niff_def2 [in Ergo.DoubleNegUtils]
niff_def [in Ergo.DoubleNegUtils]
nimp_def [in Ergo.DoubleNegUtils]
not_or_and_not [in Ergo.DoubleNegUtils]
not_and_or_not [in Ergo.DoubleNegUtils]
num_classes_merge'_lt [in Ergo.Uf]
num_classes_merge' [in Ergo.Uf]
num_classes_add [in Ergo.Uf]
num_classes_empty [in Ergo.Uf]

O

or_and_distr [in Ergo.DoubleNegUtils]
or_distr_and [in Ergo.DoubleNegUtils]

P

peirce_or_is_it [in Demo]
peirce_or_is_it [in AltDemo]
pgcd_fix_Z [in Demo]
pgcd_fix_sat [in Demo]
pgcd_fix_congruence [in Demo]
pgcd_fix [in Demo]
pgcd_fix_Z [in AltDemo]
pgcd_fix_sat [in AltDemo]
pgcd_fix_congruence [in AltDemo]
pgcd_fix [in AltDemo]
push_minus [in Ergo.TheoryArith]
push_mult [in Ergo.TheoryArith]
push_addk [in Ergo.TheoryArith]
push_tminus_tmult [in Ergo.TheoryArith]
push_right_eq [in Ergo.TheoryArith]

Q

QasDT.eq_dec [in Ergo.Rational]
Qfloor_isZ [in Ergo.TheoryArith]
Qfloor_opp [in Ergo.TheoryArith]
Qfloor_mult [in Ergo.TheoryArith]
Qfloor_addk [in Ergo.TheoryArith]
Q_neq [in Ergo.TheoryArith]
Q_cancel [in Ergo.TheoryArith]

R

range_merge' [in Ergo.Uf]
range_merge [in Ergo.Uf]
range_add [in Ergo.Uf]
range_empty [in Ergo.Uf]
range_mem [in Ergo.Uf]
RAWCCX.filter_subset_gen [in Ergo.CCX]
RAWCCX.find_congr_equations_terms [in Ergo.CCX]
RAWCCX.find_congr_equations2_terms [in Ergo.CCX]
RAWCCX.find_congr_equations1_terms [in Ergo.CCX]
RAWCCX.inter_leaves_terms [in Ergo.CCX]
RAWCCX.merge_decreases [in Ergo.CCX]
RAWCCX.num_pending_wf [in Ergo.CCX]
RAWCCX.num_distincts_wf [in Ergo.CCX]
RAWCCX.num_distinct_pairs_le [in Ergo.CCX]
RAWCCX.Specs.add_term_terms_dec [in Ergo.CCX]
RAWCCX.Specs.are_diff_dec [in Ergo.CCX]
RAWCCX.Specs.are_equal_dec [in Ergo.CCX]
RAWCCX.Specs.assumed_inconsistent [in Ergo.CCX]
RAWCCX.Specs.assumed_assume [in Ergo.CCX]
RAWCCX.Specs.assumed_empty [in Ergo.CCX]
RAWCCX.Specs.assume_dec [in Ergo.CCX]
RAWCCX.Specs.clean_up_dec [in Ergo.CCX]
RAWCCX.Specs.coherent_diff [in Ergo.CCX]
RAWCCX.Specs.coherent_merge [in Ergo.CCX]
RAWCCX.Specs.coherent_add [in Ergo.CCX]
RAWCCX.Specs.coincides_weaken [in Ergo.CCX]
RAWCCX.Specs.coincides_merge [in Ergo.CCX]
RAWCCX.Specs.coincides_add [in Ergo.CCX]
RAWCCX.Specs.coincides_inputs [in Ergo.CCX]
RAWCCX.Specs.coincides_submodel [in Ergo.CCX]
RAWCCX.Specs.coincides'_merge [in Ergo.CCX]
RAWCCX.Specs.diff_dec [in Ergo.CCX]
RAWCCX.Specs.find_congr_equations_extend [in Ergo.CCX]
RAWCCX.Specs.find_congr_equations_correct [in Ergo.CCX]
RAWCCX.Specs.find_congr_equations2_extend [in Ergo.CCX]
RAWCCX.Specs.find_congr_equations2_correct [in Ergo.CCX]
RAWCCX.Specs.find_congr_equations1_extend [in Ergo.CCX]
RAWCCX.Specs.find_congr_equations1_correct [in Ergo.CCX]
RAWCCX.Specs.find_add_equations_extend [in Ergo.CCX]
RAWCCX.Specs.find_add_equations_correct [in Ergo.CCX]
RAWCCX.Specs.incoherent_true [in Ergo.CCX]
RAWCCX.Specs.incoherent_false [in Ergo.CCX]
RAWCCX.Specs.iter_correct [in Ergo.CCX]
RAWCCX.Specs.justify_merge [in Ergo.CCX]
RAWCCX.Specs.justify_add [in Ergo.CCX]
RAWCCX.Specs.justify_coincides [in Ergo.CCX]
RAWCCX.Specs.lcongr_merge [in Ergo.CCX]
RAWCCX.Specs.lcongr_add [in Ergo.CCX]
RAWCCX.Specs.merge_dec [in Ergo.CCX]
RAWCCX.Specs.Ncoincides_separate [in Ergo.CCX]
RAWCCX.Specs.Ncoincides_weaken [in Ergo.CCX]
RAWCCX.Specs.Ncoincides_inputs [in Ergo.CCX]
RAWCCX.Specs.Ncoincides_submodel [in Ergo.CCX]
RAWCCX.Specs.no_trivial_model [in Ergo.CCX]
RAWCCX.Specs.query_true [in Ergo.CCX]
RAWCCX.Specs.query_assumed [in Ergo.CCX]
RAWCCX.Specs.query_dec [in Ergo.CCX]
RAWCCX.Specs.submodel_eq_models_list [in Ergo.CCX]
RAWCCX.Specs.theory_iter_correct [in Ergo.CCX]
RAWCCX.Specs.Wf_assume [in Ergo.CCX]
RAWCCX.Specs.Wf_diff [in Ergo.CCX]
RAWCCX.Specs.Wf_clean_up [in Ergo.CCX]
RAWCCX.Specs.Wf_merge' [in Ergo.CCX]
RAWCCX.Specs.Wf_merge [in Ergo.CCX]
RAWCCX.Specs.Wf_add_term_terms [in Ergo.CCX]
RAWCCX.t_lt_wf [in Ergo.CCX]
RAWCCX.uncongr_gen [in Ergo.CCX]
RAW.addk_dec' [in Ergo.CPolynoms]
RAW.addk_dec [in Ergo.CPolynoms]
RAW.addk_m_dec [in Ergo.CPolynoms]
RAW.add_dec' [in Ergo.CPolynoms]
RAW.add_monome_dec' [in Ergo.CPolynoms]
RAW.add_const_dec' [in Ergo.CPolynoms]
RAW.add_dec [in Ergo.CPolynoms]
RAW.add_monome_dec [in Ergo.CPolynoms]
RAW.cancel_dec' [in Ergo.CPolynoms]
RAW.choose_dec [in Ergo.CPolynoms]
RAW.div_dec' [in Ergo.CPolynoms]
RAW.div_dec [in Ergo.CPolynoms]
RAW.expand_compat [in Ergo.LLazy]
RAW.extract_embed [in Ergo.CPolynoms]
RAW.extract_dec [in Ergo.CPolynoms]
RAW.is_const_dec [in Ergo.CPolynoms]
RAW.literal_ind [in Ergo.LLazy]
RAW.lt_trans [in Ergo.LLazy]
RAW.lt_not_eq [in Ergo.LLazy]
RAW.mk_not_invol [in Ergo.LLazy]
RAW.mult_dec' [in Ergo.CPolynoms]
RAW.mult_dec [in Ergo.CPolynoms]
RAW.size_expand [in Ergo.LLazy]
RAW.size_pos [in Ergo.LLazy]
RAW.size_m [in Ergo.LLazy]
RAW.sub_dec' [in Ergo.CPolynoms]
RAW.sub_dec [in Ergo.CPolynoms]
RAW.wf_equiv_iff [in Ergo.CPolynoms]
RAW.Wf_addk_m [in Ergo.CPolynoms]
replace [in Ergo.Term]
replace' [in Ergo.Term]
reprs_merge' [in Ergo.Uf]
reprs_merge [in Ergo.Uf]
reprs_add_2 [in Ergo.Uf]
reprs_add_1 [in Ergo.Uf]
reprs_empty [in Ergo.Uf]
reprs_mem [in Ergo.Uf]
rev_rec [in Ergo.FoldProps]
rev_list_rec [in Ergo.FoldProps]
rowProd_inv [in Ergo.DiagProd]

S

SATCAML.bcp_complete [in Ergo.SatCaml]
SATCAML.bcp_monotonic_env [in Ergo.SatCaml]
SATCAML.bcp_consistent [in Ergo.SatCaml]
SATCAML.bcp_progress [in Ergo.SatCaml]
SATCAML.bcp_unsat [in Ergo.SatCaml]
SATCAML.bcp_correct [in Ergo.SatCaml]
SATCAML.dpll_correct [in Ergo.SatCaml]
SATCAML.expand_nonrec_2 [in Ergo.SatCaml]
SATCAML.expand_nonrec [in Ergo.SatCaml]
SATCAML.llsize_app [in Ergo.SatCaml]
SATCAML.ll2s_map_elements [in Ergo.SatCaml]
SATCAML.ll2s_expand [in Ergo.SatCaml]
SATCAML.ll2s_cfl [in Ergo.SatCaml]
SATCAML.ll2s_app [in Ergo.SatCaml]
SATCAML.lsize_pos [in Ergo.SatCaml]
SATCAML.l2s_elements [in Ergo.SatCaml]
SATCAML.l2s_Subset [in Ergo.SatCaml]
SATCAML.l2s_iff [in Ergo.SatCaml]
SATCAML.proof_search_sat [in Ergo.SatCaml]
SATCAML.proof_search_unsat [in Ergo.SatCaml]
SATCAML.reduce_complete [in Ergo.SatCaml]
SATCAML.reduce_correct [in Ergo.SatCaml]
SATCAML.reduce_spec [in Ergo.SatCaml]
SATCAML.remove_union [in Ergo.SatCaml]
SATCAML.remove_transpose [in Ergo.SatCaml]
SATCAML.union_remove [in Ergo.SatCaml]
SATCAML.weak_assume [in Ergo.SatCaml]
SAT.AStrongRed [in Ergo.Sat]
SAT.cfl_expand_m [in Ergo.Sat]
SAT.csize_in [in Ergo.Sat]
SAT.csize_acc_ge [in Ergo.Sat]
SAT.csize_lt_compat [in Ergo.Sat]
SAT.csize_monotonic [in Ergo.Sat]
SAT.csize_acc [in Ergo.Sat]
SAT.derivable_m [in Ergo.Sat]
SAT.dpll_correct [in Ergo.Sat]
SAT.expand_models [in Ergo.Sat]
SAT.find_3 [in Ergo.Sat]
SAT.find_2 [in Ergo.Sat]
SAT.find_1 [in Ergo.Sat]
SAT.lsize_acc [in Ergo.Sat]
SAT.lsize_lt_compat [in Ergo.Sat]
SAT.lsize_monotonic [in Ergo.Sat]
SAT.proof_search_sat [in Ergo.Sat]
SAT.proof_search_unsat [in Ergo.Sat]
SAT.size_right_unsat_dec [in Ergo.Sat]
SAT.size_left_unsat_dec [in Ergo.Sat]
SAT.size_assume_dec [in Ergo.Sat]
SAT.size_expand [in Ergo.Sat]
SAT.size_union [in Ergo.Sat]
SAT.size_red_dec [in Ergo.Sat]
SAT.size_elim_dec [in Ergo.Sat]
SAT.size_add [in Ergo.Sat]
SAT.size_in [in Ergo.Sat]
SAT.size_m [in Ergo.Sat]
SAT.soundness [in Ergo.Sat]
SAT.submodel_add [in Ergo.Sat]
SAT.T_csize [in Ergo.Sat]
SAT.T_lsize [in Ergo.Sat]
SAT.unitary_singl [in Ergo.Sat]
SAT.weakening [in Ergo.Sat]
SEMANTICS.model_as_model_of [in Ergo.Semantics]
SemFacts.model_expand [in Ergo.Semantics]
SemFacts.model_true [in Ergo.Semantics]
SemFacts.model_full [in Ergo.Semantics]
SemFacts.model_em [in Ergo.Semantics]
SemFacts.model_m [in Ergo.Semantics]
SemFacts.submodel_empty [in Ergo.Semantics]
SEMLAZY.consistent [in Ergo.SemLazy]
SEMLAZY.full [in Ergo.SemLazy]
SEMLAZY.models_eq_congr [in Ergo.SemLazy]
SEMLAZY.models_list_in [in Ergo.SemLazy]
SEMLAZY.models_neq_sym [in Ergo.SemLazy]
SEMLAZY.models_neq_irrefl [in Ergo.SemLazy]
SEMLAZY.models_eq_trans [in Ergo.SemLazy]
SEMLAZY.models_eq_sym [in Ergo.SemLazy]
SEMLAZY.models_eq_refl [in Ergo.SemLazy]
SEMLAZY.models_neq_iff [in Ergo.SemLazy]
SEMLAZY.models_eq_iff [in Ergo.SemLazy]
SEMLAZY.morphism [in Ergo.SemLazy]
SEMLAZY.wf_expand [in Ergo.SemLazy]
SEMLAZY.wf_expand_lift [in Ergo.SemLazy]
SEMLAZY.wf_expand_ [in Ergo.SemLazy]
SEMLAZY.wf_true [in Ergo.SemLazy]
separate_conservative [in Ergo.Diff]
SetFoldInd.fold_rel [in Ergo.FoldProps]
SetFoldInd.fold_ind2 [in Ergo.FoldProps]
SetFoldInd.fold_ind [in Ergo.FoldProps]
SetFoldInd.fold_ind_aux [in Ergo.FoldProps]
SetFoldInd.Hli [in Ergo.FoldProps]
SetFoldInd.sofl_1 [in Ergo.FoldProps]
shankar_01 [in Demo]
shankar_01 [in AltDemo]
simple_congr_congruence [in Demo]
simple_congr [in Demo]
simple_congr_congruence [in AltDemo]
simple_congr [in AltDemo]
solution_eq_trans [in Ergo.Theory]
solution_eq_sym [in Ergo.Theory]
solution_eq_refl [in Ergo.Theory]
solved_iff [in Ergo.TheoryArith]
solve_dec [in Ergo.TheoryArith]
solve_basic_dec [in Ergo.TheoryArith]
solve_trivial [in Ergo.Theory]
submodel_eq_In [in Ergo.CCX]
subst_idem [in Ergo.TheoryArith]
subst_idem_2 [in Ergo.TheoryArith]
subst_idem_1 [in Ergo.TheoryArith]
subst_as_addk [in Ergo.TheoryArith]
subst_linear [in Ergo.TheoryArith]
subst_full_dec [in Ergo.TheoryArith]
subst_dec [in Ergo.TheoryArith]
sub_as_addk [in Ergo.TheoryArith]
symbol_cmp_spec [in Ergo.TermUtils]
symbol_lt_irrefl [in Ergo.TermUtils]
symbol_lt_trans [in Ergo.TermUtils]

T

tequal_iff [in Ergo.Term]
tequal_2 [in Ergo.Term]
tequal_1 [in Ergo.Term]
terms_of_merge [in Ergo.Use]
terms_of_find [in Ergo.Use]
terms_of_empty [in Ergo.Use]
terms_of_iff [in Ergo.Use]
terms_lt_not_eq [in Ergo.TermUtils]
term_of_R_add_const [in Ergo.TheoryArith]
term_of_R_add_monome [in Ergo.TheoryArith]
term_of_R_cancel [in Ergo.TheoryArith]
term_of_R_sub [in Ergo.TheoryArith]
term_of_R_add [in Ergo.TheoryArith]
term_of_R_mult [in Ergo.TheoryArith]
term_of_R_addk [in Ergo.TheoryArith]
term_of_R_embed [in Ergo.TheoryArith]
term_of_R_Pq [in Ergo.TheoryArith]
term_of_R_P1 [in Ergo.TheoryArith]
term_of_R_P0 [in Ergo.TheoryArith]
term_terms_lt_trans [in Ergo.TermUtils]
term_lt_not_eq [in Ergo.TermUtils]
term_mutual_ind [in Ergo.TermUtils]
test_arith_nat_sat [in Demo]
test_arithZ [in Demo]
test_arith_nat_sat [in AltDemo]
test_arithZ [in AltDemo]
tmult_0_equal [in Ergo.TheoryArith]
topp_const [in Ergo.TheoryArith]
touched_spec [in Ergo.Uf]
tplus_0_equal [in Ergo.TheoryArith]
types_of_congr [in Ergo.Term]
type_of_congr [in Ergo.Term]
type_dec [in Ergo.Term]

U

unsolvable_iff [in Ergo.TheoryArith]

W

well_typed_formula_iff_binterp [in Ergo.Ergo]
well_typed_dec [in Ergo.Term]
wf_lt_lexico [in Ergo.Lexico]
wf_inverse_image [in Ergo.Lexico]
wf_incl [in Ergo.Lexico]
what_if_its_not_valid [in Demo]
what_if_its_not_valid [in AltDemo]
WithClassic.vhole2 [in Demo]

Z

Zify_Q [in Ergo.TheoryArith]
ZRing_well_type_eq [in Ergo.ModelsRingExt]
ZRing_well_type_2 [in Ergo.ModelsRingExt]
ZRing_well_type_1 [in Ergo.ModelsRingExt]

---

Constructor Index

A

app [in Ergo.Term]

B

bad_div_cancel [in Ergo.ModelsRingExt]
bad_opp_cancel [in Ergo.ModelsRingExt]
bad_1_neutral [in Ergo.ModelsRingExt]
bad_0_neutral [in Ergo.ModelsRingExt]

C

CCX.mk_t [in Ergo.CCX]
congruent_false [in Ergo.Uf]
congruent_true [in Ergo.Uf]
Cst [in Ergo.Term]

D

Disequation [in Ergo.CCX]
Div [in Ergo.Term]
DomainN [in Ergo.Term]
DomainNat [in Ergo.Term]
DomainPos [in Ergo.Term]
DomainQ [in Ergo.Term]
DomainZ [in Ergo.Term]
DPLL.Sat [in Ergo.Dpll]
DPLL.Unsat [in Ergo.Dpll]

E

ENVLAZY.Build_t [in Ergo.EnvLazy]
ENV.Build_t [in Ergo.Env]
Equation [in Ergo.CCX]
eq_terms_cons [in Ergo.Term]
eq_terms_nil [in Ergo.Term]

F

FAnd [in Ergo.Ergo]
FEq [in Ergo.Ergo]
FFalse [in Ergo.Ergo]
FIff [in Ergo.Ergo]
FImp [in Ergo.Ergo]
FNot [in Ergo.Ergo]
FOr [in Ergo.Ergo]
FTrue [in Ergo.Ergo]
FULL.addk_spec_intro [in Ergo.CPolynoms]
FULL.add_spec_intro [in Ergo.CPolynoms]
FULL.add_monome_spec_intro [in Ergo.CPolynoms]
FULL.add_const_spec_intro [in Ergo.CPolynoms]
FULL.cancel_spec_intro [in Ergo.CPolynoms]
FULL.choose_spec_Some [in Ergo.CPolynoms]
FULL.choose_spec_None [in Ergo.CPolynoms]
FULL.embed_spec_intro [in Ergo.CPolynoms]
FULL.extract_spec_Some [in Ergo.CPolynoms]
FULL.extract_spec_None [in Ergo.CPolynoms]
FULL.is_const_spec_false [in Ergo.CPolynoms]
FULL.is_const_spec_true [in Ergo.CPolynoms]
FULL.mk_poly [in Ergo.CPolynoms]
FULL.mult_spec_intro [in Ergo.CPolynoms]
FULL.sub_spec_intro [in Ergo.CPolynoms]
FVar [in Ergo.Ergo]

G

GenericCongrClosure.mext_cons [in Ergo.ModelsRingExt]
GenericCongrClosure.mext_nil [in Ergo.ModelsRingExt]
GenericCongrClosure.mext_congr [in Ergo.ModelsRingExt]
GenericCongrClosure.mext_trans [in Ergo.ModelsRingExt]
GenericCongrClosure.mext_sym [in Ergo.ModelsRingExt]
GenericCongrClosure.mext_refl [in Ergo.ModelsRingExt]
GenericCongrClosure.mext_rule [in Ergo.ModelsRingExt]
GenericCongrClosure.rel_chain_cons [in Ergo.ModelsRingExt]
GenericCongrClosure.rel_chain_nil [in Ergo.ModelsRingExt]
GenericCongrClosure.rel_at_terms_S [in Ergo.ModelsRingExt]
GenericCongrClosure.rel_at_terms_0 [in Ergo.ModelsRingExt]
GenericCongrClosure.rel_at_next [in Ergo.ModelsRingExt]
GenericCongrClosure.rel_at_here [in Ergo.ModelsRingExt]

I

Inconsistent [in Ergo.Env]
isZ_intro [in Ergo.TheoryArith]

L

LITINDEX.Atom [in Ergo.LLazy]
LITINDEX.Equation [in Ergo.LLazy]
LLAZYFY.mk_literal [in Ergo.LLazy]
LLAZYFY.wf_lit_wk_proxy [in Ergo.LLazy]
LLAZYFY.wf_lit_wk_lit [in Ergo.LLazy]
LLAZYFY.wf_lit_proxy [in Ergo.LLazy]
LLAZYFY.wf_lit_lit [in Ergo.LLazy]
LoadTactic.Sat [in Ergo.TacticLazy]
LoadTactic.Unsat [in Ergo.TacticLazy]

M

mext_cons [in Ergo.ModelsRingExt]
mext_nil [in Ergo.ModelsRingExt]
mext_rule [in Ergo.ModelsRingExt]
mext_congr [in Ergo.ModelsRingExt]
mext_trans [in Ergo.ModelsRingExt]
mext_sym [in Ergo.ModelsRingExt]
mext_refl [in Ergo.ModelsRingExt]
mext_wt [in Ergo.ModelsRingExt]
Minus [in Ergo.Term]
mk_varmaps [in Ergo.Ergo]
mk_dummy [in Ergo.Term]
mk_a [in Generators]
mk_x [in Generators]
mk_occ [in Generators]
mk_t [in Ergo.Uf]
mk_z [in GeneratorsEq]
mk_y [in GeneratorsEq]
mk_x [in GeneratorsEq]
Mult [in Ergo.Term]

N

Normal [in Ergo.Env]

O

Op [in Ergo.Term]
Opp [in Ergo.Term]

P

Plus [in Ergo.Term]

R

RAWCCX.mk_env [in Ergo.CCX]
RAWCCX.Specs.add_terms_spec_Normal [in Ergo.CCX]
RAWCCX.Specs.add_term_spec_Normal [in Ergo.CCX]
RAWCCX.Specs.are_diff_spec_false [in Ergo.CCX]
RAWCCX.Specs.are_diff_spec_true [in Ergo.CCX]
RAWCCX.Specs.are_equal_spec_false [in Ergo.CCX]
RAWCCX.Specs.are_equal_spec_true [in Ergo.CCX]
RAWCCX.Specs.assume_spec_Inconsistent [in Ergo.CCX]
RAWCCX.Specs.assume_spec_Input [in Ergo.CCX]
RAWCCX.Specs.clean_up_Normal [in Ergo.CCX]
RAWCCX.Specs.clean_up_Inconsistent [in Ergo.CCX]
RAWCCX.Specs.diff_spec_Normal [in Ergo.CCX]
RAWCCX.Specs.diff_spec_Inconsistent [in Ergo.CCX]
RAWCCX.Specs.justify_cons [in Ergo.CCX]
RAWCCX.Specs.justify_nil [in Ergo.CCX]
RAWCCX.Specs.merge_spec_Normal [in Ergo.CCX]
RAWCCX.Specs.merge_spec_Inconsistent [in Ergo.CCX]
RAWCCX.Specs.mk_coincides [in Ergo.CCX]
RAWCCX.Specs.query_spec_false [in Ergo.CCX]
RAWCCX.Specs.query_spec_true [in Ergo.CCX]
RAWCCX.t_lt_2 [in Ergo.CCX]
RAWCCX.t_lt_1 [in Ergo.CCX]
RAW.addk_spec'_intro [in Ergo.CPolynoms]
RAW.addk_spec_intro [in Ergo.CPolynoms]
RAW.addk_spec_0 [in Ergo.CPolynoms]
RAW.addk_m_spec_intro [in Ergo.CPolynoms]
RAW.add_spec'_intro [in Ergo.CPolynoms]
RAW.add_monome_spec'_intro [in Ergo.CPolynoms]
RAW.add_const_spec'_intro [in Ergo.CPolynoms]
RAW.add_spec_intro [in Ergo.CPolynoms]
RAW.add_monome_spec_intro [in Ergo.CPolynoms]
RAW.add_monome_spec_0 [in Ergo.CPolynoms]
RAW.cancel_spec'_intro [in Ergo.CPolynoms]
RAW.choose_spec_Some [in Ergo.CPolynoms]
RAW.choose_spec_None [in Ergo.CPolynoms]
RAW.extract_spec_Some [in Ergo.CPolynoms]
RAW.extract_spec_None [in Ergo.CPolynoms]
RAW.is_const_spec_false [in Ergo.CPolynoms]
RAW.is_const_spec_true [in Ergo.CPolynoms]
RAW.is_add_monome_add [in Ergo.CPolynoms]
RAW.is_add_monome_diff [in Ergo.CPolynoms]
RAW.is_add_monome_adjust [in Ergo.CPolynoms]
RAW.is_addk_of_2 [in Ergo.CPolynoms]
RAW.is_addk_of_1 [in Ergo.CPolynoms]
RAW.is_addk_of_both [in Ergo.CPolynoms]
RAW.is_mult_intro [in Ergo.CPolynoms]
RAW.Lit [in Ergo.LLazy]
RAW.mult_spec'_intro [in Ergo.CPolynoms]
RAW.mult_spec_intro [in Ergo.CPolynoms]
RAW.Proxy [in Ergo.LLazy]
RAW.sub_spec'_intro [in Ergo.CPolynoms]
RAW.sub_spec_intro [in Ergo.CPolynoms]

S

SATCAML.bcpNone [in Ergo.SatCaml]
SATCAML.bcpSome [in Ergo.SatCaml]
SATCAML.redNone [in Ergo.SatCaml]
SATCAML.redSome [in Ergo.SatCaml]
SATCAML.reduce_redNone [in Ergo.SatCaml]
SATCAML.reduce_redSome [in Ergo.SatCaml]
SATCAML.Sat [in Ergo.SatCaml]
SATCAML.Unsat [in Ergo.SatCaml]
SAT.AAssume [in Ergo.Sat]
SAT.AConflict [in Ergo.Sat]
SAT.AElim [in Ergo.Sat]
SAT.ARed [in Ergo.Sat]
SAT.AUnsat [in Ergo.Sat]
SAT.mk_sequent [in Ergo.Sat]
SAT.Sat [in Ergo.Sat]
SAT.Unsat [in Ergo.Sat]
SEMANTICS.mk_model [in Ergo.Semantics]
SEMLAZY.models_list_cons [in Ergo.SemLazy]
SEMLAZY.models_list_nil [in Ergo.SemLazy]
solution_eq_Subst [in Ergo.Theory]
solution_eq_Unsolvable [in Ergo.Theory]
solution_eq_Solved [in Ergo.Theory]
Solved [in Ergo.Theory]
solve_basic_Subst [in Ergo.TheoryArith]
solve_basic_Unsolvable [in Ergo.TheoryArith]
solve_basic_Solved [in Ergo.TheoryArith]
solve_specs_Subst [in Ergo.Theory]
solve_specs_Unsolvable [in Ergo.Theory]
solve_specs_Solved [in Ergo.Theory]
submodel_cons_neq [in Ergo.CCX]
submodel_cons_eq [in Ergo.CCX]
submodel_nil [in Ergo.CCX]
Subst [in Ergo.Theory]
subst_spec_other [in Ergo.TheoryArith]
subst_spec_normal [in Ergo.TheoryArith]
subst_spec_intro [in Ergo.TheoryArith]
symbol_lt_Op_2 [in Ergo.TermUtils]
symbol_lt_Op_1 [in Ergo.TermUtils]
symbol_lt_Cst_Op [in Ergo.TermUtils]
symbol_lt_Q_1 [in Ergo.TermUtils]
symbol_lt_Z_Q [in Ergo.TermUtils]
symbol_lt_Z_1 [in Ergo.TermUtils]
symbol_lt_Pos_Q [in Ergo.TermUtils]
symbol_lt_Pos_Z [in Ergo.TermUtils]
symbol_lt_Pos_1 [in Ergo.TermUtils]
symbol_lt_N_Q [in Ergo.TermUtils]
symbol_lt_N_Z [in Ergo.TermUtils]
symbol_lt_N_Pos [in Ergo.TermUtils]
symbol_lt_N_1 [in Ergo.TermUtils]
symbol_lt_Nat_Q [in Ergo.TermUtils]
symbol_lt_Nat_Z [in Ergo.TermUtils]
symbol_lt_Nat_Pos [in Ergo.TermUtils]
symbol_lt_Nat_N [in Ergo.TermUtils]
symbol_lt_Nat_1 [in Ergo.TermUtils]
symbol_lt_Unint_Op [in Ergo.TermUtils]
symbol_lt_Unint_Cst [in Ergo.TermUtils]
symbol_lt_Unint_2 [in Ergo.TermUtils]
symbol_lt_Unint_1 [in Ergo.TermUtils]

T

TAnd [in Ergo.Ergo]
TFalse [in Ergo.Ergo]
TIff [in Ergo.Ergo]
TImp [in Ergo.Ergo]
TNot [in Ergo.Ergo]
TOr [in Ergo.Ergo]
TTrue [in Ergo.Ergo]
TVar [in Ergo.Ergo]
typeArith [in Ergo.Term]
typeArrow [in Ergo.Term]
typeCst [in Ergo.Term]
typeDefault [in Ergo.Term]

U

Unint [in Ergo.Term]
Unsolvable [in Ergo.Theory]

W

wf_tcons [in Ergo.Term]
wf_tnil [in Ergo.Term]
wt_FIff [in Ergo.Ergo]
wt_FImp [in Ergo.Ergo]
wt_FNot [in Ergo.Ergo]
wt_FOr [in Ergo.Ergo]
wt_FAnd [in Ergo.Ergo]
wt_FFalse [in Ergo.Ergo]
wt_FTrue [in Ergo.Ergo]
wt_FEq [in Ergo.Ergo]
wt_FVar [in Ergo.Ergo]
wt_app [in Ergo.Term]

Z

ZRing_div_cancel [in Ergo.ModelsRingExt]
ZRing_opp_def [in Ergo.ModelsRingExt]
ZRing_sub_def [in Ergo.ModelsRingExt]
ZRing_distr_l [in Ergo.ModelsRingExt]
ZRing_mul_assoc [in Ergo.ModelsRingExt]
ZRing_mul_comm [in Ergo.ModelsRingExt]
ZRing_mul_1_l [in Ergo.ModelsRingExt]
ZRing_add_assoc [in Ergo.ModelsRingExt]
ZRing_add_comm [in Ergo.ModelsRingExt]
ZRing_add_0_l [in Ergo.ModelsRingExt]

---

Axiom Index

A

ADEQUATION.adequation [in Ergo.Adequation]
ADEQUATION.canonical_model [in Ergo.Adequation]
ADEQUATION.interp [in Ergo.Adequation]
ADEQUATION.vars [in Ergo.Adequation]

C

CCX_SIG.Specs.query_assumed [in Ergo.CCX]
CCX_SIG.Specs.query_true [in Ergo.CCX]
CCX_SIG.Specs.assumed_inconsistent [in Ergo.CCX]
CCX_SIG.Specs.assumed_assume [in Ergo.CCX]
CCX_SIG.Specs.assumed_empty [in Ergo.CCX]
CCX_SIG.assumed [in Ergo.CCX]
CCX_SIG.query [in Ergo.CCX]
CCX_SIG.assume [in Ergo.CCX]
CCX_SIG.empty [in Ergo.CCX]
CCX_SIG.t [in Ergo.CCX]
CNFLAZY_INTERFACE.Conversion.cnf [in Ergo.CNFLazyCommon]
CNFLAZY_INTERFACE.Conversion.mk_form [in Ergo.CNFLazyCommon]
CNFLAZY_INTERFACE.make_1 [in Ergo.CNFLazyCommon]
CNF.cfl [in Ergo.Cnf]
CNF.cfl_1 [in Ergo.Cnf]
CNF.formula [in Ergo.Cnf]
CNF.make [in Ergo.Cnf]
CNF.pick [in Ergo.Cnf]
CNF.pick_2 [in Ergo.Cnf]
CNF.pick_1 [in Ergo.Cnf]

D

DPLL.dpll [in Ergo.Dpll]
DPLL.dpll_correct [in Ergo.Dpll]

E

ENVLAZY.query_monotonic [in Ergo.EnvLazy]
ENV_INTERFACE.query_expand [in Ergo.Env]
ENV_INTERFACE.query_monotonic [in Ergo.Env]
ENV_INTERFACE.query_assumed [in Ergo.Env]
ENV_INTERFACE.query_true [in Ergo.Env]
ENV_INTERFACE.assumed_inconsistent [in Ergo.Env]
ENV_INTERFACE.assumed_assume [in Ergo.Env]
ENV_INTERFACE.assumed_empty [in Ergo.Env]
ENV_INTERFACE.assumed [in Ergo.Env]
ENV_INTERFACE.query [in Ergo.Env]
ENV_INTERFACE.assume [in Ergo.Env]
ENV_INTERFACE.empty [in Ergo.Env]
ENV_INTERFACE.t [in Ergo.Env]
eq_wt_iff [in Ergo.ModelsRingExt]

L

LITERALBASE.interp [in Ergo.LLazy]
LITERALBASE.interp_mk_not [in Ergo.LLazy]
LITERALBASE.lfalse [in Ergo.LLazy]
LITERALBASE.ltrue [in Ergo.LLazy]
LITERALBASE.mk_not_fix [in Ergo.LLazy]
LITERALBASE.mk_not_invol [in Ergo.LLazy]
LITERALBASE.mk_not_compat [in Ergo.LLazy]
LITERALBASE.mk_not_tf [in Ergo.LLazy]
LITERALBASE.mk_not [in Ergo.LLazy]
LITERALBASE.t [in Ergo.LLazy]
LITERAL.expand [in Ergo.Literal]
LITERAL.expand_mk_not [in Ergo.Literal]
LITERAL.expand_compat [in Ergo.Literal]
LITERAL.interp [in Ergo.Literal]
LITERAL.interp_mk_not [in Ergo.Literal]
LITERAL.is_proxy_true [in Ergo.Literal]
LITERAL.is_proxy_nil [in Ergo.Literal]
LITERAL.is_proxy_mk_not [in Ergo.Literal]
LITERAL.is_proxy [in Ergo.Literal]
LITERAL.lfalse [in Ergo.Literal]
LITERAL.ltrue [in Ergo.Literal]
LITERAL.mk_not_fix [in Ergo.Literal]
LITERAL.mk_not_invol [in Ergo.Literal]
LITERAL.mk_not_compat [in Ergo.Literal]
LITERAL.mk_not_tf [in Ergo.Literal]
LITERAL.mk_not [in Ergo.Literal]
LITERAL.size [in Ergo.Literal]
LITERAL.size_expand [in Ergo.Literal]
LITERAL.size_mk_not [in Ergo.Literal]
LITERAL.size_pos [in Ergo.Literal]
LITERAL.t [in Ergo.Literal]

S

SEM_INTERFACE.wf_expand [in Ergo.Semantics]
SEM_INTERFACE.wf_true [in Ergo.Semantics]
SEM_INTERFACE.morphism [in Ergo.Semantics]
SEM_INTERFACE.consistent [in Ergo.Semantics]
SEM_INTERFACE.full [in Ergo.Semantics]
SEM_INTERFACE.model_as_fun [in Ergo.Semantics]
SEM_INTERFACE.model [in Ergo.Semantics]

T

term_equal_2 [in Ergo.Term]
term_equal_1 [in Ergo.Term]
TestsDeCCXA.error [in Ergo.CCX]
TestsDeCCXE.error [in Ergo.CCX]

Z

zx [in GeneratorsEq]
zy [in GeneratorsEq]
zz [in GeneratorsEq]

---

Inductive Index

A

a [in Generators]
arithop [in Ergo.Term]
arith_domain [in Ergo.Term]

B

bad_equality [in Ergo.ModelsRingExt]

C

congruent_spec [in Ergo.Uf]

D

DPLL.Res [in Ergo.Dpll]
dummy [in Ergo.Term]

E

eq_terms [in Ergo.Term]
Exception [in Ergo.Env]

F

fform [in Ergo.Ergo]
form [in Ergo.Ergo]
FULL.addk_spec [in Ergo.CPolynoms]
FULL.add_spec [in Ergo.CPolynoms]
FULL.add_monome_spec [in Ergo.CPolynoms]
FULL.add_const_spec [in Ergo.CPolynoms]
FULL.cancel_spec [in Ergo.CPolynoms]
FULL.choose_spec [in Ergo.CPolynoms]
FULL.embed_spec [in Ergo.CPolynoms]
FULL.extract_spec [in Ergo.CPolynoms]
FULL.is_const_spec [in Ergo.CPolynoms]
FULL.mult_spec [in Ergo.CPolynoms]
FULL.sub_spec [in Ergo.CPolynoms]

G

GenericCongrClosure.mext [in Ergo.ModelsRingExt]
GenericCongrClosure.mext_terms [in Ergo.ModelsRingExt]
GenericCongrClosure.rel_chain [in Ergo.ModelsRingExt]
GenericCongrClosure.rel_at_terms [in Ergo.ModelsRingExt]
GenericCongrClosure.rel_at [in Ergo.ModelsRingExt]

I

input [in Ergo.CCX]
isZ [in Ergo.TheoryArith]

L

LITINDEX.atom [in Ergo.LLazy]
LLAZYFY.wf_lit_weak [in Ergo.LLazy]
LLAZYFY.wf_lit [in Ergo.LLazy]
LoadTactic.Res [in Ergo.TacticLazy]

M

mext [in Ergo.ModelsRingExt]
mext_terms [in Ergo.ModelsRingExt]

O

occ [in Generators]

R

RAWCCX.Specs.add_terms_spec [in Ergo.CCX]
RAWCCX.Specs.add_term_spec [in Ergo.CCX]
RAWCCX.Specs.are_diff_spec [in Ergo.CCX]
RAWCCX.Specs.are_equal_spec [in Ergo.CCX]
RAWCCX.Specs.assume_spec [in Ergo.CCX]
RAWCCX.Specs.clean_up_spec [in Ergo.CCX]
RAWCCX.Specs.coincides [in Ergo.CCX]
RAWCCX.Specs.diff_spec [in Ergo.CCX]
RAWCCX.Specs.justify [in Ergo.CCX]
RAWCCX.Specs.merge_spec [in Ergo.CCX]
RAWCCX.Specs.query_spec [in Ergo.CCX]
RAWCCX.t_lt [in Ergo.CCX]
RAW.addk_spec' [in Ergo.CPolynoms]
RAW.addk_spec [in Ergo.CPolynoms]
RAW.addk_m_spec [in Ergo.CPolynoms]
RAW.add_spec' [in Ergo.CPolynoms]
RAW.add_monome_spec' [in Ergo.CPolynoms]
RAW.add_const_spec' [in Ergo.CPolynoms]
RAW.add_spec [in Ergo.CPolynoms]
RAW.add_monome_spec [in Ergo.CPolynoms]
RAW.cancel_spec' [in Ergo.CPolynoms]
RAW.choose_spec [in Ergo.CPolynoms]
RAW.extract_spec [in Ergo.CPolynoms]
RAW.is_const_spec [in Ergo.CPolynoms]
RAW.is_add_monome_of [in Ergo.CPolynoms]
RAW.is_addk_of [in Ergo.CPolynoms]
RAW.is_mult_of [in Ergo.CPolynoms]
RAW.mult_spec' [in Ergo.CPolynoms]
RAW.mult_spec [in Ergo.CPolynoms]
RAW.sub_spec' [in Ergo.CPolynoms]
RAW.sub_spec [in Ergo.CPolynoms]
RAW.t_ [in Ergo.LLazy]

S

SATCAML.bcpRes [in Ergo.SatCaml]
SATCAML.redRes [in Ergo.SatCaml]
SATCAML.reduce_spec_ [in Ergo.SatCaml]
SATCAML.Res [in Ergo.SatCaml]
SAT.derivable [in Ergo.Sat]
SAT.Res [in Ergo.Sat]
SEMLAZY.models_list [in Ergo.SemLazy]
Solution [in Ergo.Theory]
solution_eq [in Ergo.Theory]
solve_basic_spec [in Ergo.TheoryArith]
solve_specs [in Ergo.Theory]
submodel_eq [in Ergo.CCX]
subst_full_spec [in Ergo.TheoryArith]
subst_spec [in Ergo.TheoryArith]
symbol [in Ergo.Term]
symbol_lt [in Ergo.TermUtils]

T

term [in Ergo.Term]
type [in Ergo.Term]

W

well_typed_formula [in Ergo.Ergo]
well_typed_terms [in Ergo.Term]
well_typed [in Ergo.Term]

X

x [in Generators]
x [in GeneratorsEq]

Y

y [in GeneratorsEq]

Z

z [in GeneratorsEq]
ZRing [in Ergo.ModelsRingExt]

---

Projection Index

C

canon [in Ergo.Uf]
CCX.this [in Ergo.CCX]
CCX.this_wf [in Ergo.CCX]

E

ENVLAZY.cc [in Ergo.EnvLazy]
ENVLAZY.env [in Ergo.EnvLazy]
ENV.this [in Ergo.Env]
ENV.wf [in Ergo.Env]

F

FULL.wf_this [in Ergo.CPolynoms]
FULL._this [in Ergo.CPolynoms]

H

Ha [in Ergo.Ergo]
Hb [in Ergo.Ergo]

I

implyX_entails [in Ergo.Theory]
implyX_dec [in Ergo.Theory]
implyX_Solve [in Ergo.Theory]
implyX_Subst [in Ergo.Theory]
is_wf [in Ergo.Uf]
is_wf [in Ergo.Diff]

L

leaves [in Ergo.Theory]
leaves_not_empty [in Ergo.Theory]
leaves_m [in Ergo.Theory]
LLAZYFY.this [in Ergo.LLazy]
LLAZYFY.wf [in Ergo.LLazy]

M

make [in Ergo.Theory]

O

one [in Ergo.Theory]

R

R [in Ergo.Theory]
ra [in Ergo.Ergo]
RAWCCX.D [in Ergo.CCX]
RAWCCX.F [in Ergo.CCX]
RAWCCX.G [in Ergo.CCX]
RAWCCX.I [in Ergo.CCX]
RAWCCX.N [in Ergo.CCX]
RAWCCX.Specs.coherence [in Ergo.CCX]
RAWCCX.Specs.Dcorrect [in Ergo.CCX]
RAWCCX.Specs.Dwf [in Ergo.CCX]
RAWCCX.Specs.Fcorrect [in Ergo.CCX]
RAWCCX.Specs.Ncorrect [in Ergo.CCX]
RAWCCX.Specs.Nwf [in Ergo.CCX]
RAW.Wf_p [in Ergo.CPolynoms]
rb [in Ergo.Ergo]
R_OT [in Ergo.Theory]

S

SAT.D [in Ergo.Sat]
SAT.G [in Ergo.Sat]
SEMANTICS.this [in Ergo.Semantics]
SEMANTICS.this_expand [in Ergo.Semantics]
SEMANTICS.this_true [in Ergo.Semantics]
SEMANTICS.this_m [in Ergo.Semantics]
SEMANTICS.this_wf [in Ergo.Semantics]
SEMANTICS.this_full [in Ergo.Semantics]
solve [in Ergo.Theory]
solve_dec [in Ergo.Theory]
solve_m [in Ergo.Theory]
subst [in Ergo.Theory]
subst_m [in Ergo.Theory]

T

this [in Ergo.Uf]
ty [in Ergo.Ergo]

V

varmaps_vsy [in Ergo.Ergo]
varmaps_vty [in Ergo.Ergo]
varmaps_lits [in Ergo.Ergo]

---

Instance Index

A

are_diff_m [in Ergo.Diff]
arithop_UOT [in Ergo.TermUtils]
Arith_theory [in Ergo.TheoryArith]
arith_domain_UOT [in Ergo.TermUtils]

D

diagProd_subset_m [in Ergo.DiagProd]
diagProd_m [in Ergo.DiagProd]

E

EmptyTheory.Empty_theory_specs [in Ergo.Theory]
EmptyTheory.Empty_theory_implyX [in Ergo.Theory]
EmptyTheory.Empty_theory [in Ergo.Theory]
ENVLAZY.is_prop_m [in Ergo.EnvLazy]
ENV_INTERFACE.query_m [in Ergo.Env]
ENV.query_m [in Ergo.Env]

F

FULL.addk_equiv [in Ergo.CPolynoms]
FULL.add_equiv [in Ergo.CPolynoms]
FULL.add_monome_equiv [in Ergo.CPolynoms]
FULL.add_const_equiv [in Ergo.CPolynoms]
FULL.cancel_equiv [in Ergo.CPolynoms]
FULL.choose_equiv [in Ergo.CPolynoms]
FULL.coef_of_equiv [in Ergo.CPolynoms]
FULL.div_equiv [in Ergo.CPolynoms]
FULL.equiv_Equivalence [in Ergo.CPolynoms]
FULL.extract_equiv [in Ergo.CPolynoms]
FULL.is_const_equiv [in Ergo.CPolynoms]
FULL.leaves_equiv [in Ergo.CPolynoms]
FULL.mult_equiv [in Ergo.CPolynoms]
FULL.poly_OT [in Ergo.CPolynoms]
FULL.poly_SOT [in Ergo.CPolynoms]
FULL.sub_equiv [in Ergo.CPolynoms]
f_m [in Ergo.TheoryArith]

I

implyX_Trans [in Ergo.Theory]
implyX_Sym [in Ergo.Theory]
implyX_Refl [in Ergo.Theory]
implyX_m [in Ergo.Theory]
INDEX.t_UOT [in Ergo.Index]
isMpoly_m [in Ergo.TheoryArith]
isZpoly_m [in Ergo.TheoryArith]
isZ_m [in Ergo.TheoryArith]

L

leaves_m [in Ergo.TheoryArith]
LITERALBASE.t_OT [in Ergo.LLazy]
LITERAL.is_proxy_m [in Ergo.Literal]
LITERAL.mk_not_m [in Ergo.Literal]
LITERAL.size_m [in Ergo.Literal]
LITERAL.t_OT [in Ergo.Literal]
LITINDEX.atom_UOT [in Ergo.LLazy]
LITINDEX.t_OT [in Ergo.LLazy]
LLAZYFY.is_proxy_m [in Ergo.LLazy]
LLAZYFY.mk_not_m [in Ergo.LLazy]
LLAZYFY.size_m [in Ergo.LLazy]
LLAZYFY.t_OT [in Ergo.LLazy]

M

models_eq_Trans [in Ergo.TheoryArith]
models_eq_Sym [in Ergo.TheoryArith]
models_eq_Refl [in Ergo.TheoryArith]

N

neqs_m [in Ergo.Diff]

Q

Q2Qc_m [in Ergo.TheoryArith]

R

rational_UOT [in Ergo.Rational]
RAWCCX.Specs.Wf_add_terms [in Ergo.CCX]
RAWCCX.Specs.Wf_add_term [in Ergo.CCX]
RAWCCX.Specs.Wf_empty [in Ergo.CCX]
RAWCCX.uncongr_m [in Ergo.CCX]
RAW.addk_morphism [in Ergo.CPolynoms]
RAW.addk_m_m [in Ergo.CPolynoms]
RAW.add_equiv [in Ergo.CPolynoms]
RAW.add_monome_equiv [in Ergo.CPolynoms]
RAW.add_const_equiv [in Ergo.CPolynoms]
RAW.add_monome_m [in Ergo.CPolynoms]
RAW.add_const_m [in Ergo.CPolynoms]
RAW.add_m [in Ergo.CPolynoms]
RAW.cancel_equiv [in Ergo.CPolynoms]
RAW.cancel_m [in Ergo.CPolynoms]
RAW.cardinal_m [in Ergo.CPolynoms]
RAW.choose_m [in Ergo.CPolynoms]
RAW.coef_of_m [in Ergo.CPolynoms]
RAW.coef_of_equiv [in Ergo.CPolynoms]
RAW.div_equiv [in Ergo.CPolynoms]
RAW.div_m [in Ergo.CPolynoms]
RAW.elements_m [in Ergo.CPolynoms]
RAW.embed_m [in Ergo.CPolynoms]
RAW.equiv_Transitive [in Ergo.CPolynoms]
RAW.equiv_Symmetric [in Ergo.CPolynoms]
RAW.equiv_Reflexive [in Ergo.CPolynoms]
RAW.eq_equiv [in Ergo.CPolynoms]
RAW.extract_m [in Ergo.CPolynoms]
RAW.find_m [in Ergo.CPolynoms]
RAW.fold_coefs_m [in Ergo.CPolynoms]
RAW.fold_m [in Ergo.CPolynoms]
RAW.In_m [in Ergo.CPolynoms]
RAW.is_compare_m [in Ergo.CPolynoms]
RAW.leaves_m [in Ergo.CPolynoms]
RAW.map2_m [in Ergo.CPolynoms]
RAW.mult_equiv [in Ergo.CPolynoms]
RAW.mult_m [in Ergo.CPolynoms]
RAW.padd_m [in Ergo.CPolynoms]
RAW.remove_m [in Ergo.CPolynoms]
RAW.sub_equiv [in Ergo.CPolynoms]
RAW.sub_m [in Ergo.CPolynoms]
RAW.Wf_div [in Ergo.CPolynoms]
RAW.Wf_sub [in Ergo.CPolynoms]
RAW.Wf_add [in Ergo.CPolynoms]
RAW.Wf_add_monome [in Ergo.CPolynoms]
RAW.Wf_addk [in Ergo.CPolynoms]
RAW.Wf_cancel [in Ergo.CPolynoms]
RAW.Wf_add_const [in Ergo.CPolynoms]
RAW.Wf_mult [in Ergo.CPolynoms]
RAW.Wf_embed [in Ergo.CPolynoms]
RAW.Wf_Pq [in Ergo.CPolynoms]
RAW.Wf_Pz [in Ergo.CPolynoms]
RAW.Wf_P1 [in Ergo.CPolynoms]
RAW.Wf_P0 [in Ergo.CPolynoms]

S

SAT.compat_unitary [in Ergo.Sat]
SAT.compat_red [in Ergo.Sat]
SAT.compat_mem2 [in Ergo.Sat]
SAT.compat_elim [in Ergo.Sat]
SAT.compat_mem [in Ergo.Sat]
SAT.C_csize [in Ergo.Sat]
SAT.C_lsize [in Ergo.Sat]
SAT.derivable_morphism [in Ergo.Sat]
SAT.eq_Seq_m [in Ergo.Sat]
SAT.eq_Seq_Equivalence [in Ergo.Sat]
solution_eq_Equiv [in Ergo.Theory]
solve_m [in Ergo.TheoryArith]
subst_m [in Ergo.TheoryArith]
symbol_UOT [in Ergo.TermUtils]

T

terms_UOT [in Ergo.TermUtils]
term_of_R_m [in Ergo.TheoryArith]
term_UOT [in Ergo.TermUtils]
THEORY.Th [in Ergo.CCX]
THEORY.ThSpecs [in Ergo.CCX]
tminus_m [in Ergo.TheoryArith]
tmult_m [in Ergo.TheoryArith]
topp_m [in Ergo.TheoryArith]
tplus_m [in Ergo.TheoryArith]

W

Wf_merge' [in Ergo.Uf]
Wf_merge [in Ergo.Uf]
Wf_add [in Ergo.Uf]
Wf_empty [in Ergo.Uf]
Wf_separate [in Ergo.Diff]
Wf_empty [in Ergo.Diff]

---

Section Index

A

Abstractions [in Ergo.Ergo]
Abstractions2 [in Ergo.Ergo]
AdequationLazy.Adequation [in Ergo.TacticLazy]
AnyOrderedType [in Ergo.Diff]
AnyOrderedType.WithSpecs [in Ergo.Diff]

C

CanonicalStructure [in Ergo.Term]
Compose [in Ergo.DistrNeg]

D

DBExample [in GeneratorsNG]
DBExample [in Generators]
DBExample2 [in Generators]
DistrNeg [in Ergo.DistrNeg]

E

Einstein [in EinsteinEasy]
Einstein [in EinsteinEasy2]
EquivExample [in Generators]
Example [in GeneratorsNG]
Example [in Generators]

F

FExample [in Generators]
FInterp [in Ergo.Ergo]
FormSize [in Ergo.CNFLazyN]
FULL.WithVars [in Ergo.CPolynoms]

G

GenericCongrClosure.WithRelation [in Ergo.ModelsRingExt]
GenericCongrClosure.WithRelation.Closure [in Ergo.ModelsRingExt]

H

HoleWithListVars [in GeneratorsNG]

I

IllTypedEqualities [in Ergo.ModelsRingExt]
Interp [in Ergo.Ergo]
Interp [in Ergo.Term]
Interp [in Ergo.DistrNeg]
Interp.Interps [in Ergo.Term]
Inverse_Image [in Ergo.Lexico]
IterOps [in Ergo.TheoryArith]

L

LITERAL.ExpandNot [in Ergo.Literal]
LITINDEX.AtomOrderedType [in Ergo.LLazy]
LLAZYFY.ExpandNot [in Ergo.LLazy]
LtList [in Ergo.LLazy]

M

Morphisms [in Ergo.DistrNeg]
Morphisms2 [in Ergo.DistrNeg]

P

Props [in Ergo.DistrNeg]

R

RAWCCX.CleanUp [in Ergo.CCX]
RAW.Interp [in Ergo.LLazy]
RAW.ListSize [in Ergo.LLazy]
RAW.LiteralInduction [in Ergo.LLazy]
RAW.LiteralInductionDefault [in Ergo.LLazy]
RAW.OrderedType [in Ergo.LLazy]
RAW.Size [in Ergo.LLazy]
RAW.WithVars [in Ergo.CPolynoms]
Reverse_Induction [in Ergo.FoldProps]

S

SATCAML.BCP [in Ergo.SatCaml]
SATCAML.Reduce [in Ergo.SatCaml]
SAT.Filtering [in Ergo.Sat]
SAT.Filtering.Finding [in Ergo.Sat]
SAT.Measure [in Ergo.Sat]
SAT.Weakening [in Ergo.Sat]
SEMANTICS.Creation [in Ergo.Semantics]
SEM_INTERFACE.WF [in Ergo.Semantics]
SetFoldInd.fold_relation [in Ergo.FoldProps]
SetFoldInd.fold_induction [in Ergo.FoldProps]
SExample [in Generators]
Solution_OT [in Ergo.Theory]
Symbol_as_UOT.Arithop_as_UOT [in Ergo.TermUtils]
Symbol_as_UOT.ArithDomain_as_UOT [in Ergo.TermUtils]
Symbol_as_UOT [in Ergo.TermUtils]

T

TermInduction [in Ergo.Term]
TermMutualInduction [in Ergo.TermUtils]
Test [in Ergo.TheoryArith]
TheorySpecs [in Ergo.Theory]
TInterp [in Ergo.Term]

V

VExample [in Generators]

W

WfInclusion [in Ergo.Lexico]
Wf_lt_lexic [in Ergo.Lexico]
WithListVars [in GeneratorsNG]
WithModelsAndR [in Ergo.ModelsRingExt]
WithOT [in Ergo.DiagProd]
WithTheory [in Ergo.Use]
WithTheory [in Ergo.Uf]
WithTheorySpecs [in Ergo.Use]
WithTheorySpecs [in Ergo.Uf]
WithTheorySpecs [in Ergo.Theory]

Z

ZEntailment [in Ergo.TheoryArith]
ZEntailment.MakeOps [in Ergo.TheoryArith]

---

Abbreviation Index

C

CNFLAZYCOMMON.clause [in Ergo.CNFLazyCommon]
CNFLAZYCOMMON.cset [in Ergo.CNFLazyCommon]
CNFLAZYCOMMON.lset [in Ergo.CNFLazyCommon]
CNF.clause [in Ergo.Cnf]
CNF.cset [in Ergo.Cnf]
CNF.lset [in Ergo.Cnf]

F

f_idx2 [in Ergo.TheoryArith]
f_idx1 [in Ergo.TheoryArith]

G

g_idx2 [in Ergo.TheoryArith]
g_idx1 [in Ergo.TheoryArith]

I

is_system [in EinsteinEasy]
is_person [in EinsteinEasy]
is_color [in EinsteinEasy]
is_house [in EinsteinEasy]
is_system [in EinsteinEasy2]
is_person [in EinsteinEasy2]
is_color [in EinsteinEasy2]
is_house [in EinsteinEasy2]

L

LITERAL.clause [in Ergo.Literal]
LITERAL.cset [in Ergo.Literal]
LITERAL.lset [in Ergo.Literal]
LLAZYFY.clause [in Ergo.LLazy]
LLAZYFY.cset [in Ergo.LLazy]
LLAZYFY.lllt [in Ergo.LLazy]
LLAZYFY.llt [in Ergo.LLazy]
LLAZYFY.lset [in Ergo.LLazy]

R

RAW.lllt [in Ergo.LLazy]
RAW.llt [in Ergo.LLazy]
r1 [in Ergo.TheoryArith]
r2 [in Ergo.TheoryArith]

T

t [in Ergo.TheoryArith]
tcons [in Ergo.Term]
terms [in Ergo.Term]
TestsDeCCXA.a [in Ergo.CCX]
TestsDeCCXA.b [in Ergo.CCX]
TestsDeCCXA.bottom [in Ergo.CCX]
TestsDeCCXA.c [in Ergo.CCX]
TestsDeCCXA.f [in Ergo.CCX]
TestsDeCCXA.fa [in Ergo.CCX]
TestsDeCCXA.fb [in Ergo.CCX]
TestsDeCCXA.fc [in Ergo.CCX]
TestsDeCCXA.f2a [in Ergo.CCX]
TestsDeCCXA.f3a [in Ergo.CCX]
TestsDeCCXA.f4a [in Ergo.CCX]
TestsDeCCXA.f5a [in Ergo.CCX]
TestsDeCCXA.g [in Ergo.CCX]
TestsDeCCXA.ga [in Ergo.CCX]
TestsDeCCXA.gb [in Ergo.CCX]
TestsDeCCXA.gc [in Ergo.CCX]
TestsDeCCXA.one [in Ergo.CCX]
TestsDeCCXA.ta [in Ergo.CCX]
TestsDeCCXA.tb [in Ergo.CCX]
TestsDeCCXA.tc [in Ergo.CCX]
TestsDeCCXA.tfx [in Ergo.CCX]
TestsDeCCXA.tfxzero [in Ergo.CCX]
TestsDeCCXA.tf1 [in Ergo.CCX]
TestsDeCCXA.tone [in Ergo.CCX]
TestsDeCCXA.tx [in Ergo.CCX]
TestsDeCCXA.txzero [in Ergo.CCX]
TestsDeCCXA.tzero [in Ergo.CCX]
TestsDeCCXA.x [in Ergo.CCX]
TestsDeCCXA.zero [in Ergo.CCX]
TestsDeCCXE.a [in Ergo.CCX]
TestsDeCCXE.b [in Ergo.CCX]
TestsDeCCXE.c [in Ergo.CCX]
TestsDeCCXE.f [in Ergo.CCX]
TestsDeCCXE.fa [in Ergo.CCX]
TestsDeCCXE.fb [in Ergo.CCX]
TestsDeCCXE.fc [in Ergo.CCX]
TestsDeCCXE.f2a [in Ergo.CCX]
TestsDeCCXE.f3a [in Ergo.CCX]
TestsDeCCXE.f4a [in Ergo.CCX]
TestsDeCCXE.f5a [in Ergo.CCX]
TestsDeCCXE.g [in Ergo.CCX]
TestsDeCCXE.ga [in Ergo.CCX]
TestsDeCCXE.gb [in Ergo.CCX]
TestsDeCCXE.gc [in Ergo.CCX]
TestsDeCCXE.ta [in Ergo.CCX]
TestsDeCCXE.tb [in Ergo.CCX]
TestsDeCCXE.tc [in Ergo.CCX]
tnil [in Ergo.Term]
tr1 [in Ergo.TheoryArith]
tr2 [in Ergo.TheoryArith]
t0 [in Ergo.TheoryArith]
t1 [in Ergo.TheoryArith]

U

u [in Ergo.TheoryArith]

Z

Z_idx [in Ergo.TheoryArith]

---

Definition Index

A

add [in Ergo.Use]
add [in Ergo.Uf]
AdequationLazy.canonical_model [in Ergo.TacticLazy]
AdequationLazy.interp [in Ergo.TacticLazy]
ainterp [in Ergo.Ergo]
ainterp_eq [in Ergo.Ergo]
all_are_true [in Generators]
all_variables_differ [in Generators]
ant [in Generators]
are_diff [in Ergo.Diff]
arithop_equal [in Ergo.Term]
arithop_OT [in Ergo.TermUtils]
ArithTheory.Th [in Ergo.TheoryArith]
arith_domain_OT [in Ergo.TermUtils]

B

binterp [in Ergo.Ergo]
binterp_eq [in Ergo.Ergo]
BoolasDT.eq_dec [in Ergo.Term]
BoolasDT.U [in Ergo.Term]

C

CCX.assume [in Ergo.CCX]
CCX.assumed [in Ergo.CCX]
CCX.empty [in Ergo.CCX]
CCX.query [in Ergo.CCX]
CCX.t [in Ergo.CCX]
cinterp [in Ergo.DistrNeg]
cmp_terms_sym [in Ergo.TermUtils]
cmp_term_sym [in Ergo.TermUtils]
cmp_terms_eq [in Ergo.TermUtils]
cmp_term_eq [in Ergo.TermUtils]
CNFLAZYCOMMON.clause_OT [in Ergo.CNFLazyCommon]
CNFLAZYCOMMON.formula [in Ergo.CNFLazyCommon]
CNFLAZYCOMMON.pick [in Ergo.CNFLazyCommon]
CNFLAZYN.and_interp [in Ergo.CNFLazyN]
CNFLAZYN.cfl [in Ergo.CNFLazyN]
CNFLAZYN.Conversion.mk_form [in Ergo.CNFLazyN]
CNFLAZYN.Conversion.mk_or_list [in Ergo.CNFLazyN]
CNFLAZYN.Conversion.mk_and_list [in Ergo.CNFLazyN]
CNFLAZYN.interp [in Ergo.CNFLazyN]
CNFLAZYN.make [in Ergo.CNFLazyN]
CNFLAZYN.mk_iff [in Ergo.CNFLazyN]
CNFLAZYN.mk_iff_ [in Ergo.CNFLazyN]
CNFLAZYN.mk_impl [in Ergo.CNFLazyN]
CNFLAZYN.mk_impl_ [in Ergo.CNFLazyN]
CNFLAZYN.mk_and [in Ergo.CNFLazyN]
CNFLAZYN.mk_and_ [in Ergo.CNFLazyN]
CNFLAZYN.mk_or [in Ergo.CNFLazyN]
CNFLAZYN.mk_or_ [in Ergo.CNFLazyN]
CNFLAZYN.mk_false [in Ergo.CNFLazyN]
CNFLAZYN.mk_true [in Ergo.CNFLazyN]
CNFLAZYN.mk_lit [in Ergo.CNFLazyN]
CNFLAZYN.mk_lit_ [in Ergo.CNFLazyN]
CNFLAZYN.or_interp [in Ergo.CNFLazyN]
CNFLAZY_INTERFACE.interp [in Ergo.CNFLazyCommon]
CNFLAZY.cfl [in Ergo.CNFLazy]
CNFLAZY.Conversion.mk_form [in Ergo.CNFLazy]
CNFLAZY.interp [in Ergo.CNFLazy]
CNFLAZY.make [in Ergo.CNFLazy]
CNFLAZY.mk_iff [in Ergo.CNFLazy]
CNFLAZY.mk_impl [in Ergo.CNFLazy]
CNFLAZY.mk_and [in Ergo.CNFLazy]
CNFLAZY.mk_or [in Ergo.CNFLazy]
CNFLAZY.mk_false [in Ergo.CNFLazy]
CNFLAZY.mk_true [in Ergo.CNFLazy]
CNFLAZY.mk_lit [in Ergo.CNFLazy]
CNFRAW.mk_iff [in Ergo.CNFLazy]
CNFRAW.mk_impl [in Ergo.CNFLazy]
CNFRAW.mk_and [in Ergo.CNFLazy]
CNFRAW.mk_or [in Ergo.CNFLazy]
CNFRAW.mk_false [in Ergo.CNFLazy]
CNFRAW.mk_true [in Ergo.CNFLazy]
CNFRAW.mk_lit [in Ergo.CNFLazy]
common_denom [in Ergo.TheoryArith]
compare_list [in Ergo.LLazy]
compare_cst [in Ergo.TermUtils]
congruent [in Ergo.Uf]
crowded [in Generators]
crowded_aux [in Generators]
crowded_aux_2 [in Generators]
cst_equal [in Ergo.Term]

D

deb1 [in GeneratorsNG]
deb1 [in Generators]
deb10 [in GeneratorsNG]
deb10 [in Generators]
deb2 [in GeneratorsNG]
deb2 [in Generators]
deb50 [in GeneratorsNG]
deb50 [in Generators]
deb6 [in GeneratorsNG]
deb6 [in Generators]
depvarmap [in Ergo.Term]
de_bruijn [in GeneratorsNG]
de_bruijn [in Generators]
diagProd [in Ergo.DiagProd]
diagProd_aux [in Ergo.DiagProd]
diamond [in GeneratorsEq]
diamond_Zequations [in GeneratorsEq]
diamond_equations [in GeneratorsEq]
differs [in Generators]
distr_neg [in Ergo.DistrNeg]
dom [in Ergo.Term]
DomainDT.U [in Ergo.TermUtils]
dom_equal [in Ergo.Term]
dom_interp [in Ergo.Term]

E

empty [in Ergo.Use]
empty [in Ergo.Uf]
empty [in Ergo.Diff]
EmptyTheory.Th [in Ergo.Theory]
EmptyTheory.ThSpecs [in Ergo.Theory]
empty_maps [in Ergo.Ergo]
ENVLAZY.assume [in Ergo.EnvLazy]
ENVLAZY.assumed [in Ergo.EnvLazy]
ENVLAZY.empty [in Ergo.EnvLazy]
ENVLAZY.is_prop [in Ergo.EnvLazy]
ENVLAZY.oapply [in Ergo.EnvLazy]
ENVLAZY.query [in Ergo.EnvLazy]
ENVLAZY.t [in Ergo.EnvLazy]
ENV.assume [in Ergo.Env]
ENV.assumed [in Ergo.Env]
ENV.empty [in Ergo.Env]
ENV.query [in Ergo.Env]
ENV.t [in Ergo.Env]
eq [in Ergo.ModelsRingExt]
eq [in Ergo.Term]
equals [in GeneratorsNG]
equals [in Generators]
equivn [in Generators]
equiv1 [in Generators]
equiv10 [in Generators]
equiv2 [in Generators]
equiv30 [in Generators]
eq_congr [in Ergo.ModelsRingExt]
eq_trans [in Ergo.ModelsRingExt]
eq_sym [in Ergo.ModelsRingExt]
eq_refl [in Ergo.ModelsRingExt]
everyone_happy [in GeneratorsNG]
everyone_happy_aux [in GeneratorsNG]
everyone_home [in GeneratorsNG]
everyone_home_aux [in GeneratorsNG]
everyone_happy [in Generators]
everyone_happy_aux [in Generators]
everyone_home [in Generators]
everyone_home_aux [in Generators]

F

fdiamond [in GeneratorsEq]
fdiamond_equations [in GeneratorsEq]
fibo [in GeneratorsEq]
fibo_arith [in GeneratorsEq]
fibo_defs [in GeneratorsEq]
find [in Ergo.Use]
find [in Ergo.Uf]
finterp [in Ergo.Ergo]
Fn [in Generators]
form_size [in Ergo.CNFLazyN]
FP [in AltDemo]
FULL.add [in Ergo.CPolynoms]
FULL.addk [in Ergo.CPolynoms]
FULL.add_monome [in Ergo.CPolynoms]
FULL.add_const [in Ergo.CPolynoms]
FULL.cancel [in Ergo.CPolynoms]
FULL.choose [in Ergo.CPolynoms]
FULL.coef_of [in Ergo.CPolynoms]
FULL.div [in Ergo.CPolynoms]
FULL.embed [in Ergo.CPolynoms]
FULL.equiv [in Ergo.CPolynoms]
FULL.extract [in Ergo.CPolynoms]
FULL.is_const [in Ergo.CPolynoms]
FULL.leaves [in Ergo.CPolynoms]
FULL.mult [in Ergo.CPolynoms]
FULL.Pq [in Ergo.CPolynoms]
FULL.Pz [in Ergo.CPolynoms]
FULL.P0 [in Ergo.CPolynoms]
FULL.P1 [in Ergo.CPolynoms]
FULL.reminder [in Ergo.CPolynoms]
FULL.sub [in Ergo.CPolynoms]
f1 [in Generators]
f10 [in Generators]
f2 [in Generators]
f30 [in Generators]

G

GenericCongrClosure.Congruence [in Ergo.ModelsRingExt]
GenericCongrClosure.forall2 [in Ergo.ModelsRingExt]
GenericCongrClosure.forall3 [in Ergo.ModelsRingExt]
GenericCongrClosure.linked [in Ergo.ModelsRingExt]
GenericCongrClosure.path [in Ergo.ModelsRingExt]
GenericCongrClosure.plunge_and_flatten [in Ergo.ModelsRingExt]

H

has_type [in Ergo.Term]
have_type [in Ergo.Term]
hole [in GeneratorsNG]
hole [in Generators]
hole1 [in GeneratorsNG]
hole1 [in Generators]
hole10 [in GeneratorsNG]
hole10 [in Generators]
hole2 [in GeneratorsNG]
hole2 [in Generators]
hole6 [in GeneratorsNG]
hole6 [in Generators]

I

implyX [in Ergo.Theory]
INDEX.compare_ [in Ergo.Index]
INDEX.eq [in Ergo.Index]
INDEX.lt [in Ergo.Index]
INDEX.t [in Ergo.Index]
INDEX.t_OT [in Ergo.Index]
input_to_lit [in Ergo.CCX]
int [in Ergo.Term]
interp [in Ergo.Ergo]
interp [in Ergo.Term]
interps [in Ergo.Term]
interps_ [in Ergo.Term]
interp_op [in Ergo.Term]
interp' [in Ergo.Term]
introduce_vars [in GeneratorsNG]
in_list [in Ergo.Use]
isM [in Ergo.TheoryArith]
isMpoly [in Ergo.TheoryArith]
isZpoly [in Ergo.TheoryArith]
is_home [in GeneratorsNG]
is_home [in Generators]
iter [in Ergo.Theory]

K

K.classic [in Ergo.AllInstances]

L

leaves [in Ergo.TheoryArith]
lex2 [in Ergo.Lexico]
LITERAL.clause_OT [in Ergo.Literal]
LITERAL.llsize [in Ergo.Literal]
LITERAL.lsize [in Ergo.Literal]
LITINDEX.interp [in Ergo.LLazy]
LITINDEX.interp_atom [in Ergo.LLazy]
LITINDEX.lfalse [in Ergo.LLazy]
LITINDEX.lookup [in Ergo.LLazy]
LITINDEX.ltrue [in Ergo.LLazy]
LITINDEX.mk_not [in Ergo.LLazy]
LITINDEX.t [in Ergo.LLazy]
LLAZYFY.clause_OT [in Ergo.LLazy]
LLAZYFY.eq [in Ergo.LLazy]
LLAZYFY.expand [in Ergo.LLazy]
LLAZYFY.interp [in Ergo.LLazy]
LLAZYFY.interp_mk_not [in Ergo.LLazy]
LLAZYFY.is_proxy [in Ergo.LLazy]
LLAZYFY.lfalse [in Ergo.LLazy]
LLAZYFY.llsize [in Ergo.LLazy]
LLAZYFY.lsize [in Ergo.LLazy]
LLAZYFY.lt [in Ergo.LLazy]
LLAZYFY.ltrue [in Ergo.LLazy]
LLAZYFY.mk_not [in Ergo.LLazy]
LLAZYFY.negation [in Ergo.LLazy]
LLAZYFY.size [in Ergo.LLazy]
LLAZYFY.t [in Ergo.LLazy]
ll_interp [in Ergo.DistrNeg]
Ln [in Generators]
LoadTactic.dpll [in Ergo.TacticLazy]
LoadTactic.dpll' [in Ergo.TacticLazy]
lookup [in Ergo.Term]
lookup_type [in Ergo.Term]
lt_list [in Ergo.LLazy]
l_interp [in Ergo.DistrNeg]

M

make [in Ergo.TheoryArith]
mem [in Ergo.Uf]
merge [in Ergo.Use]
merge [in Ergo.Uf]
merge_touched_spec_2 [in Ergo.Uf]
merge_touched_spec [in Ergo.Uf]
merge_touched [in Ergo.Uf]
merge' [in Ergo.Uf]
mi [in Ergo.TheoryArith]
mk_term [in Ergo.TheoryArith]
mk_depvmap [in Ergo.Term]
mk_symbol [in Ergo.Term]
myType [in Ergo.CCX]

N

neqs [in Ergo.Diff]
num_classes [in Ergo.Uf]

O

occ [in GeneratorsNG]
one [in Ergo.TheoryArith]
one_is_false [in Generators]
one_is_crowded [in Generators]
one_is_crowded_aux [in Generators]
orderAB [in Ergo.Lexico]

P

partage [in Generators]
partage2 [in Generators]
pinterp [in Ergo.DistrNeg]
pl [in Ergo.TheoryArith]
power [in Demo]
power [in AltDemo]
power [in GeneratorsEq]
powerZ [in Demo]
powerZ [in AltDemo]

Q

QasDT.U [in Ergo.Rational]

R

R [in Ergo.TheoryArith]
range [in Ergo.Uf]
rational_OT [in Ergo.Rational]
RAWCCX.are_diff [in Ergo.CCX]
RAWCCX.are_equal [in Ergo.CCX]
RAWCCX.assume [in Ergo.CCX]
RAWCCX.assumed [in Ergo.CCX]
RAWCCX.diff [in Ergo.CCX]
RAWCCX.empty [in Ergo.CCX]
RAWCCX.find_add_equations [in Ergo.CCX]
RAWCCX.find_congr_equations [in Ergo.CCX]
RAWCCX.find_congr_equations2 [in Ergo.CCX]
RAWCCX.find_congr_equations1 [in Ergo.CCX]
RAWCCX.guard [in Ergo.CCX]
RAWCCX.guarded_wf_lt [in Ergo.CCX]
RAWCCX.incoherent [in Ergo.CCX]
RAWCCX.inter_leaves [in Ergo.CCX]
RAWCCX.lcongr [in Ergo.CCX]
RAWCCX.lexists [in Ergo.CCX]
RAWCCX.lleaves [in Ergo.CCX]
RAWCCX.merge [in Ergo.CCX]
RAWCCX.num_pending [in Ergo.CCX]
RAWCCX.num_distinct_pairs [in Ergo.CCX]
RAWCCX.query [in Ergo.CCX]
RAWCCX.Specs.add_terms_dec [in Ergo.CCX]
RAWCCX.Specs.add_term_dec [in Ergo.CCX]
RAWCCX.Specs.coherent [in Ergo.CCX]
RAWCCX.Specs.eqns_of [in Ergo.CCX]
RAWCCX.Specs.input_range [in Ergo.CCX]
RAWCCX.Specs.input_assume [in Ergo.CCX]
RAWCCX.Specs.iter [in Ergo.CCX]
RAWCCX.Specs.Ncoincides [in Ergo.CCX]
RAWCCX.Specs.pack [in Ergo.CCX]
RAWCCX.t [in Ergo.CCX]
RAWCCX.terms_of [in Ergo.CCX]
RAWCCX.terms_of_list [in Ergo.CCX]
RAWCCX.uncongr [in Ergo.CCX]
RAW.add [in Ergo.CPolynoms]
RAW.addk [in Ergo.CPolynoms]
RAW.addk_m [in Ergo.CPolynoms]
RAW.add_monome [in Ergo.CPolynoms]
RAW.add_const [in Ergo.CPolynoms]
RAW.cancel [in Ergo.CPolynoms]
RAW.choose [in Ergo.CPolynoms]
RAW.cinterp [in Ergo.LLazy]
RAW.coef_of [in Ergo.CPolynoms]
RAW.compare_ [in Ergo.LLazy]
RAW.div [in Ergo.CPolynoms]
RAW.embed [in Ergo.CPolynoms]
RAW.eq [in Ergo.LLazy]
RAW.equiv [in Ergo.CPolynoms]
RAW.expand [in Ergo.LLazy]
RAW.extract [in Ergo.CPolynoms]
RAW.fold_coefs [in Ergo.CPolynoms]
RAW.interp [in Ergo.LLazy]
RAW.is_const [in Ergo.CPolynoms]
RAW.leaves [in Ergo.CPolynoms]
RAW.lfalse [in Ergo.LLazy]
RAW.literal_ind2 [in Ergo.LLazy]
RAW.llsize [in Ergo.LLazy]
RAW.lsize [in Ergo.LLazy]
RAW.lt [in Ergo.LLazy]
RAW.ltrue [in Ergo.LLazy]
RAW.MapQ_OT [in Ergo.CPolynoms]
RAW.mk_not [in Ergo.LLazy]
RAW.mult [in Ergo.CPolynoms]
RAW.pinterp [in Ergo.LLazy]
RAW.poly [in Ergo.CPolynoms]
RAW.poly_OT [in Ergo.CPolynoms]
RAW.Pq [in Ergo.CPolynoms]
RAW.Pz [in Ergo.CPolynoms]
RAW.P0 [in Ergo.CPolynoms]
RAW.P1 [in Ergo.CPolynoms]
RAW.size [in Ergo.LLazy]
RAW.sub [in Ergo.CPolynoms]
RAW.t [in Ergo.LLazy]
RAW.vars_of [in Ergo.CPolynoms]
reprs [in Ergo.Uf]
Rn [in Generators]
room_mate [in Generators]
Rz [in Ergo.TheoryArith]
R_OT [in Ergo.TheoryArith]
R0 [in Ergo.TheoryArith]
R1 [in Ergo.TheoryArith]

S

safe [in GeneratorsNG]
safe [in Generators]
sane [in GeneratorsNG]
sane [in Generators]
sane_aux [in GeneratorsNG]
sane_aux_2 [in GeneratorsNG]
sane_aux [in Generators]
sane_aux_2 [in Generators]
SATCAML.bcp [in Ergo.SatCaml]
SATCAML.compatible_e [in Ergo.SatCaml]
SATCAML.dpll [in Ergo.SatCaml]
SATCAML.extend [in Ergo.SatCaml]
SATCAML.ll2s [in Ergo.SatCaml]
SATCAML.l2s [in Ergo.SatCaml]
SATCAML.proof_search [in Ergo.SatCaml]
SATCAML.reduce [in Ergo.SatCaml]
SATCAML.submodel_e [in Ergo.SatCaml]
SAT.csize [in Ergo.Sat]
SAT.dpll [in Ergo.Sat]
SAT.eliminable [in Ergo.Sat]
SAT.eq_Seq [in Ergo.Sat]
SAT.find [in Ergo.Sat]
SAT.incompatible [in Ergo.Sat]
SAT.lsize [in Ergo.Sat]
SAT.model_expand [in Ergo.Sat]
SAT.proof_search [in Ergo.Sat]
SAT.reducible [in Ergo.Sat]
SAT.sat_goal_e [in Ergo.Sat]
SAT.sat_clause_e [in Ergo.Sat]
SAT.select [in Ergo.Sat]
SAT.size [in Ergo.Sat]
SAT.sub_sequent [in Ergo.Sat]
SAT.unitary [in Ergo.Sat]
SAT.wf_expand [in Ergo.Sat]
SAT.wf_context [in Ergo.Sat]
schwicht [in Generators]
SEMANTICS.consistent [in Ergo.Semantics]
SEMANTICS.full [in Ergo.Semantics]
SEMANTICS.incompatible [in Ergo.Semantics]
SEMANTICS.model [in Ergo.Semantics]
SEMANTICS.model_of [in Ergo.Semantics]
SEMANTICS.model_as_fun [in Ergo.Semantics]
SEMANTICS.model_ [in Ergo.Semantics]
SEMANTICS.morphism [in Ergo.Semantics]
SEMANTICS.sat_goal_p [in Ergo.Semantics]
SEMANTICS.sat_clause_p [in Ergo.Semantics]
SEMANTICS.sat_goal [in Ergo.Semantics]
SEMANTICS.sat_clause [in Ergo.Semantics]
SEMANTICS.submodel [in Ergo.Semantics]
SEMANTICS.wf_expand [in Ergo.Semantics]
SEMANTICS.wf_true [in Ergo.Semantics]
SEMANTICS.WF.consistent [in Ergo.Semantics]
SEMANTICS.WF.full [in Ergo.Semantics]
SEMANTICS.WF.morphism [in Ergo.Semantics]
SEMANTICS.WF.wf_expand [in Ergo.Semantics]
SEMANTICS.WF.wf_true [in Ergo.Semantics]
SEMLAZY.disequation [in Ergo.SemLazy]
SEMLAZY.entails [in Ergo.SemLazy]
SEMLAZY.equation [in Ergo.SemLazy]
SEMLAZY.incompatible [in Ergo.SemLazy]
SEMLAZY.model [in Ergo.SemLazy]
SEMLAZY.models_list_iff [in Ergo.SemLazy]
SEMLAZY.models_neq [in Ergo.SemLazy]
SEMLAZY.models_eq [in Ergo.SemLazy]
SEMLAZY.model_as_fun [in Ergo.SemLazy]
SEMLAZY.model_as_fun_l [in Ergo.SemLazy]
SEMLAZY.sat_goal_p [in Ergo.SemLazy]
SEMLAZY.sat_clause_p [in Ergo.SemLazy]
SEMLAZY.sat_goal [in Ergo.SemLazy]
SEMLAZY.sat_clause [in Ergo.SemLazy]
SEMLAZY.submodel [in Ergo.SemLazy]
SEM_INTERFACE.sat_goal_p [in Ergo.Semantics]
SEM_INTERFACE.sat_clause_p [in Ergo.Semantics]
SEM_INTERFACE.incompatible [in Ergo.Semantics]
SEM_INTERFACE.submodel [in Ergo.Semantics]
SEM_INTERFACE.sat_goal [in Ergo.Semantics]
SEM_INTERFACE.sat_clause [in Ergo.Semantics]
separate [in Ergo.Diff]
SetFoldInd.Pl [in Ergo.FoldProps]
SetFoldInd.set_of_list [in Ergo.FoldProps]
size [in Ergo.CNFLazyN]
solve [in Ergo.TheoryArith]
some_are_equal [in GeneratorsNG]
some_are_equal [in Generators]
stripR [in Ergo.TheoryArith]
subst [in Ergo.TheoryArith]
symbol_equal [in Ergo.Term]
symbol_OT [in Ergo.TermUtils]
symbol_cmp [in Ergo.TermUtils]
symbol_StrictOrder [in Ergo.TermUtils]
s1 [in Generators]
s10 [in Generators]
s2 [in Generators]
s30 [in Generators]

T

t [in Ergo.Use]
t [in Ergo.Uf]
t [in Ergo.Diff]
tdiv [in Ergo.ModelsRingExt]
tequal [in Ergo.Term]
terms_of [in Ergo.Use]
terms_OT [in Ergo.TermUtils]
terms_lt_trans [in Ergo.TermUtils]
terms_lt [in Ergo.TermUtils]
term_of_R [in Ergo.TheoryArith]
term_env [in Ergo.Term]
term_equal [in Ergo.Term]
term_terms_rect [in Ergo.Term]
term_OT [in Ergo.TermUtils]
term_lt_trans [in Ergo.TermUtils]
term_lt [in Ergo.TermUtils]
term_terms_rect_default [in Ergo.TermUtils]
TestsDeCCXA.e [in Ergo.CCX]
TestsDeCCXA.ea1 [in Ergo.CCX]
TestsDeCCXA.ea2 [in Ergo.CCX]
TestsDeCCXA.ea2' [in Ergo.CCX]
TestsDeCCXA.ea2'' [in Ergo.CCX]
TestsDeCCXA.ea2''' [in Ergo.CCX]
TestsDeCCXA.ea2'''' [in Ergo.CCX]
TestsDeCCXA.ea2''''' [in Ergo.CCX]
TestsDeCCXA.e1 [in Ergo.CCX]
TestsDeCCXA.e1' [in Ergo.CCX]
TestsDeCCXA.e1'' [in Ergo.CCX]
TestsDeCCXA.e2 [in Ergo.CCX]
TestsDeCCXA.e3 [in Ergo.CCX]
TestsDeCCXA.strip [in Ergo.CCX]
TestsDeCCXA.stripR [in Ergo.CCX]
TestsDeCCXA.TestNewUse.e1 [in Ergo.CCX]
TestsDeCCXA.TestNewUse.e2 [in Ergo.CCX]
TestsDeCCXE.e [in Ergo.CCX]
TestsDeCCXE.e1 [in Ergo.CCX]
TestsDeCCXE.e1' [in Ergo.CCX]
TestsDeCCXE.e1'' [in Ergo.CCX]
TestsDeCCXE.e2 [in Ergo.CCX]
TestsDeCCXE.e3 [in Ergo.CCX]
TestsDeCCXE.strip [in Ergo.CCX]
TestsDeCCXE.TestNewUse.e1 [in Ergo.CCX]
TestsDeCCXE.TestNewUse.e2 [in Ergo.CCX]
TestsDeCCXE.TestNewUse.e3 [in Ergo.CCX]
TestWithNat.a [in Ergo.Term]
TestWithNat.anatbool [in Ergo.Term]
TestWithNat.anatbool_x [in Ergo.Term]
TestWithNat.anatnat [in Ergo.Term]
TestWithNat.b [in Ergo.Term]
TestWithNat.bfalse [in Ergo.Term]
TestWithNat.bfalse2 [in Ergo.Term]
TestWithNat.bool_varmap [in Ergo.Term]
TestWithNat.bool_idx [in Ergo.Term]
TestWithNat.btrue [in Ergo.Term]
TestWithNat.bx [in Ergo.Term]
TestWithNat.fx [in Ergo.Term]
TestWithNat.f3x [in Ergo.Term]
TestWithNat.f5x [in Ergo.Term]
TestWithNat.ia [in Ergo.Term]
TestWithNat.ib [in Ergo.Term]
TestWithNat.inbx [in Ergo.Term]
TestWithNat.interp [in Ergo.Term]
TestWithNat.itwo [in Ergo.Term]
TestWithNat.ix [in Ergo.Term]
TestWithNat.izero [in Ergo.Term]
TestWithNat.nat_arrow_nat_varmap [in Ergo.Term]
TestWithNat.nat_arrow_bool_varmap [in Ergo.Term]
TestWithNat.nat_varmap [in Ergo.Term]
TestWithNat.nat_arrow_nat_idx [in Ergo.Term]
TestWithNat.nat_arrow_bool_idx [in Ergo.Term]
TestWithNat.nat_idx [in Ergo.Term]
TestWithNat.nx [in Ergo.Term]
TestWithNat.n0 [in Ergo.Term]
TestWithNat.n1 [in Ergo.Term]
TestWithNat.n2 [in Ergo.Term]
TestWithNat.power [in Ergo.Term]
TestWithNat.succ [in Ergo.Term]
TestWithNat.tbool [in Ergo.Term]
TestWithNat.test0 [in Ergo.Term]
TestWithNat.tnat [in Ergo.Term]
TestWithNat.tnat_arrow_nat [in Ergo.Term]
TestWithNat.tnat_arrow_bool [in Ergo.Term]
TestWithNat.two [in Ergo.Term]
TestWithNat.variables [in Ergo.Term]
TestWithNat.vtypes [in Ergo.Term]
TestWithNat.x [in Ergo.Term]
TestWithNat.zero [in Ergo.Term]
Test.a [in Ergo.Term]
Test.anatbool [in Ergo.Term]
Test.anatbool_x [in Ergo.Term]
Test.anatnat [in Ergo.Term]
Test.b [in Ergo.Term]
Test.bfalse [in Ergo.Term]
Test.bfalse2 [in Ergo.Term]
Test.bool_varmap [in Ergo.Term]
Test.bool_idx [in Ergo.Term]
Test.btrue [in Ergo.Term]
Test.bx [in Ergo.Term]
Test.fx [in Ergo.Term]
Test.f3x [in Ergo.Term]
Test.f5x [in Ergo.Term]
Test.ia [in Ergo.Term]
Test.ib [in Ergo.Term]
Test.inbx [in Ergo.Term]
Test.interp [in Ergo.Term]
Test.itwo [in Ergo.Term]
Test.ix [in Ergo.Term]
Test.izero [in Ergo.Term]
Test.nat_arrow_nat_varmap [in Ergo.Term]
Test.nat_arrow_bool_varmap [in Ergo.Term]
Test.nat_varmap [in Ergo.Term]
Test.nat_arrow_nat_idx [in Ergo.Term]
Test.nat_arrow_bool_idx [in Ergo.Term]
Test.nat_idx [in Ergo.Term]
Test.nx [in Ergo.Term]
Test.n0 [in Ergo.Term]
Test.n1 [in Ergo.Term]
Test.n2 [in Ergo.Term]
Test.power [in Ergo.Term]
Test.succ [in Ergo.Term]
Test.tbool [in Ergo.Term]
Test.test0 [in Ergo.Term]
Test.tnat [in Ergo.Term]
Test.tnat_arrow_nat [in Ergo.Term]
Test.tnat_arrow_bool [in Ergo.Term]
Test.two [in Ergo.Term]
Test.variables [in Ergo.Term]
Test.vtypes [in Ergo.Term]
Test.x [in Ergo.Term]
Test.zero [in Ergo.Term]
tinterp [in Ergo.Term]
tminus [in Ergo.ModelsRingExt]
tminus [in Ergo.TheoryArith]
tmult [in Ergo.ModelsRingExt]
tmult [in Ergo.TheoryArith]
topp [in Ergo.ModelsRingExt]
topp [in Ergo.TheoryArith]
tplus [in Ergo.ModelsRingExt]
tplus [in Ergo.TheoryArith]
TypeasDT.eq_dec [in Ergo.Term]
TypeasDT.U [in Ergo.Term]
typeBinop [in Ergo.Term]
types_of [in Ergo.Term]
typeUnop [in Ergo.Term]
typeZ [in Ergo.ModelsRingExt]
type_of [in Ergo.Term]
type_env [in Ergo.Term]

U

udeb1 [in Generators]
udeb10 [in Generators]
udeb2 [in Generators]
udeb50 [in Generators]
udeb6 [in Generators]
ude_bruijn [in Generators]
using_all [in Ergo.Use]

V

vhole [in Generators]
vhole1 [in Generators]
vhole10 [in Generators]
vhole2 [in Generators]
vhole6 [in Generators]

X

x [in GeneratorsNG]

Z

Zdiamond [in GeneratorsEq]

---

Record Index

A

abstraction [in Ergo.Ergo]

C

CCX.t_ [in Ergo.CCX]

E

ENVLAZY.t_ [in Ergo.EnvLazy]
ENV.t_ [in Ergo.Env]

F

FULL.poly [in Ergo.CPolynoms]

I

implyX_Specs [in Ergo.Theory]

L

LLAZYFY.t_ [in Ergo.LLazy]

R

RAWCCX.Specs.Wf [in Ergo.CCX]
RAWCCX.t_ [in Ergo.CCX]
RAW.Wf [in Ergo.CPolynoms]

S

SAT.sequent [in Ergo.Sat]
SEMANTICS.model_with_props [in Ergo.Semantics]

T

Theory [in Ergo.Theory]
TheorySpecs [in Ergo.Theory]
t_ [in Ergo.Uf]

V

varmaps [in Ergo.Ergo]

W

Wf [in Ergo.Uf]
Wf [in Ergo.Diff]

---

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

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

(34 entries)

Module Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

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

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

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

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

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

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

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

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

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

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

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

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

(18 entries)