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

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

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

(1 entry)

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

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

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

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

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

(7 entries)

Projection Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(11 entries)

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

(8 entries)

Abbreviation Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

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

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

(4 entries)

---

Global Index

A

axABBA [lemma, in testfree-PDL.testfree_PDL_def]
axCh [constructor, in testfree-PDL.testfree_PDL_def]
axChEl [constructor, in testfree-PDL.testfree_PDL_def]
axChEr [constructor, in testfree-PDL.testfree_PDL_def]
axCon [constructor, in testfree-PDL.testfree_PDL_def]
axConE [constructor, in testfree-PDL.testfree_PDL_def]
axDBD [lemma, in testfree-PDL.testfree_PDL_def]
axDN [constructor, in testfree-PDL.testfree_PDL_def]
axEOOE [lemma, in testfree-PDL.testfree_PDL_def]
axK [constructor, in testfree-PDL.testfree_PDL_def]
axN [constructor, in testfree-PDL.testfree_PDL_def]
axnEXF [lemma, in testfree-PDL.testfree_PDL_def]
axS [constructor, in testfree-PDL.testfree_PDL_def]
axStar [lemma, in testfree-PDL.testfree_PDL_def]
axStarEl [constructor, in testfree-PDL.testfree_PDL_def]
axStarEr [constructor, in testfree-PDL.testfree_PDL_def]
ax_cons [lemma, in testfree-PDL.hilbert_ref]

B

baseP [lemma, in testfree-PDL.hilbert_ref]
baseP0 [lemma, in testfree-PDL.hilbert_ref]
bigABBA [lemma, in testfree-PDL.testfree_PDL_def]
bigEOOE [lemma, in testfree-PDL.testfree_PDL_def]
bigxm [lemma, in testfree-PDL.hilbert_ref]
body [definition, in testfree-PDL.testfree_PDL_def]
box_request [lemma, in testfree-PDL.testfree_PDL_def]

C

clause [definition, in testfree-PDL.testfree_PDL_def]
closed_flipcl [lemma, in testfree-PDL.testfree_PDL_def]
closed_sfc [lemma, in testfree-PDL.testfree_PDL_def]
cls [projection, in testfree-PDL.demo]
cmodel [record, in testfree-PDL.testfree_PDL_def]
CModel [constructor, in testfree-PDL.testfree_PDL_def]
cmodel_of_fmodel [definition, in testfree-PDL.testfree_PDL_def]
completeness [lemma, in testfree-PDL.hilbert_ref]
coref [definition, in testfree-PDL.demo]
corefD1 [lemma, in testfree-PDL.demo]
coref_DD [lemma, in testfree-PDL.demo]

D

DD [definition, in testfree-PDL.demo]
DD_refute [lemma, in testfree-PDL.demo]
demo [record, in testfree-PDL.demo]
Demo [constructor, in testfree-PDL.demo]
demo [library]
demoD0 [projection, in testfree-PDL.demo]
demoD1 [projection, in testfree-PDL.demo]
demo_predType [definition, in testfree-PDL.demo]
demo2reach [lemma, in testfree-PDL.demo]
dmAX [lemma, in testfree-PDL.testfree_PDL_def]
drop_sign [definition, in testfree-PDL.testfree_PDL_def]
D0 [definition, in testfree-PDL.demo]
D1 [definition, in testfree-PDL.demo]

E

eq_form_dec [lemma, in testfree-PDL.testfree_PDL_def]
eq_prg_dec [lemma, in testfree-PDL.testfree_PDL_def]
eval [definition, in testfree-PDL.testfree_PDL_def]
evalb [definition, in testfree-PDL.testfree_PDL_def]
evalP [lemma, in testfree-PDL.testfree_PDL_def]
EX [definition, in testfree-PDL.testfree_PDL_def]

F

