Global Index

G

J

K

O

Q

R

V

X

Y

Z

_

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

_

(13 entries)

Module Index

A

B

C

D

F

G

H

I

J

K

L

M

N

O

P

Q

R

T

U

V

W

X

Y

Z

_

other

(2 entries)

Variable Index

A

B

C

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

T

U

V

X

Y

Z

_

other

(8 entries)

Library Index

B

F

G

H

J

K

M

O

P

Q

R

U

V

X

Y

Z

_

other

(16 entries)

Lemma Index

G

H

J

K

O

Q

R

V

X

Y

Z

_

other

(194 entries)

Constructor Index

A

B

C

G

I

J

K

L

M

O

Q

R

U

V

W

X

Y

Z

_

other

(22 entries)

Inductive Index

B

D

G

H

I

J

K

M

N

O

Q

R

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

X

Y

Z

_

other

(1 entry)

Section Index

A

B

C

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

T

U

V

X

Y

Z

_

other

(3 entries)

Definition Index

G

H

J

K

O

Q

R

V

X

Y

Z

_

other

(104 entries)

Global Index

A

Acc_incl' [lemma, in RocqSAT.Termination]
Ann [inductive, in RocqSAT.Evaluation]
Ann_sind [definition, in RocqSAT.Evaluation]
Ann_rec [definition, in RocqSAT.Evaluation]
Ann_ind [definition, in RocqSAT.Evaluation]
Ann_rect [definition, in RocqSAT.Evaluation]
Atom [definition, in RocqSAT.Atom]
Atom [library]

B

bcll [definition, in RocqSAT.Termination]
bcll__prefix_lt [lemma, in RocqSAT.Termination]
bcll' [definition, in RocqSAT.Termination]
bound [definition, in RocqSAT.Normalization]
Bounded [definition, in RocqSAT.WellFormed]
bounded_cons [lemma, in RocqSAT.WellFormed]
bounded_incl [lemma, in RocqSAT.WellFormed]
bounded_app__bounded [lemma, in RocqSAT.WellFormed]
bounded_cons__bounded [lemma, in RocqSAT.WellFormed]
bound_all_def [lemma, in RocqSAT.Normalization]
bound_only_dec [lemma, in RocqSAT.Normalization]
bound_incl [lemma, in RocqSAT.Normalization]
bound_bounded [lemma, in RocqSAT.Normalization]
bound_f [lemma, in RocqSAT.Normalization]
bound_f_aux [lemma, in RocqSAT.Normalization]
bound_c [lemma, in RocqSAT.Normalization]
bound_c_aux [lemma, in RocqSAT.Normalization]
bound_l [lemma, in RocqSAT.Normalization]

C

Clause [definition, in RocqSAT.Clause]
Clause [library]
cll [inductive, in RocqSAT.Termination]
cll_incl [lemma, in RocqSAT.Termination]
cll_sind [definition, in RocqSAT.Termination]
cll_ind [definition, in RocqSAT.Termination]
clos_nf' [lemma, in RocqSAT.Termination]
clos_nf0 [lemma, in RocqSAT.Termination]
clos_nf [lemma, in RocqSAT.Termination]
clos_refl_trans_flip [lemma, in RocqSAT.Termination]
clos_trans_flip [lemma, in RocqSAT.Termination]
CNF [definition, in RocqSAT.CNF]
cnf [definition, in RocqSAT.Termination]
CNF [library]
Conflicting [definition, in RocqSAT.Evaluation]
convert_prop_all_def [lemma, in RocqSAT.Normalization]
convert_prop_only_dec [lemma, in RocqSAT.Normalization]
convert_prop_f [lemma, in RocqSAT.Normalization]
convert_prop_c [lemma, in RocqSAT.Normalization]
convert_prop_l [lemma, in RocqSAT.Normalization]
convert_prop [definition, in RocqSAT.Normalization]
c_eval_true_extend [lemma, in RocqSAT.Evaluation]
c_eval_nil [lemma, in RocqSAT.Evaluation]
c_eval_false_extend [lemma, in RocqSAT.Evaluation]
c_eval_remove_none_l [lemma, in RocqSAT.Evaluation]
c_eval_remove_false_l [lemma, in RocqSAT.Evaluation]
c_eval_none_iff [lemma, in RocqSAT.Evaluation]
c_eval_false_iff [lemma, in RocqSAT.Evaluation]
c_eval_true_iff [lemma, in RocqSAT.Evaluation]
c_eval [definition, in RocqSAT.Evaluation]
c_eval_in [lemma, in RocqSAT.Normalization]
c_totalize_all_def [lemma, in RocqSAT.Normalization]
c_totalize_f [lemma, in RocqSAT.Normalization]
c_totalize_c [lemma, in RocqSAT.Normalization]
c_totalize_l [lemma, in RocqSAT.Normalization]
c_eval_extend_undef [lemma, in RocqSAT.Normalization]
c_totalize [definition, in RocqSAT.Normalization]

D

dec [constructor, in RocqSAT.Evaluation]
dedupe [definition, in RocqSAT.Normalization]
Dedupe [library]
dedupe_by [definition, in RocqSAT.Dedupe]
dedupe_by.eq [variable, in RocqSAT.Dedupe]
dedupe_by.A [variable, in RocqSAT.Dedupe]
dedupe_by [section, in RocqSAT.Dedupe]
dedupe_no_duplicates [lemma, in RocqSAT.Normalization]
dedupe_bounded [lemma, in RocqSAT.Normalization]
dedupe_only_dec [lemma, in RocqSAT.Normalization]
dedupe_all_def [lemma, in RocqSAT.Normalization]
dedupe_f [lemma, in RocqSAT.Normalization]
dedupe_c [lemma, in RocqSAT.Normalization]
dedupe_l [lemma, in RocqSAT.Normalization]
dedupe_l_aux [lemma, in RocqSAT.Normalization]
Def [definition, in RocqSAT.Evaluation]
def_undef [lemma, in RocqSAT.Evaluation]
Derivation [definition, in RocqSAT.Trans]
DerivationStrict [definition, in RocqSAT.Trans]
derivation_same_formula [lemma, in RocqSAT.Trans]
derivation_strict_same_formula [lemma, in RocqSAT.Trans]
derivation_entails [lemma, in RocqSAT.Entails]

