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

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

(14 entries)

Module Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

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

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

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

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

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

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

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

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

(9 entries)

Instance Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

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

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

(3 entries)

---

Global Index

A

add_A_build_kt_comm [lemma, in Vct.Mcnf.Mcnf]
add_cs_build_kt_comm [lemma, in Vct.Mcnf.Mcnf]
add_cs_nA_eq [lemma, in Vct.Mcnf.Mcnf]
add_nA [definition, in Vct.Mcnf.Mcnf]
add_A [definition, in Vct.Mcnf.Mcnf]
add_cs [definition, in Vct.Mcnf.Mcnf]
add_conflict_set [definition, in Vct.CplSolver]
add_no_new_atms [lemma, in Vct.CplSolver]
add_clause_incl_A [lemma, in Vct.CplSolver]
add_clause_incl [lemma, in Vct.CplSolver]
add_clause_cons [axiom, in Vct.CplSolver]
add_clause [axiom, in Vct.CplSolver]
agree [definition, in Vct.Nnf]
agree [definition, in Vct.Mcnf.Mcnf]
agree [definition, in Vct.Lclauses]
agree [definition, in Vct.Lit]
agree [definition, in Vct.CplClause]
agree [definition, in Vct.DiaClause]
agree [definition, in Vct.BoxClause]
agree_r [lemma, in Vct.Nnf]
agree_l [lemma, in Vct.Nnf]
agree_cons [lemma, in Vct.Mcnf.Mcnf]
AllValuations [section, in Vct.Valuation]
And [constructor, in Vct.Nnf]
And [constructor, in Vct.Fml]
And [constructor, in Vct.Nnfl]
and_sat [lemma, in Vct.Mcnf.Conversion]
and_true_r [lemma, in Vct.ImportStd]
and_true_l [lemma, in Vct.ImportStd]
Assumptions [library]
as_lit2_none [lemma, in Vct.Nnf]
as_lit2_some_inv [lemma, in Vct.Nnf]
as_lit2 [definition, in Vct.Nnf]
as_lit_none [lemma, in Vct.Nnf]
as_lit_some_inv [lemma, in Vct.Nnf]
as_lit [definition, in Vct.Nnf]
as_kt [definition, in Vct.Tree]
as_k [definition, in Vct.Tree]
atm [definition, in Vct.Lit]
atms_of [definition, in Vct.Cnf]
atms_in_ev_atms [lemma, in Vct.Valuation]
atms_of_nodup [lemma, in Vct.CplSolver]
atms_of [definition, in Vct.CplSolver]
atm_le_max [lemma, in Vct.Nnf]
atm_in_nnf_atm [lemma, in Vct.Nnf]
atm_in [definition, in Vct.Nnf]
atm_le_max [lemma, in Vct.Mcnf.Mcnf]
atm_in_cons [lemma, in Vct.Mcnf.Mcnf]
atm_in_nil [lemma, in Vct.Mcnf.Mcnf]
atm_in [definition, in Vct.Mcnf.Mcnf]
atm_in_cons [lemma, in Vct.Cnf]
atm_in_exists [lemma, in Vct.Cnf]
atm_in [definition, in Vct.Cnf]
atm_in_destruct [lemma, in Vct.Lclauses]
atm_in_cpls [lemma, in Vct.Lclauses]
atm_le_max [lemma, in Vct.Lclauses]
atm_in [definition, in Vct.Lclauses]
atm_in [definition, in Vct.Lit]
atm_le_max [lemma, in Vct.CplClause]
atm_in_cons [lemma, in Vct.CplClause]
atm_in_nil [lemma, in Vct.CplClause]
atm_in_exists [lemma, in Vct.CplClause]
atm_in [definition, in Vct.CplClause]
atm_le_max [lemma, in Vct.DiaClause]
atm_in [definition, in Vct.DiaClause]
atm_in [definition, in Vct.CplSolver]
atm_in [definition, in Vct.Assumptions]
atm_le_max [lemma, in Vct.BoxClause]
atm_in [definition, in Vct.BoxClause]
Atom [library]
atom_is_pos [lemma, in Vct.Atom]

B

bind_new_atm_unique [lemma, in Vct.Valuation]
Box [constructor, in Vct.Nnf]
Box [constructor, in Vct.Fml]
Box [constructor, in Vct.Nnfl]
BoxClause [library]
boxes [projection, in Vct.Lclauses]
box_culprits [definition, in Vct.Solver.McnfExt]
box_sat [lemma, in Vct.Mcnf.Conversion]
build_kt_sound_complete [lemma, in Vct.Mcnf.Mcnf]
build_kt_complete [lemma, in Vct.Mcnf.Mcnf]
build_kt_sound [lemma, in Vct.Mcnf.Mcnf]
build_kt_refl_iff [lemma, in Vct.Mcnf.Mcnf]
build_kt_box_cl_in_cpls [lemma, in Vct.Mcnf.Mcnf]
build_kt [definition, in Vct.Mcnf.Mcnf]

C

Cache [module, in Vct.Solver.Cached]
Cache [module, in Vct.Solver.FiredBoxes]
Cached [library]
cached_solve_fml_sound_complete [lemma, in Vct.Solver]
Caches [module, in Vct.Solver.Cached]
Caches [module, in Vct.Solver.FiredBoxes]
Caches.add [definition, in Vct.Solver.Cached]
Caches.add_contains_iff [lemma, in Vct.Solver.Cached]
Caches.contains [definition, in Vct.Solver.Cached]
Caches.destruct [definition, in Vct.Solver.Cached]
Caches.t [definition, in Vct.Solver.Cached]
Cct [library]
cct_sound [lemma, in Vct.Solver.Soundness]
cct_core_incl_A [lemma, in Vct.Solver.Soundness]
ClauseOrd1 [module, in Vct.Mcnf.Simplification]
ClauseOrd1.leb [definition, in Vct.Mcnf.Simplification]
ClauseOrd1.leb_total [lemma, in Vct.Mcnf.Simplification]
ClauseOrd1.t [definition, in Vct.Mcnf.Simplification]
ClauseOrd2 [module, in Vct.Mcnf.Simplification]
ClauseOrd2.leb [definition, in Vct.Mcnf.Simplification]
ClauseOrd2.leb_total [lemma, in Vct.Mcnf.Simplification]
ClauseOrd2.t [definition, in Vct.Mcnf.Simplification]
ClauseSort1 [module, in Vct.Mcnf.Simplification]
ClauseSort2 [module, in Vct.Mcnf.Simplification]
clauses_of_make_with_clauses [lemma, in Vct.CplSolver]
clauses_of_fold_right [lemma, in Vct.CplSolver]
clauses_of [axiom, in Vct.CplSolver]
clause_atms_incl [definition, in Vct.CplSolver]
Cnf [library]
cnf_unsat_subset [lemma, in Vct.Solver.Soundness]
compare [definition, in Vct.Lit]
Compare [module, in Vct.Atom]
compare [definition, in Vct.Atom]
CompareFacts [module, in Vct.Atom]
compare_spec [lemma, in Vct.Lit]
compare_gt_iff [definition, in Vct.Atom]
compare_lt_iff [definition, in Vct.Atom]
compare_eq_iff [definition, in Vct.Atom]
compare_refl [definition, in Vct.Atom]
compare_spec [lemma, in Vct.Atom]
Compare.compare [definition, in Vct.Atom]
Compare.compare_spec [definition, in Vct.Atom]
Compare.eq [definition, in Vct.Atom]
Compare.eq_dec [definition, in Vct.Atom]
Compare.eq_equiv [definition, in Vct.Atom]
Compare.le [definition, in Vct.Atom]
Compare.le_lteq [definition, in Vct.Atom]
Compare.lt [definition, in Vct.Atom]
Compare.lt_compat [definition, in Vct.Atom]
Compare.lt_strorder [definition, in Vct.Atom]
Compare.t [definition, in Vct.Atom]
Completeness [library]
cons_NoDupA [lemma, in Vct.ListExt]
cons_child [definition, in Vct.Tree]
Conversion [section, in Vct.Nnf]
Conversion [library]
conv_atm_range [lemma, in Vct.Mcnf.Conversion]
core_subset_assumptions [axiom, in Vct.CplSolver]
Correctness [section, in Vct.Nnf]
CplClause [library]
cpls [projection, in Vct.Lclauses]
CplSolution [library]
CplSolver [library]
cplsolver_mcnf [definition, in Vct.Solver.McnfExt]
cpls_of_add_assumptions [lemma, in Vct.Solver.Soundness]
cpl_solve [definition, in Vct.Solver.McnfExt]
cpl_from_lclauses [definition, in Vct.Solver.McnfExt]
cpl_forceb_sat [lemma, in Vct.Cnf]
cpl_forceb [definition, in Vct.Cnf]
cpl_forceb [definition, in Vct.Lit]
cpl_forceb [definition, in Vct.CplClause]
cs_incl_V [lemma, in Vct.Solver.McnfExt]
cs_preserve_sat [lemma, in Vct.Solver.Cached]

D

decreasing_sat_vals [lemma, in Vct.Solver.SearchBasics]
Dia [constructor, in Vct.Nnf]
Dia [constructor, in Vct.Fml]
Dia [constructor, in Vct.Nnfl]
DiaClause [library]
dias [projection, in Vct.Lclauses]
dia_sat [lemma, in Vct.Mcnf.Conversion]

E

empty [definition, in Vct.Lclauses]
empty [definition, in Vct.Tree]
eq [definition, in Vct.Valuation]
eq [definition, in Vct.Atom]
eqb [definition, in Vct.Lit]
eqb [definition, in Vct.Atom]
eqb_equiv [instance, in Vct.Lit]
eqb_eq [lemma, in Vct.Lit]
eqb_equiv [instance, in Vct.Atom]
eqb_trans [instance, in Vct.Atom]
eqb_sym [instance, in Vct.Atom]
eqb_refl [instance, in Vct.Atom]
eqb_neq [lemma, in Vct.Atom]
eqb_eq [lemma, in Vct.Atom]
EquisatModel [section, in Vct.Mcnf.Conversion]
EquisatModelRange [section, in Vct.Mcnf.Conversion]
equisat_kt_fml [lemma, in Vct.Nnf]
equisat_fml [lemma, in Vct.Nnf]
equisat_kt_nnf [lemma, in Vct.Mcnf.Conversion]
equisat_nnf [lemma, in Vct.Mcnf.Conversion]
equisat_nnf [lemma, in Vct.Nnfl]
equiv_fml [lemma, in Vct.Nnf]
equiv_nnf [lemma, in Vct.Nnfl]
equiv_nnf_ind [lemma, in Vct.Nnfl]
eq_in [lemma, in Vct.Valuation]
eq_nodup [lemma, in Vct.Valuation]
eq_equivalence [instance, in Vct.Valuation]
eq_atm_equivalence [instance, in Vct.Lit]
eq_atm_trans [instance, in Vct.Lit]
eq_atm_sym [instance, in Vct.Lit]
eq_atm_refl [instance, in Vct.Lit]
eq_atm [definition, in Vct.Lit]
eq_dec [lemma, in Vct.Lit]
eq_true [lemma, in Vct.ImportStd]
eq_Z_inj [lemma, in Vct.Atom]
eq_dec [lemma, in Vct.Atom]
eq_equiv [instance, in Vct.Atom]
every_valuation_unique [lemma, in Vct.Valuation]
every_valuation_perm [lemma, in Vct.Valuation]
every_valuation_nodup [lemma, in Vct.Valuation]
every_valuation_exact_atms [lemma, in Vct.Valuation]
every_valuation_of_atms [definition, in Vct.Valuation]
every_sat_valuation_nodup [lemma, in Vct.CplSolver]
every_valuation_nodup [lemma, in Vct.CplSolver]
every_sat_valuation [definition, in Vct.CplSolver]
every_valuation [definition, in Vct.CplSolver]
Exists_singleton [lemma, in Vct.ListExt]
Extract [library]
ex_eqA_iff_inA [lemma, in Vct.ListExt]