fAX [constructor, in testfree-PDL.testfree_PDL_def]
fF [constructor, in testfree-PDL.testfree_PDL_def]
fImp [constructor, in testfree-PDL.testfree_PDL_def]
FiniteModels [section, in testfree-PDL.testfree_PDL_def]
FiniteModels.M [variable, in testfree-PDL.testfree_PDL_def]
finite_soundness [lemma, in testfree-PDL.testfree_PDL_def]
fin_modelP [lemma, in testfree-PDL.testfree_PDL_def]
flabel [projection, in testfree-PDL.testfree_PDL_def]
flip [definition, in testfree-PDL.testfree_PDL_def]
flipcl [definition, in testfree-PDL.testfree_PDL_def]
flipcl_refl [lemma, in testfree-PDL.testfree_PDL_def]
flip_closed [definition, in testfree-PDL.testfree_PDL_def]
flip_drop_sign [lemma, in testfree-PDL.testfree_PDL_def]
fmodel [record, in testfree-PDL.testfree_PDL_def]
FModel [constructor, in testfree-PDL.testfree_PDL_def]
form [inductive, in testfree-PDL.testfree_PDL_def]
formChoice [module, in testfree-PDL.testfree_PDL_def]
formChoice.pickle [definition, in testfree-PDL.testfree_PDL_def]
formChoice.pickleP [lemma, in testfree-PDL.testfree_PDL_def]
formChoice.pickle_prgP [lemma, in testfree-PDL.testfree_PDL_def]
formChoice.pickle_prg [definition, in testfree-PDL.testfree_PDL_def]
formChoice.unpickle [definition, in testfree-PDL.testfree_PDL_def]
formChoice.unpickle_prg [definition, in testfree-PDL.testfree_PDL_def]
form_CountType [definition, in testfree-PDL.testfree_PDL_def]
form_ChoiceType [definition, in testfree-PDL.testfree_PDL_def]
form_choiceMixin [definition, in testfree-PDL.testfree_PDL_def]
form_countMixin [definition, in testfree-PDL.testfree_PDL_def]
form_eqType [definition, in testfree-PDL.testfree_PDL_def]
form_eqMixin [definition, in testfree-PDL.testfree_PDL_def]
fstate [projection, in testfree-PDL.testfree_PDL_def]
ftrans [projection, in testfree-PDL.testfree_PDL_def]
fV [constructor, in testfree-PDL.testfree_PDL_def]
f_size [definition, in testfree-PDL.testfree_PDL_def]

H

Hilbert [section, in testfree-PDL.testfree_PDL_def]
hilbert_ref [library]
_ ---> _ [notation, in testfree-PDL.testfree_PDL_def]
hintikka [definition, in testfree-PDL.testfree_PDL_def]
Hintikka [section, in testfree-PDL.testfree_PDL_def]
hintikka' [definition, in testfree-PDL.testfree_PDL_def]
Hintikka.C [variable, in testfree-PDL.testfree_PDL_def]
Hintikka.F [variable, in testfree-PDL.testfree_PDL_def]
Hintikka.hint_C [variable, in testfree-PDL.testfree_PDL_def]
Hintikka.sfc_F [variable, in testfree-PDL.testfree_PDL_def]
hint_dia_star [lemma, in testfree-PDL.testfree_PDL_def]
hint_box_star [lemma, in testfree-PDL.testfree_PDL_def]
hint_dia_ch [lemma, in testfree-PDL.testfree_PDL_def]
hint_box_ch [lemma, in testfree-PDL.testfree_PDL_def]
hint_box_con [lemma, in testfree-PDL.testfree_PDL_def]
hint_imp_neg [lemma, in testfree-PDL.testfree_PDL_def]
hint_imp_pos [lemma, in testfree-PDL.testfree_PDL_def]
hint_eval [lemma, in testfree-PDL.demo]
hint_reach_pos [lemma, in testfree-PDL.demo]
href_of [lemma, in testfree-PDL.hilbert_ref]

I

informative_completeness [lemma, in testfree-PDL.hilbert_ref]
interp [definition, in testfree-PDL.testfree_PDL_def]
isBox [definition, in testfree-PDL.testfree_PDL_def]
isBoxP [lemma, in testfree-PDL.testfree_PDL_def]
isBox_false [constructor, in testfree-PDL.testfree_PDL_def]
isBox_true [constructor, in testfree-PDL.testfree_PDL_def]
isBox_spec [inductive, in testfree-PDL.testfree_PDL_def]
isDia [definition, in testfree-PDL.testfree_PDL_def]
isDiaP [lemma, in testfree-PDL.testfree_PDL_def]
isDia_false [constructor, in testfree-PDL.testfree_PDL_def]
isDia_true [constructor, in testfree-PDL.testfree_PDL_def]
isDia_spec [inductive, in testfree-PDL.testfree_PDL_def]

L