E

entailment [lemma, in RocqSAT.Entails]
Entails [inductive, in RocqSAT.Entails]
Entails [library]
entails_clip [lemma, in RocqSAT.Entails]
entails_clip_aux' [lemma, in RocqSAT.Entails]
entails_clip_aux [lemma, in RocqSAT.Entails]
Entails_sind [definition, in RocqSAT.Entails]
Entails_ind [definition, in RocqSAT.Entails]
eqb [definition, in RocqSAT.Lit]
eqb [definition, in RocqSAT.Atom]
eqb_neq [lemma, in RocqSAT.Lit]
eqb_eq [lemma, in RocqSAT.Lit]
eqb_sym [lemma, in RocqSAT.Lit]
eqb_refl [lemma, in RocqSAT.Lit]
eqb_compat [lemma, in RocqSAT.Neg]
eqb_by_atom [definition, in RocqSAT.Normalization]
eqb_eq [lemma, in RocqSAT.Atom]
eqb_sym [lemma, in RocqSAT.Atom]
eqb_refl [lemma, in RocqSAT.Atom]
eq_compat [lemma, in RocqSAT.Neg]
EvalExamples [module, in RocqSAT.Evaluation]
EvalExamples.example_c_eval_3 [definition, in RocqSAT.Evaluation]
EvalExamples.example_c_eval_2 [definition, in RocqSAT.Evaluation]
EvalExamples.example_c_eval_1 [definition, in RocqSAT.Evaluation]
EvalExamples.example_l_eval_3 [definition, in RocqSAT.Evaluation]
EvalExamples.example_l_eval_2 [definition, in RocqSAT.Evaluation]
EvalExamples.example_l_eval_1 [definition, in RocqSAT.Evaluation]
Evaluation [library]
extract [definition, in RocqSAT.Lit]
extract_neqb_iff [lemma, in RocqSAT.Normalization]
e_irrelevant [constructor, in RocqSAT.Entails]
e_decide [constructor, in RocqSAT.Entails]
e_intro [constructor, in RocqSAT.Entails]

F

fail [constructor, in RocqSAT.Trans]
FailLt [inductive, in RocqSAT.Termination]
FailLt_sind [definition, in RocqSAT.Termination]
FailLt_ind [definition, in RocqSAT.Termination]
fail_predecessor [lemma, in RocqSAT.Trans]
fail_final [lemma, in RocqSAT.Trans]
Final [definition, in RocqSAT.Trans]
FinalB [definition, in RocqSAT.Trans]
final_unsat_refl [lemma, in RocqSAT.Satisfiability]
final_sat_refl [lemma, in RocqSAT.Satisfiability]
final_model [lemma, in RocqSAT.Satisfiability]
final_exists [lemma, in RocqSAT.Satisfiability]
final__final_b [lemma, in RocqSAT.Trans]
find_decision_exists [lemma, in RocqSAT.Strategy]
find_undef_l_exists [lemma, in RocqSAT.Strategy]
find_undef_l_undef [lemma, in RocqSAT.Strategy]
find_undef_l_in_c [lemma, in RocqSAT.Strategy]
find_decision_decomp [lemma, in RocqSAT.Strategy]
find_unit_conflicting [lemma, in RocqSAT.Strategy]
find_decision_bounded [lemma, in RocqSAT.Strategy]
find_decision_undef [lemma, in RocqSAT.Strategy]
find_decision [definition, in RocqSAT.Strategy]
find_undef_l_def [lemma, in RocqSAT.Strategy]
find_undef_l [definition, in RocqSAT.Strategy]
find_unit_bounded [lemma, in RocqSAT.Strategy]
find_unit_c_in_f [lemma, in RocqSAT.Strategy]
find_unit_l_in_c [lemma, in RocqSAT.Strategy]
find_unit_l_l_in_c [lemma, in RocqSAT.Strategy]
find_unit_undef [lemma, in RocqSAT.Strategy]
find_unit [definition, in RocqSAT.Strategy]
find_unit_l [definition, in RocqSAT.Strategy]
find_conflict_exists_iff [lemma, in RocqSAT.Strategy]
find_conflict_conflicting [lemma, in RocqSAT.Strategy]
find_conflict_c_in_f [lemma, in RocqSAT.Strategy]
find_conflict [definition, in RocqSAT.Strategy]
f_eval_true_extend [lemma, in RocqSAT.Evaluation]
f_eval_true_iff [lemma, in RocqSAT.Evaluation]
f_eval_false_extend [lemma, in RocqSAT.Evaluation]
f_eval_false_iff [lemma, in RocqSAT.Evaluation]
f_eval [definition, in RocqSAT.Evaluation]
f_totalize_all_def [lemma, in RocqSAT.Normalization]
f_totalize_f [lemma, in RocqSAT.Normalization]
f_totalize_c [lemma, in RocqSAT.Normalization]
f_totalize_l [lemma, in RocqSAT.Normalization]
f_eval_extend_undef [lemma, in RocqSAT.Normalization]
f_eval_cons [lemma, in RocqSAT.Normalization]
f_totalize [definition, in RocqSAT.Normalization]
f_fail [constructor, in RocqSAT.Termination]

