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

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

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

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

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

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

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

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

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

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

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

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

(6 entries)

---

Global Index

A

ABbranches [definition, in octalgo.octalgo.fintrees]
ABheight [definition, in octalgo.octalgo.fintrees]
ABin [definition, in octalgo.octalgo.fintrees]
ABin_extract [lemma, in octalgo.octalgo.fintrees]
ABLeaf [constructor, in octalgo.octalgo.fintrees]
ABmap [definition, in octalgo.octalgo.fintrees]
ABNode [constructor, in octalgo.octalgo.fintrees]
ABnotin [definition, in octalgo.octalgo.fintrees]
ABnotin_branches [lemma, in octalgo.octalgo.fintrees]
ABnotin_map [lemma, in octalgo.octalgo.fintrees]
ABnotin_node_and [lemma, in octalgo.octalgo.fintrees]
ABroot [definition, in octalgo.octalgo.fintrees]
ABtree [inductive, in octalgo.octalgo.fintrees]
ABtree [section, in octalgo.octalgo.fintrees]
abtree_htreeK [lemma, in octalgo.octalgo.fintrees]
ABtree_to_H [definition, in octalgo.octalgo.fintrees]
ABtree_eqMixin [definition, in octalgo.octalgo.fintrees]
abtree_eq_axiom [lemma, in octalgo.octalgo.fintrees]
abtree_inv [lemma, in octalgo.octalgo.fintrees]
abtree_eq_refl [lemma, in octalgo.octalgo.fintrees]
abtree_eq [definition, in octalgo.octalgo.fintrees]
abtree_ind_prop [lemma, in octalgo.octalgo.fintrees]
abtree_ind [lemma, in octalgo.octalgo.fintrees]
ABtree.ABtree_utils [section, in octalgo.octalgo.fintrees]
ABtree.ABtree_countType [section, in octalgo.octalgo.fintrees]
ABtree.ABtree_eqType [section, in octalgo.octalgo.fintrees]
ABtree.InducType [section, in octalgo.octalgo.fintrees]
ABtree.InducType.A [variable, in octalgo.octalgo.fintrees]
ABtree.InducType.B [variable, in octalgo.octalgo.fintrees]
ABuniq [definition, in octalgo.octalgo.fintrees]
ABuniq_map [lemma, in octalgo.octalgo.fintrees]
ABwidth [definition, in octalgo.octalgo.fintrees]
ABwidth_map [lemma, in octalgo.octalgo.fintrees]
ABwidth_cons [lemma, in octalgo.octalgo.fintrees]
ab_ind [projection, in octalgo.octalgo.occurrences]
AB_to_WUnotin_seq [lemma, in octalgo.octalgo.fintrees]
AB_countMixin [definition, in octalgo.octalgo.fintrees]
AB_choiceMixin [definition, in octalgo.octalgo.fintrees]
AB_to_gen [definition, in octalgo.octalgo.fintrees]
add [definition, in octalgo.datalogcert.subs]
addE [lemma, in octalgo.datalogcert.subs]
add_untyped_untyped [lemma, in octalgo.datalogcert.subs]
add_typed_untyped [lemma, in octalgo.datalogcert.subs]
add_com [lemma, in octalgo.datalogcert.subs]
add_add [lemma, in octalgo.datalogcert.subs]
add_seq_gr_def [lemma, in octalgo.octalgo.projection]
all_prop_prop_decr [lemma, in octalgo.octalgo.utils]
all_prop_seq_decr [lemma, in octalgo.octalgo.utils]
all_prop_in [lemma, in octalgo.octalgo.utils]
all_prop_cat [lemma, in octalgo.octalgo.utils]
all_prop_cat_r [lemma, in octalgo.octalgo.utils]
all_prop_cat_l [lemma, in octalgo.octalgo.utils]
all_prop [definition, in octalgo.octalgo.utils]
all_prop [section, in octalgo.octalgo.utils]
all_exist_tuple [lemma, in octalgo.octalgo.utils]
all_exist_enum [lemma, in octalgo.octalgo.utils]
all_exist_seq [lemma, in octalgo.octalgo.utils]
all_dom_empty [lemma, in octalgo.datalogcert.subs]
all_dom [definition, in octalgo.datalogcert.subs]
all_mem_edb_tst [lemma, in octalgo.octalgo.tSemantics]
all_prop_cons_notin [lemma, in octalgo.octalgo.fintrees]
always_cons_in_vals [lemma, in octalgo.octalgo.projection]
analysis [section, in octalgo.octalgo.static]
analysis [definition, in octalgo.octalgo.extract_static]
analysis.completeness [section, in octalgo.octalgo.static]
analysis.completeness.df [variable, in octalgo.octalgo.static]
analysis.completeness.docc [variable, in octalgo.octalgo.static]
analysis.completeness.gat_def [variable, in octalgo.octalgo.static]
analysis.dt [variable, in octalgo.octalgo.static]
analysis.dv [variable, in octalgo.octalgo.static]
analysis.p [variable, in octalgo.octalgo.static]
analysis.rules [section, in octalgo.octalgo.static]
analyze_incr [lemma, in octalgo.octalgo.static]
analyze_disj [lemma, in octalgo.octalgo.static]
analyze_var [definition, in octalgo.octalgo.static]
analyze_var_prev [definition, in octalgo.octalgo.static]
andP_to_uniq [lemma, in octalgo.octalgo.finseqs]
aocc_countprod [definition, in octalgo.octalgo.occurrences]
arg_atom_vars_in [lemma, in octalgo.octalgo.occurrences]
arg_c_match [lemma, in octalgo.datalogcert.soundness]
arg_wf_atom [definition, in octalgo.datalogcert.syntax]
arg_atom [definition, in octalgo.datalogcert.syntax]
arg_wf_gatom [definition, in octalgo.datalogcert.syntax]
arg_gatom [definition, in octalgo.datalogcert.syntax]
arity [axiom, in octalgo.datalogcert.syntax]
ar_ind [projection, in octalgo.octalgo.occurrences]
atom [record, in octalgo.datalogcert.syntax]
Atom [constructor, in octalgo.datalogcert.syntax]
AtomFinType [section, in octalgo.datalogcert.syntax]
atoms_prog [definition, in octalgo.datalogcert.syntax]
atoms_cl [definition, in octalgo.datalogcert.syntax]
atom_occ [definition, in octalgo.octalgo.occurrences]
atom_vars_sub_gr_def [lemma, in octalgo.datalogcert.subs]
atom_vars_sub_gr [lemma, in octalgo.datalogcert.subs]
atom_gr [definition, in octalgo.datalogcert.subs]
atom_vars_clone_c [lemma, in octalgo.octalgo.projection]
atom_clone_not_f [lemma, in octalgo.octalgo.projection]
atom_clone [definition, in octalgo.octalgo.projection]
atom_vars [definition, in octalgo.datalogcert.syntax]
atom_fenc [definition, in octalgo.datalogcert.syntax]
atom_enc [abbreviation, in octalgo.datalogcert.syntax]
attach_cl_nb [definition, in octalgo.octalgo.occurrences]
at_at [definition, in octalgo.octalgo.occurrences]
aux_leaf0 [lemma, in octalgo.octalgo.fintrees]
a_occ_finMixin [definition, in octalgo.octalgo.occurrences]
a_occ_countMixin [definition, in octalgo.octalgo.occurrences]
a_occ_choiceMixin [definition, in octalgo.octalgo.occurrences]
a_occ_eqMixin [definition, in octalgo.octalgo.occurrences]
a_occ_pre [definition, in octalgo.octalgo.occurrences]
a_occ_rep [definition, in octalgo.octalgo.occurrences]
a_occ [record, in octalgo.octalgo.occurrences]
A_occ [constructor, in octalgo.octalgo.occurrences]

B

base_sem_t [definition, in octalgo.octalgo.tSemantics]
Bcons [constructor, in octalgo.octalgo.finseqs]
BigCupSeq [section, in octalgo.third_party.bigop_aux]
BigCupSeq.I [variable, in octalgo.third_party.bigop_aux]
BigCupSeq.T [variable, in octalgo.third_party.bigop_aux]
bigcups_seqP [lemma, in octalgo.third_party.bigop_aux]
bigcup_cart [definition, in octalgo.octalgo.static]
bigcup_tup [definition, in octalgo.octalgo.static]
bigcup_type_seq [lemma, in octalgo.octalgo.utils]
bigcup_seqP [lemma, in octalgo.third_party.bigop_aux]
bigfcups_seqP [lemma, in octalgo.third_party.bigop_aux]
bigfcup_seqP [lemma, in octalgo.third_party.bigop_aux]
BigFOpsFin [section, in octalgo.third_party.bigop_aux]
BigFOpsFin.I [variable, in octalgo.third_party.bigop_aux]
BigFOpsFin.T [variable, in octalgo.third_party.bigop_aux]
BigFOpsSeq [section, in octalgo.third_party.bigop_aux]
BigFOpsSeq.I [variable, in octalgo.third_party.bigop_aux]
BigFOpsSeq.T [variable, in octalgo.third_party.bigop_aux]
bigop [section, in octalgo.octalgo.utils]
bigop_aux [library]
bindP [lemma, in octalgo.datalogcert.pmatch]
bindS [definition, in octalgo.datalogcert.pmatch]
bindSU [lemma, in octalgo.datalogcert.pmatch]
bindS_incr [lemma, in octalgo.datalogcert.monotonicity]
bindUS [lemma, in octalgo.datalogcert.pmatch]
BLeaf [constructor, in octalgo.octalgo.fintrees]
bmatch [definition, in octalgo.datalogcert.pmatch]
bmatch_match_body [lemma, in octalgo.datalogcert.soundness]
bn [axiom, in octalgo.datalogcert.syntax]
Bnil [constructor, in octalgo.octalgo.finseqs]
BNode [constructor, in octalgo.octalgo.fintrees]
body_cl [definition, in octalgo.datalogcert.syntax]
body_gcl [definition, in octalgo.datalogcert.syntax]
boolUtils [section, in octalgo.octalgo.utils]
bool_des_rew [lemma, in octalgo.octalgo.utils]
bool_to_prop_r [lemma, in octalgo.octalgo.utils]
bool_to_prop_l [lemma, in octalgo.octalgo.utils]
bp [definition, in octalgo.datalogcert.completeness]
bpM [lemma, in octalgo.datalogcert.completeness]
branch_t_ind_eq [lemma, in octalgo.octalgo.norec_sem]
branch_t_ind [definition, in octalgo.octalgo.norec_sem]
branch_pred_eq [lemma, in octalgo.octalgo.norec_sem]
branch_pred [definition, in octalgo.octalgo.norec_sem]
br_adequate [definition, in octalgo.octalgo.norec_sem]
bSemantics [section, in octalgo.datalogcert.bSemantics]
bSemantics [library]
buniq [projection, in octalgo.octalgo.finseqs]
b_ind [projection, in octalgo.octalgo.occurrences]

C

C [constructor, in octalgo.datalogcert.syntax]
cadequacy [lemma, in octalgo.octalgo.rinstance]
cancelffgg [lemma, in octalgo.octalgo.finseqs]
cancelfg [lemma, in octalgo.octalgo.finseqs]
cancelflgl [lemma, in octalgo.octalgo.fintrees]
cancel_fflggl [lemma, in octalgo.octalgo.fintrees]
canc_abtree_gentree [lemma, in octalgo.octalgo.fintrees]
ccompleteness [lemma, in octalgo.octalgo.rinstance]
Clause [constructor, in octalgo.datalogcert.syntax]
clause [inductive, in octalgo.datalogcert.syntax]
ClauseInstances [section, in octalgo.datalogcert.syntax]
clauses_var_intersect [definition, in octalgo.datalogcert.syntax]
clause_repK [lemma, in octalgo.datalogcert.syntax]
clause_pre [definition, in octalgo.datalogcert.syntax]
clause_rep [definition, in octalgo.datalogcert.syntax]
clone_bmatch [lemma, in octalgo.octalgo.projection]
clone_in [lemma, in octalgo.octalgo.projection]
clone_v [lemma, in octalgo.octalgo.projection]
clone_oob [lemma, in octalgo.octalgo.projection]
cl_clone [definition, in octalgo.octalgo.projection]
cl_true [definition, in octalgo.datalogcert.syntax]
cl_vars [definition, in octalgo.datalogcert.syntax]
Completeness [section, in octalgo.datalogcert.completeness]
completeness [library]
Completeness.def [variable, in octalgo.datalogcert.completeness]
Completeness.n [variable, in octalgo.datalogcert.completeness]
Completeness.p [variable, in octalgo.datalogcert.completeness]
Completeness.p_safe [variable, in octalgo.datalogcert.completeness]
constant [inductive, in octalgo.datalogcert.syntax]
constype [axiom, in octalgo.datalogcert.syntax]
const_cl [definition, in octalgo.datalogcert.syntax]
const_tail [definition, in octalgo.datalogcert.syntax]
const_atom [definition, in octalgo.datalogcert.syntax]
const_term [definition, in octalgo.datalogcert.syntax]
cons_cl_stable [lemma, in octalgo.datalogcert.soundness]
cons_cl_sound [lemma, in octalgo.datalogcert.soundness]
cons_cl_incr [lemma, in octalgo.datalogcert.monotonicity]
cons_clause_t_desc [lemma, in octalgo.octalgo.tSemantics]
cons_clause_h [lemma, in octalgo.octalgo.tSemantics]
cons_clause_t [definition, in octalgo.octalgo.tSemantics]
cons_clause_idb [lemma, in octalgo.datalogcert.bSemantics]
cons_clause [definition, in octalgo.datalogcert.bSemantics]
csoundness [lemma, in octalgo.octalgo.rinstance]
cteq [lemma, in octalgo.octalgo.finseqs]
cteql [lemma, in octalgo.octalgo.fintrees]
c_to_gen [definition, in octalgo.octalgo.projection]

D

dbranch [definition, in octalgo.octalgo.norec_sem]
ded [definition, in octalgo.octalgo.tSemantics]
deducing_c_to_gen [lemma, in octalgo.octalgo.projection]
ded_gr_equal_stail [lemma, in octalgo.octalgo.tSemantics]
ded_sub_equal_equal_to_def [lemma, in octalgo.octalgo.tSemantics]
ded_sub_equal [definition, in octalgo.octalgo.tSemantics]
dep_iota_uniq [lemma, in octalgo.octalgo.utils]
dep_iotaE [lemma, in octalgo.octalgo.utils]
dep_iota [definition, in octalgo.octalgo.utils]
disjointC [lemma, in octalgo.octalgo.utils]
disjoint_in_false [lemma, in octalgo.octalgo.utils]
dom [definition, in octalgo.datalogcert.subs]
dom_sub_grE [lemma, in octalgo.datalogcert.subs]
dom_singlesub [lemma, in octalgo.datalogcert.subs]
dom_emptysub [lemma, in octalgo.datalogcert.subs]

E

Edb [constructor, in octalgo.datalogcert.syntax]
edb_in_sem_t_descs [lemma, in octalgo.octalgo.tSemantics]
emptymin [lemma, in octalgo.datalogcert.subs]
emptysub [definition, in octalgo.datalogcert.subs]
emptysubE [lemma, in octalgo.datalogcert.subs]
eqbind_class [definition, in octalgo.datalogcert.subs]
Eqdep_dec_bool [lemma, in octalgo.octalgo.utils]
equip [definition, in octalgo.octalgo.utils]
equiv_part_set_mon [lemma, in octalgo.octalgo.utils]
equiv_part_set0 [lemma, in octalgo.octalgo.utils]
eq_foldS [lemma, in octalgo.datalogcert.pmatch]
eq_bindS [lemma, in octalgo.datalogcert.pmatch]
eq_singlesub [lemma, in octalgo.datalogcert.subs]
eq_fwd_chain [lemma, in octalgo.datalogcert.soundness]
extract_vals_sub_adequate [lemma, in octalgo.octalgo.extract_static]
extract_vals_sub [definition, in octalgo.octalgo.extract_static]
extract_vals [definition, in octalgo.octalgo.extract_static]
extract_vals_disj [definition, in octalgo.octalgo.extract_static]
extract_vals_conj [definition, in octalgo.octalgo.extract_static]
extract_vals_br [definition, in octalgo.octalgo.extract_static]
extract_subs_spec [definition, in octalgo.octalgo.extract_static]
extract_gr_v [lemma, in octalgo.octalgo.projection]
extract_sub_seq_rem_map [lemma, in octalgo.octalgo.projection]
extract_sub_seq_map [lemma, in octalgo.octalgo.projection]
extract_dom [lemma, in octalgo.octalgo.projection]
extract_in_v [lemma, in octalgo.octalgo.projection]
extract_sub_ga [definition, in octalgo.octalgo.projection]
extract_sub_seq_c [definition, in octalgo.octalgo.projection]
extract_static [library]

F