label [projection, in testfree-PDL.testfree_PDL_def]
LCF [lemma, in testfree-PDL.demo]
lcons [definition, in testfree-PDL.testfree_PDL_def]
ldec [definition, in testfree-PDL.testfree_PDL_def]
LI_sound [lemma, in testfree-PDL.testfree_PDL_def]

M

maximal [definition, in testfree-PDL.testfree_PDL_def]
Mlabel [definition, in testfree-PDL.demo]
ModelExistience [section, in testfree-PDL.demo]
ModelExistience.S [variable, in testfree-PDL.demo]
modelP [projection, in testfree-PDL.testfree_PDL_def]
model_of [definition, in testfree-PDL.demo]
Mtrans [definition, in testfree-PDL.demo]
Mtype [definition, in testfree-PDL.demo]

N

negative [definition, in testfree-PDL.testfree_PDL_def]
negatives [definition, in testfree-PDL.testfree_PDL_def]
negE [lemma, in testfree-PDL.testfree_PDL_def]
neg_or [lemma, in testfree-PDL.hilbert_ref]
neq_contra [lemma, in testfree-PDL.hilbert_ref]
not_hint_max [lemma, in testfree-PDL.hilbert_ref]
nsub_contra [lemma, in testfree-PDL.hilbert_ref]

O

or_S [lemma, in testfree-PDL.hilbert_ref]

P

pCh [constructor, in testfree-PDL.testfree_PDL_def]
pCon [constructor, in testfree-PDL.testfree_PDL_def]
pcond [definition, in testfree-PDL.demo]
posE [lemma, in testfree-PDL.testfree_PDL_def]
positive [definition, in testfree-PDL.testfree_PDL_def]
positives [definition, in testfree-PDL.testfree_PDL_def]
prg [inductive, in testfree-PDL.testfree_PDL_def]
prune_D1 [lemma, in testfree-PDL.demo]
prune_D0 [lemma, in testfree-PDL.demo]
Pruning [section, in testfree-PDL.demo]
pruning_completeness [lemma, in testfree-PDL.demo]
Pruning.F [variable, in testfree-PDL.demo]
Pruning.sfc_F [variable, in testfree-PDL.demo]
_ |> _ [notation, in testfree-PDL.demo]
prv [inductive, in testfree-PDL.testfree_PDL_def]
prv_dec [lemma, in testfree-PDL.hilbert_ref]
prv_ref_sound [lemma, in testfree-PDL.hilbert_ref]
prv_pSystem [definition, in testfree-PDL.testfree_PDL_def]
prv_mSystem [definition, in testfree-PDL.testfree_PDL_def]
pStar [constructor, in testfree-PDL.testfree_PDL_def]
PU [abbreviation, in testfree-PDL.hilbert_ref]
PU [definition, in testfree-PDL.demo]
pV [constructor, in testfree-PDL.testfree_PDL_def]
p_size [definition, in testfree-PDL.testfree_PDL_def]
P1 [definition, in testfree-PDL.demo]

R

R [definition, in testfree-PDL.testfree_PDL_def]
RE [lemma, in testfree-PDL.testfree_PDL_def]
reach [definition, in testfree-PDL.testfree_PDL_def]
Reachability [section, in testfree-PDL.testfree_PDL_def]
Reachability.e [variable, in testfree-PDL.testfree_PDL_def]
Reachability.f [variable, in testfree-PDL.testfree_PDL_def]
Reachability.fX [variable, in testfree-PDL.testfree_PDL_def]
Reachability.X [variable, in testfree-PDL.testfree_PDL_def]
reachb [definition, in testfree-PDL.testfree_PDL_def]
reachP [lemma, in testfree-PDL.testfree_PDL_def]
reach_demo [definition, in testfree-PDL.demo]
reach2demo [lemma, in testfree-PDL.demo]
ref [definition, in testfree-PDL.hilbert_ref]
ref [inductive, in testfree-PDL.demo]
refE1n [lemma, in testfree-PDL.hilbert_ref]
refI1n [lemma, in testfree-PDL.hilbert_ref]
RefPred [section, in testfree-PDL.hilbert_ref]
RefPred.ContextRefutations [section, in testfree-PDL.hilbert_ref]
RefPred.ContextRefutations.coref_S [variable, in testfree-PDL.hilbert_ref]
RefPred.ContextRefutations.S [variable, in testfree-PDL.hilbert_ref]
RefPred.ContextRefutations.sub_S [variable, in testfree-PDL.hilbert_ref]
RefPred.F [variable, in testfree-PDL.hilbert_ref]
RefPred.sfc_F [variable, in testfree-PDL.hilbert_ref]
rEXn [lemma, in testfree-PDL.testfree_PDL_def]
RinU [lemma, in testfree-PDL.testfree_PDL_def]
rMP [constructor, in testfree-PDL.testfree_PDL_def]
rNec [constructor, in testfree-PDL.testfree_PDL_def]
rNorm [lemma, in testfree-PDL.testfree_PDL_def]
Rpos [lemma, in testfree-PDL.testfree_PDL_def]
rStar_ind [constructor, in testfree-PDL.testfree_PDL_def]
rtrans [definition, in testfree-PDL.demo]
RU [lemma, in testfree-PDL.testfree_PDL_def]
R0 [lemma, in testfree-PDL.testfree_PDL_def]
R1 [lemma, in testfree-PDL.hilbert_ref]
R1 [lemma, in testfree-PDL.testfree_PDL_def]
R1 [constructor, in testfree-PDL.demo]
R2 [lemma, in testfree-PDL.hilbert_ref]
R2 [constructor, in testfree-PDL.demo]
R2_aux [lemma, in testfree-PDL.hilbert_ref]