H

hd_less [constructor, in RocqSAT.Termination]

I

incl_dedupe [lemma, in RocqSAT.Dedupe]
initial_refl [lemma, in RocqSAT.Trans]
initial_wf [lemma, in RocqSAT.Trans]
inspect [definition, in RocqSAT.Inspect]
Inspect [library]
involutive [lemma, in RocqSAT.Neg]
is_undefined_l [definition, in RocqSAT.Strategy]
is_conflict [definition, in RocqSAT.Strategy]

L

list_to_sum [definition, in RocqSAT.Termination]
Lit [inductive, in RocqSAT.Lit]
Lit [library]
Lit_sind [definition, in RocqSAT.Lit]
Lit_rec [definition, in RocqSAT.Lit]
Lit_ind [definition, in RocqSAT.Lit]
Lit_rect [definition, in RocqSAT.Lit]
l_in_c_false_iff [lemma, in RocqSAT.Clause]
l_in_c_true_iff [lemma, in RocqSAT.Clause]
l_in_c [definition, in RocqSAT.Clause]
l_remove_in_iff [lemma, in RocqSAT.Clause]
l_remove [definition, in RocqSAT.Clause]
l_eval_nodup_extend [lemma, in RocqSAT.Entails]
l_in_f_false_iff [lemma, in RocqSAT.CNF]
l_in_f_true_iff [lemma, in RocqSAT.CNF]
l_in_f [definition, in RocqSAT.CNF]
l_eval_head [lemma, in RocqSAT.Evaluation]
l_eval_true_extend [lemma, in RocqSAT.Evaluation]
l_eval_false_extend [lemma, in RocqSAT.Evaluation]
l_eval_false_in [lemma, in RocqSAT.Evaluation]
l_eval_some_iff [lemma, in RocqSAT.Evaluation]
l_eval_neg_some_iff [lemma, in RocqSAT.Evaluation]
l_eval_neg_none_iff [lemma, in RocqSAT.Evaluation]
l_eval [definition, in RocqSAT.Evaluation]
l_eval_extend_undef [lemma, in RocqSAT.Normalization]

M

max_atom_f_le [lemma, in RocqSAT.Termination]
max_atom_c_le [lemma, in RocqSAT.Termination]
max_atom_f [definition, in RocqSAT.Termination]
max_atom_c [definition, in RocqSAT.Termination]
Model [definition, in RocqSAT.Satisfiability]
m_eval_nodup_extend' [lemma, in RocqSAT.Entails]
m_eval_nodup_extend [lemma, in RocqSAT.Entails]
m_eval_nodup_refl [lemma, in RocqSAT.Entails]
m_eval_head_refl [lemma, in RocqSAT.Evaluation]
m_eval_transfer_c [lemma, in RocqSAT.Evaluation]
m_eval_transfer_l [lemma, in RocqSAT.Evaluation]
m_eval_true_iff [lemma, in RocqSAT.Evaluation]
m_eval [definition, in RocqSAT.Evaluation]
m_eval_extend_undef [lemma, in RocqSAT.Normalization]

N

Neg [constructor, in RocqSAT.Lit]
neg [definition, in RocqSAT.Neg]
Neg [library]
neqb_of [definition, in RocqSAT.Dedupe]
next_state_strategy [lemma, in RocqSAT.Strategy]
next_state_exists [lemma, in RocqSAT.Strategy]
next_state_sound [lemma, in RocqSAT.Strategy]
next_state [definition, in RocqSAT.Strategy]
NoDecisions [definition, in RocqSAT.Evaluation]
NoDuplicates [definition, in RocqSAT.WellFormed]
nodup_cons [lemma, in RocqSAT.WellFormed]
nodup_cons__undef [lemma, in RocqSAT.WellFormed]
nodup_app__nodup' [lemma, in RocqSAT.WellFormed]
nodup_app__nodup [lemma, in RocqSAT.WellFormed]
nodup_cons__nodup' [lemma, in RocqSAT.WellFormed]
nodup_cons__nodup [lemma, in RocqSAT.WellFormed]
Normalization [library]
normalize [definition, in RocqSAT.Normalization]
normalize_derivation [lemma, in RocqSAT.Normalization]
normalize_derivation_aux [lemma, in RocqSAT.Normalization]
normalize_wf [lemma, in RocqSAT.Normalization]
normalize_no_duplicates [lemma, in RocqSAT.Normalization]
normalize_bounded [lemma, in RocqSAT.Normalization]
normalize_only_dec [lemma, in RocqSAT.Normalization]
normalize_all_def [lemma, in RocqSAT.Normalization]
normalize_f [lemma, in RocqSAT.Normalization]
no_decisions_tail' [lemma, in RocqSAT.Entails]
no_decisions_tail [lemma, in RocqSAT.Entails]

P

PA [definition, in RocqSAT.Evaluation]
pigeon [lemma, in RocqSAT.Termination]
Pos [constructor, in RocqSAT.Lit]
PrefixLt [inductive, in RocqSAT.Termination]
PrefixLt_sind [definition, in RocqSAT.Termination]
PrefixLt_ind [definition, in RocqSAT.Termination]
prefix_app [lemma, in RocqSAT.Termination]
prefix_prop [lemma, in RocqSAT.Termination]
prefix_prefix [lemma, in RocqSAT.Termination]
prefix_shift [lemma, in RocqSAT.Termination]
prefix_postfix [lemma, in RocqSAT.Termination]
prefix_repeat [lemma, in RocqSAT.Termination]
prop [constructor, in RocqSAT.Evaluation]
p_tail [constructor, in RocqSAT.Termination]
p_head [constructor, in RocqSAT.Termination]