f [definition, in octalgo.octalgo.finseqs]
fenc_atomK [lemma, in octalgo.datalogcert.syntax]
fenc_atom [definition, in octalgo.datalogcert.syntax]
fenc_gatomK [lemma, in octalgo.datalogcert.syntax]
fenc_gatom [definition, in octalgo.datalogcert.syntax]
ff [definition, in octalgo.octalgo.finseqs]
ffl [definition, in octalgo.octalgo.fintrees]
ffl_aux [definition, in octalgo.octalgo.fintrees]
ffp [definition, in octalgo.octalgo.rinstance]
ffp_comp [lemma, in octalgo.octalgo.rinstance]
find_iota [lemma, in octalgo.octalgo.utils]
find_eq_nth_uniq [lemma, in octalgo.octalgo.utils]
find_val [lemma, in octalgo.octalgo.utils]
finseqs [library]
finset [section, in octalgo.octalgo.utils]
fintrees [library]
fixpoint [library]
Fixpoints [section, in octalgo.datalogcert.fixpoint]
Fixpoints.f [variable, in octalgo.datalogcert.fixpoint]
Fixpoints.f_ubound [variable, in octalgo.datalogcert.fixpoint]
Fixpoints.f_inc [variable, in octalgo.datalogcert.fixpoint]
Fixpoints.f_mono [variable, in octalgo.datalogcert.fixpoint]
Fixpoints.s0 [variable, in octalgo.datalogcert.fixpoint]
Fixpoints.s0_bound [variable, in octalgo.datalogcert.fixpoint]
Fixpoints.T [variable, in octalgo.datalogcert.fixpoint]
Fixpoints.ub [variable, in octalgo.datalogcert.fixpoint]
fix_iter [lemma, in octalgo.datalogcert.fixpoint]
fl [definition, in octalgo.octalgo.fintrees]
fl_aux [definition, in octalgo.octalgo.fintrees]
foldl_0 [lemma, in octalgo.datalogcert.soundness]
foldl_0_gen [lemma, in octalgo.datalogcert.soundness]
foldObindNone [lemma, in octalgo.octalgo.utils]
foldr_maxn_base [lemma, in octalgo.octalgo.utils]
foldS [definition, in octalgo.datalogcert.pmatch]
foldSU [lemma, in octalgo.datalogcert.pmatch]
foldS_incr [lemma, in octalgo.datalogcert.monotonicity]
fold_maxn_n_map_ltn [lemma, in octalgo.octalgo.utils]
fold_maxn_n_map_leq [lemma, in octalgo.octalgo.utils]
fold_maxn_n_map_gtn [lemma, in octalgo.octalgo.utils]
fold_maxn_n_map_geq [lemma, in octalgo.octalgo.utils]
fold_add_mapsto [lemma, in octalgo.datalogcert.soundness]
FSetMonoids [section, in octalgo.third_party.bigop_aux]
FSetMonoids.T [variable, in octalgo.third_party.bigop_aux]
fwd_chain_complete [lemma, in octalgo.datalogcert.completeness]
fwd_chain_mod [lemma, in octalgo.datalogcert.soundness]
fwd_chain_sym [lemma, in octalgo.datalogcert.soundness]
fwd_chain_cat [lemma, in octalgo.datalogcert.soundness]
fwd_chainP [lemma, in octalgo.datalogcert.soundness]
fwd_chain_stable [lemma, in octalgo.datalogcert.soundness]
fwd_chain_sound [lemma, in octalgo.datalogcert.soundness]
fwd_chain_inc [lemma, in octalgo.datalogcert.monotonicity]
fwd_chain_pincr [lemma, in octalgo.datalogcert.monotonicity]
fwd_chain_incr [lemma, in octalgo.datalogcert.monotonicity]
fwd_chain_inc_single [lemma, in octalgo.octalgo.tSemantics]
fwd_chain_t_inc_single [lemma, in octalgo.octalgo.tSemantics]
fwd_chain_t_inc [lemma, in octalgo.octalgo.tSemantics]
fwd_chain_t [definition, in octalgo.octalgo.tSemantics]
fwd_chain [definition, in octalgo.datalogcert.bSemantics]

G

g [definition, in octalgo.octalgo.finseqs]
gatom [record, in octalgo.datalogcert.syntax]
GAtom [constructor, in octalgo.datalogcert.syntax]
GatomFinType [section, in octalgo.datalogcert.syntax]
gatom_clone_f [lemma, in octalgo.octalgo.projection]
gatom_clone_not_f [lemma, in octalgo.octalgo.projection]
gatom_clone [definition, in octalgo.octalgo.projection]
gatom_fenc [definition, in octalgo.datalogcert.syntax]
gatom_enc [abbreviation, in octalgo.datalogcert.syntax]
gatom_eta [lemma, in octalgo.datalogcert.syntax]
ga_ded [lemma, in octalgo.datalogcert.soundness]
ga_a_ex_sym_eq [lemma, in octalgo.octalgo.projection]
GClause [constructor, in octalgo.datalogcert.syntax]
gclause [inductive, in octalgo.datalogcert.syntax]
gclause_repK [lemma, in octalgo.datalogcert.syntax]
gclause_pre [definition, in octalgo.datalogcert.syntax]
gclause_rep [definition, in octalgo.datalogcert.syntax]
gclause_eqMixin [definition, in octalgo.datalogcert.syntax]
gclause_eq_axiom [lemma, in octalgo.datalogcert.syntax]
gclause_eq_inv [lemma, in octalgo.datalogcert.syntax]
gclause_eq_refl [lemma, in octalgo.datalogcert.syntax]
gclause_eq [definition, in octalgo.datalogcert.syntax]
gcl_true [definition, in octalgo.datalogcert.syntax]
gen_cart_prod [definition, in octalgo.octalgo.utils]
gen_c_f_c_size [lemma, in octalgo.octalgo.projection]
gen_c_f_c [definition, in octalgo.octalgo.projection]
gen_f_c [definition, in octalgo.octalgo.projection]
gen_vars_rem_all_v [lemma, in octalgo.octalgo.projection]
gen_vars_j_all_v [lemma, in octalgo.octalgo.projection]
gen_vars_rem_uniq [lemma, in octalgo.octalgo.projection]
gen_vars_j_uniq [lemma, in octalgo.octalgo.projection]
gen_vars_j_find [lemma, in octalgo.octalgo.projection]
gen_vars_c_f [definition, in octalgo.octalgo.projection]
gen_vars_rem [definition, in octalgo.octalgo.projection]
gen_vars_rem_j [definition, in octalgo.octalgo.projection]
gen_vars [definition, in octalgo.octalgo.projection]
gen_vars_j [definition, in octalgo.octalgo.projection]
gen_to_AB [definition, in octalgo.octalgo.fintrees]
geq_max_r [lemma, in octalgo.octalgo.utils]
geq_max_l [lemma, in octalgo.octalgo.utils]
get_cl_var_leq [lemma, in octalgo.octalgo.occurrences]
get_cl_var [definition, in octalgo.octalgo.occurrences]
gg [definition, in octalgo.octalgo.finseqs]
ggl [definition, in octalgo.octalgo.fintrees]
gl [definition, in octalgo.octalgo.fintrees]
gr [definition, in octalgo.datalogcert.syntax]
Grounding [section, in octalgo.datalogcert.syntax]
gr_term_def_eq_in_dom [lemma, in octalgo.datalogcert.subs]
gr_cl_def [definition, in octalgo.datalogcert.subs]
gr_atom_defK [lemma, in octalgo.datalogcert.subs]
gr_atom_defP [lemma, in octalgo.datalogcert.subs]
gr_atom_def [definition, in octalgo.datalogcert.subs]
gr_atom_def_proof [lemma, in octalgo.datalogcert.subs]
gr_raw_atom_scl_eq [lemma, in octalgo.datalogcert.subs]
gr_raw_atom_def [definition, in octalgo.datalogcert.subs]
gr_term_sub [lemma, in octalgo.datalogcert.subs]
gr_term_defP [lemma, in octalgo.datalogcert.subs]
gr_term_def_scl_eq [lemma, in octalgo.datalogcert.subs]
gr_term_def [definition, in octalgo.datalogcert.subs]
gr_atom_defE [lemma, in octalgo.datalogcert.soundness]
gr_atom_def_clone_eq [lemma, in octalgo.octalgo.projection]
gr_term_def_seq_add_notin [lemma, in octalgo.octalgo.projection]
gr_cl [definition, in octalgo.datalogcert.syntax]
gr_tl [definition, in octalgo.datalogcert.syntax]
gr_atom [definition, in octalgo.datalogcert.syntax]
gr_atom_proof [definition, in octalgo.datalogcert.syntax]
gr_raw_atom [definition, in octalgo.datalogcert.syntax]
gr_term [definition, in octalgo.datalogcert.syntax]
gtn_max_r [lemma, in octalgo.octalgo.utils]
gtn_max_l [lemma, in octalgo.octalgo.utils]

H

has_lfp [lemma, in octalgo.datalogcert.fixpoint]
Hclp_not_cloned [lemma, in octalgo.octalgo.projection]
head_cl [definition, in octalgo.datalogcert.syntax]
head_gcl [definition, in octalgo.datalogcert.syntax]
height_WUtree [lemma, in octalgo.octalgo.fintrees]
hsym_prog [definition, in octalgo.datalogcert.syntax]
hsym_cl [definition, in octalgo.datalogcert.syntax]
Htree [inductive, in octalgo.octalgo.fintrees]
HTree [section, in octalgo.octalgo.fintrees]
htreen_finType [definition, in octalgo.octalgo.fintrees]
htreen_finMixin [definition, in octalgo.octalgo.fintrees]
htreen_countType [definition, in octalgo.octalgo.fintrees]
htreen_countMixin [definition, in octalgo.octalgo.fintrees]
htreen_choiceType [definition, in octalgo.octalgo.fintrees]
htreen_choiceMixin [definition, in octalgo.octalgo.fintrees]
htreen_eqType [definition, in octalgo.octalgo.fintrees]
htreen_eqMixin [definition, in octalgo.octalgo.fintrees]
Htree_to_ABwidth [lemma, in octalgo.octalgo.fintrees]
htree_wutreeK [lemma, in octalgo.octalgo.fintrees]
htree_abtreeK [lemma, in octalgo.octalgo.fintrees]
htree_uniq_ind_prop_seq [lemma, in octalgo.octalgo.fintrees]
htree_uniq_ind_prop [lemma, in octalgo.octalgo.fintrees]
htree_uniq_ind [lemma, in octalgo.octalgo.fintrees]
HTree.HtreeChoiceType [section, in octalgo.octalgo.fintrees]
HTree.HtreeChoiceType.A [variable, in octalgo.octalgo.fintrees]
HTree.HtreeChoiceType.B [variable, in octalgo.octalgo.fintrees]
HTree.HtreeCountType [section, in octalgo.octalgo.fintrees]
HTree.HtreeCountType.A [variable, in octalgo.octalgo.fintrees]
HTree.HtreeCountType.B [variable, in octalgo.octalgo.fintrees]
HTree.HtreeEqType [section, in octalgo.octalgo.fintrees]
HTree.HtreeEqType.A [variable, in octalgo.octalgo.fintrees]
HTree.HtreeEqType.B [variable, in octalgo.octalgo.fintrees]
HTree.HtreeFinType [section, in octalgo.octalgo.fintrees]
HTree.HtreeFinType.A [variable, in octalgo.octalgo.fintrees]
HTree.HtreeFinType.B [variable, in octalgo.octalgo.fintrees]
HTree.HtreeUtils [section, in octalgo.octalgo.fintrees]
HTree.InducType [section, in octalgo.octalgo.fintrees]
HTree.InducType.A [variable, in octalgo.octalgo.fintrees]
HTree.InducType.B [variable, in octalgo.octalgo.fintrees]
HTree.w [variable, in octalgo.octalgo.fintrees]
htree0_finType [definition, in octalgo.octalgo.fintrees]
htree0_finMixin [definition, in octalgo.octalgo.fintrees]
htree0_countType [definition, in octalgo.octalgo.fintrees]
htree0_countMixin [definition, in octalgo.octalgo.fintrees]
htree0_choiceType [definition, in octalgo.octalgo.fintrees]
htree0_choiceMixin [definition, in octalgo.octalgo.fintrees]
htree0_eqType [definition, in octalgo.octalgo.fintrees]
htree0_eqMixin [definition, in octalgo.octalgo.fintrees]
Huniq [definition, in octalgo.octalgo.fintrees]
Huniq_to_ABuniq [lemma, in octalgo.octalgo.fintrees]
hutree_abtreeK [lemma, in octalgo.octalgo.fintrees]
Hwht [projection, in octalgo.octalgo.fintrees]
h_to_wu_tree [definition, in octalgo.octalgo.fintrees]
h_to_ab_w_bound [lemma, in octalgo.octalgo.fintrees]
h_to_ab_tree [definition, in octalgo.octalgo.fintrees]

I

Idb [constructor, in octalgo.datalogcert.syntax]
idb_in_sem_t_descs [lemma, in octalgo.octalgo.tSemantics]
increasing [definition, in octalgo.datalogcert.fixpoint]
Increasing [section, in octalgo.datalogcert.monotonicity]
Increasing.Overlinear [section, in octalgo.datalogcert.monotonicity]
incr_fwd_chain_complete [lemma, in octalgo.datalogcert.completeness]
ind_in_gen_vars [lemma, in octalgo.octalgo.projection]
ind_in_gen_vars_j [lemma, in octalgo.octalgo.projection]
ind_vals [definition, in octalgo.octalgo.projection]
ind_terms [definition, in octalgo.octalgo.projection]
inE_bis [definition, in octalgo.datalogcert.subs]
inst_rule [definition, in octalgo.octalgo.rinstance]
interp [abbreviation, in octalgo.datalogcert.syntax]
interp_t [abbreviation, in octalgo.octalgo.tSemantics]
in_nth_P [lemma, in octalgo.octalgo.utils]
in_rem [lemma, in octalgo.octalgo.utils]
in_extract_c_v [lemma, in octalgo.octalgo.projection]
is_clone_ga_f [lemma, in octalgo.octalgo.projection]
is_clone_ga [definition, in octalgo.octalgo.projection]
is_clone_clone_pred [lemma, in octalgo.octalgo.projection]
is_clone_pred [definition, in octalgo.octalgo.projection]
is_var [definition, in octalgo.datalogcert.syntax]
iterf [definition, in octalgo.datalogcert.fixpoint]
iterf_incr_bound [lemma, in octalgo.datalogcert.fixpoint]
iterf_incr [abbreviation, in octalgo.datalogcert.fixpoint]
iter_fun_incr [lemma, in octalgo.octalgo.utils]
iter_mon.f_lb [variable, in octalgo.datalogcert.fixpoint]
iter_mon.lb [variable, in octalgo.datalogcert.fixpoint]
iter_mon [lemma, in octalgo.datalogcert.fixpoint]
iter_mon.f_mon [variable, in octalgo.datalogcert.fixpoint]
iter_mon.f [variable, in octalgo.datalogcert.fixpoint]
iter_mon.T [variable, in octalgo.datalogcert.fixpoint]
iter_mon [section, in octalgo.datalogcert.fixpoint]
iter_leq_fix [lemma, in octalgo.datalogcert.fixpoint]
iter_fwd_chain_stable [lemma, in octalgo.datalogcert.soundness]
iter_fwd_chain_sym [lemma, in octalgo.datalogcert.soundness]
iter_fwd_chain_subset [lemma, in octalgo.datalogcert.monotonicity]
ite_id [lemma, in octalgo.octalgo.utils]

K

keep_atom_tail_match [lemma, in octalgo.octalgo.purge]
keep_atom_sem [lemma, in octalgo.octalgo.purge]
keep_rule [definition, in octalgo.octalgo.purge]
keep_atom [definition, in octalgo.octalgo.purge]

L

leaf0 [lemma, in octalgo.octalgo.fintrees]
leq_fold_base [lemma, in octalgo.octalgo.utils]
leq_fold_maxl [lemma, in octalgo.octalgo.utils]
lfpE [lemma, in octalgo.datalogcert.fixpoint]
lfp_incr [abbreviation, in octalgo.datalogcert.fixpoint]
ltn_leq_trans [lemma, in octalgo.octalgo.utils]

M