S

sat [definition, in testfree-PDL.demo]
satA [lemma, in testfree-PDL.testfree_PDL_def]
sat_dec [lemma, in testfree-PDL.hilbert_ref]
sfc [definition, in testfree-PDL.testfree_PDL_def]
sfcU [lemma, in testfree-PDL.testfree_PDL_def]
sfc_bigcup [lemma, in testfree-PDL.testfree_PDL_def]
sfc_ssub [lemma, in testfree-PDL.testfree_PDL_def]
sfc_ssubbox [lemma, in testfree-PDL.testfree_PDL_def]
sform [definition, in testfree-PDL.testfree_PDL_def]
sf_ssub [lemma, in testfree-PDL.testfree_PDL_def]
sf_ssubbox [lemma, in testfree-PDL.testfree_PDL_def]
sf_closed'_mon [lemma, in testfree-PDL.testfree_PDL_def]
sf_closed_box [lemma, in testfree-PDL.testfree_PDL_def]
sf_closed [definition, in testfree-PDL.testfree_PDL_def]
sf_closed' [definition, in testfree-PDL.testfree_PDL_def]
size_flipcl [lemma, in testfree-PDL.testfree_PDL_def]
size_ssub [lemma, in testfree-PDL.testfree_PDL_def]
size_ssubbox [lemma, in testfree-PDL.testfree_PDL_def]
small_models [lemma, in testfree-PDL.hilbert_ref]
soundness [lemma, in testfree-PDL.testfree_PDL_def]
ssub [definition, in testfree-PDL.testfree_PDL_def]
ssubbox [definition, in testfree-PDL.testfree_PDL_def]
ssubbox_refl [lemma, in testfree-PDL.testfree_PDL_def]
ssub_refl [lemma, in testfree-PDL.testfree_PDL_def]
stable [definition, in testfree-PDL.testfree_PDL_def]
star [inductive, in testfree-PDL.testfree_PDL_def]
starb [definition, in testfree-PDL.testfree_PDL_def]
StarL [constructor, in testfree-PDL.testfree_PDL_def]
starP [lemma, in testfree-PDL.testfree_PDL_def]
Star0 [constructor, in testfree-PDL.testfree_PDL_def]
state [projection, in testfree-PDL.testfree_PDL_def]
sts_of [projection, in testfree-PDL.testfree_PDL_def]
sub_sfc [lemma, in testfree-PDL.testfree_PDL_def]
supp [definition, in testfree-PDL.demo]
S0 [abbreviation, in testfree-PDL.hilbert_ref]
S0 [definition, in testfree-PDL.demo]

T

testfree_PDL_def [library]
trans [projection, in testfree-PDL.testfree_PDL_def]
ts [record, in testfree-PDL.testfree_PDL_def]
TS [constructor, in testfree-PDL.testfree_PDL_def]
ts_of_fmodel [definition, in testfree-PDL.testfree_PDL_def]

V