S

Sat [definition, in RocqSAT.Satisfiability]
Satisfiability [library]
sat_decidable [lemma, in RocqSAT.Satisfiability]
score [definition, in RocqSAT.Termination]
ScoreExamples [module, in RocqSAT.Termination]
ScoreExamples.score_total_4 [definition, in RocqSAT.Termination]
ScoreExamples.score_total_3 [definition, in RocqSAT.Termination]
ScoreExamples.score_total_2 [definition, in RocqSAT.Termination]
ScoreExamples.score_total_1 [definition, in RocqSAT.Termination]
ScoreExamples.score_4 [definition, in RocqSAT.Termination]
ScoreExamples.score_3 [definition, in RocqSAT.Termination]
ScoreExamples.score_2 [definition, in RocqSAT.Termination]
ScoreExamples.score_1 [definition, in RocqSAT.Termination]
score_aux_split [lemma, in RocqSAT.Termination]
score_dec [lemma, in RocqSAT.Termination]
score_aux_in_le [lemma, in RocqSAT.Termination]
score_aux_length_le [lemma, in RocqSAT.Termination]
score_aux_length [lemma, in RocqSAT.Termination]
score_total [definition, in RocqSAT.Termination]
score_aux [definition, in RocqSAT.Termination]
self_neqb_neg [lemma, in RocqSAT.Neg]
self_neq_neg [lemma, in RocqSAT.Neg]
solve [definition, in RocqSAT.Solve]
Solve [section, in RocqSAT.Solve]
Solve [library]
solve_final_derivation [lemma, in RocqSAT.Solve]
solve_aux [definition, in RocqSAT.Solve]
Solve.f [variable, in RocqSAT.Solve]
Solve.Hstrat [variable, in RocqSAT.Solve]
Solve.next [variable, in RocqSAT.Solve]
split_none_iff [lemma, in RocqSAT.Strategy]
split_decomp [lemma, in RocqSAT.Strategy]
split_last_decision [definition, in RocqSAT.Strategy]
state [constructor, in RocqSAT.Trans]
State [inductive, in RocqSAT.Trans]
StateLexLt [definition, in RocqSAT.Termination]
StateLt [definition, in RocqSAT.Termination]
StateLtTransClos [definition, in RocqSAT.Termination]
statelt_incl [lemma, in RocqSAT.Termination]
State_sind [definition, in RocqSAT.Trans]
State_rec [definition, in RocqSAT.Trans]
State_ind [definition, in RocqSAT.Trans]
State_rect [definition, in RocqSAT.Trans]
state_measure [definition, in RocqSAT.Termination]
Strategy [definition, in RocqSAT.Strategy]
Strategy [library]
strategy_trans [lemma, in RocqSAT.Strategy]

T

tb_backtrack [constructor, in RocqSAT.Trans]
tb_decide [constructor, in RocqSAT.Trans]
tb_fail [constructor, in RocqSAT.Trans]
Termination [library]
tl_less [constructor, in RocqSAT.Termination]
Total [definition, in RocqSAT.Satisfiability]
TotalLt [definition, in RocqSAT.Termination]
total_decide [lemma, in RocqSAT.Termination]
to_statelt0' [lemma, in RocqSAT.Termination]
to_statelt0 [lemma, in RocqSAT.Termination]
to_statelt' [lemma, in RocqSAT.Termination]
to_statelt [lemma, in RocqSAT.Termination]
Trans [inductive, in RocqSAT.Trans]
Trans [library]
TransB [inductive, in RocqSAT.Trans]
TransB_sind [definition, in RocqSAT.Trans]
TransB_ind [definition, in RocqSAT.Trans]
trans_same_formula [lemma, in RocqSAT.Trans]
Trans_sind [definition, in RocqSAT.Trans]
Trans_ind [definition, in RocqSAT.Trans]
trans_entails [lemma, in RocqSAT.Entails]
trans__state_lt [lemma, in RocqSAT.Termination]
t_pure [constructor, in RocqSAT.Trans]
t_backtrack [constructor, in RocqSAT.Trans]
t_decide [constructor, in RocqSAT.Trans]
t_unit [constructor, in RocqSAT.Trans]
t_fail [constructor, in RocqSAT.Trans]

U

Undef [definition, in RocqSAT.Evaluation]
undef_decision_exists [lemma, in RocqSAT.Strategy]
undef_remove_false__undef [lemma, in RocqSAT.Evaluation]
Unsat [definition, in RocqSAT.Satisfiability]

W

WellFormed [definition, in RocqSAT.WellFormed]
WellFormed [library]
WfInclusion [section, in RocqSAT.Termination]
WfInclusion.A [variable, in RocqSAT.Termination]
WfInclusion.R1 [variable, in RocqSAT.Termination]
WfInclusion.R2 [variable, in RocqSAT.Termination]
wf_decide [lemma, in RocqSAT.Strategy]
wf_unit [lemma, in RocqSAT.Strategy]
wf_backtrack [lemma, in RocqSAT.Strategy]
wf_app__wf [lemma, in RocqSAT.WellFormed]
wf_cons__wf [lemma, in RocqSAT.WellFormed]
wf_strict_derivation [instance, in RocqSAT.Solve]
wf_strict_derivation [lemma, in RocqSAT.Termination]
wf_trans [lemma, in RocqSAT.Termination]
wf_trans0 [lemma, in RocqSAT.Termination]
wf_length_le [lemma, in RocqSAT.Termination]
wf_le [lemma, in RocqSAT.Termination]
wf_state_lt_trans_clos [lemma, in RocqSAT.Termination]
wf_state_lt [lemma, in RocqSAT.Termination]
wf_state_lex_lt [lemma, in RocqSAT.Termination]
wf_total_lt [lemma, in RocqSAT.Termination]
wf_prefix_lt [lemma, in RocqSAT.Termination]
wf_bcll [lemma, in RocqSAT.Termination]
wf_fail_lt [lemma, in RocqSAT.Termination]