F

FiredBoxes [library]
fired_boxes [definition, in Vct.Solver.McnfExt]
fired_boxes_solve_fml_sound_complete [lemma, in Vct.Solver]
Fml [library]
Forall_singleton [lemma, in Vct.ListExt]
forall_and_distrib [lemma, in Vct.Nnfl]
force [definition, in Vct.Nnf]
force [definition, in Vct.Mcnf.Mcnf]
force [definition, in Vct.Fml]
force [definition, in Vct.Cnf]
force [definition, in Vct.Lclauses]
force [definition, in Vct.Lit]
force [definition, in Vct.CplClause]
force [definition, in Vct.DiaClause]
force [definition, in Vct.BoxClause]
force [inductive, in Vct.Nnfl]
forceb_app [lemma, in Vct.Cnf]
forceb_cons [lemma, in Vct.Cnf]
forceb_nil [lemma, in Vct.Cnf]
forceb_forall [lemma, in Vct.Cnf]
forceb_exists [lemma, in Vct.CplClause]
forceb_cons [lemma, in Vct.CplClause]
forceb_nil [lemma, in Vct.CplClause]
ForceIff [section, in Vct.Nnfl]
ForceIff.M [variable, in Vct.Nnfl]
ForceIff.R [variable, in Vct.Nnfl]
ForceIff.W [variable, in Vct.Nnfl]
ForceIff.w0 [variable, in Vct.Nnfl]
forces_atm_iff_in [lemma, in Vct.Valuation]
forces_atm [definition, in Vct.Valuation]
force_negate_iff_not_force [lemma, in Vct.Nnf]
force_add_no_assumptions [lemma, in Vct.Solver.McnfExt]
force_app_and [lemma, in Vct.Solver.McnfExt]
force_rm_assumptions [lemma, in Vct.Solver.McnfExt]
force_ctx_first_next [lemma, in Vct.Solver.McnfExt]
force_assumptions_comm [lemma, in Vct.Solver.McnfExt]
force_refl_closure [lemma, in Vct.Mcnf.Mcnf]
force_build_kt_next [lemma, in Vct.Mcnf.Mcnf]
force_kt_build_kt_next [lemma, in Vct.Mcnf.Mcnf]
force_fst_mc [lemma, in Vct.Mcnf.Mcnf]
force_zip_merge_and [lemma, in Vct.Mcnf.Mcnf]
force_pos_cs_jump [lemma, in Vct.Solver.Soundness]
force_not_A_neg_A [lemma, in Vct.Solver.Soundness]
force_new_cpls [lemma, in Vct.Solver.Soundness]
force_fst_cpls [lemma, in Vct.Solver.Soundness]
force_local [lemma, in Vct.Cnf]
force_singleton [lemma, in Vct.Cnf]
force_from_assumptions [lemma, in Vct.Cnf]
force_map [lemma, in Vct.Cnf]
force_app [lemma, in Vct.Cnf]
force_cons [lemma, in Vct.Cnf]
force_nil [lemma, in Vct.Cnf]
force_cpl_forceb [lemma, in Vct.Cnf]
force_forall [lemma, in Vct.Cnf]
force_merge_app_sym [lemma, in Vct.Lclauses]
force_app_sym [lemma, in Vct.Lclauses]
force_destruct_forall [lemma, in Vct.Lclauses]
force_destruct [lemma, in Vct.Lclauses]
force_cpls [lemma, in Vct.Lclauses]
force_empty [lemma, in Vct.Lclauses]
force_cpls_cons [lemma, in Vct.Lclauses]
force_cpls_app [lemma, in Vct.Lclauses]
force_merge_and [lemma, in Vct.Lclauses]
force_local [lemma, in Vct.Lit]
force_cpl_forceb [lemma, in Vct.Lit]
force_local [lemma, in Vct.CplClause]
force_singleton [lemma, in Vct.CplClause]
force_cpl_forceb [lemma, in Vct.CplClause]
force_cons [lemma, in Vct.CplClause]
force_nil [lemma, in Vct.CplClause]
force_exists [lemma, in Vct.CplClause]
force_no_assumptions [lemma, in Vct.Solver.Kt]
force_no_assumptions [lemma, in Vct.Solver.Completeness]
force_dia_iff [lemma, in Vct.Nnfl]
force_box_iff [lemma, in Vct.Nnfl]
force_or_iff [lemma, in Vct.Nnfl]
force_and_iff [lemma, in Vct.Nnfl]
force_lit_iff [lemma, in Vct.Nnfl]
force_sind [definition, in Vct.Nnfl]
force_ind [definition, in Vct.Nnfl]
force_dia [constructor, in Vct.Nnfl]
force_box [constructor, in Vct.Nnfl]
force_or [constructor, in Vct.Nnfl]
force_and [constructor, in Vct.Nnfl]
force_lit [constructor, in Vct.Nnfl]
from_fml [definition, in Vct.Nnf]
from_assumptions [definition, in Vct.Cnf]
from_lit [definition, in Vct.CplClause]
from_nnf [definition, in Vct.Mcnf.Conversion]
from_nnf_with_sur [definition, in Vct.Mcnf.Conversion]
from_n_nnf [definition, in Vct.Mcnf.Conversion]
from_nnf [definition, in Vct.Nnfl]
fst_dias [definition, in Vct.Mcnf.Mcnf]
fst_boxes [definition, in Vct.Mcnf.Mcnf]
fst_cpls [definition, in Vct.Mcnf.Mcnf]
fst_mc [definition, in Vct.Mcnf.Mcnf]
fst_mc_destruct [lemma, in Vct.Solver.Soundness]

G

gather_or [definition, in Vct.Nnfl]
gather_and [definition, in Vct.Nnfl]
get_pos [definition, in Vct.Lit]
get_fired_boxes [definition, in Vct.Solver.FiredBoxes]
get_core [definition, in Vct.Solver.Cct]
group_by [definition, in Vct.Mcnf.Simplification]

I

IH [definition, in Vct.Mcnf.Conversion]
Impl [constructor, in Vct.Fml]
ImportStd [library]
imp_true_l_forall [lemma, in Vct.ImportStd]
imp_true_l [lemma, in Vct.ImportStd]
imp_true_r [lemma, in Vct.ImportStd]
imp_false_r [lemma, in Vct.ImportStd]
InA_length_2 [lemma, in Vct.ListExt]
InA_concat [lemma, in Vct.ListExt]
InA_flat_map [lemma, in Vct.ListExt]
inclA_nil [lemma, in Vct.ListExt]
inclA_cons [lemma, in Vct.ListExt]
incl_middle [lemma, in Vct.ListExt]
incl_A_sat [lemma, in Vct.Solver.McnfExt]
incl_A_force [lemma, in Vct.Solver.McnfExt]
incl_cpls_force [lemma, in Vct.Solver.McnfExt]
incl_unsat [lemma, in Vct.Cnf]
incl_force [lemma, in Vct.Cnf]
Inj_atom_Z [instance, in Vct.Atom]
inline_pair_lemma [lemma, in Vct.Tactics]
In_nil_iff [lemma, in Vct.ListExt]
In_singleton [lemma, in Vct.ListExt]
in_zip_merge_or [lemma, in Vct.Mcnf.Mcnf]
in_atms_of [lemma, in Vct.Cnf]
in_merge_or [lemma, in Vct.Lclauses]
is_prefix [definition, in Vct.ListExt]
is_unsat [definition, in Vct.CplSolution]
is_sat [definition, in Vct.CplSolution]
is_sat_spec [lemma, in Vct.Solver.NoWit]

J

JumpRestart [constructor, in Vct.Solver.Cct]
JumpRestartCond [constructor, in Vct.Solver.Cct]
JumpSolution [module, in Vct.Solver.Cached]
JumpSolution [module, in Vct.Solver.TailRec]
JumpSolution [module, in Vct.Solver.FiredBoxes]
JumpSolution [module, in Vct.Solver.Kt]
JumpSolution [module, in Vct.Solver.NoWit]
JumpSolution [module, in Vct.Solver.Spec]
JumpSolution.from_spec [definition, in Vct.Solver.NoWit]
JumpSolution.get_caches_unsat [lemma, in Vct.Solver.Cached]
JumpSolution.get_caches_sat [lemma, in Vct.Solver.Cached]
JumpSolution.get_caches [definition, in Vct.Solver.Cached]
JumpSolution.Sat [constructor, in Vct.Solver.Cached]
JumpSolution.Sat [constructor, in Vct.Solver.NoWit]
JumpSolution.Sat [constructor, in Vct.Solver.Spec]
JumpSolution.t [inductive, in Vct.Solver.Cached]
JumpSolution.t [inductive, in Vct.Solver.NoWit]
JumpSolution.t [inductive, in Vct.Solver.Spec]
JumpSolution.t_sind [definition, in Vct.Solver.Cached]
JumpSolution.t_rec [definition, in Vct.Solver.Cached]
JumpSolution.t_ind [definition, in Vct.Solver.Cached]
JumpSolution.t_rect [definition, in Vct.Solver.Cached]
JumpSolution.t_sind [definition, in Vct.Solver.NoWit]
JumpSolution.t_rec [definition, in Vct.Solver.NoWit]
JumpSolution.t_ind [definition, in Vct.Solver.NoWit]
JumpSolution.t_rect [definition, in Vct.Solver.NoWit]
JumpSolution.t_sind [definition, in Vct.Solver.Spec]
JumpSolution.t_rec [definition, in Vct.Solver.Spec]
JumpSolution.t_ind [definition, in Vct.Solver.Spec]
JumpSolution.t_rect [definition, in Vct.Solver.Spec]
JumpSolution.Unsat [constructor, in Vct.Solver.Cached]
JumpSolution.Unsat [constructor, in Vct.Solver.NoWit]
JumpSolution.Unsat [constructor, in Vct.Solver.Spec]
JumpSolution.without_caches [definition, in Vct.Solver.Cached]
jump_cct_core [lemma, in Vct.Solver.Soundness]
jump_failed_dia [lemma, in Vct.Solver.Soundness]
jump_c_forced [lemma, in Vct.Solver.Cached]
jump_cct_core [lemma, in Vct.Solver.Kt]
jump_failed_dia [lemma, in Vct.Solver.Kt]
jump_c_forced [lemma, in Vct.Solver.Kt]
jump_c_forced [lemma, in Vct.Solver.NoWit]
jump_c_forced [lemma, in Vct.Solver.Spec]

K

Kripke [library]
Kt [library]
kt_force_unboxed [lemma, in Vct.Mcnf.Mcnf]
kt_forces_weak [lemma, in Vct.Solver.Kt]
kt_spec_solve_fml_sound_complete [lemma, in Vct.Solver]

L