valid [definition, in testfree-PDL.testfree_PDL_def]
valid_dec [lemma, in testfree-PDL.hilbert_ref]
var [definition, in testfree-PDL.testfree_PDL_def]

X

xaf [abbreviation, in testfree-PDL.hilbert_ref]
xm_soundness [lemma, in testfree-PDL.testfree_PDL_def]

other

_ ^+ [notation, in testfree-PDL.testfree_PDL_def]
_ ^- [notation, in testfree-PDL.testfree_PDL_def]
_ + _ [notation, in testfree-PDL.testfree_PDL_def]
_ ;; _ [notation, in testfree-PDL.testfree_PDL_def]
_ ^* [notation, in testfree-PDL.testfree_PDL_def]
_ |> _ [notation, in testfree-PDL.demo]
[ af _ ] [notation, in testfree-PDL.testfree_PDL_def]
[ _ ] _ [notation, in testfree-PDL.testfree_PDL_def]

---

Notation Index

H

_ ---> _ [in testfree-PDL.testfree_PDL_def]

P

_ |> _ [in testfree-PDL.demo]

other

_ ^+ [in testfree-PDL.testfree_PDL_def]
_ ^- [in testfree-PDL.testfree_PDL_def]
_ + _ [in testfree-PDL.testfree_PDL_def]
_ ;; _ [in testfree-PDL.testfree_PDL_def]
_ ^* [in testfree-PDL.testfree_PDL_def]
_ |> _ [in testfree-PDL.demo]
[ af _ ] [in testfree-PDL.testfree_PDL_def]
[ _ ] _ [in testfree-PDL.testfree_PDL_def]

---

Module Index

F

formChoice [in testfree-PDL.testfree_PDL_def]

---

Variable Index

F

FiniteModels.M [in testfree-PDL.testfree_PDL_def]

H

Hintikka.C [in testfree-PDL.testfree_PDL_def]
Hintikka.F [in testfree-PDL.testfree_PDL_def]
Hintikka.hint_C [in testfree-PDL.testfree_PDL_def]
Hintikka.sfc_F [in testfree-PDL.testfree_PDL_def]

M

ModelExistience.S [in testfree-PDL.demo]

P

Pruning.F [in testfree-PDL.demo]
Pruning.sfc_F [in testfree-PDL.demo]

R

Reachability.e [in testfree-PDL.testfree_PDL_def]
Reachability.f [in testfree-PDL.testfree_PDL_def]
Reachability.fX [in testfree-PDL.testfree_PDL_def]
Reachability.X [in testfree-PDL.testfree_PDL_def]
RefPred.ContextRefutations.coref_S [in testfree-PDL.hilbert_ref]
RefPred.ContextRefutations.S [in testfree-PDL.hilbert_ref]
RefPred.ContextRefutations.sub_S [in testfree-PDL.hilbert_ref]
RefPred.F [in testfree-PDL.hilbert_ref]
RefPred.sfc_F [in testfree-PDL.hilbert_ref]

---

Library Index

D

demo

H

hilbert_ref

T

testfree_PDL_def

---

Lemma Index

A

axABBA [in testfree-PDL.testfree_PDL_def]
axDBD [in testfree-PDL.testfree_PDL_def]
axEOOE [in testfree-PDL.testfree_PDL_def]
axnEXF [in testfree-PDL.testfree_PDL_def]
axStar [in testfree-PDL.testfree_PDL_def]
ax_cons [in testfree-PDL.hilbert_ref]

B

baseP [in testfree-PDL.hilbert_ref]
baseP0 [in testfree-PDL.hilbert_ref]
bigABBA [in testfree-PDL.testfree_PDL_def]
bigEOOE [in testfree-PDL.testfree_PDL_def]
bigxm [in testfree-PDL.hilbert_ref]
box_request [in testfree-PDL.testfree_PDL_def]

C

closed_flipcl [in testfree-PDL.testfree_PDL_def]
closed_sfc [in testfree-PDL.testfree_PDL_def]
completeness [in testfree-PDL.hilbert_ref]
corefD1 [in testfree-PDL.demo]
coref_DD [in testfree-PDL.demo]

D

DD_refute [in testfree-PDL.demo]
demo2reach [in testfree-PDL.demo]
dmAX [in testfree-PDL.testfree_PDL_def]

E

eq_form_dec [in testfree-PDL.testfree_PDL_def]
eq_prg_dec [in testfree-PDL.testfree_PDL_def]
evalP [in testfree-PDL.testfree_PDL_def]