other

_ =? _ (atom_scope) [notation, in RocqSAT.Atom]
_ =? _ (lit_scope) [notation, in RocqSAT.Lit]
¬ _ (neg_scope) [notation, in RocqSAT.Neg]
_ ++p _ (pa_scope) [notation, in RocqSAT.Evaluation]
_ ++d _ (pa_scope) [notation, in RocqSAT.Evaluation]
_ ++a _ (pa_scope) [notation, in RocqSAT.Evaluation]
_ ==>+ _ (trans_scope) [notation, in RocqSAT.Trans]
_ ==>* _ (trans_scope) [notation, in RocqSAT.Trans]
_ ==>b _ (trans_scope) [notation, in RocqSAT.Trans]
_ ==> _ (trans_scope) [notation, in RocqSAT.Trans]
_ eqn : _ [notation, in RocqSAT.Inspect]
_ >>+[ _ ] _ [notation, in RocqSAT.Termination]
_ >>[ _ ] _ [notation, in RocqSAT.Termination]

Notation Index

other

_ =? _ (atom_scope) [in RocqSAT.Atom]
_ =? _ (lit_scope) [in RocqSAT.Lit]
¬ _ (neg_scope) [in RocqSAT.Neg]
_ ++p _ (pa_scope) [in RocqSAT.Evaluation]
_ ++d _ (pa_scope) [in RocqSAT.Evaluation]
_ ++a _ (pa_scope) [in RocqSAT.Evaluation]
_ ==>+ _ (trans_scope) [in RocqSAT.Trans]
_ ==>* _ (trans_scope) [in RocqSAT.Trans]
_ ==>b _ (trans_scope) [in RocqSAT.Trans]
_ ==> _ (trans_scope) [in RocqSAT.Trans]
_ eqn : _ [in RocqSAT.Inspect]
_ >>+[ _ ] _ [in RocqSAT.Termination]
_ >>[ _ ] _ [in RocqSAT.Termination]

Module Index

E

EvalExamples [in RocqSAT.Evaluation]

S

ScoreExamples [in RocqSAT.Termination]

Variable Index

D

dedupe_by.eq [in RocqSAT.Dedupe]
dedupe_by.A [in RocqSAT.Dedupe]

S

Solve.f [in RocqSAT.Solve]
Solve.Hstrat [in RocqSAT.Solve]
Solve.next [in RocqSAT.Solve]

W

WfInclusion.A [in RocqSAT.Termination]
WfInclusion.R1 [in RocqSAT.Termination]
WfInclusion.R2 [in RocqSAT.Termination]

Library Index

A

Atom

C

Clause
CNF

D

Dedupe

E

Entails
Evaluation

I

L

Lit

N

Neg
Normalization

S

Satisfiability
Solve
Strategy

T

Termination
Trans

W

Lemma Index

A

Acc_incl' [in RocqSAT.Termination]

B

bcll__prefix_lt [in RocqSAT.Termination]
bounded_cons [in RocqSAT.WellFormed]
bounded_incl [in RocqSAT.WellFormed]
bounded_app__bounded [in RocqSAT.WellFormed]
bounded_cons__bounded [in RocqSAT.WellFormed]
bound_all_def [in RocqSAT.Normalization]
bound_only_dec [in RocqSAT.Normalization]
bound_incl [in RocqSAT.Normalization]
bound_bounded [in RocqSAT.Normalization]
bound_f [in RocqSAT.Normalization]
bound_f_aux [in RocqSAT.Normalization]
bound_c [in RocqSAT.Normalization]
bound_c_aux [in RocqSAT.Normalization]
bound_l [in RocqSAT.Normalization]

C

cll_incl [in RocqSAT.Termination]
clos_nf' [in RocqSAT.Termination]
clos_nf0 [in RocqSAT.Termination]
clos_nf [in RocqSAT.Termination]
clos_refl_trans_flip [in RocqSAT.Termination]
clos_trans_flip [in RocqSAT.Termination]
convert_prop_all_def [in RocqSAT.Normalization]
convert_prop_only_dec [in RocqSAT.Normalization]
convert_prop_f [in RocqSAT.Normalization]
convert_prop_c [in RocqSAT.Normalization]
convert_prop_l [in RocqSAT.Normalization]
c_eval_true_extend [in RocqSAT.Evaluation]
c_eval_nil [in RocqSAT.Evaluation]
c_eval_false_extend [in RocqSAT.Evaluation]
c_eval_remove_none_l [in RocqSAT.Evaluation]
c_eval_remove_false_l [in RocqSAT.Evaluation]
c_eval_none_iff [in RocqSAT.Evaluation]
c_eval_false_iff [in RocqSAT.Evaluation]
c_eval_true_iff [in RocqSAT.Evaluation]
c_eval_in [in RocqSAT.Normalization]
c_totalize_all_def [in RocqSAT.Normalization]
c_totalize_f [in RocqSAT.Normalization]
c_totalize_c [in RocqSAT.Normalization]
c_totalize_l [in RocqSAT.Normalization]
c_eval_extend_undef [in RocqSAT.Normalization]

D