Lclauses [library]
le [definition, in Vct.Atom]
leb [definition, in Vct.Lit]
leb [definition, in Vct.Atom]
leb_trans [instance, in Vct.Lit]
leb_total [lemma, in Vct.Lit]
leb_total [lemma, in Vct.Atom]
leb_gt [lemma, in Vct.Atom]
leb_le [lemma, in Vct.Atom]
lexnat2_lt_wf [instance, in Vct.Solver.SearchBasics]
lexnat2_lt [definition, in Vct.Solver.SearchBasics]
le_mapped_list_max [lemma, in Vct.Atom]
le_list_max [lemma, in Vct.Atom]
le_list_max_ind [lemma, in Vct.Atom]
le_max_r [lemma, in Vct.Atom]
le_max_l [lemma, in Vct.Atom]
le_trans [instance, in Vct.Atom]
le_refl [instance, in Vct.Atom]
le_lteq [lemma, in Vct.Atom]
lhs_opt [definition, in Vct.Mcnf.Simplification]
ListExt [library]
list_max [definition, in Vct.Atom]
Lit [constructor, in Vct.Nnf]
Lit [constructor, in Vct.Nnfl]
Lit [library]
lit_sat [lemma, in Vct.Mcnf.Conversion]
Local [constructor, in Vct.Solver.Cct]
LocalCond [constructor, in Vct.Solver.Cct]
logically_equivalent [definition, in Vct.Cnf]
lt [definition, in Vct.Lit]
lt [definition, in Vct.Atom]
ltb [definition, in Vct.Atom]
ltb_ge [lemma, in Vct.Atom]
ltb_lt [lemma, in Vct.Atom]
lt_trans [instance, in Vct.Atom]
lt_compat [lemma, in Vct.Atom]
lt_strorder [instance, in Vct.Atom]

M

m [definition, in Vct.Solver.Cct]
make [constructor, in Vct.Tree]
Make [module, in Vct.Trie]
make [definition, in Vct.Kripke]
make [axiom, in Vct.CplSolver]
make_cpls [definition, in Vct.Lclauses]
make_is_empty [axiom, in Vct.CplSolver]
make_with_clauses [definition, in Vct.CplSolver]
Make.add [definition, in Vct.Trie]
Make.addf [definition, in Vct.Trie]
Make.add_contains_iff [lemma, in Vct.Trie]
Make.Cons [constructor, in Vct.Trie]
Make.contains [definition, in Vct.Trie]
Make.containsf [definition, in Vct.Trie]
Make.contains_singleton [lemma, in Vct.Trie]
Make.contains_add_other [lemma, in Vct.Trie]
Make.contains_addf_other [lemma, in Vct.Trie]
Make.contains_add_inv [lemma, in Vct.Trie]
Make.contains_addf_inv [lemma, in Vct.Trie]
Make.contains_add [lemma, in Vct.Trie]
Make.contains_addf [lemma, in Vct.Trie]
Make.contains_singletonf [lemma, in Vct.Trie]
Make.empty [definition, in Vct.Trie]
Make.Empty [constructor, in Vct.Trie]
Make.forest [inductive, in Vct.Trie]
Make.forest_sind [definition, in Vct.Trie]
Make.forest_rec [definition, in Vct.Trie]
Make.forest_ind [definition, in Vct.Trie]
Make.forest_rect [definition, in Vct.Trie]
Make.KFacts [module, in Vct.Trie]
Make.KFacts.compare_eq_iff' [lemma, in Vct.Trie]
Make.K' [module, in Vct.Trie]
Make.K'.compare [definition, in Vct.Trie]
Make.K'.compare_spec [definition, in Vct.Trie]
Make.K'.eq [definition, in Vct.Trie]
Make.K'.eq_dec [definition, in Vct.Trie]
Make.K'.eq_equiv [definition, in Vct.Trie]
Make.K'.le [definition, in Vct.Trie]
Make.K'.le_lteq [definition, in Vct.Trie]
Make.K'.lt [definition, in Vct.Trie]
Make.K'.lt_compat [definition, in Vct.Trie]
Make.K'.lt_strorder [definition, in Vct.Trie]
Make.K'.t [definition, in Vct.Trie]
Make.Nil [constructor, in Vct.Trie]
Make.Root [constructor, in Vct.Trie]
Make.singleton [definition, in Vct.Trie]
Make.singletonf [definition, in Vct.Trie]
Make.t [inductive, in Vct.Trie]
Make.t_sind [definition, in Vct.Trie]
Make.t_rec [definition, in Vct.Trie]
Make.t_ind [definition, in Vct.Trie]
Make.t_rect [definition, in Vct.Trie]
max [definition, in Vct.Atom]
max_atm [definition, in Vct.Nnf]
max_atm [definition, in Vct.Mcnf.Mcnf]
max_atm [definition, in Vct.Lclauses]
max_atm [definition, in Vct.CplClause]
max_atm [definition, in Vct.DiaClause]
max_atm [definition, in Vct.BoxClause]
max_le_iff [lemma, in Vct.Atom]
Mcnf [library]
Mcnf [library]
McnfExt [library]
mcnf_solve_sat [lemma, in Vct.Solver.McnfExt]
mcnf_solve_unsat [lemma, in Vct.Solver.McnfExt]
mcnf_resolution_cs [lemma, in Vct.Solver.Soundness]
mcnf_resolution [lemma, in Vct.Solver.Soundness]
mcnf_cpls [lemma, in Vct.Solver.Soundness]
mcnf_to_nnf_forces [lemma, in Vct.Mcnf.Conversion]
meaningful_valuations [lemma, in Vct.Nnf]
meaningful_valuations [lemma, in Vct.Mcnf.Mcnf]
meaningful_valuations [lemma, in Vct.Lclauses]
meaningful_valuations [lemma, in Vct.Lit]
meaningful_valuations [lemma, in Vct.CplClause]
meaningful_valuations [lemma, in Vct.DiaClause]
meaningful_valuations [lemma, in Vct.BoxClause]
merge [definition, in Vct.Lclauses]
M'_force_n_impl_phi [lemma, in Vct.Mcnf.Conversion]

N

n [definition, in Vct.Solver.Cct]
named_model_overrides_all_sur [lemma, in Vct.Mcnf.Conversion]
named_model_vals_name_iff_force [lemma, in Vct.Mcnf.Conversion]
named_model_changes_sur_only [lemma, in Vct.Mcnf.Conversion]
named_model [definition, in Vct.Mcnf.Conversion]
Neg [constructor, in Vct.Fml]
Neg [constructor, in Vct.Lit]
negate [definition, in Vct.Nnf]
negate [definition, in Vct.Lit]
negate_involution [lemma, in Vct.Lit]
negate_eq_atm [lemma, in Vct.Lit]
negb_exb_forallb [lemma, in Vct.ListExt]
NegKEx [section, in Vct.Solver.Cct]
+ _ [notation, in Vct.Solver.Cct]
- _ [notation, in Vct.Solver.Cct]
next_mc_build_kt_comm [lemma, in Vct.Mcnf.Mcnf]
next_mc [definition, in Vct.Mcnf.Mcnf]
Nnf [library]
Nnfl [library]
NnfToMcnf [section, in Vct.Mcnf.Conversion]
NnfToMcnf.M [variable, in Vct.Mcnf.Conversion]
NnfToMcnf.R [variable, in Vct.Mcnf.Conversion]
NnfToMcnf.W [variable, in Vct.Mcnf.Conversion]
nnf_to_mcnf_forces [lemma, in Vct.Mcnf.Conversion]
nodup [definition, in Vct.Valuation]
NoDupA_length_2 [lemma, in Vct.ListExt]
NoDupA_swap_iff [lemma, in Vct.ListExt]
NoDupA_concat [lemma, in Vct.ListExt]
NoDupA_filter [lemma, in Vct.ListExt]
NoDupA_length_incl [lemma, in Vct.ListExt]
NoDupA_incl_length [lemma, in Vct.ListExt]
NoDup_PermutationA_bis [lemma, in Vct.ListExt]
nodup_nil [lemma, in Vct.Valuation]
Notations [module, in Vct.Atom]
_ =? _ (atom_scope) [notation, in Vct.Atom]
_ < _ <= _ (atom_scope) [notation, in Vct.Atom]
_ < _ < _ (atom_scope) [notation, in Vct.Atom]
_ <= _ < _ (atom_scope) [notation, in Vct.Atom]
_ <= _ <= _ (atom_scope) [notation, in Vct.Atom]
_ <=? _ (atom_scope) [notation, in Vct.Atom]
_ <= _ (atom_scope) [notation, in Vct.Atom]
_ <? _ (atom_scope) [notation, in Vct.Atom]
_ < _ (atom_scope) [notation, in Vct.Atom]
not_all_some_true [lemma, in Vct.Solver.Soundness]
not_force_forallb [lemma, in Vct.Valuation]
not_force_negate [lemma, in Vct.Lit]
not_true [lemma, in Vct.ImportStd]
not_false [lemma, in Vct.ImportStd]
NoWit [library]
nowit_solve_fml_sound_complete [lemma, in Vct.Solver]

O

of_pos_eq_iff [lemma, in Vct.Atom]
one [definition, in Vct.Atom]
opt_on_groups [definition, in Vct.Mcnf.Simplification]
Op_atom_max [instance, in Vct.Atom]
Op_atom_succ [instance, in Vct.Atom]
Op_Z_atom [instance, in Vct.Atom]
Op_eq_atom [instance, in Vct.Atom]
Op_atom_le [instance, in Vct.Atom]
Op_atom_lt [instance, in Vct.Atom]
Or [constructor, in Vct.Nnf]
Or [constructor, in Vct.Fml]
Or [constructor, in Vct.Nnfl]
Ordered [module, in Vct.Lit]
Ordered.compare [definition, in Vct.Lit]
Ordered.compare_spec [definition, in Vct.Lit]
Ordered.eq [definition, in Vct.Lit]
Ordered.eq_equiv [definition, in Vct.Lit]
Ordered.eq_dec [definition, in Vct.Lit]
Ordered.le [definition, in Vct.Lit]
Ordered.le_lteq [lemma, in Vct.Lit]
Ordered.lt [definition, in Vct.Lit]
Ordered.lt_compat [lemma, in Vct.Lit]
Ordered.lt_strorder [lemma, in Vct.Lit]
Ordered.t [definition, in Vct.Lit]
or_sat [lemma, in Vct.Mcnf.Conversion]
or_false_r [lemma, in Vct.ImportStd]
or_false_l [lemma, in Vct.ImportStd]

P

p [definition, in Vct.Solver.Cct]
PermutationA_length [lemma, in Vct.ListExt]
PermutationA_swap_heads [lemma, in Vct.ListExt]
PermutationA_map [lemma, in Vct.ListExt]
PermutationA_flat_map [lemma, in Vct.ListExt]
PermutationA_inclA [lemma, in Vct.ListExt]
PermutationA_inA [lemma, in Vct.ListExt]
Permutation_ne_in [lemma, in Vct.ListExt]
Permutation_head_ne [lemma, in Vct.ListExt]
Permutation_heads_ne [lemma, in Vct.ListExt]
permutation_unsat [lemma, in Vct.Cnf]
permutation_sat [lemma, in Vct.Cnf]
permutation_force [lemma, in Vct.Cnf]
perm_forallb [lemma, in Vct.ListExt]
perm_existsb [lemma, in Vct.ListExt]
Pos [constructor, in Vct.Lit]
pos_binrel [definition, in Vct.Atom]
pos_unrel [definition, in Vct.Atom]
pos_binop [definition, in Vct.Atom]
pos_unop [definition, in Vct.Atom]
prefix_cons [lemma, in Vct.ListExt]
prefix_of_singleton [lemma, in Vct.ListExt]
prefix_of_empty [lemma, in Vct.ListExt]
prefix_empty_of [lemma, in Vct.ListExt]
prefix_incl [lemma, in Vct.ListExt]
proper_cpl_forceb [instance, in Vct.Cnf]
proper_cpl_forceb [instance, in Vct.Lit]
proper_cpl_forceb [instance, in Vct.CplClause]

Q

q [definition, in Vct.Solver.Cct]

R