F

finite_soundness [in testfree-PDL.testfree_PDL_def]
fin_modelP [in testfree-PDL.testfree_PDL_def]
flipcl_refl [in testfree-PDL.testfree_PDL_def]
flip_drop_sign [in testfree-PDL.testfree_PDL_def]
formChoice.pickleP [in testfree-PDL.testfree_PDL_def]
formChoice.pickle_prgP [in testfree-PDL.testfree_PDL_def]

H

hint_dia_star [in testfree-PDL.testfree_PDL_def]
hint_box_star [in testfree-PDL.testfree_PDL_def]
hint_dia_ch [in testfree-PDL.testfree_PDL_def]
hint_box_ch [in testfree-PDL.testfree_PDL_def]
hint_box_con [in testfree-PDL.testfree_PDL_def]
hint_imp_neg [in testfree-PDL.testfree_PDL_def]
hint_imp_pos [in testfree-PDL.testfree_PDL_def]
hint_eval [in testfree-PDL.demo]
hint_reach_pos [in testfree-PDL.demo]
href_of [in testfree-PDL.hilbert_ref]

I

informative_completeness [in testfree-PDL.hilbert_ref]
isBoxP [in testfree-PDL.testfree_PDL_def]
isDiaP [in testfree-PDL.testfree_PDL_def]

L

LCF [in testfree-PDL.demo]
LI_sound [in testfree-PDL.testfree_PDL_def]

N

negE [in testfree-PDL.testfree_PDL_def]
neg_or [in testfree-PDL.hilbert_ref]
neq_contra [in testfree-PDL.hilbert_ref]
not_hint_max [in testfree-PDL.hilbert_ref]
nsub_contra [in testfree-PDL.hilbert_ref]

O

or_S [in testfree-PDL.hilbert_ref]

P

posE [in testfree-PDL.testfree_PDL_def]
prune_D1 [in testfree-PDL.demo]
prune_D0 [in testfree-PDL.demo]
pruning_completeness [in testfree-PDL.demo]
prv_dec [in testfree-PDL.hilbert_ref]
prv_ref_sound [in testfree-PDL.hilbert_ref]

R

RE [in testfree-PDL.testfree_PDL_def]
reachP [in testfree-PDL.testfree_PDL_def]
reach2demo [in testfree-PDL.demo]
refE1n [in testfree-PDL.hilbert_ref]
refI1n [in testfree-PDL.hilbert_ref]
rEXn [in testfree-PDL.testfree_PDL_def]
RinU [in testfree-PDL.testfree_PDL_def]
rNorm [in testfree-PDL.testfree_PDL_def]
Rpos [in testfree-PDL.testfree_PDL_def]
RU [in testfree-PDL.testfree_PDL_def]
R0 [in testfree-PDL.testfree_PDL_def]
R1 [in testfree-PDL.hilbert_ref]
R1 [in testfree-PDL.testfree_PDL_def]
R2 [in testfree-PDL.hilbert_ref]
R2_aux [in testfree-PDL.hilbert_ref]

S

satA [in testfree-PDL.testfree_PDL_def]
sat_dec [in testfree-PDL.hilbert_ref]
sfcU [in testfree-PDL.testfree_PDL_def]
sfc_bigcup [in testfree-PDL.testfree_PDL_def]
sfc_ssub [in testfree-PDL.testfree_PDL_def]
sfc_ssubbox [in testfree-PDL.testfree_PDL_def]
sf_ssub [in testfree-PDL.testfree_PDL_def]
sf_ssubbox [in testfree-PDL.testfree_PDL_def]
sf_closed'_mon [in testfree-PDL.testfree_PDL_def]
sf_closed_box [in testfree-PDL.testfree_PDL_def]
size_flipcl [in testfree-PDL.testfree_PDL_def]
size_ssub [in testfree-PDL.testfree_PDL_def]
size_ssubbox [in testfree-PDL.testfree_PDL_def]
small_models [in testfree-PDL.hilbert_ref]
soundness [in testfree-PDL.testfree_PDL_def]
ssubbox_refl [in testfree-PDL.testfree_PDL_def]
ssub_refl [in testfree-PDL.testfree_PDL_def]
starP [in testfree-PDL.testfree_PDL_def]
sub_sfc [in testfree-PDL.testfree_PDL_def]