dedupe_no_duplicates [in RocqSAT.Normalization]
dedupe_bounded [in RocqSAT.Normalization]
dedupe_only_dec [in RocqSAT.Normalization]
dedupe_all_def [in RocqSAT.Normalization]
dedupe_f [in RocqSAT.Normalization]
dedupe_c [in RocqSAT.Normalization]
dedupe_l [in RocqSAT.Normalization]
dedupe_l_aux [in RocqSAT.Normalization]
def_undef [in RocqSAT.Evaluation]
derivation_same_formula [in RocqSAT.Trans]
derivation_strict_same_formula [in RocqSAT.Trans]
derivation_entails [in RocqSAT.Entails]

E

entailment [in RocqSAT.Entails]
entails_clip [in RocqSAT.Entails]
entails_clip_aux' [in RocqSAT.Entails]
entails_clip_aux [in RocqSAT.Entails]
eqb_neq [in RocqSAT.Lit]
eqb_eq [in RocqSAT.Lit]
eqb_sym [in RocqSAT.Lit]
eqb_refl [in RocqSAT.Lit]
eqb_compat [in RocqSAT.Neg]
eqb_eq [in RocqSAT.Atom]
eqb_sym [in RocqSAT.Atom]
eqb_refl [in RocqSAT.Atom]
eq_compat [in RocqSAT.Neg]
extract_neqb_iff [in RocqSAT.Normalization]

F

fail_predecessor [in RocqSAT.Trans]
fail_final [in RocqSAT.Trans]
final_unsat_refl [in RocqSAT.Satisfiability]
final_sat_refl [in RocqSAT.Satisfiability]
final_model [in RocqSAT.Satisfiability]
final_exists [in RocqSAT.Satisfiability]
final__final_b [in RocqSAT.Trans]
find_decision_exists [in RocqSAT.Strategy]
find_undef_l_exists [in RocqSAT.Strategy]
find_undef_l_undef [in RocqSAT.Strategy]
find_undef_l_in_c [in RocqSAT.Strategy]
find_decision_decomp [in RocqSAT.Strategy]
find_unit_conflicting [in RocqSAT.Strategy]
find_decision_bounded [in RocqSAT.Strategy]
find_decision_undef [in RocqSAT.Strategy]
find_undef_l_def [in RocqSAT.Strategy]
find_unit_bounded [in RocqSAT.Strategy]
find_unit_c_in_f [in RocqSAT.Strategy]
find_unit_l_in_c [in RocqSAT.Strategy]
find_unit_l_l_in_c [in RocqSAT.Strategy]
find_unit_undef [in RocqSAT.Strategy]
find_conflict_exists_iff [in RocqSAT.Strategy]
find_conflict_conflicting [in RocqSAT.Strategy]
find_conflict_c_in_f [in RocqSAT.Strategy]
f_eval_true_extend [in RocqSAT.Evaluation]
f_eval_true_iff [in RocqSAT.Evaluation]
f_eval_false_extend [in RocqSAT.Evaluation]
f_eval_false_iff [in RocqSAT.Evaluation]
f_totalize_all_def [in RocqSAT.Normalization]
f_totalize_f [in RocqSAT.Normalization]
f_totalize_c [in RocqSAT.Normalization]
f_totalize_l [in RocqSAT.Normalization]
f_eval_extend_undef [in RocqSAT.Normalization]
f_eval_cons [in RocqSAT.Normalization]

I

incl_dedupe [in RocqSAT.Dedupe]
initial_refl [in RocqSAT.Trans]
initial_wf [in RocqSAT.Trans]
involutive [in RocqSAT.Neg]

L

l_in_c_false_iff [in RocqSAT.Clause]
l_in_c_true_iff [in RocqSAT.Clause]
l_remove_in_iff [in RocqSAT.Clause]
l_eval_nodup_extend [in RocqSAT.Entails]
l_in_f_false_iff [in RocqSAT.CNF]
l_in_f_true_iff [in RocqSAT.CNF]
l_eval_head [in RocqSAT.Evaluation]
l_eval_true_extend [in RocqSAT.Evaluation]
l_eval_false_extend [in RocqSAT.Evaluation]
l_eval_false_in [in RocqSAT.Evaluation]
l_eval_some_iff [in RocqSAT.Evaluation]
l_eval_neg_some_iff [in RocqSAT.Evaluation]
l_eval_neg_none_iff [in RocqSAT.Evaluation]
l_eval_extend_undef [in RocqSAT.Normalization]

M

max_atom_f_le [in RocqSAT.Termination]
max_atom_c_le [in RocqSAT.Termination]
m_eval_nodup_extend' [in RocqSAT.Entails]
m_eval_nodup_extend [in RocqSAT.Entails]
m_eval_nodup_refl [in RocqSAT.Entails]
m_eval_head_refl [in RocqSAT.Evaluation]
m_eval_transfer_c [in RocqSAT.Evaluation]
m_eval_transfer_l [in RocqSAT.Evaluation]
m_eval_true_iff [in RocqSAT.Evaluation]
m_eval_extend_undef [in RocqSAT.Normalization]

N

next_state_strategy [in RocqSAT.Strategy]
next_state_exists [in RocqSAT.Strategy]
next_state_sound [in RocqSAT.Strategy]
nodup_cons [in RocqSAT.WellFormed]
nodup_cons__undef [in RocqSAT.WellFormed]
nodup_app__nodup' [in RocqSAT.WellFormed]
nodup_app__nodup [in RocqSAT.WellFormed]
nodup_cons__nodup' [in RocqSAT.WellFormed]
nodup_cons__nodup [in RocqSAT.WellFormed]
normalize_derivation [in RocqSAT.Normalization]
normalize_derivation_aux [in RocqSAT.Normalization]
normalize_wf [in RocqSAT.Normalization]
normalize_no_duplicates [in RocqSAT.Normalization]
normalize_bounded [in RocqSAT.Normalization]
normalize_only_dec [in RocqSAT.Normalization]
normalize_all_def [in RocqSAT.Normalization]
normalize_f [in RocqSAT.Normalization]
no_decisions_tail' [in RocqSAT.Entails]
no_decisions_tail [in RocqSAT.Entails]