R [definition, in Vct.Tree]
Range [section, in Vct.Nnf]
refined_solver_sat_vals_subset [lemma, in Vct.CplSolver]
refined_solver_diff_val [lemma, in Vct.CplSolver]
refl_closure_refl [instance, in Vct.ImportStd]
refl_closure [definition, in Vct.ImportStd]
remove_cs_preserve_sat [lemma, in Vct.Solver.Cached]
rhs_opt [definition, in Vct.Mcnf.Simplification]
R_kt_refl [instance, in Vct.Tree]
R_kt [definition, in Vct.Tree]

S

same_atms_valuation_set [lemma, in Vct.CplSolver]
Sat [constructor, in Vct.CplSolution]
satisfiable [definition, in Vct.Nnf]
satisfiable [definition, in Vct.Mcnf.Mcnf]
satisfiable [definition, in Vct.Fml]
satisfiable [definition, in Vct.Cnf]
satisfiable [definition, in Vct.Nnfl]
satisfiable_kt [definition, in Vct.Nnf]
satisfiable_kt [definition, in Vct.Mcnf.Mcnf]
satisfiable_kt [definition, in Vct.Fml]
sat_add_no_assumptions [lemma, in Vct.Solver.McnfExt]
sat_pos_cs_jump [lemma, in Vct.Solver.Soundness]
sat_not_A_neg_A [lemma, in Vct.Solver.Soundness]
sat_caches_cons_iff [lemma, in Vct.Solver.Cached]
sat_caches_add_empty_mc0 [lemma, in Vct.Solver.Cached]
sat_caches_add [lemma, in Vct.Solver.Cached]
sat_cache_add [lemma, in Vct.Solver.Cached]
sat_caches_contains_sat [lemma, in Vct.Solver.Cached]
sat_caches_sind [definition, in Vct.Solver.Cached]
sat_caches_ind [definition, in Vct.Solver.Cached]
sat_caches_cons [constructor, in Vct.Solver.Cached]
sat_caches_nil [constructor, in Vct.Solver.Cached]
sat_caches [inductive, in Vct.Solver.Cached]
sat_cache [definition, in Vct.Solver.Cached]
sat_mcnf_to_nnf [lemma, in Vct.Mcnf.Conversion]
sat_nnf_to_mcnf [lemma, in Vct.Mcnf.Conversion]
SearchBasics [library]
set_kripke_at_n_iff_force [definition, in Vct.Mcnf.Conversion]
Simplification [library]
simplify [definition, in Vct.Mcnf.Simplification]
simplify_sur [definition, in Vct.Mcnf.Simplification]
simplify_eq_lhs [definition, in Vct.Mcnf.Simplification]
simplify_eq_rhs [definition, in Vct.Mcnf.Simplification]
singleton_tree_force [lemma, in Vct.Solver.Completeness]
Solution [module, in Vct.Solver.Cached]
Solution [module, in Vct.Solver.TailRec]
Solution [module, in Vct.Solver.FiredBoxes]
Solution [module, in Vct.Solver.Kt]
Solution [module, in Vct.Solver.NoWit]
Solution [module, in Vct.Solver.Spec]
solution_completeness [axiom, in Vct.CplSolver]
solution_soundness [axiom, in Vct.CplSolver]
Solution.from_spec [definition, in Vct.Solver.NoWit]
Solution.get_caches_unsat [lemma, in Vct.Solver.Cached]
Solution.get_caches_sat [lemma, in Vct.Solver.Cached]
Solution.get_caches [definition, in Vct.Solver.Cached]
Solution.is_sat [definition, in Vct.Solver.Cached]
Solution.is_sat_eq [lemma, in Vct.Solver.NoWit]
Solution.is_sat [definition, in Vct.Solver.NoWit]
Solution.is_sat [definition, in Vct.Solver.Spec]
Solution.Sat [constructor, in Vct.Solver.Cached]
Solution.Sat [constructor, in Vct.Solver.NoWit]
Solution.Sat [constructor, in Vct.Solver.Spec]
Solution.t [inductive, in Vct.Solver.Cached]
Solution.t [inductive, in Vct.Solver.NoWit]
Solution.t [inductive, in Vct.Solver.Spec]
Solution.t_sind [definition, in Vct.Solver.Cached]
Solution.t_rec [definition, in Vct.Solver.Cached]
Solution.t_ind [definition, in Vct.Solver.Cached]
Solution.t_rect [definition, in Vct.Solver.Cached]
Solution.t_sind [definition, in Vct.Solver.NoWit]
Solution.t_rec [definition, in Vct.Solver.NoWit]
Solution.t_ind [definition, in Vct.Solver.NoWit]
Solution.t_rect [definition, in Vct.Solver.NoWit]
Solution.t_sind [definition, in Vct.Solver.Spec]
Solution.t_rec [definition, in Vct.Solver.Spec]
Solution.t_ind [definition, in Vct.Solver.Spec]
Solution.t_rect [definition, in Vct.Solver.Spec]
Solution.Unsat [constructor, in Vct.Solver.Cached]
Solution.Unsat [constructor, in Vct.Solver.NoWit]
Solution.Unsat [constructor, in Vct.Solver.Spec]
Solution.without_caches_sat [lemma, in Vct.Solver.Cached]
Solution.without_caches [definition, in Vct.Solver.Cached]
solved_clauses [definition, in Vct.CplSolver]
Solver [library]
solve_fml_sound_contrapos [lemma, in Vct.Solver.Soundness]
solve_mcnf_sound_contrapos [lemma, in Vct.Solver.Soundness]
solve_fml_sound [lemma, in Vct.Solver.Soundness]
solve_mcnf_sound [lemma, in Vct.Solver.Soundness]
solve_fml_cct [lemma, in Vct.Solver.Soundness]
solve_mcnf_cct [lemma, in Vct.Solver.Soundness]
solve_fml [definition, in Vct.Solver.Cached]
solve_mcnf [definition, in Vct.Solver.Cached]
solve_fml [definition, in Vct.Solver.TailRec]
solve_mcnf [definition, in Vct.Solver.TailRec]
solve_fml [definition, in Vct.Solver.FiredBoxes]
solve_mcnf [definition, in Vct.Solver.FiredBoxes]
solve_fml_sound_contrapos [lemma, in Vct.Solver.Kt]
solve_mcnf_sound_contrapos [lemma, in Vct.Solver.Kt]
solve_fml_sound [lemma, in Vct.Solver.Kt]
solve_mcnf_sound_kt [lemma, in Vct.Solver.Kt]
solve_mcnf_sound [lemma, in Vct.Solver.Kt]
solve_fml_cct [lemma, in Vct.Solver.Kt]
solve_mcnf_cct [lemma, in Vct.Solver.Kt]
solve_fml_complete_sat [lemma, in Vct.Solver.Kt]
solve_mcnf_complete_force [lemma, in Vct.Solver.Kt]
solve_fml [definition, in Vct.Solver.Kt]
solve_mcnf [definition, in Vct.Solver.Kt]
solve_fml [definition, in Vct.Solver.NoWit]
solve_mcnf [definition, in Vct.Solver.NoWit]
solve_fml [definition, in Vct.Solver.Spec]
solve_mcnf [definition, in Vct.Solver.Spec]
solve_with_assumptions [axiom, in Vct.CplSolver]
solve_fml_complete_sat [lemma, in Vct.Solver.Completeness]
solve_mcnf_complete_sat [lemma, in Vct.Solver.Completeness]
solve_fml_complete_force [lemma, in Vct.Solver.Completeness]
solve_mcnf_complete_force [lemma, in Vct.Solver.Completeness]
Soundness [library]
Spec [library]
spec_solve_fml_sound_complete [lemma, in Vct.Solver]
strong_force_weak [lemma, in Vct.Solver.Kt]
succ [definition, in Vct.Atom]
sur_input_le_return [lemma, in Vct.Mcnf.Conversion]

T

t [inductive, in Vct.Nnf]
t [definition, in Vct.Mcnf.Mcnf]
t [inductive, in Vct.Fml]
t [definition, in Vct.Cnf]
t [record, in Vct.Lclauses]
t [inductive, in Vct.Tree]
t [definition, in Vct.Valuation]
t [inductive, in Vct.Lit]
t [definition, in Vct.CplClause]
t [inductive, in Vct.CplSolution]
t [inductive, in Vct.Solver.Cct]
t [record, in Vct.Kripke]
t [definition, in Vct.DiaClause]
t [axiom, in Vct.CplSolver]
t [definition, in Vct.Assumptions]
t [definition, in Vct.BoxClause]
t [inductive, in Vct.Nnfl]
t [record, in Vct.Atom]
tableau [definition, in Vct.Solver.Cached]
tableau [definition, in Vct.Solver.TailRec]
tableau [definition, in Vct.Solver.FiredBoxes]
tableau [definition, in Vct.Solver.Kt]
tableau [definition, in Vct.Solver.NoWit]
tableau [definition, in Vct.Solver.Spec]
tableau_sound_contrapos [lemma, in Vct.Solver.Soundness]
tableau_sound [lemma, in Vct.Solver.Soundness]
tableau_jumps_cct [lemma, in Vct.Solver.Soundness]
tableau_cct [lemma, in Vct.Solver.Soundness]
tableau_jumps_cct_ind [lemma, in Vct.Solver.Soundness]
tableau_cct_core [lemma, in Vct.Solver.Soundness]
tableau_sound_complete [lemma, in Vct.Solver.Cached]
tableau_nowit_sat_caches [lemma, in Vct.Solver.Cached]
tableau_jumps_nowit_sat_caches [lemma, in Vct.Solver.Cached]
tableau_correct [definition, in Vct.Solver.Cached]
tableau_jumps_correct [definition, in Vct.Solver.Cached]
tableau_jumps [definition, in Vct.Solver.Cached]
tableau_spec [lemma, in Vct.Solver.TailRec]
tableau_jumps_spec_init [lemma, in Vct.Solver.TailRec]
tableau_jumps_spec [lemma, in Vct.Solver.TailRec]
tableau_jumps [definition, in Vct.Solver.TailRec]
tableau_cached [lemma, in Vct.Solver.FiredBoxes]
tableau_jumps_cached [lemma, in Vct.Solver.FiredBoxes]
tableau_jumps [definition, in Vct.Solver.FiredBoxes]
tableau_jumps_cct [lemma, in Vct.Solver.Kt]
tableau_cct [lemma, in Vct.Solver.Kt]
tableau_jumps_cct_ind [lemma, in Vct.Solver.Kt]
tableau_cct_core [lemma, in Vct.Solver.Kt]
tableau_completeness_force [lemma, in Vct.Solver.Kt]
tableau_completeness_force_weak [lemma, in Vct.Solver.Kt]
tableau_jumps_completeness_weak [lemma, in Vct.Solver.Kt]
tableau_jumps [definition, in Vct.Solver.Kt]
tableau_sound_complete [lemma, in Vct.Solver.NoWit]
tableau_jumps_spec [lemma, in Vct.Solver.NoWit]
tableau_spec [lemma, in Vct.Solver.NoWit]
tableau_jumps_spec_ind [lemma, in Vct.Solver.NoWit]
tableau_jumps [definition, in Vct.Solver.NoWit]
tableau_jumps [definition, in Vct.Solver.Spec]
tableau_completeness_sat [lemma, in Vct.Solver.Completeness]
tableau_completeness_force [lemma, in Vct.Solver.Completeness]
tableau_jumps_completeness [lemma, in Vct.Solver.Completeness]
Tactics [library]
TailRec [library]
tailrec_solve_fml_sound_complete [lemma, in Vct.Solver]
to_kt [definition, in Vct.Kripke]
to_Z [definition, in Vct.Atom]
to_pos [projection, in Vct.Atom]
Tree [library]
Trie [library]
t_sind [definition, in Vct.Nnf]
t_rec [definition, in Vct.Nnf]
t_ind [definition, in Vct.Nnf]
t_rect [definition, in Vct.Nnf]
t_sind [definition, in Vct.Fml]
t_rec [definition, in Vct.Fml]
t_ind [definition, in Vct.Fml]
t_rect [definition, in Vct.Fml]
t_sind [definition, in Vct.Tree]
t_rec [definition, in Vct.Tree]
t_ind [definition, in Vct.Tree]
t_rect [definition, in Vct.Tree]
t_sind [definition, in Vct.Lit]
t_rec [definition, in Vct.Lit]
t_ind [definition, in Vct.Lit]
t_rect [definition, in Vct.Lit]
t_sind [definition, in Vct.CplSolution]
t_rec [definition, in Vct.CplSolution]
t_ind [definition, in Vct.CplSolution]
t_rect [definition, in Vct.CplSolution]
t_sind [definition, in Vct.Solver.Cct]
t_rec [definition, in Vct.Solver.Cct]
t_ind [definition, in Vct.Solver.Cct]
t_rect [definition, in Vct.Solver.Cct]
t_sind [definition, in Vct.Nnfl]
t_rec [definition, in Vct.Nnfl]
t_ind [definition, in Vct.Nnfl]
t_rect [definition, in Vct.Nnfl]