map_square_eq [lemma, in octalgo.octalgo.utils]
Match [section, in octalgo.datalogcert.pmatch]
match_body [definition, in octalgo.datalogcert.pmatch]
match_atomsP [lemma, in octalgo.datalogcert.pmatch]
match_atom_all [definition, in octalgo.datalogcert.pmatch]
match_atom [definition, in octalgo.datalogcert.pmatch]
match_raw_atom [definition, in octalgo.datalogcert.pmatch]
match_term_sub [lemma, in octalgo.datalogcert.pmatch]
match_term [definition, in octalgo.datalogcert.pmatch]
match_body_bmatch [lemma, in octalgo.datalogcert.soundness]
match_term_head_some [lemma, in octalgo.datalogcert.soundness]
match_body_strata [lemma, in octalgo.datalogcert.soundness]
match_atom_all_strata [lemma, in octalgo.datalogcert.soundness]
match_atom_allU [lemma, in octalgo.datalogcert.soundness]
match_tl_sound [lemma, in octalgo.datalogcert.soundness]
match_domsI [lemma, in octalgo.datalogcert.soundness]
match_vars_seteq [lemma, in octalgo.datalogcert.soundness]
match_vars_subset [lemma, in octalgo.datalogcert.soundness]
match_atoms_vars_subset [lemma, in octalgo.datalogcert.soundness]
match_pbody_sub [lemma, in octalgo.datalogcert.soundness]
match_subset_vars [lemma, in octalgo.datalogcert.soundness]
match_atom_all_dom [lemma, in octalgo.datalogcert.soundness]
match_atom_dom [lemma, in octalgo.datalogcert.soundness]
match_atom_diff_heads [lemma, in octalgo.datalogcert.soundness]
match_atom_diff_cons [lemma, in octalgo.datalogcert.soundness]
match_atom_dif_lengths [lemma, in octalgo.datalogcert.soundness]
match_pbody_sound [lemma, in octalgo.datalogcert.soundness]
match_atom_all_sub [lemma, in octalgo.datalogcert.soundness]
match_tl_complete [lemma, in octalgo.datalogcert.soundness]
match_ptl_sub_complete [lemma, in octalgo.datalogcert.soundness]
match_ptl_complete [lemma, in octalgo.datalogcert.soundness]
match_atom_complete [lemma, in octalgo.datalogcert.soundness]
match_term_complete [lemma, in octalgo.datalogcert.soundness]
match_atoms_pbody [lemma, in octalgo.datalogcert.soundness]
match_body_pbody [lemma, in octalgo.datalogcert.soundness]
match_pbody_cons [lemma, in octalgo.datalogcert.soundness]
match_pbody_incr [lemma, in octalgo.datalogcert.soundness]
match_pbody [definition, in octalgo.datalogcert.soundness]
match_atoms_sub [lemma, in octalgo.datalogcert.soundness]
match_atom_sub [lemma, in octalgo.datalogcert.soundness]
match_atom_sound [lemma, in octalgo.datalogcert.soundness]
match_term_sound [lemma, in octalgo.datalogcert.soundness]
match_clone_not_f [lemma, in octalgo.octalgo.projection]
match_clone [lemma, in octalgo.octalgo.projection]
match_atom_all_clone_v [lemma, in octalgo.octalgo.projection]
match_atom_all_clone_cnone [lemma, in octalgo.octalgo.projection]
match_atom_clone_v [lemma, in octalgo.octalgo.projection]
match_atom_clone_cnone [lemma, in octalgo.octalgo.projection]
match_fold_clone [lemma, in octalgo.octalgo.projection]
match_body_incr [lemma, in octalgo.datalogcert.monotonicity]
match_atom_all_incr [lemma, in octalgo.datalogcert.monotonicity]
Match.def [variable, in octalgo.datalogcert.pmatch]
maxn_0_n [lemma, in octalgo.octalgo.fintrees]
max_ar_bound [lemma, in octalgo.datalogcert.syntax]
max_ar [abbreviation, in octalgo.datalogcert.syntax]
mem_pset_set [lemma, in octalgo.octalgo.utils]
mem_set_pset [lemma, in octalgo.octalgo.utils]
mem_body [lemma, in octalgo.octalgo.utils]
mem_bindE [lemma, in octalgo.datalogcert.subs]
mem_binding [definition, in octalgo.datalogcert.subs]
mem_free [definition, in octalgo.datalogcert.subs]
mem_bound [definition, in octalgo.datalogcert.subs]
min_lfp_all [lemma, in octalgo.datalogcert.fixpoint]
monotone [definition, in octalgo.datalogcert.fixpoint]
monotonicity [library]
my_tst_sub [definition, in octalgo.octalgo.tSemantics]

N

n [axiom, in octalgo.datalogcert.syntax]
nat [section, in octalgo.octalgo.utils]
nat.max [section, in octalgo.octalgo.utils]
negb_has_predC_all [lemma, in octalgo.octalgo.utils]
neq_sym [lemma, in octalgo.octalgo.fintrees]
nil_list0 [lemma, in octalgo.octalgo.finseqs]
nil0 [lemma, in octalgo.octalgo.finseqs]
NoDepGrounding [section, in octalgo.datalogcert.subs]
NoDepGrounding.def [variable, in octalgo.datalogcert.subs]
nomega_fp [lemma, in octalgo.octalgo.rinstance]
norec_sem [library]
notin [section, in octalgo.octalgo.utils]
notinnil [lemma, in octalgo.octalgo.finseqs]
not_set1P [lemma, in octalgo.octalgo.utils]
no_rec_needed [lemma, in octalgo.octalgo.norec_sem]
no_rec_traces.df [variable, in octalgo.octalgo.norec_sem]
no_rec_traces.dv [variable, in octalgo.octalgo.norec_sem]
no_rec_traces.dt [variable, in octalgo.octalgo.norec_sem]
no_rec_traces.gat_def [variable, in octalgo.octalgo.norec_sem]
no_rec_traces.p [variable, in octalgo.octalgo.norec_sem]
no_rec_traces [section, in octalgo.octalgo.norec_sem]
no_rec_capt_nf [lemma, in octalgo.octalgo.static]
no_rec_capt [lemma, in octalgo.octalgo.static]
no_deduced_leaf [lemma, in octalgo.octalgo.tSemantics]
nth_default_size [lemma, in octalgo.octalgo.utils]
nth_error_some_none_size [lemma, in octalgo.octalgo.utils]
nth_error_case [lemma, in octalgo.octalgo.utils]
nth_error_leq_size [lemma, in octalgo.octalgo.utils]
nth_error_size_leq [lemma, in octalgo.octalgo.utils]
nth_error_sremove_eq [lemma, in octalgo.octalgo.utils]
nth_error_sremove [lemma, in octalgo.octalgo.utils]
nth_error_size_notin [lemma, in octalgo.octalgo.utils]
nth_error_notin_size [lemma, in octalgo.octalgo.utils]
nth_error_in_size [lemma, in octalgo.octalgo.utils]
nth_error_preim [lemma, in octalgo.octalgo.utils]
nth_error_set_nth [lemma, in octalgo.octalgo.utils]
nth_error_ncons1 [lemma, in octalgo.octalgo.utils]
nth_error_nth [lemma, in octalgo.octalgo.utils]
nth_error_map_none [lemma, in octalgo.octalgo.utils]
nth_error_map [lemma, in octalgo.octalgo.utils]
nth_error_in [lemma, in octalgo.octalgo.utils]
nth_error [definition, in octalgo.octalgo.utils]
nth_cons_rew_dep [definition, in octalgo.datalogcert.syntax]
nth_term [definition, in octalgo.datalogcert.syntax]
nth_cons [definition, in octalgo.datalogcert.syntax]

O

occ [definition, in octalgo.octalgo.occurrences]
occsInAtom [definition, in octalgo.octalgo.occurrences]
occsInAtomList [definition, in octalgo.octalgo.occurrences]
occsInAtomListV [lemma, in octalgo.octalgo.occurrences]
occsInAtomListVint [lemma, in octalgo.octalgo.occurrences]
occsInAtomV [lemma, in octalgo.octalgo.occurrences]
occsInProgram [definition, in octalgo.octalgo.occurrences]
occsInProgramV [lemma, in octalgo.octalgo.occurrences]
occsInRule [definition, in octalgo.octalgo.occurrences]
occsInRuleV [lemma, in octalgo.octalgo.occurrences]
occsInTermList [definition, in octalgo.octalgo.occurrences]
occurrences [section, in octalgo.octalgo.occurrences]
occurrences [library]
occurrences.a_occ.p [variable, in octalgo.octalgo.occurrences]
occurrences.a_occ [section, in octalgo.octalgo.occurrences]
occurrences.df [variable, in octalgo.octalgo.occurrences]
occurrences.dt [variable, in octalgo.octalgo.occurrences]
occurrences.dv [variable, in octalgo.octalgo.occurrences]
occurrences.prog_occ [section, in octalgo.octalgo.occurrences]
occurrences.t_occ.p [variable, in octalgo.octalgo.occurrences]
occurrences.t_occ [section, in octalgo.octalgo.occurrences]
of_constant [definition, in octalgo.datalogcert.syntax]
only_untyped_match [lemma, in octalgo.datalogcert.soundness]
only_variables_in_heads [definition, in octalgo.datalogcert.syntax]
only_variables_head [definition, in octalgo.datalogcert.syntax]
only_variables_atom [definition, in octalgo.datalogcert.syntax]
oob_nth_error [lemma, in octalgo.octalgo.utils]
oob_atom_args [lemma, in octalgo.datalogcert.syntax]
oob_gatom_args [lemma, in octalgo.datalogcert.syntax]
ord [section, in octalgo.octalgo.utils]
ord_shift [definition, in octalgo.octalgo.utils]
ord_shiftl [lemma, in octalgo.octalgo.utils]
original_sem_no_clone [lemma, in octalgo.octalgo.projection]

P

pair_seq_nth_proj_l [lemma, in octalgo.octalgo.utils]
pimset [definition, in octalgo.octalgo.utils]
pmap_size_leq [lemma, in octalgo.octalgo.utils]
pmatch [library]
pmatch_vars_subset [lemma, in octalgo.datalogcert.soundness]
pmatch_subset_vars [lemma, in octalgo.datalogcert.soundness]
pmatch_clone_not_f [lemma, in octalgo.octalgo.projection]
pmatch_clone [lemma, in octalgo.octalgo.projection]
pp [definition, in octalgo.octalgo.purge]
pp_p [lemma, in octalgo.octalgo.purge]
predtype [axiom, in octalgo.datalogcert.syntax]
pred_ltn [lemma, in octalgo.octalgo.utils]
pred_ltn0_l [lemma, in octalgo.octalgo.utils]
pred_clone_c [lemma, in octalgo.octalgo.projection]
pred_type_eqMixin [definition, in octalgo.datalogcert.syntax]
pred_type_eq_axiom [lemma, in octalgo.datalogcert.syntax]
pred_type_eq [definition, in octalgo.datalogcert.syntax]
pred_type [inductive, in octalgo.datalogcert.syntax]
Prod [section, in octalgo.octalgo.utils]
prod_of_a_occK [lemma, in octalgo.octalgo.occurrences]
prod_of_t_occK [lemma, in octalgo.octalgo.occurrences]
prod_eq [lemma, in octalgo.octalgo.utils]
program [definition, in octalgo.datalogcert.syntax]
prog_true [definition, in octalgo.datalogcert.syntax]
prog_safe_hds [definition, in octalgo.datalogcert.syntax]
prog_safe [definition, in octalgo.datalogcert.syntax]
Projection [section, in octalgo.octalgo.projection]
projection [library]
Projection.always_cons [variable, in octalgo.octalgo.projection]
Projection.arity_vars [variable, in octalgo.octalgo.projection]
Projection.bn_not_zero [variable, in octalgo.octalgo.projection]
Projection.def [variable, in octalgo.octalgo.projection]
Projection.f [variable, in octalgo.octalgo.projection]
Projection.ftype [variable, in octalgo.octalgo.projection]
Projection.i [variable, in octalgo.octalgo.projection]
Projection.ifresh [variable, in octalgo.octalgo.projection]
Projection.ind [variable, in octalgo.octalgo.projection]
Projection.isafe [variable, in octalgo.octalgo.projection]
Projection.p [variable, in octalgo.octalgo.projection]
Projection.parity [variable, in octalgo.octalgo.projection]
Projection.pclone [variable, in octalgo.octalgo.projection]
Projection.pfresh [variable, in octalgo.octalgo.projection]
Projection.pinj [variable, in octalgo.octalgo.projection]
Projection.pnotf [variable, in octalgo.octalgo.projection]
Projection.psafe [variable, in octalgo.octalgo.projection]
proj_soundness [lemma, in octalgo.octalgo.projection]
proj_soundness_u [lemma, in octalgo.octalgo.projection]
proj_completeness [lemma, in octalgo.octalgo.projection]
proj_completeness_u [lemma, in octalgo.octalgo.projection]
proj_prog [definition, in octalgo.octalgo.projection]
pset [definition, in octalgo.octalgo.utils]
pucons [definition, in octalgo.octalgo.finseqs]
Purge [section, in octalgo.octalgo.purge]
purge [library]
purge_sem_adequacy [lemma, in octalgo.octalgo.purge]
purge_sem_soundness [lemma, in octalgo.octalgo.purge]
purge_sem_completeness [lemma, in octalgo.octalgo.purge]
Purge.def [variable, in octalgo.octalgo.purge]
Purge.f [variable, in octalgo.octalgo.purge]
Purge.i [variable, in octalgo.octalgo.purge]
Purge.ind [variable, in octalgo.octalgo.purge]
Purge.p [variable, in octalgo.octalgo.purge]
Purge.vals [variable, in octalgo.octalgo.purge]
Purge.vals_adeq [variable, in octalgo.octalgo.purge]
p_at [definition, in octalgo.octalgo.occurrences]

R

RawAtom [constructor, in octalgo.datalogcert.syntax]
RawAtomInstances [section, in octalgo.datalogcert.syntax]
RawGAtom [constructor, in octalgo.datalogcert.syntax]
RawGAtomInstances [section, in octalgo.datalogcert.syntax]
raw_gen_c_f_c_wf [lemma, in octalgo.octalgo.projection]
raw_gen_f_c [definition, in octalgo.octalgo.projection]
raw_gen_f_c_wf [lemma, in octalgo.octalgo.projection]
raw_gen_c_f [definition, in octalgo.octalgo.projection]
raw_gatom_clone [definition, in octalgo.octalgo.projection]
raw_atom_clone [definition, in octalgo.octalgo.projection]
raw_atom_vars_cons [lemma, in octalgo.datalogcert.syntax]
raw_atom_vars_cons_sub [lemma, in octalgo.datalogcert.syntax]
raw_atom_vars [definition, in octalgo.datalogcert.syntax]
raw_atom_repK [lemma, in octalgo.datalogcert.syntax]
raw_atom_pre [definition, in octalgo.datalogcert.syntax]
raw_atom_rep [definition, in octalgo.datalogcert.syntax]
raw_atom [inductive, in octalgo.datalogcert.syntax]
raw_gatom_repK [lemma, in octalgo.datalogcert.syntax]
raw_gatom_pre [definition, in octalgo.datalogcert.syntax]
raw_gatom_rep [definition, in octalgo.datalogcert.syntax]
raw_gatom [inductive, in octalgo.datalogcert.syntax]
rinstance [library]
RS [constructor, in octalgo.octalgo.tSemantics]
RuleInstance [section, in octalgo.octalgo.rinstance]
RuleInstance.def [variable, in octalgo.octalgo.rinstance]
RuleInstance.i [variable, in octalgo.octalgo.rinstance]
RuleInstance.p [variable, in octalgo.octalgo.rinstance]
RuleInstance.psafe [variable, in octalgo.octalgo.rinstance]
RuleInstance.Rv [variable, in octalgo.octalgo.rinstance]
RuleInstance.subs [variable, in octalgo.octalgo.rinstance]
RuleInstance.subs_comp [variable, in octalgo.octalgo.rinstance]
rul_gr_finMixin [definition, in octalgo.octalgo.tSemantics]
rul_gr_countMixin [definition, in octalgo.octalgo.tSemantics]
rul_gr_choiceMixin [definition, in octalgo.octalgo.tSemantics]
rul_gr_eqMixin [definition, in octalgo.octalgo.tSemantics]
rul_gr_repK [lemma, in octalgo.octalgo.tSemantics]
rul_gr_pre [definition, in octalgo.octalgo.tSemantics]
rul_gr_rep [definition, in octalgo.octalgo.tSemantics]
rul_gr [inductive, in octalgo.octalgo.tSemantics]
r_ind [projection, in octalgo.octalgo.occurrences]
r_dom_body [lemma, in octalgo.datalogcert.soundness]
r_dom_atom [lemma, in octalgo.datalogcert.soundness]
r_dom_term [lemma, in octalgo.datalogcert.soundness]

S

