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