U

Unsat [constructor, in Vct.CplSolution]
unsatisfiable [definition, in Vct.Nnf]
unsatisfiable [definition, in Vct.Mcnf.Mcnf]
unsatisfiable [definition, in Vct.Fml]
unsatisfiable [definition, in Vct.Cnf]
unsatisfiable [definition, in Vct.Nnfl]
unsatisfiable_kt [definition, in Vct.Nnf]
unsatisfiable_kt [definition, in Vct.Mcnf.Mcnf]
unsatisfiable_kt [definition, in Vct.Fml]
unsat_pos_cs_jump [lemma, in Vct.Solver.Soundness]

V

valuation [definition, in Vct.Tree]
valuation [projection, in Vct.Kripke]
Valuation [library]
valuation_in_every_sat_valuation [lemma, in Vct.CplSolver]
valuation_in_every_valuation_of [lemma, in Vct.CplSolver]
valuation_in_clauses [axiom, in Vct.CplSolver]
valuation_nodup [axiom, in Vct.CplSolver]
val_subset_no_new_atms [lemma, in Vct.Solver.McnfExt]
val_with_atms_in_every_val [lemma, in Vct.Valuation]
val_in_vals [definition, in Vct.Valuation]
Var [constructor, in Vct.Fml]

W

weak_force [definition, in Vct.Solver.Kt]
wf [inductive, in Vct.Solver.Cct]
wf_cct_neg_k [definition, in Vct.Solver.Cct]
wf_sind [definition, in Vct.Solver.Cct]
wf_ind [definition, in Vct.Solver.Cct]
with_fst_cpls [definition, in Vct.Mcnf.Mcnf]
with_global_val [definition, in Vct.Mcnf.Conversion]

Z

zip_merge [definition, in Vct.Mcnf.Mcnf]

other

_ $ _ [notation, in Vct.Solver.SearchBasics]
_ eqn : _ [notation, in Vct.Solver.SearchBasics]
_ |> _ [notation, in Vct.ImportStd]

---

Notation Index

N

+ _ [in Vct.Solver.Cct]
- _ [in Vct.Solver.Cct]
_ =? _ (atom_scope) [in Vct.Atom]
_ < _ <= _ (atom_scope) [in Vct.Atom]
_ < _ < _ (atom_scope) [in Vct.Atom]
_ <= _ < _ (atom_scope) [in Vct.Atom]
_ <= _ <= _ (atom_scope) [in Vct.Atom]
_ <=? _ (atom_scope) [in Vct.Atom]
_ <= _ (atom_scope) [in Vct.Atom]
_ <? _ (atom_scope) [in Vct.Atom]
_ < _ (atom_scope) [in Vct.Atom]

other

_ $ _ [in Vct.Solver.SearchBasics]
_ eqn : _ [in Vct.Solver.SearchBasics]
_ |> _ [in Vct.ImportStd]

---

Module Index

C

Cache [in Vct.Solver.Cached]
Cache [in Vct.Solver.FiredBoxes]
Caches [in Vct.Solver.Cached]
Caches [in Vct.Solver.FiredBoxes]
ClauseOrd1 [in Vct.Mcnf.Simplification]
ClauseOrd2 [in Vct.Mcnf.Simplification]
ClauseSort1 [in Vct.Mcnf.Simplification]
ClauseSort2 [in Vct.Mcnf.Simplification]
Compare [in Vct.Atom]
CompareFacts [in Vct.Atom]

J

JumpSolution [in Vct.Solver.Cached]
JumpSolution [in Vct.Solver.TailRec]
JumpSolution [in Vct.Solver.FiredBoxes]
JumpSolution [in Vct.Solver.Kt]
JumpSolution [in Vct.Solver.NoWit]
JumpSolution [in Vct.Solver.Spec]

M

Make [in Vct.Trie]
Make.KFacts [in Vct.Trie]
Make.K' [in Vct.Trie]

N

Notations [in Vct.Atom]

O

Ordered [in Vct.Lit]

S

Solution [in Vct.Solver.Cached]
Solution [in Vct.Solver.TailRec]
Solution [in Vct.Solver.FiredBoxes]
Solution [in Vct.Solver.Kt]
Solution [in Vct.Solver.NoWit]
Solution [in Vct.Solver.Spec]

---

Variable Index

F

ForceIff.M [in Vct.Nnfl]
ForceIff.R [in Vct.Nnfl]
ForceIff.W [in Vct.Nnfl]
ForceIff.w0 [in Vct.Nnfl]

N

NnfToMcnf.M [in Vct.Mcnf.Conversion]
NnfToMcnf.R [in Vct.Mcnf.Conversion]
NnfToMcnf.W [in Vct.Mcnf.Conversion]

---

Library Index

A

Assumptions
Atom

B

BoxClause

C

Cached
Cct
Cnf
Completeness
Conversion
CplClause
CplSolution
CplSolver

D

DiaClause

E

Extract

F

FiredBoxes
Fml

I

ImportStd

K

Kripke
Kt

L

Lclauses
ListExt
Lit

M

Mcnf
Mcnf
McnfExt

N

Nnf
Nnfl
NoWit

S

SearchBasics
Simplification
Solver
Soundness
Spec

T

Tactics
TailRec
Tree
Trie

V

Valuation

---

Lemma Index

A

add_A_build_kt_comm [in Vct.Mcnf.Mcnf]
add_cs_build_kt_comm [in Vct.Mcnf.Mcnf]
add_cs_nA_eq [in Vct.Mcnf.Mcnf]
add_no_new_atms [in Vct.CplSolver]
add_clause_incl_A [in Vct.CplSolver]
add_clause_incl [in Vct.CplSolver]
agree_r [in Vct.Nnf]
agree_l [in Vct.Nnf]
agree_cons [in Vct.Mcnf.Mcnf]
and_sat [in Vct.Mcnf.Conversion]
and_true_r [in Vct.ImportStd]
and_true_l [in Vct.ImportStd]
as_lit2_none [in Vct.Nnf]
as_lit2_some_inv [in Vct.Nnf]
as_lit_none [in Vct.Nnf]
as_lit_some_inv [in Vct.Nnf]
atms_in_ev_atms [in Vct.Valuation]
atms_of_nodup [in Vct.CplSolver]
atm_le_max [in Vct.Nnf]
atm_in_nnf_atm [in Vct.Nnf]
atm_le_max [in Vct.Mcnf.Mcnf]
atm_in_cons [in Vct.Mcnf.Mcnf]
atm_in_nil [in Vct.Mcnf.Mcnf]
atm_in_cons [in Vct.Cnf]
atm_in_exists [in Vct.Cnf]
atm_in_destruct [in Vct.Lclauses]
atm_in_cpls [in Vct.Lclauses]
atm_le_max [in Vct.Lclauses]
atm_le_max [in Vct.CplClause]
atm_in_cons [in Vct.CplClause]
atm_in_nil [in Vct.CplClause]
atm_in_exists [in Vct.CplClause]
atm_le_max [in Vct.DiaClause]
atm_le_max [in Vct.BoxClause]
atom_is_pos [in Vct.Atom]

B

bind_new_atm_unique [in Vct.Valuation]
box_sat [in Vct.Mcnf.Conversion]
build_kt_sound_complete [in Vct.Mcnf.Mcnf]
build_kt_complete [in Vct.Mcnf.Mcnf]
build_kt_sound [in Vct.Mcnf.Mcnf]
build_kt_refl_iff [in Vct.Mcnf.Mcnf]
build_kt_box_cl_in_cpls [in Vct.Mcnf.Mcnf]

C

cached_solve_fml_sound_complete [in Vct.Solver]
Caches.add_contains_iff [in Vct.Solver.Cached]
cct_sound [in Vct.Solver.Soundness]
cct_core_incl_A [in Vct.Solver.Soundness]
ClauseOrd1.leb_total [in Vct.Mcnf.Simplification]
ClauseOrd2.leb_total [in Vct.Mcnf.Simplification]
clauses_of_make_with_clauses [in Vct.CplSolver]
clauses_of_fold_right [in Vct.CplSolver]
cnf_unsat_subset [in Vct.Solver.Soundness]
compare_spec [in Vct.Lit]
compare_spec [in Vct.Atom]
cons_NoDupA [in Vct.ListExt]
conv_atm_range [in Vct.Mcnf.Conversion]
cpls_of_add_assumptions [in Vct.Solver.Soundness]
cpl_forceb_sat [in Vct.Cnf]
cs_incl_V [in Vct.Solver.McnfExt]
cs_preserve_sat [in Vct.Solver.Cached]

D

decreasing_sat_vals [in Vct.Solver.SearchBasics]
dia_sat [in Vct.Mcnf.Conversion]

E

eqb_eq [in Vct.Lit]
eqb_neq [in Vct.Atom]
eqb_eq [in Vct.Atom]
equisat_kt_fml [in Vct.Nnf]
equisat_fml [in Vct.Nnf]
equisat_kt_nnf [in Vct.Mcnf.Conversion]
equisat_nnf [in Vct.Mcnf.Conversion]
equisat_nnf [in Vct.Nnfl]
equiv_fml [in Vct.Nnf]
equiv_nnf [in Vct.Nnfl]
equiv_nnf_ind [in Vct.Nnfl]
eq_in [in Vct.Valuation]
eq_nodup [in Vct.Valuation]
eq_dec [in Vct.Lit]
eq_true [in Vct.ImportStd]
eq_Z_inj [in Vct.Atom]
eq_dec [in Vct.Atom]
every_valuation_unique [in Vct.Valuation]
every_valuation_perm [in Vct.Valuation]
every_valuation_nodup [in Vct.Valuation]
every_valuation_exact_atms [in Vct.Valuation]
every_sat_valuation_nodup [in Vct.CplSolver]
every_valuation_nodup [in Vct.CplSolver]
Exists_singleton [in Vct.ListExt]
ex_eqA_iff_inA [in Vct.ListExt]

F