safe_edb [definition, in octalgo.datalogcert.syntax]
safe_cl_hd [definition, in octalgo.datalogcert.syntax]
safe_cl [definition, in octalgo.datalogcert.syntax]
satom [definition, in octalgo.datalogcert.subs]
satomeq_subU [lemma, in octalgo.datalogcert.subs]
satom_vars_subset [lemma, in octalgo.datalogcert.subs]
satom_sub [lemma, in octalgo.datalogcert.subs]
satom_proof [lemma, in octalgo.datalogcert.subs]
scl [definition, in octalgo.datalogcert.subs]
sem [definition, in octalgo.datalogcert.bSemantics]
sem_m_star_incr [lemma, in octalgo.datalogcert.monotonicity]
sem_inc [lemma, in octalgo.datalogcert.monotonicity]
sem_m_incr [lemma, in octalgo.datalogcert.monotonicity]
sem_t_Idb_pred [lemma, in octalgo.octalgo.tSemantics]
sem_t_Edb_pred [lemma, in octalgo.octalgo.tSemantics]
sem_t_leaf [lemma, in octalgo.octalgo.tSemantics]
sem_t [definition, in octalgo.octalgo.tSemantics]
sem_tree_to_inter [definition, in octalgo.octalgo.tSemantics]
sem_idb_in [lemma, in octalgo.datalogcert.bSemantics]
sem_idb_safe [lemma, in octalgo.datalogcert.bSemantics]
seq [section, in octalgo.octalgo.utils]
seq_in_ind [lemma, in octalgo.octalgo.utils]
seq_inj [lemma, in octalgo.octalgo.utils]
seq_in_rem_size [lemma, in octalgo.octalgo.utils]
seq_notin_f_in [lemma, in octalgo.octalgo.utils]
seq_inj [lemma, in octalgo.datalogcert.soundness]
seq_wlist_uncut_K [lemma, in octalgo.octalgo.finseqs]
seq_to_wlist_uncut [definition, in octalgo.octalgo.finseqs]
seq_wlistK [lemma, in octalgo.octalgo.finseqs]
seq_to_bnil [lemma, in octalgo.octalgo.finseqs]
seq_to_wlist [definition, in octalgo.octalgo.finseqs]
seq.all [section, in octalgo.octalgo.utils]
seq.find [section, in octalgo.octalgo.utils]
seq.fold [section, in octalgo.octalgo.utils]
seq.nth_error [section, in octalgo.octalgo.utils]
seq.rem [section, in octalgo.octalgo.utils]
seq.size_map_leq [section, in octalgo.octalgo.utils]
setIdP_bool_to_prop [lemma, in octalgo.octalgo.tSemantics]
set_nth_notin [lemma, in octalgo.octalgo.utils]
set_nth_notin_base [lemma, in octalgo.octalgo.utils]
set_notin_f_in [lemma, in octalgo.octalgo.utils]
set0_set1_neq [lemma, in octalgo.octalgo.utils]
shift [definition, in octalgo.octalgo.utils]
shift1 [definition, in octalgo.octalgo.occurrences]
simple_cons_eq_inversion [lemma, in octalgo.octalgo.tSemantics]
size_dep_iota [lemma, in octalgo.octalgo.utils]
size_map_leq [lemma, in octalgo.octalgo.utils]
size_gen_vars [lemma, in octalgo.octalgo.projection]
size_gen_vars_j [lemma, in octalgo.octalgo.projection]
size_wmap [lemma, in octalgo.octalgo.finseqs]
size_useq [lemma, in octalgo.octalgo.finseqs]
Soundness [section, in octalgo.datalogcert.soundness]
soundness [library]
sraw_atom [definition, in octalgo.datalogcert.subs]
sremove [definition, in octalgo.octalgo.utils]
sremove_nth [lemma, in octalgo.octalgo.utils]
sremove_rem [lemma, in octalgo.octalgo.utils]
sremove_map [lemma, in octalgo.octalgo.utils]
sremove_in_size [lemma, in octalgo.octalgo.utils]
sremove_size [lemma, in octalgo.octalgo.utils]
sstree_height [lemma, in octalgo.octalgo.fintrees]
stail [definition, in octalgo.datalogcert.subs]
staileq_subU [lemma, in octalgo.datalogcert.subs]
stail_vars_subset [lemma, in octalgo.datalogcert.subs]
stail_ded_eq [lemma, in octalgo.octalgo.tSemantics]
stail_eq_to_gr_atom_eq [lemma, in octalgo.octalgo.tSemantics]
static [library]
static_extraction_adequacy [lemma, in octalgo.octalgo.extract_static]
static_extract_spec [lemma, in octalgo.octalgo.extract_static]
sterm [definition, in octalgo.datalogcert.subs]
sterm_sub [lemma, in octalgo.datalogcert.subs]
sterm_ga_eq [lemma, in octalgo.octalgo.tSemantics]
strict_subtree [definition, in octalgo.octalgo.fintrees]
stv [definition, in octalgo.octalgo.rinstance]
sub [definition, in octalgo.datalogcert.subs]
subs [library]
subset_to_in [lemma, in octalgo.octalgo.utils]
subset_iterf [lemma, in octalgo.datalogcert.fixpoint]
substE [lemma, in octalgo.datalogcert.subs]
Substitutions [section, in octalgo.datalogcert.subs]
_ \sub _ (bool_scope) [notation, in octalgo.datalogcert.subs]
substP [lemma, in octalgo.datalogcert.subs]
substss [lemma, in octalgo.datalogcert.subs]
subst_trans [lemma, in octalgo.datalogcert.subs]
subst0s [lemma, in octalgo.datalogcert.subs]
subtree [definition, in octalgo.octalgo.fintrees]
subtree_ssubtree [lemma, in octalgo.octalgo.fintrees]
subtree_refl [lemma, in octalgo.octalgo.fintrees]
subU [definition, in octalgo.datalogcert.subs]
subU_eq [lemma, in octalgo.datalogcert.subs]
subU_addl [lemma, in octalgo.datalogcert.subs]
subU_0r [lemma, in octalgo.datalogcert.subs]
subU_0l [lemma, in octalgo.datalogcert.subs]
subU_match [lemma, in octalgo.datalogcert.soundness]
sub_val_map [lemma, in octalgo.octalgo.utils]
sub_rem_seq [lemma, in octalgo.octalgo.utils]
sub_all_and_r [lemma, in octalgo.octalgo.utils]
sub_all_and_l [lemma, in octalgo.octalgo.utils]
sub_rem [lemma, in octalgo.octalgo.utils]
sub_sub_filter [lemma, in octalgo.datalogcert.subs]
sub_filter_eq [lemma, in octalgo.datalogcert.subs]
sub_filter_subset_t [lemma, in octalgo.datalogcert.subs]
sub_filter_subset_s [lemma, in octalgo.datalogcert.subs]
sub_filter [definition, in octalgo.datalogcert.subs]
sub_dom [lemma, in octalgo.datalogcert.subs]
sub_add [lemma, in octalgo.datalogcert.subs]
sub_st [definition, in octalgo.datalogcert.subs]
sub_elim [lemma, in octalgo.datalogcert.subs]
sub_st_add [lemma, in octalgo.datalogcert.soundness]
sub_dom_ga [lemma, in octalgo.datalogcert.soundness]
sub_dom_raw [lemma, in octalgo.datalogcert.soundness]
sub_dom_gra [lemma, in octalgo.datalogcert.soundness]
sub_dom_grt [lemma, in octalgo.datalogcert.soundness]
sub_branches_head [lemma, in octalgo.octalgo.fintrees]
symtype [axiom, in octalgo.datalogcert.syntax]
sym_satom [lemma, in octalgo.datalogcert.subs]
sym_tl [definition, in octalgo.datalogcert.soundness]
sym_pengine_subset_hsymp [lemma, in octalgo.datalogcert.soundness]
sym_satom_gatom [lemma, in octalgo.octalgo.projection]
sym_prog [definition, in octalgo.datalogcert.syntax]
sym_cl [definition, in octalgo.datalogcert.syntax]
sym_atom [definition, in octalgo.datalogcert.syntax]
sym_i [definition, in octalgo.datalogcert.syntax]
sym_gatom [definition, in octalgo.datalogcert.syntax]
syntax [library]

T

tag_of_dbranchK [lemma, in octalgo.octalgo.finseqs]
tag_of_uniq_seq [definition, in octalgo.octalgo.finseqs]
tail [definition, in octalgo.datalogcert.syntax]
tailvars_trans [lemma, in octalgo.datalogcert.syntax]
tail_gr [definition, in octalgo.datalogcert.subs]
tail_mem [lemma, in octalgo.datalogcert.soundness]
tail_clone [definition, in octalgo.octalgo.projection]
tail_vars_1 [lemma, in octalgo.datalogcert.syntax]
tail_vars_nil [lemma, in octalgo.datalogcert.syntax]
tail_vars_head [lemma, in octalgo.datalogcert.syntax]
tail_vars_consUP [lemma, in octalgo.datalogcert.syntax]
tail_vars_sub_cons [lemma, in octalgo.datalogcert.syntax]
tail_vars_cons [lemma, in octalgo.datalogcert.syntax]
tail_vars [definition, in octalgo.datalogcert.syntax]
term [inductive, in octalgo.datalogcert.syntax]
termRep [abbreviation, in octalgo.datalogcert.syntax]
term_to_var [definition, in octalgo.octalgo.occurrences]
term_vars [definition, in octalgo.datalogcert.syntax]
term_repK [lemma, in octalgo.datalogcert.syntax]
term_con [definition, in octalgo.datalogcert.syntax]
term_rep [definition, in octalgo.datalogcert.syntax]
term_of_cons [definition, in octalgo.datalogcert.syntax]
Theory [section, in octalgo.datalogcert.syntax]
Theory.Constants [section, in octalgo.datalogcert.syntax]
Theory.Variables [section, in octalgo.datalogcert.syntax]
tnth_nth_error [lemma, in octalgo.octalgo.utils]
tocc_countprod [definition, in octalgo.octalgo.occurrences]
tocs [definition, in octalgo.octalgo.occurrences]
to_atom_satom_eq [lemma, in octalgo.datalogcert.subs]
to_grP [lemma, in octalgo.datalogcert.subs]
to_subE [lemma, in octalgo.datalogcert.subs]
to_sub [definition, in octalgo.datalogcert.subs]
to_gr [definition, in octalgo.datalogcert.subs]
to_tail [definition, in octalgo.datalogcert.subs]
to_gr_sub [lemma, in octalgo.datalogcert.soundness]
to_gr_atomP [lemma, in octalgo.datalogcert.soundness]
to_sub_gra [lemma, in octalgo.datalogcert.soundness]
to_sub_grt [lemma, in octalgo.datalogcert.soundness]
to_atom [definition, in octalgo.datalogcert.syntax]
to_atom_proof [lemma, in octalgo.datalogcert.syntax]
to_raw_atom [definition, in octalgo.datalogcert.syntax]
tprog [definition, in octalgo.octalgo.rinstance]
trace_sem_completeness_b [lemma, in octalgo.octalgo.tSemantics]
trace_sem_head_match [lemma, in octalgo.octalgo.tSemantics]
trace_sem_soundness [lemma, in octalgo.octalgo.tSemantics]
trace_sem_completeness [lemma, in octalgo.octalgo.tSemantics]
trace_sem_prev_trees_m1 [lemma, in octalgo.octalgo.tSemantics]
trace_sem_prev_trees [lemma, in octalgo.octalgo.tSemantics]
trace_sem_trees [definition, in octalgo.octalgo.tSemantics]
Transformation [section, in octalgo.octalgo.extract_static]
Transformation.def [variable, in octalgo.octalgo.extract_static]
Transformation.df [variable, in octalgo.octalgo.extract_static]
Transformation.dga [variable, in octalgo.octalgo.extract_static]
Transformation.docc [variable, in octalgo.octalgo.extract_static]
Transformation.dv [variable, in octalgo.octalgo.extract_static]
Transformation.Hpsafe [variable, in octalgo.octalgo.extract_static]
Transformation.Hpsafehds [variable, in octalgo.octalgo.extract_static]
Transformation.Hsafe_edb [variable, in octalgo.octalgo.extract_static]
Transformation.Hvarinhead [variable, in octalgo.octalgo.extract_static]
Transformation.Hvns [variable, in octalgo.octalgo.extract_static]
Transformation.i [variable, in octalgo.octalgo.extract_static]
Transformation.p [variable, in octalgo.octalgo.extract_static]
Transformation.v [variable, in octalgo.octalgo.extract_static]
tr_cl_in [lemma, in octalgo.octalgo.tSemantics]
tSemantics [section, in octalgo.octalgo.tSemantics]
tSemantics [library]
tSemantics.gat_def [variable, in octalgo.octalgo.tSemantics]
tSemantics.p [variable, in octalgo.octalgo.tSemantics]
tSemantics.rul_gr [section, in octalgo.octalgo.tSemantics]
tSemantics.trace_sem_trees [section, in octalgo.octalgo.tSemantics]
tst_node_head [definition, in octalgo.octalgo.tSemantics]
tst_uniq_ind_prop [lemma, in octalgo.octalgo.fintrees]
tst_uniq_ind [lemma, in octalgo.octalgo.fintrees]
tuple_to_wlist [definition, in octalgo.octalgo.finseqs]
type_preserving_inversion [lemma, in octalgo.octalgo.tSemantics]
t_at_vars_in [lemma, in octalgo.octalgo.occurrences]
t_at [definition, in octalgo.octalgo.occurrences]
t_occ_finMixin [definition, in octalgo.octalgo.occurrences]
t_occ_countMixin [definition, in octalgo.octalgo.occurrences]
t_occ_choiceMixin [definition, in octalgo.octalgo.occurrences]
t_occ_eqMixin [definition, in octalgo.octalgo.occurrences]
t_occ_pre [definition, in octalgo.octalgo.occurrences]
t_occ_rep [definition, in octalgo.octalgo.occurrences]
t_ind [projection, in octalgo.octalgo.occurrences]
t_occ [record, in octalgo.octalgo.occurrences]
T_occ [constructor, in octalgo.octalgo.occurrences]

U

ua [projection, in octalgo.datalogcert.syntax]
ubound [definition, in octalgo.datalogcert.fixpoint]
ucons [definition, in octalgo.octalgo.finseqs]
ucons1 [definition, in octalgo.octalgo.finseqs]
uga [projection, in octalgo.datalogcert.syntax]
unil [definition, in octalgo.octalgo.finseqs]
uniq_seq_finMixin [definition, in octalgo.octalgo.finseqs]
uniq_seq_of_tag [definition, in octalgo.octalgo.finseqs]
uniq_behead [lemma, in octalgo.octalgo.finseqs]
uniq_seq [record, in octalgo.octalgo.finseqs]
uniq_seq [section, in octalgo.octalgo.finseqs]
uniq_h_wutree [lemma, in octalgo.octalgo.fintrees]
uniq_ab_htree [lemma, in octalgo.octalgo.fintrees]
uniq_ab_size [lemma, in octalgo.octalgo.fintrees]
uniq_desc [lemma, in octalgo.octalgo.fintrees]
uniq_desc_r [lemma, in octalgo.octalgo.fintrees]
uniq_desc_l [lemma, in octalgo.octalgo.fintrees]
unrec_trace_gen_normal_form [lemma, in octalgo.octalgo.norec_sem]
unrec_trace_gen_count_incr [lemma, in octalgo.octalgo.norec_sem]
unrec_trace_gen_notin [lemma, in octalgo.octalgo.norec_sem]
unrec_trace [definition, in octalgo.octalgo.norec_sem]
unrec_trace_gen [definition, in octalgo.octalgo.norec_sem]
untyped_in_scl_match_body [lemma, in octalgo.datalogcert.soundness]
untyped_in_scl_match_pbody [lemma, in octalgo.datalogcert.soundness]
useq [projection, in octalgo.octalgo.finseqs]
useq_hd [definition, in octalgo.octalgo.finseqs]
useq_behead [definition, in octalgo.octalgo.finseqs]
utemptysub [lemma, in octalgo.datalogcert.subs]
utils [library]

V

Val [constructor, in octalgo.datalogcert.syntax]
Var [constructor, in octalgo.datalogcert.syntax]
vars_not_shared [definition, in octalgo.datalogcert.syntax]
var_neq [lemma, in octalgo.octalgo.projection]
vns_cl_eq [lemma, in octalgo.datalogcert.syntax]
v_in_dom_stail [lemma, in octalgo.datalogcert.subs]
v_in_dom_satom [lemma, in octalgo.datalogcert.subs]
v_in_extract [lemma, in octalgo.octalgo.projection]
v_in_extract_c [lemma, in octalgo.octalgo.projection]

W