V

valid_dec [in testfree-PDL.hilbert_ref]

X

xm_soundness [in testfree-PDL.testfree_PDL_def]

---

Constructor Index

A

axCh [in testfree-PDL.testfree_PDL_def]
axChEl [in testfree-PDL.testfree_PDL_def]
axChEr [in testfree-PDL.testfree_PDL_def]
axCon [in testfree-PDL.testfree_PDL_def]
axConE [in testfree-PDL.testfree_PDL_def]
axDN [in testfree-PDL.testfree_PDL_def]
axK [in testfree-PDL.testfree_PDL_def]
axN [in testfree-PDL.testfree_PDL_def]
axS [in testfree-PDL.testfree_PDL_def]
axStarEl [in testfree-PDL.testfree_PDL_def]
axStarEr [in testfree-PDL.testfree_PDL_def]

C

CModel [in testfree-PDL.testfree_PDL_def]

D

Demo [in testfree-PDL.demo]

F

fAX [in testfree-PDL.testfree_PDL_def]
fF [in testfree-PDL.testfree_PDL_def]
fImp [in testfree-PDL.testfree_PDL_def]
FModel [in testfree-PDL.testfree_PDL_def]
fV [in testfree-PDL.testfree_PDL_def]

I

isBox_false [in testfree-PDL.testfree_PDL_def]
isBox_true [in testfree-PDL.testfree_PDL_def]
isDia_false [in testfree-PDL.testfree_PDL_def]
isDia_true [in testfree-PDL.testfree_PDL_def]

P

pCh [in testfree-PDL.testfree_PDL_def]
pCon [in testfree-PDL.testfree_PDL_def]
pStar [in testfree-PDL.testfree_PDL_def]
pV [in testfree-PDL.testfree_PDL_def]

R

rMP [in testfree-PDL.testfree_PDL_def]
rNec [in testfree-PDL.testfree_PDL_def]
rStar_ind [in testfree-PDL.testfree_PDL_def]
R1 [in testfree-PDL.demo]
R2 [in testfree-PDL.demo]

S

StarL [in testfree-PDL.testfree_PDL_def]
Star0 [in testfree-PDL.testfree_PDL_def]

T

TS [in testfree-PDL.testfree_PDL_def]

---

Inductive Index

F

form [in testfree-PDL.testfree_PDL_def]

I

isBox_spec [in testfree-PDL.testfree_PDL_def]
isDia_spec [in testfree-PDL.testfree_PDL_def]

P

prg [in testfree-PDL.testfree_PDL_def]
prv [in testfree-PDL.testfree_PDL_def]

R

ref [in testfree-PDL.demo]

S

star [in testfree-PDL.testfree_PDL_def]

---

Projection Index

C

cls [in testfree-PDL.demo]

D

demoD0 [in testfree-PDL.demo]
demoD1 [in testfree-PDL.demo]

F

flabel [in testfree-PDL.testfree_PDL_def]
fstate [in testfree-PDL.testfree_PDL_def]
ftrans [in testfree-PDL.testfree_PDL_def]

L

label [in testfree-PDL.testfree_PDL_def]

M

modelP [in testfree-PDL.testfree_PDL_def]

S

state [in testfree-PDL.testfree_PDL_def]
sts_of [in testfree-PDL.testfree_PDL_def]

T

trans [in testfree-PDL.testfree_PDL_def]

---

Section Index

F

FiniteModels [in testfree-PDL.testfree_PDL_def]

H

Hilbert [in testfree-PDL.testfree_PDL_def]
Hintikka [in testfree-PDL.testfree_PDL_def]

M

ModelExistience [in testfree-PDL.demo]

P

Pruning [in testfree-PDL.demo]

R

Reachability [in testfree-PDL.testfree_PDL_def]
RefPred [in testfree-PDL.hilbert_ref]
RefPred.ContextRefutations [in testfree-PDL.hilbert_ref]

---

Abbreviation Index

P

PU [in testfree-PDL.hilbert_ref]

S

S0 [in testfree-PDL.hilbert_ref]

X

xaf [in testfree-PDL.hilbert_ref]

---

Definition Index

B

body [in testfree-PDL.testfree_PDL_def]

C

clause [in testfree-PDL.testfree_PDL_def]
cmodel_of_fmodel [in testfree-PDL.testfree_PDL_def]
coref [in testfree-PDL.demo]