fired_boxes_solve_fml_sound_complete [in Vct.Solver]
Forall_singleton [in Vct.ListExt]
forall_and_distrib [in Vct.Nnfl]
forceb_app [in Vct.Cnf]
forceb_cons [in Vct.Cnf]
forceb_nil [in Vct.Cnf]
forceb_forall [in Vct.Cnf]
forceb_exists [in Vct.CplClause]
forceb_cons [in Vct.CplClause]
forceb_nil [in Vct.CplClause]
forces_atm_iff_in [in Vct.Valuation]
force_negate_iff_not_force [in Vct.Nnf]
force_add_no_assumptions [in Vct.Solver.McnfExt]
force_app_and [in Vct.Solver.McnfExt]
force_rm_assumptions [in Vct.Solver.McnfExt]
force_ctx_first_next [in Vct.Solver.McnfExt]
force_assumptions_comm [in Vct.Solver.McnfExt]
force_refl_closure [in Vct.Mcnf.Mcnf]
force_build_kt_next [in Vct.Mcnf.Mcnf]
force_kt_build_kt_next [in Vct.Mcnf.Mcnf]
force_fst_mc [in Vct.Mcnf.Mcnf]
force_zip_merge_and [in Vct.Mcnf.Mcnf]
force_pos_cs_jump [in Vct.Solver.Soundness]
force_not_A_neg_A [in Vct.Solver.Soundness]
force_new_cpls [in Vct.Solver.Soundness]
force_fst_cpls [in Vct.Solver.Soundness]
force_local [in Vct.Cnf]
force_singleton [in Vct.Cnf]
force_from_assumptions [in Vct.Cnf]
force_map [in Vct.Cnf]
force_app [in Vct.Cnf]
force_cons [in Vct.Cnf]
force_nil [in Vct.Cnf]
force_cpl_forceb [in Vct.Cnf]
force_forall [in Vct.Cnf]
force_merge_app_sym [in Vct.Lclauses]
force_app_sym [in Vct.Lclauses]
force_destruct_forall [in Vct.Lclauses]
force_destruct [in Vct.Lclauses]
force_cpls [in Vct.Lclauses]
force_empty [in Vct.Lclauses]
force_cpls_cons [in Vct.Lclauses]
force_cpls_app [in Vct.Lclauses]
force_merge_and [in Vct.Lclauses]
force_local [in Vct.Lit]
force_cpl_forceb [in Vct.Lit]
force_local [in Vct.CplClause]
force_singleton [in Vct.CplClause]
force_cpl_forceb [in Vct.CplClause]
force_cons [in Vct.CplClause]
force_nil [in Vct.CplClause]
force_exists [in Vct.CplClause]
force_no_assumptions [in Vct.Solver.Kt]
force_no_assumptions [in Vct.Solver.Completeness]
force_dia_iff [in Vct.Nnfl]
force_box_iff [in Vct.Nnfl]
force_or_iff [in Vct.Nnfl]
force_and_iff [in Vct.Nnfl]
force_lit_iff [in Vct.Nnfl]
fst_mc_destruct [in Vct.Solver.Soundness]

I

imp_true_l_forall [in Vct.ImportStd]
imp_true_l [in Vct.ImportStd]
imp_true_r [in Vct.ImportStd]
imp_false_r [in Vct.ImportStd]
InA_length_2 [in Vct.ListExt]
InA_concat [in Vct.ListExt]
InA_flat_map [in Vct.ListExt]
inclA_nil [in Vct.ListExt]
inclA_cons [in Vct.ListExt]
incl_middle [in Vct.ListExt]
incl_A_sat [in Vct.Solver.McnfExt]
incl_A_force [in Vct.Solver.McnfExt]
incl_cpls_force [in Vct.Solver.McnfExt]
incl_unsat [in Vct.Cnf]
incl_force [in Vct.Cnf]
inline_pair_lemma [in Vct.Tactics]
In_nil_iff [in Vct.ListExt]
In_singleton [in Vct.ListExt]
in_zip_merge_or [in Vct.Mcnf.Mcnf]
in_atms_of [in Vct.Cnf]
in_merge_or [in Vct.Lclauses]
is_sat_spec [in Vct.Solver.NoWit]

J

JumpSolution.get_caches_unsat [in Vct.Solver.Cached]
JumpSolution.get_caches_sat [in Vct.Solver.Cached]
jump_cct_core [in Vct.Solver.Soundness]
jump_failed_dia [in Vct.Solver.Soundness]
jump_c_forced [in Vct.Solver.Cached]
jump_cct_core [in Vct.Solver.Kt]
jump_failed_dia [in Vct.Solver.Kt]
jump_c_forced [in Vct.Solver.Kt]
jump_c_forced [in Vct.Solver.NoWit]
jump_c_forced [in Vct.Solver.Spec]

K

kt_force_unboxed [in Vct.Mcnf.Mcnf]
kt_forces_weak [in Vct.Solver.Kt]
kt_spec_solve_fml_sound_complete [in Vct.Solver]

L

leb_total [in Vct.Lit]
leb_total [in Vct.Atom]
leb_gt [in Vct.Atom]
leb_le [in Vct.Atom]
le_mapped_list_max [in Vct.Atom]
le_list_max [in Vct.Atom]
le_list_max_ind [in Vct.Atom]
le_max_r [in Vct.Atom]
le_max_l [in Vct.Atom]
le_lteq [in Vct.Atom]
lit_sat [in Vct.Mcnf.Conversion]
ltb_ge [in Vct.Atom]
ltb_lt [in Vct.Atom]
lt_compat [in Vct.Atom]

M

Make.add_contains_iff [in Vct.Trie]
Make.contains_singleton [in Vct.Trie]
Make.contains_add_other [in Vct.Trie]
Make.contains_addf_other [in Vct.Trie]
Make.contains_add_inv [in Vct.Trie]
Make.contains_addf_inv [in Vct.Trie]
Make.contains_add [in Vct.Trie]
Make.contains_addf [in Vct.Trie]
Make.contains_singletonf [in Vct.Trie]
Make.KFacts.compare_eq_iff' [in Vct.Trie]
max_le_iff [in Vct.Atom]
mcnf_solve_sat [in Vct.Solver.McnfExt]
mcnf_solve_unsat [in Vct.Solver.McnfExt]
mcnf_resolution_cs [in Vct.Solver.Soundness]
mcnf_resolution [in Vct.Solver.Soundness]
mcnf_cpls [in Vct.Solver.Soundness]
mcnf_to_nnf_forces [in Vct.Mcnf.Conversion]
meaningful_valuations [in Vct.Nnf]
meaningful_valuations [in Vct.Mcnf.Mcnf]
meaningful_valuations [in Vct.Lclauses]
meaningful_valuations [in Vct.Lit]
meaningful_valuations [in Vct.CplClause]
meaningful_valuations [in Vct.DiaClause]
meaningful_valuations [in Vct.BoxClause]
M'_force_n_impl_phi [in Vct.Mcnf.Conversion]

N

named_model_overrides_all_sur [in Vct.Mcnf.Conversion]
named_model_vals_name_iff_force [in Vct.Mcnf.Conversion]
named_model_changes_sur_only [in Vct.Mcnf.Conversion]
negate_involution [in Vct.Lit]
negate_eq_atm [in Vct.Lit]
negb_exb_forallb [in Vct.ListExt]
next_mc_build_kt_comm [in Vct.Mcnf.Mcnf]
nnf_to_mcnf_forces [in Vct.Mcnf.Conversion]
NoDupA_length_2 [in Vct.ListExt]
NoDupA_swap_iff [in Vct.ListExt]
NoDupA_concat [in Vct.ListExt]
NoDupA_filter [in Vct.ListExt]
NoDupA_length_incl [in Vct.ListExt]
NoDupA_incl_length [in Vct.ListExt]
NoDup_PermutationA_bis [in Vct.ListExt]
nodup_nil [in Vct.Valuation]
not_all_some_true [in Vct.Solver.Soundness]
not_force_forallb [in Vct.Valuation]
not_force_negate [in Vct.Lit]
not_true [in Vct.ImportStd]
not_false [in Vct.ImportStd]
nowit_solve_fml_sound_complete [in Vct.Solver]

O

of_pos_eq_iff [in Vct.Atom]
Ordered.le_lteq [in Vct.Lit]
Ordered.lt_compat [in Vct.Lit]
Ordered.lt_strorder [in Vct.Lit]
or_sat [in Vct.Mcnf.Conversion]
or_false_r [in Vct.ImportStd]
or_false_l [in Vct.ImportStd]

P

PermutationA_length [in Vct.ListExt]
PermutationA_swap_heads [in Vct.ListExt]
PermutationA_map [in Vct.ListExt]
PermutationA_flat_map [in Vct.ListExt]
PermutationA_inclA [in Vct.ListExt]
PermutationA_inA [in Vct.ListExt]
Permutation_ne_in [in Vct.ListExt]
Permutation_head_ne [in Vct.ListExt]
Permutation_heads_ne [in Vct.ListExt]
permutation_unsat [in Vct.Cnf]
permutation_sat [in Vct.Cnf]
permutation_force [in Vct.Cnf]
perm_forallb [in Vct.ListExt]
perm_existsb [in Vct.ListExt]
prefix_cons [in Vct.ListExt]
prefix_of_singleton [in Vct.ListExt]
prefix_of_empty [in Vct.ListExt]
prefix_empty_of [in Vct.ListExt]
prefix_incl [in Vct.ListExt]

R

refined_solver_sat_vals_subset [in Vct.CplSolver]
refined_solver_diff_val [in Vct.CplSolver]
remove_cs_preserve_sat [in Vct.Solver.Cached]

S

same_atms_valuation_set [in Vct.CplSolver]
sat_add_no_assumptions [in Vct.Solver.McnfExt]
sat_pos_cs_jump [in Vct.Solver.Soundness]
sat_not_A_neg_A [in Vct.Solver.Soundness]
sat_caches_cons_iff [in Vct.Solver.Cached]
sat_caches_add_empty_mc0 [in Vct.Solver.Cached]
sat_caches_add [in Vct.Solver.Cached]
sat_cache_add [in Vct.Solver.Cached]
sat_caches_contains_sat [in Vct.Solver.Cached]
sat_mcnf_to_nnf [in Vct.Mcnf.Conversion]
sat_nnf_to_mcnf [in Vct.Mcnf.Conversion]
singleton_tree_force [in Vct.Solver.Completeness]
Solution.get_caches_unsat [in Vct.Solver.Cached]
Solution.get_caches_sat [in Vct.Solver.Cached]
Solution.is_sat_eq [in Vct.Solver.NoWit]
Solution.without_caches_sat [in Vct.Solver.Cached]
solve_fml_sound_contrapos [in Vct.Solver.Soundness]
solve_mcnf_sound_contrapos [in Vct.Solver.Soundness]
solve_fml_sound [in Vct.Solver.Soundness]
solve_mcnf_sound [in Vct.Solver.Soundness]
solve_fml_cct [in Vct.Solver.Soundness]
solve_mcnf_cct [in Vct.Solver.Soundness]
solve_fml_sound_contrapos [in Vct.Solver.Kt]
solve_mcnf_sound_contrapos [in Vct.Solver.Kt]
solve_fml_sound [in Vct.Solver.Kt]
solve_mcnf_sound_kt [in Vct.Solver.Kt]
solve_mcnf_sound [in Vct.Solver.Kt]
solve_fml_cct [in Vct.Solver.Kt]
solve_mcnf_cct [in Vct.Solver.Kt]
solve_fml_complete_sat [in Vct.Solver.Kt]
solve_mcnf_complete_force [in Vct.Solver.Kt]
solve_fml_complete_sat [in Vct.Solver.Completeness]
solve_mcnf_complete_sat [in Vct.Solver.Completeness]
solve_fml_complete_force [in Vct.Solver.Completeness]
solve_mcnf_complete_force [in Vct.Solver.Completeness]
spec_solve_fml_sound_complete [in Vct.Solver]
strong_force_weak [in Vct.Solver.Kt]
sur_input_le_return [in Vct.Mcnf.Conversion]