wall [definition, in octalgo.octalgo.finseqs]
wall_to_all [lemma, in octalgo.octalgo.finseqs]
wall_allK [lemma, in octalgo.octalgo.finseqs]
wapp [definition, in octalgo.octalgo.finseqs]
wf_gclone [lemma, in octalgo.octalgo.projection]
wf_clone [lemma, in octalgo.octalgo.projection]
wf_atom [definition, in octalgo.datalogcert.syntax]
wf_gatom [definition, in octalgo.datalogcert.syntax]
wht [projection, in octalgo.octalgo.fintrees]
Wht [constructor, in octalgo.octalgo.fintrees]
width_desc_r [lemma, in octalgo.octalgo.fintrees]
width_desc_l [lemma, in octalgo.octalgo.fintrees]
Wlist [inductive, in octalgo.octalgo.finseqs]
Wlist [section, in octalgo.octalgo.finseqs]
wlistn_finType [definition, in octalgo.octalgo.finseqs]
wlistn_finMixin [definition, in octalgo.octalgo.finseqs]
wlistn_countType [definition, in octalgo.octalgo.finseqs]
wlistn_countMixin [definition, in octalgo.octalgo.finseqs]
wlistn_choiceType [definition, in octalgo.octalgo.finseqs]
wlistn_choiceMixin [definition, in octalgo.octalgo.finseqs]
wlistn_eqType [definition, in octalgo.octalgo.finseqs]
wlistn_eqMixin [definition, in octalgo.octalgo.finseqs]
wlist_subType [definition, in octalgo.octalgo.finseqs]
wlist_ind [lemma, in octalgo.octalgo.finseqs]
wlist_elim [lemma, in octalgo.octalgo.finseqs]
wlist_to_seq_size [lemma, in octalgo.octalgo.finseqs]
wlist_seqK [lemma, in octalgo.octalgo.finseqs]
wlist_to_seq [definition, in octalgo.octalgo.finseqs]
Wlist.Cancel [section, in octalgo.octalgo.finseqs]
Wlist.Cancel.A [variable, in octalgo.octalgo.finseqs]
Wlist.WlistChoiceType [section, in octalgo.octalgo.finseqs]
Wlist.WlistChoiceType.A [variable, in octalgo.octalgo.finseqs]
Wlist.WlistCountType [section, in octalgo.octalgo.finseqs]
Wlist.WlistCountType.A [variable, in octalgo.octalgo.finseqs]
Wlist.WlistEqType [section, in octalgo.octalgo.finseqs]
Wlist.WlistEqType.A [variable, in octalgo.octalgo.finseqs]
Wlist.WlistFinType [section, in octalgo.octalgo.finseqs]
Wlist.WlistFinType.A [variable, in octalgo.octalgo.finseqs]
Wlist.WlistSubType [section, in octalgo.octalgo.finseqs]
Wlist.WlistUtils [section, in octalgo.octalgo.finseqs]
wlist0_finType [definition, in octalgo.octalgo.finseqs]
wlist0_finMixin [definition, in octalgo.octalgo.finseqs]
wlist0_countType [definition, in octalgo.octalgo.finseqs]
wlist0_countMixin [definition, in octalgo.octalgo.finseqs]
wlist0_choiceType [definition, in octalgo.octalgo.finseqs]
wlist0_choiceMixin [definition, in octalgo.octalgo.finseqs]
wlist0_eqType [definition, in octalgo.octalgo.finseqs]
wlist0_eqMixin [definition, in octalgo.octalgo.finseqs]
wmap [definition, in octalgo.octalgo.finseqs]
wmapcoK [lemma, in octalgo.octalgo.finseqs]
wmapK [lemma, in octalgo.octalgo.finseqs]
wmap_nil [lemma, in octalgo.octalgo.finseqs]
wsize [definition, in octalgo.octalgo.finseqs]
WUnotin [definition, in octalgo.octalgo.fintrees]
WUtree [record, in octalgo.octalgo.fintrees]
WUtree [section, in octalgo.octalgo.fintrees]
wutree_option_fsfType [definition, in octalgo.octalgo.fintrees]
wutree_option_finType [definition, in octalgo.octalgo.fintrees]
wutree_finMixin [definition, in octalgo.octalgo.fintrees]
wutree_subcountMixin [definition, in octalgo.octalgo.fintrees]
wutree_countMixin [definition, in octalgo.octalgo.fintrees]
wutree_choiceMixin [definition, in octalgo.octalgo.fintrees]
wutree_eqMixin [definition, in octalgo.octalgo.fintrees]
wutree_subType [definition, in octalgo.octalgo.fintrees]
wutree_htreeK [lemma, in octalgo.octalgo.fintrees]
wutree_htree_valK [lemma, in octalgo.octalgo.fintrees]
WUtree_to_H [definition, in octalgo.octalgo.fintrees]
WUtree.WUtree_utils [section, in octalgo.octalgo.fintrees]
WUtree.WUtree_subFinType [section, in octalgo.octalgo.fintrees]
WUtree.WUtree_finType [section, in octalgo.octalgo.fintrees]
wu_map [definition, in octalgo.octalgo.fintrees]
wu_pcons_tup [definition, in octalgo.octalgo.fintrees]
wu_pcons_seq [definition, in octalgo.octalgo.fintrees]
wu_pcons_wlist [definition, in octalgo.octalgo.fintrees]
wu_cons_wlist [definition, in octalgo.octalgo.fintrees]
wu_cons [definition, in octalgo.octalgo.fintrees]
wu_list_width [lemma, in octalgo.octalgo.fintrees]
wu_cons_uniq [lemma, in octalgo.octalgo.fintrees]
wu_leaf [definition, in octalgo.octalgo.fintrees]
wu_pred_leaf [lemma, in octalgo.octalgo.fintrees]
WU_fsf [definition, in octalgo.octalgo.fintrees]
WU_sf_subK [lemma, in octalgo.octalgo.fintrees]
WU_sf_elim [lemma, in octalgo.octalgo.fintrees]
WU_sf_sub [definition, in octalgo.octalgo.fintrees]
wu_htree_elim [lemma, in octalgo.octalgo.fintrees]
wu_tree_of_htree [definition, in octalgo.octalgo.fintrees]
wu_merge [definition, in octalgo.octalgo.fintrees]
wu_pred_map [lemma, in octalgo.octalgo.fintrees]
wu_pred_sub [lemma, in octalgo.octalgo.fintrees]
wu_pred_descs [lemma, in octalgo.octalgo.fintrees]
wu_pred [definition, in octalgo.octalgo.fintrees]
w_all_prop [definition, in octalgo.octalgo.finseqs]
w_subtype [definition, in octalgo.octalgo.finseqs]

other

_ \sub _ (bool_scope) [notation, in octalgo.datalogcert.subs]
\bigcup_ ( _ in _ ) _ (fset_scope) [notation, in octalgo.third_party.bigop_aux]
\bigcup_ ( _ in _ | _ ) _ (fset_scope) [notation, in octalgo.third_party.bigop_aux]
\bigcup_ ( _ | _ ) _ (fset_scope) [notation, in octalgo.third_party.bigop_aux]
\bigcup_ ( _ <- _ ) _ (fset_scope) [notation, in octalgo.third_party.bigop_aux]
\bigcup_ ( _ <- _ | _ ) _ (fset_scope) [notation, in octalgo.third_party.bigop_aux]

---

Notation Index

S

_ \sub _ (bool_scope) [in octalgo.datalogcert.subs]

other

_ \sub _ (bool_scope) [in octalgo.datalogcert.subs]
\bigcup_ ( _ in _ ) _ (fset_scope) [in octalgo.third_party.bigop_aux]
\bigcup_ ( _ in _ | _ ) _ (fset_scope) [in octalgo.third_party.bigop_aux]
\bigcup_ ( _ | _ ) _ (fset_scope) [in octalgo.third_party.bigop_aux]
\bigcup_ ( _ <- _ ) _ (fset_scope) [in octalgo.third_party.bigop_aux]
\bigcup_ ( _ <- _ | _ ) _ (fset_scope) [in octalgo.third_party.bigop_aux]

---

Variable Index

A

ABtree.InducType.A [in octalgo.octalgo.fintrees]
ABtree.InducType.B [in octalgo.octalgo.fintrees]
analysis.completeness.df [in octalgo.octalgo.static]
analysis.completeness.docc [in octalgo.octalgo.static]
analysis.completeness.gat_def [in octalgo.octalgo.static]
analysis.dt [in octalgo.octalgo.static]
analysis.dv [in octalgo.octalgo.static]
analysis.p [in octalgo.octalgo.static]

B

BigCupSeq.I [in octalgo.third_party.bigop_aux]
BigCupSeq.T [in octalgo.third_party.bigop_aux]
BigFOpsFin.I [in octalgo.third_party.bigop_aux]
BigFOpsFin.T [in octalgo.third_party.bigop_aux]
BigFOpsSeq.I [in octalgo.third_party.bigop_aux]
BigFOpsSeq.T [in octalgo.third_party.bigop_aux]

C

Completeness.def [in octalgo.datalogcert.completeness]
Completeness.n [in octalgo.datalogcert.completeness]
Completeness.p [in octalgo.datalogcert.completeness]
Completeness.p_safe [in octalgo.datalogcert.completeness]

F

Fixpoints.f [in octalgo.datalogcert.fixpoint]
Fixpoints.f_ubound [in octalgo.datalogcert.fixpoint]
Fixpoints.f_inc [in octalgo.datalogcert.fixpoint]
Fixpoints.f_mono [in octalgo.datalogcert.fixpoint]
Fixpoints.s0 [in octalgo.datalogcert.fixpoint]
Fixpoints.s0_bound [in octalgo.datalogcert.fixpoint]
Fixpoints.T [in octalgo.datalogcert.fixpoint]
Fixpoints.ub [in octalgo.datalogcert.fixpoint]
FSetMonoids.T [in octalgo.third_party.bigop_aux]

H

HTree.HtreeChoiceType.A [in octalgo.octalgo.fintrees]
HTree.HtreeChoiceType.B [in octalgo.octalgo.fintrees]
HTree.HtreeCountType.A [in octalgo.octalgo.fintrees]
HTree.HtreeCountType.B [in octalgo.octalgo.fintrees]
HTree.HtreeEqType.A [in octalgo.octalgo.fintrees]
HTree.HtreeEqType.B [in octalgo.octalgo.fintrees]
HTree.HtreeFinType.A [in octalgo.octalgo.fintrees]
HTree.HtreeFinType.B [in octalgo.octalgo.fintrees]
HTree.InducType.A [in octalgo.octalgo.fintrees]
HTree.InducType.B [in octalgo.octalgo.fintrees]
HTree.w [in octalgo.octalgo.fintrees]

I

iter_mon.f_lb [in octalgo.datalogcert.fixpoint]
iter_mon.lb [in octalgo.datalogcert.fixpoint]
iter_mon.f_mon [in octalgo.datalogcert.fixpoint]
iter_mon.f [in octalgo.datalogcert.fixpoint]
iter_mon.T [in octalgo.datalogcert.fixpoint]

M

Match.def [in octalgo.datalogcert.pmatch]

N

NoDepGrounding.def [in octalgo.datalogcert.subs]
no_rec_traces.df [in octalgo.octalgo.norec_sem]
no_rec_traces.dv [in octalgo.octalgo.norec_sem]
no_rec_traces.dt [in octalgo.octalgo.norec_sem]
no_rec_traces.gat_def [in octalgo.octalgo.norec_sem]
no_rec_traces.p [in octalgo.octalgo.norec_sem]

O

occurrences.a_occ.p [in octalgo.octalgo.occurrences]
occurrences.df [in octalgo.octalgo.occurrences]
occurrences.dt [in octalgo.octalgo.occurrences]
occurrences.dv [in octalgo.octalgo.occurrences]
occurrences.t_occ.p [in octalgo.octalgo.occurrences]

P

Projection.always_cons [in octalgo.octalgo.projection]
Projection.arity_vars [in octalgo.octalgo.projection]
Projection.bn_not_zero [in octalgo.octalgo.projection]
Projection.def [in octalgo.octalgo.projection]
Projection.f [in octalgo.octalgo.projection]
Projection.ftype [in octalgo.octalgo.projection]
Projection.i [in octalgo.octalgo.projection]
Projection.ifresh [in octalgo.octalgo.projection]
Projection.ind [in octalgo.octalgo.projection]
Projection.isafe [in octalgo.octalgo.projection]
Projection.p [in octalgo.octalgo.projection]
Projection.parity [in octalgo.octalgo.projection]
Projection.pclone [in octalgo.octalgo.projection]
Projection.pfresh [in octalgo.octalgo.projection]
Projection.pinj [in octalgo.octalgo.projection]
Projection.pnotf [in octalgo.octalgo.projection]
Projection.psafe [in octalgo.octalgo.projection]
Purge.def [in octalgo.octalgo.purge]
Purge.f [in octalgo.octalgo.purge]
Purge.i [in octalgo.octalgo.purge]
Purge.ind [in octalgo.octalgo.purge]
Purge.p [in octalgo.octalgo.purge]
Purge.vals [in octalgo.octalgo.purge]
Purge.vals_adeq [in octalgo.octalgo.purge]

R

RuleInstance.def [in octalgo.octalgo.rinstance]
RuleInstance.i [in octalgo.octalgo.rinstance]
RuleInstance.p [in octalgo.octalgo.rinstance]
RuleInstance.psafe [in octalgo.octalgo.rinstance]
RuleInstance.Rv [in octalgo.octalgo.rinstance]
RuleInstance.subs [in octalgo.octalgo.rinstance]
RuleInstance.subs_comp [in octalgo.octalgo.rinstance]

T

Transformation.def [in octalgo.octalgo.extract_static]
Transformation.df [in octalgo.octalgo.extract_static]
Transformation.dga [in octalgo.octalgo.extract_static]
Transformation.docc [in octalgo.octalgo.extract_static]
Transformation.dv [in octalgo.octalgo.extract_static]
Transformation.Hpsafe [in octalgo.octalgo.extract_static]
Transformation.Hpsafehds [in octalgo.octalgo.extract_static]
Transformation.Hsafe_edb [in octalgo.octalgo.extract_static]
Transformation.Hvarinhead [in octalgo.octalgo.extract_static]
Transformation.Hvns [in octalgo.octalgo.extract_static]
Transformation.i [in octalgo.octalgo.extract_static]
Transformation.p [in octalgo.octalgo.extract_static]
Transformation.v [in octalgo.octalgo.extract_static]
tSemantics.gat_def [in octalgo.octalgo.tSemantics]
tSemantics.p [in octalgo.octalgo.tSemantics]

W

Wlist.Cancel.A [in octalgo.octalgo.finseqs]
Wlist.WlistChoiceType.A [in octalgo.octalgo.finseqs]
Wlist.WlistCountType.A [in octalgo.octalgo.finseqs]
Wlist.WlistEqType.A [in octalgo.octalgo.finseqs]
Wlist.WlistFinType.A [in octalgo.octalgo.finseqs]

---

Library Index

B

bigop_aux
bSemantics

C

completeness

E

extract_static

F

finseqs
fintrees
fixpoint

M

monotonicity

N

norec_sem

O

occurrences

P

pmatch
projection
purge

R

rinstance

S

soundness
static
subs
syntax

T

tSemantics

U

utils

---

Lemma Index

A

ABin_extract [in octalgo.octalgo.fintrees]
ABnotin_branches [in octalgo.octalgo.fintrees]
ABnotin_map [in octalgo.octalgo.fintrees]
ABnotin_node_and [in octalgo.octalgo.fintrees]
abtree_htreeK [in octalgo.octalgo.fintrees]
abtree_eq_axiom [in octalgo.octalgo.fintrees]
abtree_inv [in octalgo.octalgo.fintrees]
abtree_eq_refl [in octalgo.octalgo.fintrees]
abtree_ind_prop [in octalgo.octalgo.fintrees]
abtree_ind [in octalgo.octalgo.fintrees]
ABuniq_map [in octalgo.octalgo.fintrees]
ABwidth_map [in octalgo.octalgo.fintrees]
ABwidth_cons [in octalgo.octalgo.fintrees]
AB_to_WUnotin_seq [in octalgo.octalgo.fintrees]
addE [in octalgo.datalogcert.subs]
add_untyped_untyped [in octalgo.datalogcert.subs]
add_typed_untyped [in octalgo.datalogcert.subs]
add_com [in octalgo.datalogcert.subs]
add_add [in octalgo.datalogcert.subs]
add_seq_gr_def [in octalgo.octalgo.projection]
all_prop_prop_decr [in octalgo.octalgo.utils]
all_prop_seq_decr [in octalgo.octalgo.utils]
all_prop_in [in octalgo.octalgo.utils]
all_prop_cat [in octalgo.octalgo.utils]
all_prop_cat_r [in octalgo.octalgo.utils]
all_prop_cat_l [in octalgo.octalgo.utils]
all_exist_tuple [in octalgo.octalgo.utils]
all_exist_enum [in octalgo.octalgo.utils]
all_exist_seq [in octalgo.octalgo.utils]
all_dom_empty [in octalgo.datalogcert.subs]
all_mem_edb_tst [in octalgo.octalgo.tSemantics]
all_prop_cons_notin [in octalgo.octalgo.fintrees]
always_cons_in_vals [in octalgo.octalgo.projection]
analyze_incr [in octalgo.octalgo.static]
analyze_disj [in octalgo.octalgo.static]
andP_to_uniq [in octalgo.octalgo.finseqs]
arg_atom_vars_in [in octalgo.octalgo.occurrences]
arg_c_match [in octalgo.datalogcert.soundness]
atom_vars_sub_gr_def [in octalgo.datalogcert.subs]
atom_vars_sub_gr [in octalgo.datalogcert.subs]
atom_vars_clone_c [in octalgo.octalgo.projection]
atom_clone_not_f [in octalgo.octalgo.projection]
aux_leaf0 [in octalgo.octalgo.fintrees]

B

bigcups_seqP [in octalgo.third_party.bigop_aux]
bigcup_type_seq [in octalgo.octalgo.utils]
bigcup_seqP [in octalgo.third_party.bigop_aux]
bigfcups_seqP [in octalgo.third_party.bigop_aux]
bigfcup_seqP [in octalgo.third_party.bigop_aux]
bindP [in octalgo.datalogcert.pmatch]
bindSU [in octalgo.datalogcert.pmatch]
bindS_incr [in octalgo.datalogcert.monotonicity]
bindUS [in octalgo.datalogcert.pmatch]
bmatch_match_body [in octalgo.datalogcert.soundness]
bool_des_rew [in octalgo.octalgo.utils]
bool_to_prop_r [in octalgo.octalgo.utils]
bool_to_prop_l [in octalgo.octalgo.utils]
bpM [in octalgo.datalogcert.completeness]
branch_t_ind_eq [in octalgo.octalgo.norec_sem]
branch_pred_eq [in octalgo.octalgo.norec_sem]

C

cadequacy [in octalgo.octalgo.rinstance]
cancelffgg [in octalgo.octalgo.finseqs]
cancelfg [in octalgo.octalgo.finseqs]
cancelflgl [in octalgo.octalgo.fintrees]
cancel_fflggl [in octalgo.octalgo.fintrees]
canc_abtree_gentree [in octalgo.octalgo.fintrees]
ccompleteness [in octalgo.octalgo.rinstance]
clause_repK [in octalgo.datalogcert.syntax]
clone_bmatch [in octalgo.octalgo.projection]
clone_in [in octalgo.octalgo.projection]
clone_v [in octalgo.octalgo.projection]
clone_oob [in octalgo.octalgo.projection]
cons_cl_stable [in octalgo.datalogcert.soundness]
cons_cl_sound [in octalgo.datalogcert.soundness]
cons_cl_incr [in octalgo.datalogcert.monotonicity]
cons_clause_t_desc [in octalgo.octalgo.tSemantics]
cons_clause_h [in octalgo.octalgo.tSemantics]
cons_clause_idb [in octalgo.datalogcert.bSemantics]
csoundness [in octalgo.octalgo.rinstance]
cteq [in octalgo.octalgo.finseqs]
cteql [in octalgo.octalgo.fintrees]

D

deducing_c_to_gen [in octalgo.octalgo.projection]
ded_gr_equal_stail [in octalgo.octalgo.tSemantics]
ded_sub_equal_equal_to_def [in octalgo.octalgo.tSemantics]
dep_iota_uniq [in octalgo.octalgo.utils]
dep_iotaE [in octalgo.octalgo.utils]
disjointC [in octalgo.octalgo.utils]
disjoint_in_false [in octalgo.octalgo.utils]
dom_sub_grE [in octalgo.datalogcert.subs]
dom_singlesub [in octalgo.datalogcert.subs]
dom_emptysub [in octalgo.datalogcert.subs]