D

DD [in testfree-PDL.demo]
demo_predType [in testfree-PDL.demo]
drop_sign [in testfree-PDL.testfree_PDL_def]
D0 [in testfree-PDL.demo]
D1 [in testfree-PDL.demo]

E

eval [in testfree-PDL.testfree_PDL_def]
evalb [in testfree-PDL.testfree_PDL_def]
EX [in testfree-PDL.testfree_PDL_def]

F

flip [in testfree-PDL.testfree_PDL_def]
flipcl [in testfree-PDL.testfree_PDL_def]
flip_closed [in testfree-PDL.testfree_PDL_def]
formChoice.pickle [in testfree-PDL.testfree_PDL_def]
formChoice.pickle_prg [in testfree-PDL.testfree_PDL_def]
formChoice.unpickle [in testfree-PDL.testfree_PDL_def]
formChoice.unpickle_prg [in testfree-PDL.testfree_PDL_def]
form_CountType [in testfree-PDL.testfree_PDL_def]
form_ChoiceType [in testfree-PDL.testfree_PDL_def]
form_choiceMixin [in testfree-PDL.testfree_PDL_def]
form_countMixin [in testfree-PDL.testfree_PDL_def]
form_eqType [in testfree-PDL.testfree_PDL_def]
form_eqMixin [in testfree-PDL.testfree_PDL_def]
f_size [in testfree-PDL.testfree_PDL_def]

H

hintikka [in testfree-PDL.testfree_PDL_def]
hintikka' [in testfree-PDL.testfree_PDL_def]

I

interp [in testfree-PDL.testfree_PDL_def]
isBox [in testfree-PDL.testfree_PDL_def]
isDia [in testfree-PDL.testfree_PDL_def]

L

lcons [in testfree-PDL.testfree_PDL_def]
ldec [in testfree-PDL.testfree_PDL_def]

M

maximal [in testfree-PDL.testfree_PDL_def]
Mlabel [in testfree-PDL.demo]
model_of [in testfree-PDL.demo]
Mtrans [in testfree-PDL.demo]
Mtype [in testfree-PDL.demo]

N

negative [in testfree-PDL.testfree_PDL_def]
negatives [in testfree-PDL.testfree_PDL_def]

P

pcond [in testfree-PDL.demo]
positive [in testfree-PDL.testfree_PDL_def]
positives [in testfree-PDL.testfree_PDL_def]
prv_pSystem [in testfree-PDL.testfree_PDL_def]
prv_mSystem [in testfree-PDL.testfree_PDL_def]
PU [in testfree-PDL.demo]
p_size [in testfree-PDL.testfree_PDL_def]
P1 [in testfree-PDL.demo]

R

R [in testfree-PDL.testfree_PDL_def]
reach [in testfree-PDL.testfree_PDL_def]
reachb [in testfree-PDL.testfree_PDL_def]
reach_demo [in testfree-PDL.demo]
ref [in testfree-PDL.hilbert_ref]
rtrans [in testfree-PDL.demo]

S

sat [in testfree-PDL.demo]
sfc [in testfree-PDL.testfree_PDL_def]
sform [in testfree-PDL.testfree_PDL_def]
sf_closed [in testfree-PDL.testfree_PDL_def]
sf_closed' [in testfree-PDL.testfree_PDL_def]
ssub [in testfree-PDL.testfree_PDL_def]
ssubbox [in testfree-PDL.testfree_PDL_def]
stable [in testfree-PDL.testfree_PDL_def]
starb [in testfree-PDL.testfree_PDL_def]
supp [in testfree-PDL.demo]
S0 [in testfree-PDL.demo]

T

ts_of_fmodel [in testfree-PDL.testfree_PDL_def]

V

valid [in testfree-PDL.testfree_PDL_def]
var [in testfree-PDL.testfree_PDL_def]

---

Record Index

C

cmodel [in testfree-PDL.testfree_PDL_def]

D

demo [in testfree-PDL.demo]

F

fmodel [in testfree-PDL.testfree_PDL_def]

T

ts [in testfree-PDL.testfree_PDL_def]

---

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

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

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

(1 entry)

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

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

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

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

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

(7 entries)

Projection Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(11 entries)

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

(8 entries)

Abbreviation Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

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

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

(4 entries)

Generated by coqdoc and improved with CoqdocJS