T

tableau_sound_contrapos [in Vct.Solver.Soundness]
tableau_sound [in Vct.Solver.Soundness]
tableau_jumps_cct [in Vct.Solver.Soundness]
tableau_cct [in Vct.Solver.Soundness]
tableau_jumps_cct_ind [in Vct.Solver.Soundness]
tableau_cct_core [in Vct.Solver.Soundness]
tableau_sound_complete [in Vct.Solver.Cached]
tableau_nowit_sat_caches [in Vct.Solver.Cached]
tableau_jumps_nowit_sat_caches [in Vct.Solver.Cached]
tableau_spec [in Vct.Solver.TailRec]
tableau_jumps_spec_init [in Vct.Solver.TailRec]
tableau_jumps_spec [in Vct.Solver.TailRec]
tableau_cached [in Vct.Solver.FiredBoxes]
tableau_jumps_cached [in Vct.Solver.FiredBoxes]
tableau_jumps_cct [in Vct.Solver.Kt]
tableau_cct [in Vct.Solver.Kt]
tableau_jumps_cct_ind [in Vct.Solver.Kt]
tableau_cct_core [in Vct.Solver.Kt]
tableau_completeness_force [in Vct.Solver.Kt]
tableau_completeness_force_weak [in Vct.Solver.Kt]
tableau_jumps_completeness_weak [in Vct.Solver.Kt]
tableau_sound_complete [in Vct.Solver.NoWit]
tableau_jumps_spec [in Vct.Solver.NoWit]
tableau_spec [in Vct.Solver.NoWit]
tableau_jumps_spec_ind [in Vct.Solver.NoWit]
tableau_completeness_sat [in Vct.Solver.Completeness]
tableau_completeness_force [in Vct.Solver.Completeness]
tableau_jumps_completeness [in Vct.Solver.Completeness]
tailrec_solve_fml_sound_complete [in Vct.Solver]

U

unsat_pos_cs_jump [in Vct.Solver.Soundness]

V

valuation_in_every_sat_valuation [in Vct.CplSolver]
valuation_in_every_valuation_of [in Vct.CplSolver]
val_subset_no_new_atms [in Vct.Solver.McnfExt]
val_with_atms_in_every_val [in Vct.Valuation]

---

Constructor Index

A

And [in Vct.Nnf]
And [in Vct.Fml]
And [in Vct.Nnfl]

B

Box [in Vct.Nnf]
Box [in Vct.Fml]
Box [in Vct.Nnfl]

D

Dia [in Vct.Nnf]
Dia [in Vct.Fml]
Dia [in Vct.Nnfl]

F

force_dia [in Vct.Nnfl]
force_box [in Vct.Nnfl]
force_or [in Vct.Nnfl]
force_and [in Vct.Nnfl]
force_lit [in Vct.Nnfl]

I

Impl [in Vct.Fml]

J

JumpRestart [in Vct.Solver.Cct]
JumpRestartCond [in Vct.Solver.Cct]
JumpSolution.Sat [in Vct.Solver.Cached]
JumpSolution.Sat [in Vct.Solver.NoWit]
JumpSolution.Sat [in Vct.Solver.Spec]
JumpSolution.Unsat [in Vct.Solver.Cached]
JumpSolution.Unsat [in Vct.Solver.NoWit]
JumpSolution.Unsat [in Vct.Solver.Spec]

L

Lit [in Vct.Nnf]
Lit [in Vct.Nnfl]
Local [in Vct.Solver.Cct]
LocalCond [in Vct.Solver.Cct]

M

make [in Vct.Tree]
Make.Cons [in Vct.Trie]
Make.Empty [in Vct.Trie]
Make.Nil [in Vct.Trie]
Make.Root [in Vct.Trie]

N

Neg [in Vct.Fml]
Neg [in Vct.Lit]

O

Or [in Vct.Nnf]
Or [in Vct.Fml]
Or [in Vct.Nnfl]

P

Pos [in Vct.Lit]

S

Sat [in Vct.CplSolution]
sat_caches_cons [in Vct.Solver.Cached]
sat_caches_nil [in Vct.Solver.Cached]
Solution.Sat [in Vct.Solver.Cached]
Solution.Sat [in Vct.Solver.NoWit]
Solution.Sat [in Vct.Solver.Spec]
Solution.Unsat [in Vct.Solver.Cached]
Solution.Unsat [in Vct.Solver.NoWit]
Solution.Unsat [in Vct.Solver.Spec]

U

Unsat [in Vct.CplSolution]

V

Var [in Vct.Fml]

---

Axiom Index

A

add_clause_cons [in Vct.CplSolver]
add_clause [in Vct.CplSolver]

C

clauses_of [in Vct.CplSolver]
core_subset_assumptions [in Vct.CplSolver]

M

make [in Vct.CplSolver]
make_is_empty [in Vct.CplSolver]

S

solution_completeness [in Vct.CplSolver]
solution_soundness [in Vct.CplSolver]
solve_with_assumptions [in Vct.CplSolver]

T

t [in Vct.CplSolver]

V

valuation_in_clauses [in Vct.CplSolver]
valuation_nodup [in Vct.CplSolver]

---

Inductive Index

F

force [in Vct.Nnfl]

J

JumpSolution.t [in Vct.Solver.Cached]
JumpSolution.t [in Vct.Solver.NoWit]
JumpSolution.t [in Vct.Solver.Spec]

M

Make.forest [in Vct.Trie]
Make.t [in Vct.Trie]

S

sat_caches [in Vct.Solver.Cached]
Solution.t [in Vct.Solver.Cached]
Solution.t [in Vct.Solver.NoWit]
Solution.t [in Vct.Solver.Spec]

T

t [in Vct.Nnf]
t [in Vct.Fml]
t [in Vct.Tree]
t [in Vct.Lit]
t [in Vct.CplSolution]
t [in Vct.Solver.Cct]
t [in Vct.Nnfl]

W

wf [in Vct.Solver.Cct]

---

Projection Index

B

boxes [in Vct.Lclauses]

C

cpls [in Vct.Lclauses]

D

dias [in Vct.Lclauses]

T

to_pos [in Vct.Atom]

V

valuation [in Vct.Kripke]

---

Section Index

A

AllValuations [in Vct.Valuation]

C

Conversion [in Vct.Nnf]
Correctness [in Vct.Nnf]

E

EquisatModel [in Vct.Mcnf.Conversion]
EquisatModelRange [in Vct.Mcnf.Conversion]

F

ForceIff [in Vct.Nnfl]

N

NegKEx [in Vct.Solver.Cct]
NnfToMcnf [in Vct.Mcnf.Conversion]

R

Range [in Vct.Nnf]

---

Instance Index

E

eqb_equiv [in Vct.Lit]
eqb_equiv [in Vct.Atom]
eqb_trans [in Vct.Atom]
eqb_sym [in Vct.Atom]
eqb_refl [in Vct.Atom]
eq_equivalence [in Vct.Valuation]
eq_atm_equivalence [in Vct.Lit]
eq_atm_trans [in Vct.Lit]
eq_atm_sym [in Vct.Lit]
eq_atm_refl [in Vct.Lit]
eq_equiv [in Vct.Atom]

I

Inj_atom_Z [in Vct.Atom]

L

leb_trans [in Vct.Lit]
lexnat2_lt_wf [in Vct.Solver.SearchBasics]
le_trans [in Vct.Atom]
le_refl [in Vct.Atom]
lt_trans [in Vct.Atom]
lt_strorder [in Vct.Atom]

O

Op_atom_max [in Vct.Atom]
Op_atom_succ [in Vct.Atom]
Op_Z_atom [in Vct.Atom]
Op_eq_atom [in Vct.Atom]
Op_atom_le [in Vct.Atom]
Op_atom_lt [in Vct.Atom]

P

proper_cpl_forceb [in Vct.Cnf]
proper_cpl_forceb [in Vct.Lit]
proper_cpl_forceb [in Vct.CplClause]

R

refl_closure_refl [in Vct.ImportStd]
R_kt_refl [in Vct.Tree]

---

Definition Index

A

add_nA [in Vct.Mcnf.Mcnf]
add_A [in Vct.Mcnf.Mcnf]
add_cs [in Vct.Mcnf.Mcnf]
add_conflict_set [in Vct.CplSolver]
agree [in Vct.Nnf]
agree [in Vct.Mcnf.Mcnf]
agree [in Vct.Lclauses]
agree [in Vct.Lit]
agree [in Vct.CplClause]
agree [in Vct.DiaClause]
agree [in Vct.BoxClause]
as_lit2 [in Vct.Nnf]
as_lit [in Vct.Nnf]
as_kt [in Vct.Tree]
as_k [in Vct.Tree]
atm [in Vct.Lit]
atms_of [in Vct.Cnf]
atms_of [in Vct.CplSolver]
atm_in [in Vct.Nnf]
atm_in [in Vct.Mcnf.Mcnf]
atm_in [in Vct.Cnf]
atm_in [in Vct.Lclauses]
atm_in [in Vct.Lit]
atm_in [in Vct.CplClause]
atm_in [in Vct.DiaClause]
atm_in [in Vct.CplSolver]
atm_in [in Vct.Assumptions]
atm_in [in Vct.BoxClause]

B

box_culprits [in Vct.Solver.McnfExt]
build_kt [in Vct.Mcnf.Mcnf]

C

Caches.add [in Vct.Solver.Cached]
Caches.contains [in Vct.Solver.Cached]
Caches.destruct [in Vct.Solver.Cached]
Caches.t [in Vct.Solver.Cached]
ClauseOrd1.leb [in Vct.Mcnf.Simplification]
ClauseOrd1.t [in Vct.Mcnf.Simplification]
ClauseOrd2.leb [in Vct.Mcnf.Simplification]
ClauseOrd2.t [in Vct.Mcnf.Simplification]
clause_atms_incl [in Vct.CplSolver]
compare [in Vct.Lit]
compare [in Vct.Atom]
compare_gt_iff [in Vct.Atom]
compare_lt_iff [in Vct.Atom]
compare_eq_iff [in Vct.Atom]
compare_refl [in Vct.Atom]
Compare.compare [in Vct.Atom]
Compare.compare_spec [in Vct.Atom]
Compare.eq [in Vct.Atom]
Compare.eq_dec [in Vct.Atom]
Compare.eq_equiv [in Vct.Atom]
Compare.le [in Vct.Atom]
Compare.le_lteq [in Vct.Atom]
Compare.lt [in Vct.Atom]
Compare.lt_compat [in Vct.Atom]
Compare.lt_strorder [in Vct.Atom]
Compare.t [in Vct.Atom]
cons_child [in Vct.Tree]
cplsolver_mcnf [in Vct.Solver.McnfExt]
cpl_solve [in Vct.Solver.McnfExt]
cpl_from_lclauses [in Vct.Solver.McnfExt]
cpl_forceb [in Vct.Cnf]
cpl_forceb [in Vct.Lit]
cpl_forceb [in Vct.CplClause]

E

empty [in Vct.Lclauses]
empty [in Vct.Tree]
eq [in Vct.Valuation]
eq [in Vct.Atom]
eqb [in Vct.Lit]
eqb [in Vct.Atom]
eq_atm [in Vct.Lit]
every_valuation_of_atms [in Vct.Valuation]
every_sat_valuation [in Vct.CplSolver]
every_valuation [in Vct.CplSolver]

F