E

edb_in_sem_t_descs [in octalgo.octalgo.tSemantics]
emptymin [in octalgo.datalogcert.subs]
emptysubE [in octalgo.datalogcert.subs]
Eqdep_dec_bool [in octalgo.octalgo.utils]
equiv_part_set_mon [in octalgo.octalgo.utils]
equiv_part_set0 [in octalgo.octalgo.utils]
eq_foldS [in octalgo.datalogcert.pmatch]
eq_bindS [in octalgo.datalogcert.pmatch]
eq_singlesub [in octalgo.datalogcert.subs]
eq_fwd_chain [in octalgo.datalogcert.soundness]
extract_vals_sub_adequate [in octalgo.octalgo.extract_static]
extract_gr_v [in octalgo.octalgo.projection]
extract_sub_seq_rem_map [in octalgo.octalgo.projection]
extract_sub_seq_map [in octalgo.octalgo.projection]
extract_dom [in octalgo.octalgo.projection]
extract_in_v [in octalgo.octalgo.projection]

F

fenc_atomK [in octalgo.datalogcert.syntax]
fenc_gatomK [in octalgo.datalogcert.syntax]
ffp_comp [in octalgo.octalgo.rinstance]
find_iota [in octalgo.octalgo.utils]
find_eq_nth_uniq [in octalgo.octalgo.utils]
find_val [in octalgo.octalgo.utils]
fix_iter [in octalgo.datalogcert.fixpoint]
foldl_0 [in octalgo.datalogcert.soundness]
foldl_0_gen [in octalgo.datalogcert.soundness]
foldObindNone [in octalgo.octalgo.utils]
foldr_maxn_base [in octalgo.octalgo.utils]
foldSU [in octalgo.datalogcert.pmatch]
foldS_incr [in octalgo.datalogcert.monotonicity]
fold_maxn_n_map_ltn [in octalgo.octalgo.utils]
fold_maxn_n_map_leq [in octalgo.octalgo.utils]
fold_maxn_n_map_gtn [in octalgo.octalgo.utils]
fold_maxn_n_map_geq [in octalgo.octalgo.utils]
fold_add_mapsto [in octalgo.datalogcert.soundness]
fwd_chain_complete [in octalgo.datalogcert.completeness]
fwd_chain_mod [in octalgo.datalogcert.soundness]
fwd_chain_sym [in octalgo.datalogcert.soundness]
fwd_chain_cat [in octalgo.datalogcert.soundness]
fwd_chainP [in octalgo.datalogcert.soundness]
fwd_chain_stable [in octalgo.datalogcert.soundness]
fwd_chain_sound [in octalgo.datalogcert.soundness]
fwd_chain_inc [in octalgo.datalogcert.monotonicity]
fwd_chain_pincr [in octalgo.datalogcert.monotonicity]
fwd_chain_incr [in octalgo.datalogcert.monotonicity]
fwd_chain_inc_single [in octalgo.octalgo.tSemantics]
fwd_chain_t_inc_single [in octalgo.octalgo.tSemantics]
fwd_chain_t_inc [in octalgo.octalgo.tSemantics]

G

gatom_clone_f [in octalgo.octalgo.projection]
gatom_clone_not_f [in octalgo.octalgo.projection]
gatom_eta [in octalgo.datalogcert.syntax]
ga_ded [in octalgo.datalogcert.soundness]
ga_a_ex_sym_eq [in octalgo.octalgo.projection]
gclause_repK [in octalgo.datalogcert.syntax]
gclause_eq_axiom [in octalgo.datalogcert.syntax]
gclause_eq_inv [in octalgo.datalogcert.syntax]
gclause_eq_refl [in octalgo.datalogcert.syntax]
gen_c_f_c_size [in octalgo.octalgo.projection]
gen_vars_rem_all_v [in octalgo.octalgo.projection]
gen_vars_j_all_v [in octalgo.octalgo.projection]
gen_vars_rem_uniq [in octalgo.octalgo.projection]
gen_vars_j_uniq [in octalgo.octalgo.projection]
gen_vars_j_find [in octalgo.octalgo.projection]
geq_max_r [in octalgo.octalgo.utils]
geq_max_l [in octalgo.octalgo.utils]
get_cl_var_leq [in octalgo.octalgo.occurrences]
gr_term_def_eq_in_dom [in octalgo.datalogcert.subs]
gr_atom_defK [in octalgo.datalogcert.subs]
gr_atom_defP [in octalgo.datalogcert.subs]
gr_atom_def_proof [in octalgo.datalogcert.subs]
gr_raw_atom_scl_eq [in octalgo.datalogcert.subs]
gr_term_sub [in octalgo.datalogcert.subs]
gr_term_defP [in octalgo.datalogcert.subs]
gr_term_def_scl_eq [in octalgo.datalogcert.subs]
gr_atom_defE [in octalgo.datalogcert.soundness]
gr_atom_def_clone_eq [in octalgo.octalgo.projection]
gr_term_def_seq_add_notin [in octalgo.octalgo.projection]
gtn_max_r [in octalgo.octalgo.utils]
gtn_max_l [in octalgo.octalgo.utils]

H

has_lfp [in octalgo.datalogcert.fixpoint]
Hclp_not_cloned [in octalgo.octalgo.projection]
height_WUtree [in octalgo.octalgo.fintrees]
Htree_to_ABwidth [in octalgo.octalgo.fintrees]
htree_wutreeK [in octalgo.octalgo.fintrees]
htree_abtreeK [in octalgo.octalgo.fintrees]
htree_uniq_ind_prop_seq [in octalgo.octalgo.fintrees]
htree_uniq_ind_prop [in octalgo.octalgo.fintrees]
htree_uniq_ind [in octalgo.octalgo.fintrees]
Huniq_to_ABuniq [in octalgo.octalgo.fintrees]
hutree_abtreeK [in octalgo.octalgo.fintrees]
h_to_ab_w_bound [in octalgo.octalgo.fintrees]

I

idb_in_sem_t_descs [in octalgo.octalgo.tSemantics]
incr_fwd_chain_complete [in octalgo.datalogcert.completeness]
ind_in_gen_vars [in octalgo.octalgo.projection]
ind_in_gen_vars_j [in octalgo.octalgo.projection]
in_nth_P [in octalgo.octalgo.utils]
in_rem [in octalgo.octalgo.utils]
in_extract_c_v [in octalgo.octalgo.projection]
is_clone_ga_f [in octalgo.octalgo.projection]
is_clone_clone_pred [in octalgo.octalgo.projection]
iterf_incr_bound [in octalgo.datalogcert.fixpoint]
iter_fun_incr [in octalgo.octalgo.utils]
iter_mon [in octalgo.datalogcert.fixpoint]
iter_leq_fix [in octalgo.datalogcert.fixpoint]
iter_fwd_chain_stable [in octalgo.datalogcert.soundness]
iter_fwd_chain_sym [in octalgo.datalogcert.soundness]
iter_fwd_chain_subset [in octalgo.datalogcert.monotonicity]
ite_id [in octalgo.octalgo.utils]

K

keep_atom_tail_match [in octalgo.octalgo.purge]
keep_atom_sem [in octalgo.octalgo.purge]

L

leaf0 [in octalgo.octalgo.fintrees]
leq_fold_base [in octalgo.octalgo.utils]
leq_fold_maxl [in octalgo.octalgo.utils]
lfpE [in octalgo.datalogcert.fixpoint]
ltn_leq_trans [in octalgo.octalgo.utils]

M

map_square_eq [in octalgo.octalgo.utils]
match_atomsP [in octalgo.datalogcert.pmatch]
match_term_sub [in octalgo.datalogcert.pmatch]
match_body_bmatch [in octalgo.datalogcert.soundness]
match_term_head_some [in octalgo.datalogcert.soundness]
match_body_strata [in octalgo.datalogcert.soundness]
match_atom_all_strata [in octalgo.datalogcert.soundness]
match_atom_allU [in octalgo.datalogcert.soundness]
match_tl_sound [in octalgo.datalogcert.soundness]
match_domsI [in octalgo.datalogcert.soundness]
match_vars_seteq [in octalgo.datalogcert.soundness]
match_vars_subset [in octalgo.datalogcert.soundness]
match_atoms_vars_subset [in octalgo.datalogcert.soundness]
match_pbody_sub [in octalgo.datalogcert.soundness]
match_subset_vars [in octalgo.datalogcert.soundness]
match_atom_all_dom [in octalgo.datalogcert.soundness]
match_atom_dom [in octalgo.datalogcert.soundness]
match_atom_diff_heads [in octalgo.datalogcert.soundness]
match_atom_diff_cons [in octalgo.datalogcert.soundness]
match_atom_dif_lengths [in octalgo.datalogcert.soundness]
match_pbody_sound [in octalgo.datalogcert.soundness]
match_atom_all_sub [in octalgo.datalogcert.soundness]
match_tl_complete [in octalgo.datalogcert.soundness]
match_ptl_sub_complete [in octalgo.datalogcert.soundness]
match_ptl_complete [in octalgo.datalogcert.soundness]
match_atom_complete [in octalgo.datalogcert.soundness]
match_term_complete [in octalgo.datalogcert.soundness]
match_atoms_pbody [in octalgo.datalogcert.soundness]
match_body_pbody [in octalgo.datalogcert.soundness]
match_pbody_cons [in octalgo.datalogcert.soundness]
match_pbody_incr [in octalgo.datalogcert.soundness]
match_atoms_sub [in octalgo.datalogcert.soundness]
match_atom_sub [in octalgo.datalogcert.soundness]
match_atom_sound [in octalgo.datalogcert.soundness]
match_term_sound [in octalgo.datalogcert.soundness]
match_clone_not_f [in octalgo.octalgo.projection]
match_clone [in octalgo.octalgo.projection]
match_atom_all_clone_v [in octalgo.octalgo.projection]
match_atom_all_clone_cnone [in octalgo.octalgo.projection]
match_atom_clone_v [in octalgo.octalgo.projection]
match_atom_clone_cnone [in octalgo.octalgo.projection]
match_fold_clone [in octalgo.octalgo.projection]
match_body_incr [in octalgo.datalogcert.monotonicity]
match_atom_all_incr [in octalgo.datalogcert.monotonicity]
maxn_0_n [in octalgo.octalgo.fintrees]
max_ar_bound [in octalgo.datalogcert.syntax]
mem_pset_set [in octalgo.octalgo.utils]
mem_set_pset [in octalgo.octalgo.utils]
mem_body [in octalgo.octalgo.utils]
mem_bindE [in octalgo.datalogcert.subs]
min_lfp_all [in octalgo.datalogcert.fixpoint]

N

negb_has_predC_all [in octalgo.octalgo.utils]
neq_sym [in octalgo.octalgo.fintrees]
nil_list0 [in octalgo.octalgo.finseqs]
nil0 [in octalgo.octalgo.finseqs]
nomega_fp [in octalgo.octalgo.rinstance]
notinnil [in octalgo.octalgo.finseqs]
not_set1P [in octalgo.octalgo.utils]
no_rec_needed [in octalgo.octalgo.norec_sem]
no_rec_capt_nf [in octalgo.octalgo.static]
no_rec_capt [in octalgo.octalgo.static]
no_deduced_leaf [in octalgo.octalgo.tSemantics]
nth_default_size [in octalgo.octalgo.utils]
nth_error_some_none_size [in octalgo.octalgo.utils]
nth_error_case [in octalgo.octalgo.utils]
nth_error_leq_size [in octalgo.octalgo.utils]
nth_error_size_leq [in octalgo.octalgo.utils]
nth_error_sremove_eq [in octalgo.octalgo.utils]
nth_error_sremove [in octalgo.octalgo.utils]
nth_error_size_notin [in octalgo.octalgo.utils]
nth_error_notin_size [in octalgo.octalgo.utils]
nth_error_in_size [in octalgo.octalgo.utils]
nth_error_preim [in octalgo.octalgo.utils]
nth_error_set_nth [in octalgo.octalgo.utils]
nth_error_ncons1 [in octalgo.octalgo.utils]
nth_error_nth [in octalgo.octalgo.utils]
nth_error_map_none [in octalgo.octalgo.utils]
nth_error_map [in octalgo.octalgo.utils]
nth_error_in [in octalgo.octalgo.utils]

O

occsInAtomListV [in octalgo.octalgo.occurrences]
occsInAtomListVint [in octalgo.octalgo.occurrences]
occsInAtomV [in octalgo.octalgo.occurrences]
occsInProgramV [in octalgo.octalgo.occurrences]
occsInRuleV [in octalgo.octalgo.occurrences]
only_untyped_match [in octalgo.datalogcert.soundness]
oob_nth_error [in octalgo.octalgo.utils]
oob_atom_args [in octalgo.datalogcert.syntax]
oob_gatom_args [in octalgo.datalogcert.syntax]
ord_shiftl [in octalgo.octalgo.utils]
original_sem_no_clone [in octalgo.octalgo.projection]

P

pair_seq_nth_proj_l [in octalgo.octalgo.utils]
pmap_size_leq [in octalgo.octalgo.utils]
pmatch_vars_subset [in octalgo.datalogcert.soundness]
pmatch_subset_vars [in octalgo.datalogcert.soundness]
pmatch_clone_not_f [in octalgo.octalgo.projection]
pmatch_clone [in octalgo.octalgo.projection]
pp_p [in octalgo.octalgo.purge]
pred_ltn [in octalgo.octalgo.utils]
pred_ltn0_l [in octalgo.octalgo.utils]
pred_clone_c [in octalgo.octalgo.projection]
pred_type_eq_axiom [in octalgo.datalogcert.syntax]
prod_of_a_occK [in octalgo.octalgo.occurrences]
prod_of_t_occK [in octalgo.octalgo.occurrences]
prod_eq [in octalgo.octalgo.utils]
proj_soundness [in octalgo.octalgo.projection]
proj_soundness_u [in octalgo.octalgo.projection]
proj_completeness [in octalgo.octalgo.projection]
proj_completeness_u [in octalgo.octalgo.projection]
purge_sem_adequacy [in octalgo.octalgo.purge]
purge_sem_soundness [in octalgo.octalgo.purge]
purge_sem_completeness [in octalgo.octalgo.purge]

R

raw_gen_c_f_c_wf [in octalgo.octalgo.projection]
raw_gen_f_c_wf [in octalgo.octalgo.projection]
raw_atom_vars_cons [in octalgo.datalogcert.syntax]
raw_atom_vars_cons_sub [in octalgo.datalogcert.syntax]
raw_atom_repK [in octalgo.datalogcert.syntax]
raw_gatom_repK [in octalgo.datalogcert.syntax]
rul_gr_repK [in octalgo.octalgo.tSemantics]
r_dom_body [in octalgo.datalogcert.soundness]
r_dom_atom [in octalgo.datalogcert.soundness]
r_dom_term [in octalgo.datalogcert.soundness]

S