P

pigeon [in RocqSAT.Termination]
prefix_app [in RocqSAT.Termination]
prefix_prop [in RocqSAT.Termination]
prefix_prefix [in RocqSAT.Termination]
prefix_shift [in RocqSAT.Termination]
prefix_postfix [in RocqSAT.Termination]
prefix_repeat [in RocqSAT.Termination]

S

sat_decidable [in RocqSAT.Satisfiability]
score_aux_split [in RocqSAT.Termination]
score_dec [in RocqSAT.Termination]
score_aux_in_le [in RocqSAT.Termination]
score_aux_length_le [in RocqSAT.Termination]
score_aux_length [in RocqSAT.Termination]
self_neqb_neg [in RocqSAT.Neg]
self_neq_neg [in RocqSAT.Neg]
solve_final_derivation [in RocqSAT.Solve]
split_none_iff [in RocqSAT.Strategy]
split_decomp [in RocqSAT.Strategy]
statelt_incl [in RocqSAT.Termination]
strategy_trans [in RocqSAT.Strategy]

T

total_decide [in RocqSAT.Termination]
to_statelt0' [in RocqSAT.Termination]
to_statelt0 [in RocqSAT.Termination]
to_statelt' [in RocqSAT.Termination]
to_statelt [in RocqSAT.Termination]
trans_same_formula [in RocqSAT.Trans]
trans_entails [in RocqSAT.Entails]
trans__state_lt [in RocqSAT.Termination]

U

undef_decision_exists [in RocqSAT.Strategy]
undef_remove_false__undef [in RocqSAT.Evaluation]

W

wf_decide [in RocqSAT.Strategy]
wf_unit [in RocqSAT.Strategy]
wf_backtrack [in RocqSAT.Strategy]
wf_app__wf [in RocqSAT.WellFormed]
wf_cons__wf [in RocqSAT.WellFormed]
wf_strict_derivation [in RocqSAT.Termination]
wf_trans [in RocqSAT.Termination]
wf_trans0 [in RocqSAT.Termination]
wf_length_le [in RocqSAT.Termination]
wf_le [in RocqSAT.Termination]
wf_state_lt_trans_clos [in RocqSAT.Termination]
wf_state_lt [in RocqSAT.Termination]
wf_state_lex_lt [in RocqSAT.Termination]
wf_total_lt [in RocqSAT.Termination]
wf_prefix_lt [in RocqSAT.Termination]
wf_bcll [in RocqSAT.Termination]
wf_fail_lt [in RocqSAT.Termination]

Constructor Index

D

dec [in RocqSAT.Evaluation]

E

e_irrelevant [in RocqSAT.Entails]
e_decide [in RocqSAT.Entails]
e_intro [in RocqSAT.Entails]

F

fail [in RocqSAT.Trans]
f_fail [in RocqSAT.Termination]

H

hd_less [in RocqSAT.Termination]

N

Neg [in RocqSAT.Lit]

P

Pos [in RocqSAT.Lit]
prop [in RocqSAT.Evaluation]
p_tail [in RocqSAT.Termination]
p_head [in RocqSAT.Termination]

S

state [in RocqSAT.Trans]

T

tb_backtrack [in RocqSAT.Trans]
tb_decide [in RocqSAT.Trans]
tb_fail [in RocqSAT.Trans]
tl_less [in RocqSAT.Termination]
t_pure [in RocqSAT.Trans]
t_backtrack [in RocqSAT.Trans]
t_decide [in RocqSAT.Trans]
t_unit [in RocqSAT.Trans]
t_fail [in RocqSAT.Trans]

Inductive Index

A

Ann [in RocqSAT.Evaluation]

C

cll [in RocqSAT.Termination]

E

Entails [in RocqSAT.Entails]

F

FailLt [in RocqSAT.Termination]

L

Lit [in RocqSAT.Lit]

P

PrefixLt [in RocqSAT.Termination]

S

State [in RocqSAT.Trans]

T

Trans [in RocqSAT.Trans]
TransB [in RocqSAT.Trans]

Instance Index

W

wf_strict_derivation [in RocqSAT.Solve]

Section Index

D

dedupe_by [in RocqSAT.Dedupe]

S

Solve [in RocqSAT.Solve]

W

WfInclusion [in RocqSAT.Termination]

Definition Index

A

Ann_sind [in RocqSAT.Evaluation]
Ann_rec [in RocqSAT.Evaluation]
Ann_ind [in RocqSAT.Evaluation]
Ann_rect [in RocqSAT.Evaluation]
Atom [in RocqSAT.Atom]

B

bcll [in RocqSAT.Termination]
bcll' [in RocqSAT.Termination]
bound [in RocqSAT.Normalization]
Bounded [in RocqSAT.WellFormed]

C

Clause [in RocqSAT.Clause]
cll_sind [in RocqSAT.Termination]
cll_ind [in RocqSAT.Termination]
CNF [in RocqSAT.CNF]
cnf [in RocqSAT.Termination]
Conflicting [in RocqSAT.Evaluation]
convert_prop [in RocqSAT.Normalization]
c_eval [in RocqSAT.Evaluation]
c_totalize [in RocqSAT.Normalization]

D