fired_boxes [in Vct.Solver.McnfExt]
force [in Vct.Nnf]
force [in Vct.Mcnf.Mcnf]
force [in Vct.Fml]
force [in Vct.Cnf]
force [in Vct.Lclauses]
force [in Vct.Lit]
force [in Vct.CplClause]
force [in Vct.DiaClause]
force [in Vct.BoxClause]
forces_atm [in Vct.Valuation]
force_sind [in Vct.Nnfl]
force_ind [in Vct.Nnfl]
from_fml [in Vct.Nnf]
from_assumptions [in Vct.Cnf]
from_lit [in Vct.CplClause]
from_nnf [in Vct.Mcnf.Conversion]
from_nnf_with_sur [in Vct.Mcnf.Conversion]
from_n_nnf [in Vct.Mcnf.Conversion]
from_nnf [in Vct.Nnfl]
fst_dias [in Vct.Mcnf.Mcnf]
fst_boxes [in Vct.Mcnf.Mcnf]
fst_cpls [in Vct.Mcnf.Mcnf]
fst_mc [in Vct.Mcnf.Mcnf]

G

gather_or [in Vct.Nnfl]
gather_and [in Vct.Nnfl]
get_pos [in Vct.Lit]
get_fired_boxes [in Vct.Solver.FiredBoxes]
get_core [in Vct.Solver.Cct]
group_by [in Vct.Mcnf.Simplification]

I

IH [in Vct.Mcnf.Conversion]
is_prefix [in Vct.ListExt]
is_unsat [in Vct.CplSolution]
is_sat [in Vct.CplSolution]

J

JumpSolution.from_spec [in Vct.Solver.NoWit]
JumpSolution.get_caches [in Vct.Solver.Cached]
JumpSolution.t_sind [in Vct.Solver.Cached]
JumpSolution.t_rec [in Vct.Solver.Cached]
JumpSolution.t_ind [in Vct.Solver.Cached]
JumpSolution.t_rect [in Vct.Solver.Cached]
JumpSolution.t_sind [in Vct.Solver.NoWit]
JumpSolution.t_rec [in Vct.Solver.NoWit]
JumpSolution.t_ind [in Vct.Solver.NoWit]
JumpSolution.t_rect [in Vct.Solver.NoWit]
JumpSolution.t_sind [in Vct.Solver.Spec]
JumpSolution.t_rec [in Vct.Solver.Spec]
JumpSolution.t_ind [in Vct.Solver.Spec]
JumpSolution.t_rect [in Vct.Solver.Spec]
JumpSolution.without_caches [in Vct.Solver.Cached]

L

le [in Vct.Atom]
leb [in Vct.Lit]
leb [in Vct.Atom]
lexnat2_lt [in Vct.Solver.SearchBasics]
lhs_opt [in Vct.Mcnf.Simplification]
list_max [in Vct.Atom]
logically_equivalent [in Vct.Cnf]
lt [in Vct.Lit]
lt [in Vct.Atom]
ltb [in Vct.Atom]

M

m [in Vct.Solver.Cct]
make [in Vct.Kripke]
make_cpls [in Vct.Lclauses]
make_with_clauses [in Vct.CplSolver]
Make.add [in Vct.Trie]
Make.addf [in Vct.Trie]
Make.contains [in Vct.Trie]
Make.containsf [in Vct.Trie]
Make.empty [in Vct.Trie]
Make.forest_sind [in Vct.Trie]
Make.forest_rec [in Vct.Trie]
Make.forest_ind [in Vct.Trie]
Make.forest_rect [in Vct.Trie]
Make.K'.compare [in Vct.Trie]
Make.K'.compare_spec [in Vct.Trie]
Make.K'.eq [in Vct.Trie]
Make.K'.eq_dec [in Vct.Trie]
Make.K'.eq_equiv [in Vct.Trie]
Make.K'.le [in Vct.Trie]
Make.K'.le_lteq [in Vct.Trie]
Make.K'.lt [in Vct.Trie]
Make.K'.lt_compat [in Vct.Trie]
Make.K'.lt_strorder [in Vct.Trie]
Make.K'.t [in Vct.Trie]
Make.singleton [in Vct.Trie]
Make.singletonf [in Vct.Trie]
Make.t_sind [in Vct.Trie]
Make.t_rec [in Vct.Trie]
Make.t_ind [in Vct.Trie]
Make.t_rect [in Vct.Trie]
max [in Vct.Atom]
max_atm [in Vct.Nnf]
max_atm [in Vct.Mcnf.Mcnf]
max_atm [in Vct.Lclauses]
max_atm [in Vct.CplClause]
max_atm [in Vct.DiaClause]
max_atm [in Vct.BoxClause]
merge [in Vct.Lclauses]

N

n [in Vct.Solver.Cct]
named_model [in Vct.Mcnf.Conversion]
negate [in Vct.Nnf]
negate [in Vct.Lit]
next_mc [in Vct.Mcnf.Mcnf]
nodup [in Vct.Valuation]

O

one [in Vct.Atom]
opt_on_groups [in Vct.Mcnf.Simplification]
Ordered.compare [in Vct.Lit]
Ordered.compare_spec [in Vct.Lit]
Ordered.eq [in Vct.Lit]
Ordered.eq_equiv [in Vct.Lit]
Ordered.eq_dec [in Vct.Lit]
Ordered.le [in Vct.Lit]
Ordered.lt [in Vct.Lit]
Ordered.t [in Vct.Lit]

P

p [in Vct.Solver.Cct]
pos_binrel [in Vct.Atom]
pos_unrel [in Vct.Atom]
pos_binop [in Vct.Atom]
pos_unop [in Vct.Atom]

Q

q [in Vct.Solver.Cct]

R

R [in Vct.Tree]
refl_closure [in Vct.ImportStd]
rhs_opt [in Vct.Mcnf.Simplification]
R_kt [in Vct.Tree]

S

satisfiable [in Vct.Nnf]
satisfiable [in Vct.Mcnf.Mcnf]
satisfiable [in Vct.Fml]
satisfiable [in Vct.Cnf]
satisfiable [in Vct.Nnfl]
satisfiable_kt [in Vct.Nnf]
satisfiable_kt [in Vct.Mcnf.Mcnf]
satisfiable_kt [in Vct.Fml]
sat_caches_sind [in Vct.Solver.Cached]
sat_caches_ind [in Vct.Solver.Cached]
sat_cache [in Vct.Solver.Cached]
set_kripke_at_n_iff_force [in Vct.Mcnf.Conversion]
simplify [in Vct.Mcnf.Simplification]
simplify_sur [in Vct.Mcnf.Simplification]
simplify_eq_lhs [in Vct.Mcnf.Simplification]
simplify_eq_rhs [in Vct.Mcnf.Simplification]
Solution.from_spec [in Vct.Solver.NoWit]
Solution.get_caches [in Vct.Solver.Cached]
Solution.is_sat [in Vct.Solver.Cached]
Solution.is_sat [in Vct.Solver.NoWit]
Solution.is_sat [in Vct.Solver.Spec]
Solution.t_sind [in Vct.Solver.Cached]
Solution.t_rec [in Vct.Solver.Cached]
Solution.t_ind [in Vct.Solver.Cached]
Solution.t_rect [in Vct.Solver.Cached]
Solution.t_sind [in Vct.Solver.NoWit]
Solution.t_rec [in Vct.Solver.NoWit]
Solution.t_ind [in Vct.Solver.NoWit]
Solution.t_rect [in Vct.Solver.NoWit]
Solution.t_sind [in Vct.Solver.Spec]
Solution.t_rec [in Vct.Solver.Spec]
Solution.t_ind [in Vct.Solver.Spec]
Solution.t_rect [in Vct.Solver.Spec]
Solution.without_caches [in Vct.Solver.Cached]
solved_clauses [in Vct.CplSolver]
solve_fml [in Vct.Solver.Cached]
solve_mcnf [in Vct.Solver.Cached]
solve_fml [in Vct.Solver.TailRec]
solve_mcnf [in Vct.Solver.TailRec]
solve_fml [in Vct.Solver.FiredBoxes]
solve_mcnf [in Vct.Solver.FiredBoxes]
solve_fml [in Vct.Solver.Kt]
solve_mcnf [in Vct.Solver.Kt]
solve_fml [in Vct.Solver.NoWit]
solve_mcnf [in Vct.Solver.NoWit]
solve_fml [in Vct.Solver.Spec]
solve_mcnf [in Vct.Solver.Spec]
succ [in Vct.Atom]

T

t [in Vct.Mcnf.Mcnf]
t [in Vct.Cnf]
t [in Vct.Valuation]
t [in Vct.CplClause]
t [in Vct.DiaClause]
t [in Vct.Assumptions]
t [in Vct.BoxClause]
tableau [in Vct.Solver.Cached]
tableau [in Vct.Solver.TailRec]
tableau [in Vct.Solver.FiredBoxes]
tableau [in Vct.Solver.Kt]
tableau [in Vct.Solver.NoWit]
tableau [in Vct.Solver.Spec]
tableau_correct [in Vct.Solver.Cached]
tableau_jumps_correct [in Vct.Solver.Cached]
tableau_jumps [in Vct.Solver.Cached]
tableau_jumps [in Vct.Solver.TailRec]
tableau_jumps [in Vct.Solver.FiredBoxes]
tableau_jumps [in Vct.Solver.Kt]
tableau_jumps [in Vct.Solver.NoWit]
tableau_jumps [in Vct.Solver.Spec]
to_kt [in Vct.Kripke]
to_Z [in Vct.Atom]
t_sind [in Vct.Nnf]
t_rec [in Vct.Nnf]
t_ind [in Vct.Nnf]
t_rect [in Vct.Nnf]
t_sind [in Vct.Fml]
t_rec [in Vct.Fml]
t_ind [in Vct.Fml]
t_rect [in Vct.Fml]
t_sind [in Vct.Tree]
t_rec [in Vct.Tree]
t_ind [in Vct.Tree]
t_rect [in Vct.Tree]
t_sind [in Vct.Lit]
t_rec [in Vct.Lit]
t_ind [in Vct.Lit]
t_rect [in Vct.Lit]
t_sind [in Vct.CplSolution]
t_rec [in Vct.CplSolution]
t_ind [in Vct.CplSolution]
t_rect [in Vct.CplSolution]
t_sind [in Vct.Solver.Cct]
t_rec [in Vct.Solver.Cct]
t_ind [in Vct.Solver.Cct]
t_rect [in Vct.Solver.Cct]
t_sind [in Vct.Nnfl]
t_rec [in Vct.Nnfl]
t_ind [in Vct.Nnfl]
t_rect [in Vct.Nnfl]

U

unsatisfiable [in Vct.Nnf]
unsatisfiable [in Vct.Mcnf.Mcnf]
unsatisfiable [in Vct.Fml]
unsatisfiable [in Vct.Cnf]
unsatisfiable [in Vct.Nnfl]
unsatisfiable_kt [in Vct.Nnf]
unsatisfiable_kt [in Vct.Mcnf.Mcnf]
unsatisfiable_kt [in Vct.Fml]

V

valuation [in Vct.Tree]
val_in_vals [in Vct.Valuation]

W

weak_force [in Vct.Solver.Kt]
wf_cct_neg_k [in Vct.Solver.Cct]
wf_sind [in Vct.Solver.Cct]
wf_ind [in Vct.Solver.Cct]
with_fst_cpls [in Vct.Mcnf.Mcnf]
with_global_val [in Vct.Mcnf.Conversion]

Z

zip_merge [in Vct.Mcnf.Mcnf]

---

Record Index

T

t [in Vct.Lclauses]
t [in Vct.Kripke]
t [in Vct.Atom]

---

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

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

(14 entries)

Module Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

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

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

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

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

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

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

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

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

(9 entries)

Instance Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

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

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

(3 entries)

Generated by coqdoc and improved with CoqdocJS