satomeq_subU [in octalgo.datalogcert.subs]
satom_vars_subset [in octalgo.datalogcert.subs]
satom_sub [in octalgo.datalogcert.subs]
satom_proof [in octalgo.datalogcert.subs]
sem_m_star_incr [in octalgo.datalogcert.monotonicity]
sem_inc [in octalgo.datalogcert.monotonicity]
sem_m_incr [in octalgo.datalogcert.monotonicity]
sem_t_Idb_pred [in octalgo.octalgo.tSemantics]
sem_t_Edb_pred [in octalgo.octalgo.tSemantics]
sem_t_leaf [in octalgo.octalgo.tSemantics]
sem_idb_in [in octalgo.datalogcert.bSemantics]
sem_idb_safe [in octalgo.datalogcert.bSemantics]
seq_in_ind [in octalgo.octalgo.utils]
seq_inj [in octalgo.octalgo.utils]
seq_in_rem_size [in octalgo.octalgo.utils]
seq_notin_f_in [in octalgo.octalgo.utils]
seq_inj [in octalgo.datalogcert.soundness]
seq_wlist_uncut_K [in octalgo.octalgo.finseqs]
seq_wlistK [in octalgo.octalgo.finseqs]
seq_to_bnil [in octalgo.octalgo.finseqs]
setIdP_bool_to_prop [in octalgo.octalgo.tSemantics]
set_nth_notin [in octalgo.octalgo.utils]
set_nth_notin_base [in octalgo.octalgo.utils]
set_notin_f_in [in octalgo.octalgo.utils]
set0_set1_neq [in octalgo.octalgo.utils]
simple_cons_eq_inversion [in octalgo.octalgo.tSemantics]
size_dep_iota [in octalgo.octalgo.utils]
size_map_leq [in octalgo.octalgo.utils]
size_gen_vars [in octalgo.octalgo.projection]
size_gen_vars_j [in octalgo.octalgo.projection]
size_wmap [in octalgo.octalgo.finseqs]
size_useq [in octalgo.octalgo.finseqs]
sremove_nth [in octalgo.octalgo.utils]
sremove_rem [in octalgo.octalgo.utils]
sremove_map [in octalgo.octalgo.utils]
sremove_in_size [in octalgo.octalgo.utils]
sremove_size [in octalgo.octalgo.utils]
sstree_height [in octalgo.octalgo.fintrees]
staileq_subU [in octalgo.datalogcert.subs]
stail_vars_subset [in octalgo.datalogcert.subs]
stail_ded_eq [in octalgo.octalgo.tSemantics]
stail_eq_to_gr_atom_eq [in octalgo.octalgo.tSemantics]
static_extraction_adequacy [in octalgo.octalgo.extract_static]
static_extract_spec [in octalgo.octalgo.extract_static]
sterm_sub [in octalgo.datalogcert.subs]
sterm_ga_eq [in octalgo.octalgo.tSemantics]
subset_to_in [in octalgo.octalgo.utils]
subset_iterf [in octalgo.datalogcert.fixpoint]
substE [in octalgo.datalogcert.subs]
substP [in octalgo.datalogcert.subs]
substss [in octalgo.datalogcert.subs]
subst_trans [in octalgo.datalogcert.subs]
subst0s [in octalgo.datalogcert.subs]
subtree_ssubtree [in octalgo.octalgo.fintrees]
subtree_refl [in octalgo.octalgo.fintrees]
subU_eq [in octalgo.datalogcert.subs]
subU_addl [in octalgo.datalogcert.subs]
subU_0r [in octalgo.datalogcert.subs]
subU_0l [in octalgo.datalogcert.subs]
subU_match [in octalgo.datalogcert.soundness]
sub_val_map [in octalgo.octalgo.utils]
sub_rem_seq [in octalgo.octalgo.utils]
sub_all_and_r [in octalgo.octalgo.utils]
sub_all_and_l [in octalgo.octalgo.utils]
sub_rem [in octalgo.octalgo.utils]
sub_sub_filter [in octalgo.datalogcert.subs]
sub_filter_eq [in octalgo.datalogcert.subs]
sub_filter_subset_t [in octalgo.datalogcert.subs]
sub_filter_subset_s [in octalgo.datalogcert.subs]
sub_dom [in octalgo.datalogcert.subs]
sub_add [in octalgo.datalogcert.subs]
sub_elim [in octalgo.datalogcert.subs]
sub_st_add [in octalgo.datalogcert.soundness]
sub_dom_ga [in octalgo.datalogcert.soundness]
sub_dom_raw [in octalgo.datalogcert.soundness]
sub_dom_gra [in octalgo.datalogcert.soundness]
sub_dom_grt [in octalgo.datalogcert.soundness]
sub_branches_head [in octalgo.octalgo.fintrees]
sym_satom [in octalgo.datalogcert.subs]
sym_pengine_subset_hsymp [in octalgo.datalogcert.soundness]
sym_satom_gatom [in octalgo.octalgo.projection]

T

tag_of_dbranchK [in octalgo.octalgo.finseqs]
tailvars_trans [in octalgo.datalogcert.syntax]
tail_mem [in octalgo.datalogcert.soundness]
tail_vars_1 [in octalgo.datalogcert.syntax]
tail_vars_nil [in octalgo.datalogcert.syntax]
tail_vars_head [in octalgo.datalogcert.syntax]
tail_vars_consUP [in octalgo.datalogcert.syntax]
tail_vars_sub_cons [in octalgo.datalogcert.syntax]
tail_vars_cons [in octalgo.datalogcert.syntax]
term_repK [in octalgo.datalogcert.syntax]
tnth_nth_error [in octalgo.octalgo.utils]
to_atom_satom_eq [in octalgo.datalogcert.subs]
to_grP [in octalgo.datalogcert.subs]
to_subE [in octalgo.datalogcert.subs]
to_gr_sub [in octalgo.datalogcert.soundness]
to_gr_atomP [in octalgo.datalogcert.soundness]
to_sub_gra [in octalgo.datalogcert.soundness]
to_sub_grt [in octalgo.datalogcert.soundness]
to_atom_proof [in octalgo.datalogcert.syntax]
trace_sem_completeness_b [in octalgo.octalgo.tSemantics]
trace_sem_head_match [in octalgo.octalgo.tSemantics]
trace_sem_soundness [in octalgo.octalgo.tSemantics]
trace_sem_completeness [in octalgo.octalgo.tSemantics]
trace_sem_prev_trees_m1 [in octalgo.octalgo.tSemantics]
trace_sem_prev_trees [in octalgo.octalgo.tSemantics]
tr_cl_in [in octalgo.octalgo.tSemantics]
tst_uniq_ind_prop [in octalgo.octalgo.fintrees]
tst_uniq_ind [in octalgo.octalgo.fintrees]
type_preserving_inversion [in octalgo.octalgo.tSemantics]
t_at_vars_in [in octalgo.octalgo.occurrences]

U

uniq_behead [in octalgo.octalgo.finseqs]
uniq_h_wutree [in octalgo.octalgo.fintrees]
uniq_ab_htree [in octalgo.octalgo.fintrees]
uniq_ab_size [in octalgo.octalgo.fintrees]
uniq_desc [in octalgo.octalgo.fintrees]
uniq_desc_r [in octalgo.octalgo.fintrees]
uniq_desc_l [in octalgo.octalgo.fintrees]
unrec_trace_gen_normal_form [in octalgo.octalgo.norec_sem]
unrec_trace_gen_count_incr [in octalgo.octalgo.norec_sem]
unrec_trace_gen_notin [in octalgo.octalgo.norec_sem]
untyped_in_scl_match_body [in octalgo.datalogcert.soundness]
untyped_in_scl_match_pbody [in octalgo.datalogcert.soundness]
utemptysub [in octalgo.datalogcert.subs]

V

var_neq [in octalgo.octalgo.projection]
vns_cl_eq [in octalgo.datalogcert.syntax]
v_in_dom_stail [in octalgo.datalogcert.subs]
v_in_dom_satom [in octalgo.datalogcert.subs]
v_in_extract [in octalgo.octalgo.projection]
v_in_extract_c [in octalgo.octalgo.projection]

W

wall_to_all [in octalgo.octalgo.finseqs]
wall_allK [in octalgo.octalgo.finseqs]
wf_gclone [in octalgo.octalgo.projection]
wf_clone [in octalgo.octalgo.projection]
width_desc_r [in octalgo.octalgo.fintrees]
width_desc_l [in octalgo.octalgo.fintrees]
wlist_ind [in octalgo.octalgo.finseqs]
wlist_elim [in octalgo.octalgo.finseqs]
wlist_to_seq_size [in octalgo.octalgo.finseqs]
wlist_seqK [in octalgo.octalgo.finseqs]
wmapcoK [in octalgo.octalgo.finseqs]
wmapK [in octalgo.octalgo.finseqs]
wmap_nil [in octalgo.octalgo.finseqs]
wutree_htreeK [in octalgo.octalgo.fintrees]
wutree_htree_valK [in octalgo.octalgo.fintrees]
wu_list_width [in octalgo.octalgo.fintrees]
wu_cons_uniq [in octalgo.octalgo.fintrees]
wu_pred_leaf [in octalgo.octalgo.fintrees]
WU_sf_subK [in octalgo.octalgo.fintrees]
WU_sf_elim [in octalgo.octalgo.fintrees]
wu_htree_elim [in octalgo.octalgo.fintrees]
wu_pred_map [in octalgo.octalgo.fintrees]
wu_pred_sub [in octalgo.octalgo.fintrees]
wu_pred_descs [in octalgo.octalgo.fintrees]

---

Constructor Index

A

ABLeaf [in octalgo.octalgo.fintrees]
ABNode [in octalgo.octalgo.fintrees]
Atom [in octalgo.datalogcert.syntax]
A_occ [in octalgo.octalgo.occurrences]

B

Bcons [in octalgo.octalgo.finseqs]
BLeaf [in octalgo.octalgo.fintrees]
Bnil [in octalgo.octalgo.finseqs]
BNode [in octalgo.octalgo.fintrees]

C

C [in octalgo.datalogcert.syntax]
Clause [in octalgo.datalogcert.syntax]

E

Edb [in octalgo.datalogcert.syntax]

G

GAtom [in octalgo.datalogcert.syntax]
GClause [in octalgo.datalogcert.syntax]

I

Idb [in octalgo.datalogcert.syntax]

R

RawAtom [in octalgo.datalogcert.syntax]
RawGAtom [in octalgo.datalogcert.syntax]
RS [in octalgo.octalgo.tSemantics]

T

T_occ [in octalgo.octalgo.occurrences]

V

Val [in octalgo.datalogcert.syntax]
Var [in octalgo.datalogcert.syntax]

W

Wht [in octalgo.octalgo.fintrees]

---

Axiom Index

A

arity [in octalgo.datalogcert.syntax]

B

bn [in octalgo.datalogcert.syntax]

C

constype [in octalgo.datalogcert.syntax]

N

n [in octalgo.datalogcert.syntax]

P

predtype [in octalgo.datalogcert.syntax]

S

symtype [in octalgo.datalogcert.syntax]

---

Projection Index

A

ab_ind [in octalgo.octalgo.occurrences]
ar_ind [in octalgo.octalgo.occurrences]

B

buniq [in octalgo.octalgo.finseqs]
b_ind [in octalgo.octalgo.occurrences]

H

Hwht [in octalgo.octalgo.fintrees]

R

r_ind [in octalgo.octalgo.occurrences]

T

t_ind [in octalgo.octalgo.occurrences]

U

ua [in octalgo.datalogcert.syntax]
uga [in octalgo.datalogcert.syntax]
useq [in octalgo.octalgo.finseqs]

W

wht [in octalgo.octalgo.fintrees]

---

Inductive Index

A

ABtree [in octalgo.octalgo.fintrees]

C

clause [in octalgo.datalogcert.syntax]
constant [in octalgo.datalogcert.syntax]

G

gclause [in octalgo.datalogcert.syntax]

H

Htree [in octalgo.octalgo.fintrees]

P

pred_type [in octalgo.datalogcert.syntax]

R

raw_atom [in octalgo.datalogcert.syntax]
raw_gatom [in octalgo.datalogcert.syntax]
rul_gr [in octalgo.octalgo.tSemantics]

T

term [in octalgo.datalogcert.syntax]

W

Wlist [in octalgo.octalgo.finseqs]

---

Section Index

A

ABtree [in octalgo.octalgo.fintrees]
ABtree.ABtree_utils [in octalgo.octalgo.fintrees]
ABtree.ABtree_countType [in octalgo.octalgo.fintrees]
ABtree.ABtree_eqType [in octalgo.octalgo.fintrees]
ABtree.InducType [in octalgo.octalgo.fintrees]
all_prop [in octalgo.octalgo.utils]
analysis [in octalgo.octalgo.static]
analysis.completeness [in octalgo.octalgo.static]
analysis.rules [in octalgo.octalgo.static]
AtomFinType [in octalgo.datalogcert.syntax]

B

BigCupSeq [in octalgo.third_party.bigop_aux]
BigFOpsFin [in octalgo.third_party.bigop_aux]
BigFOpsSeq [in octalgo.third_party.bigop_aux]
bigop [in octalgo.octalgo.utils]
boolUtils [in octalgo.octalgo.utils]
bSemantics [in octalgo.datalogcert.bSemantics]

C

ClauseInstances [in octalgo.datalogcert.syntax]
Completeness [in octalgo.datalogcert.completeness]

F

finset [in octalgo.octalgo.utils]
Fixpoints [in octalgo.datalogcert.fixpoint]
FSetMonoids [in octalgo.third_party.bigop_aux]

G

GatomFinType [in octalgo.datalogcert.syntax]
Grounding [in octalgo.datalogcert.syntax]

H

HTree [in octalgo.octalgo.fintrees]
HTree.HtreeChoiceType [in octalgo.octalgo.fintrees]
HTree.HtreeCountType [in octalgo.octalgo.fintrees]
HTree.HtreeEqType [in octalgo.octalgo.fintrees]
HTree.HtreeFinType [in octalgo.octalgo.fintrees]
HTree.HtreeUtils [in octalgo.octalgo.fintrees]
HTree.InducType [in octalgo.octalgo.fintrees]

I

Increasing [in octalgo.datalogcert.monotonicity]
Increasing.Overlinear [in octalgo.datalogcert.monotonicity]
iter_mon [in octalgo.datalogcert.fixpoint]

M

Match [in octalgo.datalogcert.pmatch]

N

nat [in octalgo.octalgo.utils]
nat.max [in octalgo.octalgo.utils]
NoDepGrounding [in octalgo.datalogcert.subs]
notin [in octalgo.octalgo.utils]
no_rec_traces [in octalgo.octalgo.norec_sem]

O

occurrences [in octalgo.octalgo.occurrences]
occurrences.a_occ [in octalgo.octalgo.occurrences]
occurrences.prog_occ [in octalgo.octalgo.occurrences]
occurrences.t_occ [in octalgo.octalgo.occurrences]
ord [in octalgo.octalgo.utils]

P

Prod [in octalgo.octalgo.utils]
Projection [in octalgo.octalgo.projection]
Purge [in octalgo.octalgo.purge]

R

RawAtomInstances [in octalgo.datalogcert.syntax]
RawGAtomInstances [in octalgo.datalogcert.syntax]
RuleInstance [in octalgo.octalgo.rinstance]

S

seq [in octalgo.octalgo.utils]
seq.all [in octalgo.octalgo.utils]
seq.find [in octalgo.octalgo.utils]
seq.fold [in octalgo.octalgo.utils]
seq.nth_error [in octalgo.octalgo.utils]
seq.rem [in octalgo.octalgo.utils]
seq.size_map_leq [in octalgo.octalgo.utils]
Soundness [in octalgo.datalogcert.soundness]
Substitutions [in octalgo.datalogcert.subs]

T

Theory [in octalgo.datalogcert.syntax]
Theory.Constants [in octalgo.datalogcert.syntax]
Theory.Variables [in octalgo.datalogcert.syntax]
Transformation [in octalgo.octalgo.extract_static]
tSemantics [in octalgo.octalgo.tSemantics]
tSemantics.rul_gr [in octalgo.octalgo.tSemantics]
tSemantics.trace_sem_trees [in octalgo.octalgo.tSemantics]

U

uniq_seq [in octalgo.octalgo.finseqs]

W

Wlist [in octalgo.octalgo.finseqs]
Wlist.Cancel [in octalgo.octalgo.finseqs]
Wlist.WlistChoiceType [in octalgo.octalgo.finseqs]
Wlist.WlistCountType [in octalgo.octalgo.finseqs]
Wlist.WlistEqType [in octalgo.octalgo.finseqs]
Wlist.WlistFinType [in octalgo.octalgo.finseqs]
Wlist.WlistSubType [in octalgo.octalgo.finseqs]
Wlist.WlistUtils [in octalgo.octalgo.finseqs]
WUtree [in octalgo.octalgo.fintrees]
WUtree.WUtree_utils [in octalgo.octalgo.fintrees]
WUtree.WUtree_subFinType [in octalgo.octalgo.fintrees]
WUtree.WUtree_finType [in octalgo.octalgo.fintrees]

---

Abbreviation Index

A

atom_enc [in octalgo.datalogcert.syntax]

G

gatom_enc [in octalgo.datalogcert.syntax]

I

interp [in octalgo.datalogcert.syntax]
interp_t [in octalgo.octalgo.tSemantics]
iterf_incr [in octalgo.datalogcert.fixpoint]

L

lfp_incr [in octalgo.datalogcert.fixpoint]

M

max_ar [in octalgo.datalogcert.syntax]

T

termRep [in octalgo.datalogcert.syntax]

---

Definition Index

A

ABbranches [in octalgo.octalgo.fintrees]
ABheight [in octalgo.octalgo.fintrees]
ABin [in octalgo.octalgo.fintrees]
ABmap [in octalgo.octalgo.fintrees]
ABnotin [in octalgo.octalgo.fintrees]
ABroot [in octalgo.octalgo.fintrees]
ABtree_to_H [in octalgo.octalgo.fintrees]
ABtree_eqMixin [in octalgo.octalgo.fintrees]
abtree_eq [in octalgo.octalgo.fintrees]
ABuniq [in octalgo.octalgo.fintrees]
ABwidth [in octalgo.octalgo.fintrees]
AB_countMixin [in octalgo.octalgo.fintrees]
AB_choiceMixin [in octalgo.octalgo.fintrees]
AB_to_gen [in octalgo.octalgo.fintrees]
add [in octalgo.datalogcert.subs]
all_prop [in octalgo.octalgo.utils]
all_dom [in octalgo.datalogcert.subs]
analysis [in octalgo.octalgo.extract_static]
analyze_var [in octalgo.octalgo.static]
analyze_var_prev [in octalgo.octalgo.static]
aocc_countprod [in octalgo.octalgo.occurrences]
arg_wf_atom [in octalgo.datalogcert.syntax]
arg_atom [in octalgo.datalogcert.syntax]
arg_wf_gatom [in octalgo.datalogcert.syntax]
arg_gatom [in octalgo.datalogcert.syntax]
atoms_prog [in octalgo.datalogcert.syntax]
atoms_cl [in octalgo.datalogcert.syntax]
atom_occ [in octalgo.octalgo.occurrences]
atom_gr [in octalgo.datalogcert.subs]
atom_clone [in octalgo.octalgo.projection]
atom_vars [in octalgo.datalogcert.syntax]
atom_fenc [in octalgo.datalogcert.syntax]
attach_cl_nb [in octalgo.octalgo.occurrences]
at_at [in octalgo.octalgo.occurrences]
a_occ_finMixin [in octalgo.octalgo.occurrences]
a_occ_countMixin [in octalgo.octalgo.occurrences]
a_occ_choiceMixin [in octalgo.octalgo.occurrences]
a_occ_eqMixin [in octalgo.octalgo.occurrences]
a_occ_pre [in octalgo.octalgo.occurrences]
a_occ_rep [in octalgo.octalgo.occurrences]