dedupe [in RocqSAT.Normalization]
dedupe_by [in RocqSAT.Dedupe]
Def [in RocqSAT.Evaluation]
Derivation [in RocqSAT.Trans]
DerivationStrict [in RocqSAT.Trans]

E

Entails_sind [in RocqSAT.Entails]
Entails_ind [in RocqSAT.Entails]
eqb [in RocqSAT.Lit]
eqb [in RocqSAT.Atom]
eqb_by_atom [in RocqSAT.Normalization]
EvalExamples.example_c_eval_3 [in RocqSAT.Evaluation]
EvalExamples.example_c_eval_2 [in RocqSAT.Evaluation]
EvalExamples.example_c_eval_1 [in RocqSAT.Evaluation]
EvalExamples.example_l_eval_3 [in RocqSAT.Evaluation]
EvalExamples.example_l_eval_2 [in RocqSAT.Evaluation]
EvalExamples.example_l_eval_1 [in RocqSAT.Evaluation]
extract [in RocqSAT.Lit]

F

FailLt_sind [in RocqSAT.Termination]
FailLt_ind [in RocqSAT.Termination]
Final [in RocqSAT.Trans]
FinalB [in RocqSAT.Trans]
find_decision [in RocqSAT.Strategy]
find_undef_l [in RocqSAT.Strategy]
find_unit [in RocqSAT.Strategy]
find_unit_l [in RocqSAT.Strategy]
find_conflict [in RocqSAT.Strategy]
f_eval [in RocqSAT.Evaluation]
f_totalize [in RocqSAT.Normalization]

I

inspect [in RocqSAT.Inspect]
is_undefined_l [in RocqSAT.Strategy]
is_conflict [in RocqSAT.Strategy]

L

list_to_sum [in RocqSAT.Termination]
Lit_sind [in RocqSAT.Lit]
Lit_rec [in RocqSAT.Lit]
Lit_ind [in RocqSAT.Lit]
Lit_rect [in RocqSAT.Lit]
l_in_c [in RocqSAT.Clause]
l_remove [in RocqSAT.Clause]
l_in_f [in RocqSAT.CNF]
l_eval [in RocqSAT.Evaluation]

M

max_atom_f [in RocqSAT.Termination]
max_atom_c [in RocqSAT.Termination]
Model [in RocqSAT.Satisfiability]
m_eval [in RocqSAT.Evaluation]

N

neg [in RocqSAT.Neg]
neqb_of [in RocqSAT.Dedupe]
next_state [in RocqSAT.Strategy]
NoDecisions [in RocqSAT.Evaluation]
NoDuplicates [in RocqSAT.WellFormed]
normalize [in RocqSAT.Normalization]

P

PA [in RocqSAT.Evaluation]
PrefixLt_sind [in RocqSAT.Termination]
PrefixLt_ind [in RocqSAT.Termination]

S

Sat [in RocqSAT.Satisfiability]
score [in RocqSAT.Termination]
ScoreExamples.score_total_4 [in RocqSAT.Termination]
ScoreExamples.score_total_3 [in RocqSAT.Termination]
ScoreExamples.score_total_2 [in RocqSAT.Termination]
ScoreExamples.score_total_1 [in RocqSAT.Termination]
ScoreExamples.score_4 [in RocqSAT.Termination]
ScoreExamples.score_3 [in RocqSAT.Termination]
ScoreExamples.score_2 [in RocqSAT.Termination]
ScoreExamples.score_1 [in RocqSAT.Termination]
score_total [in RocqSAT.Termination]
score_aux [in RocqSAT.Termination]
solve [in RocqSAT.Solve]
solve_aux [in RocqSAT.Solve]
split_last_decision [in RocqSAT.Strategy]
StateLexLt [in RocqSAT.Termination]
StateLt [in RocqSAT.Termination]
StateLtTransClos [in RocqSAT.Termination]
State_sind [in RocqSAT.Trans]
State_rec [in RocqSAT.Trans]
State_ind [in RocqSAT.Trans]
State_rect [in RocqSAT.Trans]
state_measure [in RocqSAT.Termination]
Strategy [in RocqSAT.Strategy]

T

Total [in RocqSAT.Satisfiability]
TotalLt [in RocqSAT.Termination]
TransB_sind [in RocqSAT.Trans]
TransB_ind [in RocqSAT.Trans]
Trans_sind [in RocqSAT.Trans]
Trans_ind [in RocqSAT.Trans]

U

Undef [in RocqSAT.Evaluation]
Unsat [in RocqSAT.Satisfiability]

W

WellFormed [in RocqSAT.WellFormed]

Global Index

G

J

K

O

Q

R

V

X

Y

Z

_

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

_

(13 entries)

Module Index

A

B

C

D

F

G

H

I

J

K

L

M

N

O

P

Q

R

T

U

V

W

X

Y

Z

_

other

(2 entries)

Variable Index

A

B

C

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

T

U

V

X

Y

Z

_

other

(8 entries)

Library Index

B

F

G

H

J

K

M

O

P

Q

R

U

V

X

Y

Z

_

other

(16 entries)

Lemma Index

G

H

J

K

O

Q

R

V

X

Y

Z

_

other

(194 entries)

Constructor Index

A

B

C

G

I

J

K

L

M

O

Q

R

U

V

W

X

Y

Z

_

other

(22 entries)

Inductive Index

B

D

G

H

I

J

K

M

N

O

Q

R

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

X

Y

Z

_

other

(1 entry)

Section Index

A

B

C

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

T

U

V

X

Y

Z

_

other

(3 entries)

Definition Index

G

H

J

K

O

Q

R

V

X

Y

Z

_

other

(104 entries)

This page has been generated by coqdoc