B

base_sem_t [in octalgo.octalgo.tSemantics]
bigcup_cart [in octalgo.octalgo.static]
bigcup_tup [in octalgo.octalgo.static]
bindS [in octalgo.datalogcert.pmatch]
bmatch [in octalgo.datalogcert.pmatch]
body_cl [in octalgo.datalogcert.syntax]
body_gcl [in octalgo.datalogcert.syntax]
bp [in octalgo.datalogcert.completeness]
branch_t_ind [in octalgo.octalgo.norec_sem]
branch_pred [in octalgo.octalgo.norec_sem]
br_adequate [in octalgo.octalgo.norec_sem]

C

clauses_var_intersect [in octalgo.datalogcert.syntax]
clause_pre [in octalgo.datalogcert.syntax]
clause_rep [in octalgo.datalogcert.syntax]
cl_clone [in octalgo.octalgo.projection]
cl_true [in octalgo.datalogcert.syntax]
cl_vars [in octalgo.datalogcert.syntax]
const_cl [in octalgo.datalogcert.syntax]
const_tail [in octalgo.datalogcert.syntax]
const_atom [in octalgo.datalogcert.syntax]
const_term [in octalgo.datalogcert.syntax]
cons_clause_t [in octalgo.octalgo.tSemantics]
cons_clause [in octalgo.datalogcert.bSemantics]
c_to_gen [in octalgo.octalgo.projection]

D

dbranch [in octalgo.octalgo.norec_sem]
ded [in octalgo.octalgo.tSemantics]
ded_sub_equal [in octalgo.octalgo.tSemantics]
dep_iota [in octalgo.octalgo.utils]
dom [in octalgo.datalogcert.subs]

E

emptysub [in octalgo.datalogcert.subs]
eqbind_class [in octalgo.datalogcert.subs]
equip [in octalgo.octalgo.utils]
extract_vals_sub [in octalgo.octalgo.extract_static]
extract_vals [in octalgo.octalgo.extract_static]
extract_vals_disj [in octalgo.octalgo.extract_static]
extract_vals_conj [in octalgo.octalgo.extract_static]
extract_vals_br [in octalgo.octalgo.extract_static]
extract_subs_spec [in octalgo.octalgo.extract_static]
extract_sub_ga [in octalgo.octalgo.projection]
extract_sub_seq_c [in octalgo.octalgo.projection]

F

f [in octalgo.octalgo.finseqs]
fenc_atom [in octalgo.datalogcert.syntax]
fenc_gatom [in octalgo.datalogcert.syntax]
ff [in octalgo.octalgo.finseqs]
ffl [in octalgo.octalgo.fintrees]
ffl_aux [in octalgo.octalgo.fintrees]
ffp [in octalgo.octalgo.rinstance]
fl [in octalgo.octalgo.fintrees]
fl_aux [in octalgo.octalgo.fintrees]
foldS [in octalgo.datalogcert.pmatch]
fwd_chain_t [in octalgo.octalgo.tSemantics]
fwd_chain [in octalgo.datalogcert.bSemantics]

G

g [in octalgo.octalgo.finseqs]
gatom_clone [in octalgo.octalgo.projection]
gatom_fenc [in octalgo.datalogcert.syntax]
gclause_pre [in octalgo.datalogcert.syntax]
gclause_rep [in octalgo.datalogcert.syntax]
gclause_eqMixin [in octalgo.datalogcert.syntax]
gclause_eq [in octalgo.datalogcert.syntax]
gcl_true [in octalgo.datalogcert.syntax]
gen_cart_prod [in octalgo.octalgo.utils]
gen_c_f_c [in octalgo.octalgo.projection]
gen_f_c [in octalgo.octalgo.projection]
gen_vars_c_f [in octalgo.octalgo.projection]
gen_vars_rem [in octalgo.octalgo.projection]
gen_vars_rem_j [in octalgo.octalgo.projection]
gen_vars [in octalgo.octalgo.projection]
gen_vars_j [in octalgo.octalgo.projection]
gen_to_AB [in octalgo.octalgo.fintrees]
get_cl_var [in octalgo.octalgo.occurrences]
gg [in octalgo.octalgo.finseqs]
ggl [in octalgo.octalgo.fintrees]
gl [in octalgo.octalgo.fintrees]
gr [in octalgo.datalogcert.syntax]
gr_cl_def [in octalgo.datalogcert.subs]
gr_atom_def [in octalgo.datalogcert.subs]
gr_raw_atom_def [in octalgo.datalogcert.subs]
gr_term_def [in octalgo.datalogcert.subs]
gr_cl [in octalgo.datalogcert.syntax]
gr_tl [in octalgo.datalogcert.syntax]
gr_atom [in octalgo.datalogcert.syntax]
gr_atom_proof [in octalgo.datalogcert.syntax]
gr_raw_atom [in octalgo.datalogcert.syntax]
gr_term [in octalgo.datalogcert.syntax]

H

head_cl [in octalgo.datalogcert.syntax]
head_gcl [in octalgo.datalogcert.syntax]
hsym_prog [in octalgo.datalogcert.syntax]
hsym_cl [in octalgo.datalogcert.syntax]
htreen_finType [in octalgo.octalgo.fintrees]
htreen_finMixin [in octalgo.octalgo.fintrees]
htreen_countType [in octalgo.octalgo.fintrees]
htreen_countMixin [in octalgo.octalgo.fintrees]
htreen_choiceType [in octalgo.octalgo.fintrees]
htreen_choiceMixin [in octalgo.octalgo.fintrees]
htreen_eqType [in octalgo.octalgo.fintrees]
htreen_eqMixin [in octalgo.octalgo.fintrees]
htree0_finType [in octalgo.octalgo.fintrees]
htree0_finMixin [in octalgo.octalgo.fintrees]
htree0_countType [in octalgo.octalgo.fintrees]
htree0_countMixin [in octalgo.octalgo.fintrees]
htree0_choiceType [in octalgo.octalgo.fintrees]
htree0_choiceMixin [in octalgo.octalgo.fintrees]
htree0_eqType [in octalgo.octalgo.fintrees]
htree0_eqMixin [in octalgo.octalgo.fintrees]
Huniq [in octalgo.octalgo.fintrees]
h_to_wu_tree [in octalgo.octalgo.fintrees]
h_to_ab_tree [in octalgo.octalgo.fintrees]

I

increasing [in octalgo.datalogcert.fixpoint]
ind_vals [in octalgo.octalgo.projection]
ind_terms [in octalgo.octalgo.projection]
inE_bis [in octalgo.datalogcert.subs]
inst_rule [in octalgo.octalgo.rinstance]
is_clone_ga [in octalgo.octalgo.projection]
is_clone_pred [in octalgo.octalgo.projection]
is_var [in octalgo.datalogcert.syntax]
iterf [in octalgo.datalogcert.fixpoint]

K

keep_rule [in octalgo.octalgo.purge]
keep_atom [in octalgo.octalgo.purge]

M

match_body [in octalgo.datalogcert.pmatch]
match_atom_all [in octalgo.datalogcert.pmatch]
match_atom [in octalgo.datalogcert.pmatch]
match_raw_atom [in octalgo.datalogcert.pmatch]
match_term [in octalgo.datalogcert.pmatch]
match_pbody [in octalgo.datalogcert.soundness]
mem_binding [in octalgo.datalogcert.subs]
mem_free [in octalgo.datalogcert.subs]
mem_bound [in octalgo.datalogcert.subs]
monotone [in octalgo.datalogcert.fixpoint]
my_tst_sub [in octalgo.octalgo.tSemantics]

N

nth_error [in octalgo.octalgo.utils]
nth_cons_rew_dep [in octalgo.datalogcert.syntax]
nth_term [in octalgo.datalogcert.syntax]
nth_cons [in octalgo.datalogcert.syntax]

O

occ [in octalgo.octalgo.occurrences]
occsInAtom [in octalgo.octalgo.occurrences]
occsInAtomList [in octalgo.octalgo.occurrences]
occsInProgram [in octalgo.octalgo.occurrences]
occsInRule [in octalgo.octalgo.occurrences]
occsInTermList [in octalgo.octalgo.occurrences]
of_constant [in octalgo.datalogcert.syntax]
only_variables_in_heads [in octalgo.datalogcert.syntax]
only_variables_head [in octalgo.datalogcert.syntax]
only_variables_atom [in octalgo.datalogcert.syntax]
ord_shift [in octalgo.octalgo.utils]

P

pimset [in octalgo.octalgo.utils]
pp [in octalgo.octalgo.purge]
pred_type_eqMixin [in octalgo.datalogcert.syntax]
pred_type_eq [in octalgo.datalogcert.syntax]
program [in octalgo.datalogcert.syntax]
prog_true [in octalgo.datalogcert.syntax]
prog_safe_hds [in octalgo.datalogcert.syntax]
prog_safe [in octalgo.datalogcert.syntax]
proj_prog [in octalgo.octalgo.projection]
pset [in octalgo.octalgo.utils]
pucons [in octalgo.octalgo.finseqs]
p_at [in octalgo.octalgo.occurrences]

R

raw_gen_f_c [in octalgo.octalgo.projection]
raw_gen_c_f [in octalgo.octalgo.projection]
raw_gatom_clone [in octalgo.octalgo.projection]
raw_atom_clone [in octalgo.octalgo.projection]
raw_atom_vars [in octalgo.datalogcert.syntax]
raw_atom_pre [in octalgo.datalogcert.syntax]
raw_atom_rep [in octalgo.datalogcert.syntax]
raw_gatom_pre [in octalgo.datalogcert.syntax]
raw_gatom_rep [in octalgo.datalogcert.syntax]
rul_gr_finMixin [in octalgo.octalgo.tSemantics]
rul_gr_countMixin [in octalgo.octalgo.tSemantics]
rul_gr_choiceMixin [in octalgo.octalgo.tSemantics]
rul_gr_eqMixin [in octalgo.octalgo.tSemantics]
rul_gr_pre [in octalgo.octalgo.tSemantics]
rul_gr_rep [in octalgo.octalgo.tSemantics]

S

safe_edb [in octalgo.datalogcert.syntax]
safe_cl_hd [in octalgo.datalogcert.syntax]
safe_cl [in octalgo.datalogcert.syntax]
satom [in octalgo.datalogcert.subs]
scl [in octalgo.datalogcert.subs]
sem [in octalgo.datalogcert.bSemantics]
sem_t [in octalgo.octalgo.tSemantics]
sem_tree_to_inter [in octalgo.octalgo.tSemantics]
seq_to_wlist_uncut [in octalgo.octalgo.finseqs]
seq_to_wlist [in octalgo.octalgo.finseqs]
shift [in octalgo.octalgo.utils]
shift1 [in octalgo.octalgo.occurrences]
sraw_atom [in octalgo.datalogcert.subs]
sremove [in octalgo.octalgo.utils]
stail [in octalgo.datalogcert.subs]
sterm [in octalgo.datalogcert.subs]
strict_subtree [in octalgo.octalgo.fintrees]
stv [in octalgo.octalgo.rinstance]
sub [in octalgo.datalogcert.subs]
subtree [in octalgo.octalgo.fintrees]
subU [in octalgo.datalogcert.subs]
sub_filter [in octalgo.datalogcert.subs]
sub_st [in octalgo.datalogcert.subs]
sym_tl [in octalgo.datalogcert.soundness]
sym_prog [in octalgo.datalogcert.syntax]
sym_cl [in octalgo.datalogcert.syntax]
sym_atom [in octalgo.datalogcert.syntax]
sym_i [in octalgo.datalogcert.syntax]
sym_gatom [in octalgo.datalogcert.syntax]

T

tag_of_uniq_seq [in octalgo.octalgo.finseqs]
tail [in octalgo.datalogcert.syntax]
tail_gr [in octalgo.datalogcert.subs]
tail_clone [in octalgo.octalgo.projection]
tail_vars [in octalgo.datalogcert.syntax]
term_to_var [in octalgo.octalgo.occurrences]
term_vars [in octalgo.datalogcert.syntax]
term_con [in octalgo.datalogcert.syntax]
term_rep [in octalgo.datalogcert.syntax]
term_of_cons [in octalgo.datalogcert.syntax]
tocc_countprod [in octalgo.octalgo.occurrences]
tocs [in octalgo.octalgo.occurrences]
to_sub [in octalgo.datalogcert.subs]
to_gr [in octalgo.datalogcert.subs]
to_tail [in octalgo.datalogcert.subs]
to_atom [in octalgo.datalogcert.syntax]
to_raw_atom [in octalgo.datalogcert.syntax]
tprog [in octalgo.octalgo.rinstance]
trace_sem_trees [in octalgo.octalgo.tSemantics]
tst_node_head [in octalgo.octalgo.tSemantics]
tuple_to_wlist [in octalgo.octalgo.finseqs]
t_at [in octalgo.octalgo.occurrences]
t_occ_finMixin [in octalgo.octalgo.occurrences]
t_occ_countMixin [in octalgo.octalgo.occurrences]
t_occ_choiceMixin [in octalgo.octalgo.occurrences]
t_occ_eqMixin [in octalgo.octalgo.occurrences]
t_occ_pre [in octalgo.octalgo.occurrences]
t_occ_rep [in octalgo.octalgo.occurrences]

U

ubound [in octalgo.datalogcert.fixpoint]
ucons [in octalgo.octalgo.finseqs]
ucons1 [in octalgo.octalgo.finseqs]
unil [in octalgo.octalgo.finseqs]
uniq_seq_finMixin [in octalgo.octalgo.finseqs]
uniq_seq_of_tag [in octalgo.octalgo.finseqs]
unrec_trace [in octalgo.octalgo.norec_sem]
unrec_trace_gen [in octalgo.octalgo.norec_sem]
useq_hd [in octalgo.octalgo.finseqs]
useq_behead [in octalgo.octalgo.finseqs]

V

vars_not_shared [in octalgo.datalogcert.syntax]

W

wall [in octalgo.octalgo.finseqs]
wapp [in octalgo.octalgo.finseqs]
wf_atom [in octalgo.datalogcert.syntax]
wf_gatom [in octalgo.datalogcert.syntax]
wlistn_finType [in octalgo.octalgo.finseqs]
wlistn_finMixin [in octalgo.octalgo.finseqs]
wlistn_countType [in octalgo.octalgo.finseqs]
wlistn_countMixin [in octalgo.octalgo.finseqs]
wlistn_choiceType [in octalgo.octalgo.finseqs]
wlistn_choiceMixin [in octalgo.octalgo.finseqs]
wlistn_eqType [in octalgo.octalgo.finseqs]
wlistn_eqMixin [in octalgo.octalgo.finseqs]
wlist_subType [in octalgo.octalgo.finseqs]
wlist_to_seq [in octalgo.octalgo.finseqs]
wlist0_finType [in octalgo.octalgo.finseqs]
wlist0_finMixin [in octalgo.octalgo.finseqs]
wlist0_countType [in octalgo.octalgo.finseqs]
wlist0_countMixin [in octalgo.octalgo.finseqs]
wlist0_choiceType [in octalgo.octalgo.finseqs]
wlist0_choiceMixin [in octalgo.octalgo.finseqs]
wlist0_eqType [in octalgo.octalgo.finseqs]
wlist0_eqMixin [in octalgo.octalgo.finseqs]
wmap [in octalgo.octalgo.finseqs]
wsize [in octalgo.octalgo.finseqs]
WUnotin [in octalgo.octalgo.fintrees]
wutree_option_fsfType [in octalgo.octalgo.fintrees]
wutree_option_finType [in octalgo.octalgo.fintrees]
wutree_finMixin [in octalgo.octalgo.fintrees]
wutree_subcountMixin [in octalgo.octalgo.fintrees]
wutree_countMixin [in octalgo.octalgo.fintrees]
wutree_choiceMixin [in octalgo.octalgo.fintrees]
wutree_eqMixin [in octalgo.octalgo.fintrees]
wutree_subType [in octalgo.octalgo.fintrees]
WUtree_to_H [in octalgo.octalgo.fintrees]
wu_map [in octalgo.octalgo.fintrees]
wu_pcons_tup [in octalgo.octalgo.fintrees]
wu_pcons_seq [in octalgo.octalgo.fintrees]
wu_pcons_wlist [in octalgo.octalgo.fintrees]
wu_cons_wlist [in octalgo.octalgo.fintrees]
wu_cons [in octalgo.octalgo.fintrees]
wu_leaf [in octalgo.octalgo.fintrees]
WU_fsf [in octalgo.octalgo.fintrees]
WU_sf_sub [in octalgo.octalgo.fintrees]
wu_tree_of_htree [in octalgo.octalgo.fintrees]
wu_merge [in octalgo.octalgo.fintrees]
wu_pred [in octalgo.octalgo.fintrees]
w_all_prop [in octalgo.octalgo.finseqs]
w_subtype [in octalgo.octalgo.finseqs]

---

Record Index

A

atom [in octalgo.datalogcert.syntax]
a_occ [in octalgo.octalgo.occurrences]

G

gatom [in octalgo.datalogcert.syntax]

T

t_occ [in octalgo.octalgo.occurrences]

U

uniq_seq [in octalgo.octalgo.finseqs]

W

WUtree [in octalgo.octalgo.fintrees]

---

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

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

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

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

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

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

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

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

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

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

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

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

(6 entries)

---

This page has been generated by coqdoc