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

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

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

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

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

(642 entries)

Axiom Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(6 entries)

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

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

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

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

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

(218 entries)

Record Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(6 entries)

---

Global Index

A

A [definition, in Sequent.G4WK.WKPropQuantifiers]
A [definition, in Sequent.G4CK.CKPropQuantifiers]
ABsegment [record, in ComplsegAB.general_segAB_completeness]
absorp_Or1 [lemma, in GHC.properties]
AdAxCd [definition, in ComplsegAB.general_segAB_completeness]
AdAxCd [definition, in GHC.properties]
AdAxCdIdb [definition, in Complth.general_th_completeness]
AdAxIdb [definition, in ComplsegP.general_segP_completeness]
Additional_ax.AdAx [variable, in GHC.properties]
Additional_ax [section, in GHC.properties]
additive_cut [lemma, in Sequent.G4WK.WKCut]
additive_cut [lemma, in Sequent.G4CK.CKCut]
Af [definition, in Sequent.G4WK.WKPropQuantifiers]
Af [definition, in Sequent.G4CK.CKPropQuantifiers]
Af_right [lemma, in Sequent.G4WK.WKPropQuantifiers]
Af_right [lemma, in Sequent.G4CK.CKPropQuantifiers]
AllForm [definition, in GHC.Lindenbaum_lem]
And [constructor, in Syntax.im_syntax]
AndL [constructor, in Sequent.G4WK.WKSequents]
AndL [constructor, in Sequent.G4CK.CKSequents]
AndL_rev [lemma, in Sequent.G4CK.CKSequentProps]
AndL_rev [lemma, in Sequent.G4WK.WKSequentProps]
AndR [constructor, in Sequent.G4WK.WKSequents]
AndR [constructor, in Sequent.G4CK.CKSequents]
AndR_rev [lemma, in Sequent.G4CK.CKSequentProps]
AndR_rev [lemma, in Sequent.G4WK.WKSequentProps]
AndTopL_rev [lemma, in Sequent.G4WK.WKPropQuantifiers]
AndTopL_rev [lemma, in Sequent.G4CK.CKPropQuantifiers]
And_Imp [lemma, in GHC.properties]
Atom [constructor, in Sequent.G4WK.WKSequents]
Atom [constructor, in Sequent.G4CK.CKSequents]
Ax [constructor, in GHC.CKH]
Axioms [definition, in GHC.CKH]
Ax_valid [lemma, in Soundness.general_soundness]
A_right [lemma, in Sequent.G4WK.WKPropQuantifiers]
a_rule_env_spec [lemma, in Sequent.G4WK.WKPropQuantifiers]
a_rule_env17_vars [lemma, in Sequent.G4WK.WKPropQuantifiers]
a_rule_form_vars [lemma, in Sequent.G4WK.WKPropQuantifiers]
a_rule_env_vars [lemma, in Sequent.G4WK.WKPropQuantifiers]
a_rule_env17_cong_strong [lemma, in Sequent.G4WK.WKPropQuantifiers]
a_rule_form_cong_strong [lemma, in Sequent.G4WK.WKPropQuantifiers]
a_rule_env_cong_strong [lemma, in Sequent.G4WK.WKPropQuantifiers]
a_rule_form [definition, in Sequent.G4WK.WKPropQuantifiers]
a_rule_env17 [definition, in Sequent.G4WK.WKPropQuantifiers]
a_rule_env [definition, in Sequent.G4WK.WKPropQuantifiers]
A_right [lemma, in Sequent.G4CK.CKPropQuantifiers]
a_rule_env_spec [lemma, in Sequent.G4CK.CKPropQuantifiers]
a_rule_env17_vars [lemma, in Sequent.G4CK.CKPropQuantifiers]
a_rule_env_form16_vars [lemma, in Sequent.G4CK.CKPropQuantifiers]
a_rule_form_vars [lemma, in Sequent.G4CK.CKPropQuantifiers]
a_rule_env_vars [lemma, in Sequent.G4CK.CKPropQuantifiers]
a_rule_env_form16_cong_strong [lemma, in Sequent.G4CK.CKPropQuantifiers]
a_rule_env17_cong_strong [lemma, in Sequent.G4CK.CKPropQuantifiers]
a_rule_form_cong_strong [lemma, in Sequent.G4CK.CKPropQuantifiers]
a_rule_env_cong_strong [lemma, in Sequent.G4CK.CKPropQuantifiers]
a_rule_form [definition, in Sequent.G4CK.CKPropQuantifiers]
a_rule_env17 [definition, in Sequent.G4CK.CKPropQuantifiers]
a_rule_env_form16 [definition, in Sequent.G4CK.CKPropQuantifiers]
a_rule_env [definition, in Sequent.G4CK.CKPropQuantifiers]
A16_right [lemma, in Sequent.G4CK.CKPropQuantifiers]
A17_right [lemma, in Sequent.G4WK.WKPropQuantifiers]
A17_right [lemma, in Sequent.G4CK.CKPropQuantifiers]

B

bF [instance, in Conservativity.CK_Idb_Nd_not_conserv_CK]
bF_suff_Idb [lemma, in Conservativity.CK_Idb_Nd_not_incl_CK_Cd_Idb_Ndb]
bF_suff_Ndb [lemma, in Conservativity.CK_Idb_Nd_not_incl_CK_Cd_Idb_Ndb]
bF_strong_Cd [lemma, in Conservativity.CK_Idb_Nd_not_incl_CK_Cd_Idb_Ndb]
bireach [definition, in Conservativity.CK_Idb_Nd_not_conserv_CK]
bireach_expl [lemma, in Conservativity.CK_Idb_Nd_not_conserv_CK]
bireach_trans [lemma, in Conservativity.CK_Idb_Nd_not_conserv_CK]
bireach_refl [lemma, in Conservativity.CK_Idb_Nd_not_conserv_CK]
bM [instance, in Conservativity.CK_Idb_Nd_not_conserv_CK]
bmreach [definition, in Conservativity.CK_Idb_Nd_not_conserv_CK]
bmreach_expl [lemma, in Conservativity.CK_Idb_Nd_not_conserv_CK]
Bot [constructor, in Syntax.im_syntax]
bot_not_tautology [lemma, in Sequent.G4CK.CKSequentProps]
bot_not_tautology [lemma, in Sequent.G4WK.WKSequentProps]
Box [constructor, in Syntax.im_syntax]
BoxR [constructor, in Sequent.G4WK.WKSequents]
BoxR [constructor, in Sequent.G4CK.CKSequents]
boxreflect [projection, in Complseg.general_seg_completeness]
boxreflect [lemma, in ComplsegAB.general_segAB_completeness]
boxreflect [lemma, in ComplsegP.general_segP_completeness]
box_bot_not_tautology [lemma, in Sequent.G4CK.CKSequentProps]
box_var_not_tautology [lemma, in Sequent.G4CK.CKSequentProps]
Box_list [definition, in Syntax.im_syntax]
box_bot_not_tautology [lemma, in Sequent.G4WK.WKSequentProps]
box_var_not_tautology [lemma, in Sequent.G4WK.WKSequentProps]
Box_distrib_list_Imp [lemma, in GHC.properties]
bval [definition, in Conservativity.CK_Idb_Nd_not_conserv_CK]
bval_expl [lemma, in Conservativity.CK_Idb_Nd_not_conserv_CK]
bval_persist [lemma, in Conservativity.CK_Idb_Nd_not_conserv_CK]

C

Cd [section, in Kripke.correspondence]
Cd [definition, in GHC.CKH]
CdIdbireach [definition, in Conservativity.CK_Cd_Idb_conserv_CK]
CdIdbireach_expl [lemma, in Conservativity.CK_Cd_Idb_conserv_CK]
CdIdbireach_tran [lemma, in Conservativity.CK_Cd_Idb_conserv_CK]
CdIdbireach_refl [lemma, in Conservativity.CK_Cd_Idb_conserv_CK]
CdIdbmreach [definition, in Conservativity.CK_Cd_Idb_conserv_CK]
CdIdbmreach_expl [lemma, in Conservativity.CK_Cd_Idb_conserv_CK]
CdIdbNb_frame [definition, in Soundness.IK_soundness]
CdIdbNdb_frame [definition, in Soundness.CK_Cd_Idb_Ndb_soundness]
CdIdbpersist [lemma, in Conservativity.CK_Cd_Idb_conserv_CK]
CdIdbval [definition, in Conservativity.CK_Cd_Idb_conserv_CK]
CdIdbval_expl [lemma, in Conservativity.CK_Cd_Idb_conserv_CK]
CdIdb_frame [definition, in Soundness.CK_Cd_Idb_soundness]
CdIdb_model_former [instance, in Conservativity.CK_Cd_Idb_conserv_CK]
CdIdb_frame_former_Idb_frame [lemma, in Conservativity.CK_Cd_Idb_conserv_CK]
CdIdb_frame_former_strong_Cd_frame [lemma, in Conservativity.CK_Cd_Idb_conserv_CK]
CdIdb_frame_former [instance, in Conservativity.CK_Cd_Idb_conserv_CK]
CdNdb_frame [definition, in Soundness.CK_Cd_Ndb_soundness]
CdNdireach [definition, in Conservativity.CK_Cd_Nd_conserv_CK]
CdNdireach_expl [lemma, in Conservativity.CK_Cd_Nd_conserv_CK]
CdNdireach_tran [lemma, in Conservativity.CK_Cd_Nd_conserv_CK]
CdNdireach_refl [lemma, in Conservativity.CK_Cd_Nd_conserv_CK]
CdNdmreach [definition, in Conservativity.CK_Cd_Nd_conserv_CK]
CdNdmreach_expl [lemma, in Conservativity.CK_Cd_Nd_conserv_CK]
CdNdpersist [lemma, in Conservativity.CK_Cd_Nd_conserv_CK]
CdNdval [definition, in Conservativity.CK_Cd_Nd_conserv_CK]
CdNdval_expl [lemma, in Conservativity.CK_Cd_Nd_conserv_CK]
CdNd_model_former [instance, in Conservativity.CK_Cd_Nd_conserv_CK]
CdNd_frame_former_Nd_frame [lemma, in Conservativity.CK_Cd_Nd_conserv_CK]
CdNd_frame_former_Cd_frame [lemma, in Conservativity.CK_Cd_Nd_conserv_CK]
CdNd_frame_former [instance, in Conservativity.CK_Cd_Nd_conserv_CK]
CdNd_frame [definition, in Soundness.CK_Cd_Nd_soundness]
Cd_frame [definition, in Kripke.correspondence]
cexpl [instance, in Complseg.general_seg_completeness]
cexpl [instance, in ComplsegAB.general_segAB_completeness]
cexpl [instance, in Complth.general_th_completeness]
cexpl [instance, in ComplsegP.general_segP_completeness]
cexpl_diamwitness [lemma, in Complseg.general_seg_completeness]
cexpl_boxreflect [lemma, in Complseg.general_seg_completeness]
cexpl_segPrime [lemma, in Complseg.general_seg_completeness]
cexpl_segClosed [lemma, in Complseg.general_seg_completeness]
cexpl_segAorB [lemma, in ComplsegAB.general_segAB_completeness]
cexpl_segPrime [lemma, in ComplsegAB.general_segAB_completeness]
cexpl_segClosed [lemma, in ComplsegAB.general_segAB_completeness]
cexpl_Prime [lemma, in Complth.general_th_completeness]
cexpl_Closed [lemma, in Complth.general_th_completeness]
cexpl_segP_noBot_noDiamBot [lemma, in ComplsegP.general_segP_completeness]
cexpl_segP_noBot_DiamBot [lemma, in ComplsegP.general_segP_completeness]
cexpl_segP_Bot [lemma, in ComplsegP.general_segP_completeness]
cexpl_segPrime [lemma, in ComplsegP.general_segP_completeness]
cexpl_segClosed [lemma, in ComplsegP.general_segP_completeness]
CF [instance, in Complseg.general_seg_completeness]
CF [instance, in ComplsegAB.general_segAB_completeness]
CF [instance, in Complth.general_th_completeness]
CF [instance, in ComplsegP.general_segP_completeness]
CF_Ndb [lemma, in Complth.CK_Cd_Idb_Ndb_th_completeness]
CF_suff_Ndb [lemma, in Complth.CK_Cd_Idb_Ndb_th_completeness]
CF_Ndb [lemma, in ComplsegP.CK_Idb_Ndb_segP_completeness]
CF_suff_Ndb [lemma, in ComplsegP.CK_Idb_Ndb_segP_completeness]
CF_Nd [lemma, in Complseg.WK_seg_completeness]
CF_Cd [lemma, in ComplsegAB.general_segAB_completeness]
CF_suff_Cd [lemma, in ComplsegAB.general_segAB_completeness]
CF_Nd [lemma, in ComplsegP.CK_Idb_Nd_segP_completeness]
CF_suff_Nd [lemma, in ComplsegP.CK_Idb_Nd_segP_completeness]
CF_suff_Idb [lemma, in Complth.general_th_completeness]
CF_CdIdb [lemma, in Complth.general_th_completeness]
CF_strong_Cd_weak_Idb [lemma, in Complth.general_th_completeness]
CF_Nd [lemma, in ComplsegAB.CK_Cd_Nd_segAB_completeness]
CF_Ndb [lemma, in Complseg.CK_Ndb_seg_completeness]
CF_Ndb [lemma, in ComplsegAB.CK_Cd_Ndb_segAB_completeness]
CF_Idb [lemma, in ComplsegP.general_segP_completeness]
CF_suff_Idb [lemma, in ComplsegP.general_segP_completeness]
CF_Nd [lemma, in Complth.IK_th_completeness]
CF_suff_Nd [lemma, in Complth.IK_th_completeness]
choice_code [definition, in GHC.Lindenbaum_lem]
choice_form [definition, in GHC.Lindenbaum_lem]
cireach [definition, in Complseg.general_seg_completeness]
cireach [definition, in ComplsegAB.general_segAB_completeness]
cireach [definition, in Complth.general_th_completeness]
cireach [definition, in ComplsegP.general_segP_completeness]
cireach_expl [lemma, in Complseg.general_seg_completeness]
cireach_trans [lemma, in Complseg.general_seg_completeness]
cireach_refl [lemma, in Complseg.general_seg_completeness]
cireach_expl [lemma, in ComplsegAB.general_segAB_completeness]
cireach_trans [lemma, in ComplsegAB.general_segAB_completeness]
cireach_refl [lemma, in ComplsegAB.general_segAB_completeness]
cireach_expl [lemma, in Complth.general_th_completeness]
cireach_trans [lemma, in Complth.general_th_completeness]
cireach_refl [lemma, in Complth.general_th_completeness]
cireach_expl [lemma, in ComplsegP.general_segP_completeness]
cireach_trans [lemma, in ComplsegP.general_segP_completeness]
cireach_refl [lemma, in ComplsegP.general_segP_completeness]
CKCdH_prv [definition, in GHC.CKH]
CKCdIdbH_prv [definition, in GHC.CKH]
CKCdIdbNdbH_prv [definition, in GHC.CKH]
CKCdIdbNdb_Strong_Completeness [lemma, in Complth.CK_Cd_Idb_Ndb_th_completeness]
CKCdIdbNdb_Soundness [lemma, in Soundness.CK_Cd_Idb_Ndb_soundness]
CKCdIdb_Soundness [lemma, in Soundness.CK_Cd_Idb_soundness]
CKCdIdb_Strong_Completeness [lemma, in Complth.CK_Cd_Idb_th_completeness]
CKCdIdb_conserv_CK [section, in Conservativity.CK_Cd_Idb_conserv_CK]
CKCdNdbH_prv [definition, in GHC.CKH]
CKCdNdb_conserv_CK [section, in Conservativity.CK_Cd_Nd_conserv_CK]
CKCdNdb_Soundness [lemma, in Soundness.CK_Cd_Ndb_soundness]
CKCdNdb_Strong_Completeness [lemma, in ComplsegAB.CK_Cd_Ndb_segAB_completeness]
CKCdNdH_prv [definition, in GHC.CKH]
CKCdNd_extends_CKCdNdb [lemma, in Conservativity.CK_Cd_Nd_conserv_CK]
CKCdNd_conserv_CK [section, in Conservativity.CK_Cd_Nd_conserv_CK]
CKCdNd_Soundness [lemma, in Soundness.CK_Cd_Nd_soundness]
CKCdNd_Strong_Completeness [lemma, in ComplsegAB.CK_Cd_Nd_segAB_completeness]
CKCdwCDH_prv [definition, in GHC.CKH]
CKCd_conserv_CK [section, in Conservativity.CK_Cd_Nd_conserv_CK]
CKCd_Soundness [lemma, in Soundness.CK_Cd_soundness]
CKCd_Strong_Completeness [lemma, in ComplsegAB.CK_Cd_segAB_completeness]
CKCut [library]
CKDecisionProcedure [library]
CKH [library]
CKH_prv [definition, in GHC.CKH]
CKH_export [library]
CKIdbH_prv [definition, in GHC.CKH]
CKIdbNdbH_prv [definition, in GHC.CKH]
CKIdbNdb_Strong_Completeness [lemma, in ComplsegP.CK_Idb_Ndb_segP_completeness]
CKIdbNdb_Soundness [lemma, in Soundness.CK_Idb_Ndb_soundness]
CKIdbNdb_not_conserv_CK [section, in Conservativity.CK_Idb_Ndb_not_conserv_CK]
CKIdbNdH_prv [definition, in GHC.CKH]
CKIdbNd_Soundness [lemma, in Soundness.CK_Idb_Nd_soundness]
CKIdbNd_Strong_Completeness [lemma, in ComplsegP.CK_Idb_Nd_segP_completeness]
CKIdbNd_not_conserv_CK [section, in Conservativity.CK_Idb_Nd_not_conserv_CK]
CKIdbNd_not_included_CKIdbNdb [lemma, in Conservativity.CK_Idb_Nd_not_incl_CK_Cd_Idb_Ndb]
CKIdbNd_not_incl_CKIdbNdb [section, in Conservativity.CK_Idb_Nd_not_incl_CK_Cd_Idb_Ndb]
CKIdbNd_not_included_CKCdIdbNdb [lemma, in Conservativity.CK_Idb_Nd_not_incl_CK_Cd_Idb_Ndb]
CKIdbNd_not_incl_CKCdIdbNdb [section, in Conservativity.CK_Idb_Nd_not_incl_CK_Cd_Idb_Ndb]
CKIdb_Strong_Completeness [lemma, in ComplsegP.CK_Idb_segP_completeness]
CKIdb_conserv_CK [section, in Conservativity.CK_Cd_Idb_conserv_CK]
CKIdb_Soundness [lemma, in Soundness.CK_Idb_soundness]
CKIdb_prv_wCD [lemma, in GHC.properties]
CKNdbH_prv [definition, in GHC.CKH]
CKNdb_conserv_CK [section, in Conservativity.CK_Cd_Nd_conserv_CK]
CKNdb_Soundness [lemma, in Soundness.CK_Ndb_soundness]
CKNdb_Strong_Completeness [lemma, in Complseg.CK_Ndb_seg_completeness]
CKNdb_completeness [section, in Complseg.CK_Ndb_seg_completeness]
CKOrder [library]
CKPropQuantifiers [library]
CKSequentProps [library]
CKSequents [library]
CKSoundComplete [library]
CKwCDH_prv [definition, in GHC.CKH]
CKwCDNdH_prv [definition, in GHC.CKH]
CKwCDNd_not_conserv_CK [section, in Conservativity.CK_wCD_Nd_not_conserv_CK]
CKwCDNd_prv_wCDb [lemma, in Conservativity.CK_wCD_Nd_not_conserv_CK]
CK_Cd_Ndb_soundness [section, in Soundness.CK_Cd_Ndb_soundness]
CK_Cd_Idb_Ndb_completeness [section, in Complth.CK_Cd_Idb_Ndb_th_completeness]
CK_Cd_soundness [section, in Soundness.CK_Cd_soundness]
CK_Idb_Ndb_completeness [section, in ComplsegP.CK_Idb_Ndb_segP_completeness]
CK_Cd_Idb_soundness [section, in Soundness.CK_Cd_Idb_soundness]
CK_Ndb_soundness [section, in Soundness.CK_Ndb_soundness]
CK_Cd_Idb_completeness [section, in Complth.CK_Cd_Idb_th_completeness]
CK_Idb_completeness [section, in ComplsegP.CK_Idb_segP_completeness]
CK_Idb_Nd_soundness [section, in Soundness.CK_Idb_Nd_soundness]
CK_Soundness [lemma, in Soundness.CK_soundness]
CK_soundness [section, in Soundness.CK_soundness]
CK_Cd_Nd_soundness [section, in Soundness.CK_Cd_Nd_soundness]
CK_Idb_Nd_completeness [section, in ComplsegP.CK_Idb_Nd_segP_completeness]
CK_Idb_Ndb_soundness [section, in Soundness.CK_Idb_Ndb_soundness]
CK_Cd_completeness [section, in ComplsegAB.CK_Cd_segAB_completeness]
CK_Idb_soundness [section, in Soundness.CK_Idb_soundness]
CK_Cd_Nd_completeness [section, in ComplsegAB.CK_Cd_Nd_segAB_completeness]
CK_Strong_Completeness [lemma, in Complseg.CK_seg_completeness]
CK_completeness [section, in Complseg.CK_seg_completeness]
CK_Cd_Ndb_completeness [section, in ComplsegAB.CK_Cd_Ndb_segAB_completeness]
CK_uniform_interpolation [lemma, in Sequent.G4CK.CKPropQuantifiers]
CK_Cd_Idb_Ndb_soundness [section, in Soundness.CK_Cd_Idb_Ndb_soundness]
CK_Ndb_soundness [library]
CK_Ndb_seg_completeness [library]
CK_Cd_soundness [library]
CK_Idb_segP_completeness [library]
CK_Idb_Nd_not_incl_CK_Cd_Idb_Ndb [library]
CK_Idb_Ndb_not_conserv_CK [library]
CK_Cd_Nd_segAB_completeness [library]
CK_Cd_Ndb_segAB_completeness [library]
CK_Idb_Nd_not_conserv_CK [library]
CK_soundness [library]
CK_Idb_Ndb_segP_completeness [library]
CK_Cd_Idb_Ndb_th_completeness [library]
CK_Cd_segAB_completeness [library]
CK_Cd_Nd_conserv_CK [library]
CK_Cd_Nd_soundness [library]
CK_Cd_Idb_th_completeness [library]
CK_Idb_Nd_segP_completeness [library]
CK_Cd_Idb_soundness [library]
CK_wCD_Nd_not_conserv_CK [library]
CK_Idb_Ndb_soundness [library]
CK_Cd_Idb_conserv_CK [library]
CK_Idb_Nd_soundness [library]
CK_seg_completeness [library]
CK_Idb_soundness [library]
CK_Cd_Ndb_soundness [library]
CK_Cd_Idb_Ndb_soundness [library]
Classical_facts.AdAx [variable, in GHC.classical_facts]
Classical_facts.LEM [variable, in GHC.classical_facts]
Classical_facts [section, in GHC.classical_facts]
classical_facts [library]
Closed [projection, in Complth.general_th_completeness]
closed [definition, in GHC.Lindenbaum_lem]
closeder_pair_Lind_theory [lemma, in GHC.Lindenbaum_lem_pair]
closeder_Lind_theory [lemma, in GHC.Lindenbaum_lem]
CM [instance, in Complseg.general_seg_completeness]
CM [instance, in ComplsegAB.general_segAB_completeness]
CM [instance, in Complth.general_th_completeness]
CM [instance, in ComplsegP.general_segP_completeness]
cmreach [definition, in Complseg.general_seg_completeness]
cmreach [definition, in ComplsegAB.general_segAB_completeness]
cmreach [definition, in Complth.general_th_completeness]
cmreach [definition, in ComplsegP.general_segP_completeness]
cmreach_expl [lemma, in Complseg.general_seg_completeness]
cmreach_expl [lemma, in ComplsegAB.general_segAB_completeness]
cmreach_expl [lemma, in Complth.general_th_completeness]
cmreach_expl [lemma, in ComplsegP.general_segP_completeness]
comm_Or [lemma, in GHC.properties]
comm_Or_obj [lemma, in GHC.properties]
comm_And_obj [lemma, in GHC.properties]
Completeness [section, in Sequent.G4WK.WKSoundComplete]
Completeness [section, in Sequent.G4CK.CKSoundComplete]
Consist_pair_Lind_theory [lemma, in GHC.Lindenbaum_lem_pair]
Consist_npair_Lind_theory [lemma, in GHC.Lindenbaum_lem_pair]
Consist_Lind_theory [lemma, in GHC.Lindenbaum_lem]
Consist_nLind_theory [lemma, in GHC.Lindenbaum_lem]
contraction [lemma, in Sequent.G4CK.CKSequentProps]
contraction [lemma, in Sequent.G4WK.WKSequentProps]
Contr_Bot [lemma, in GHC.properties]
Correctness [section, in Sequent.G4WK.WKPropQuantifiers]
Correctness [section, in Sequent.G4CK.CKPropQuantifiers]
Correctness.EntailmentCorrect [section, in Sequent.G4WK.WKPropQuantifiers]
Correctness.EntailmentCorrect [section, in Sequent.G4CK.CKPropQuantifiers]
Correctness.p [variable, in Sequent.G4WK.WKPropQuantifiers]
Correctness.p [variable, in Sequent.G4CK.CKPropQuantifiers]
Correctness.PropQuantCorrect [section, in Sequent.G4WK.WKPropQuantifiers]
Correctness.PropQuantCorrect [section, in Sequent.G4CK.CKPropQuantifiers]
Correctness.VariablesCorrect [section, in Sequent.G4WK.WKPropQuantifiers]
Correctness.VariablesCorrect [section, in Sequent.G4CK.CKPropQuantifiers]
correspondence [library]
correspond_Ndb [lemma, in Kripke.correspondence]
correspond_Nd [lemma, in Kripke.correspondence]
correspond_Idb [lemma, in Kripke.correspondence]
correspond_Cd [lemma, in Kripke.correspondence]
CountablyManyFormulas [section, in Sequent.syntax_facts]
cut [lemma, in Sequent.G4WK.WKCut]
cut [lemma, in Sequent.G4CK.CKCut]
cval [definition, in Complseg.general_seg_completeness]
cval [definition, in ComplsegAB.general_segAB_completeness]
cval [definition, in Complth.general_th_completeness]
cval [definition, in ComplsegP.general_segP_completeness]
cval_expl [lemma, in Complseg.general_seg_completeness]
cval_persist [lemma, in Complseg.general_seg_completeness]
cval_expl [lemma, in ComplsegAB.general_segAB_completeness]
cval_persist [lemma, in ComplsegAB.general_segAB_completeness]
cval_expl [lemma, in Complth.general_th_completeness]
cval_persist [lemma, in Complth.general_th_completeness]
cval_expl [lemma, in ComplsegP.general_segP_completeness]
cval_persist [lemma, in ComplsegP.general_segP_completeness]
cworld [record, in Complth.general_th_completeness]

D

decidable_is_diam_implication [instance, in Sequent.Environments]
decidable_is_negation [instance, in Sequent.Environments]
decidable_is_implication [instance, in Sequent.Environments]
decidable_is_double_negation [instance, in Sequent.Environments]
decide_in [lemma, in Sequent.Environments]
der_pair_Lind_theory_npair_Lind_theory [lemma, in GHC.Lindenbaum_lem_pair]
der_npair_Lind_theory_mpair_Lind_theory_le [lemma, in GHC.Lindenbaum_lem_pair]
der_Lind_theory_nLind_theory [lemma, in GHC.Lindenbaum_lem]
der_nLind_theory_mLind_theory_le [lemma, in GHC.Lindenbaum_lem]
Diam [constructor, in Syntax.im_syntax]
diamimp_partition [lemma, in Sequent.Environments]
DiamL [constructor, in Sequent.G4WK.WKSequents]
DiamL [constructor, in Sequent.G4CK.CKSequents]
diamwitness [projection, in Complseg.general_seg_completeness]
diamwitness [lemma, in ComplsegAB.general_segAB_completeness]
diamwitness [lemma, in ComplsegP.general_segP_completeness]
diam_free_eq_CKNdb_CK [lemma, in Conservativity.CK_Cd_Nd_conserv_CK]
diam_free_eq_WK_CK [lemma, in Conservativity.CK_Cd_Nd_conserv_CK]
diam_free_eq_CKCd_CK [lemma, in Conservativity.CK_Cd_Nd_conserv_CK]
diam_free_eq_CKCdNdb_CK [lemma, in Conservativity.CK_Cd_Nd_conserv_CK]
diam_free_eq_CKCdNd_CK [lemma, in Conservativity.CK_Cd_Nd_conserv_CK]
diam_bot_not_tautology [lemma, in Sequent.G4CK.CKSequentProps]
diam_var_not_tautology [lemma, in Sequent.G4CK.CKSequentProps]
diam_free [definition, in Syntax.im_syntax]
Diam_existence [lemma, in Complseg.general_seg_completeness]
diam_bot_not_tautology [lemma, in Sequent.G4WK.WKSequentProps]
diam_var_not_tautology [lemma, in Sequent.G4WK.WKSequentProps]
diam_free_eq_CKIdb_CK [lemma, in Conservativity.CK_Cd_Idb_conserv_CK]
diam_free_eq_CKCdIdb_CK [lemma, in Conservativity.CK_Cd_Idb_conserv_CK]
diam_free_strict_ext_CKIdbNdb_CK [lemma, in Conservativity.CK_Idb_Ndb_not_conserv_CK]
diam_free_ext_CKIdbNdb_CK [lemma, in Conservativity.CK_Idb_Ndb_not_conserv_CK]
diam_free_strict_ext_IK_CKIdbNd [lemma, in Conservativity.CK_Idb_Nd_not_conserv_CK]
diam_free_strict_ext_IK_CK [lemma, in Conservativity.CK_Idb_Nd_not_conserv_CK]
diam_free_ext_IK_CK [lemma, in Conservativity.CK_Idb_Nd_not_conserv_CK]
diam_free_strict_ext_CKIdbNd_CK [lemma, in Conservativity.CK_Idb_Nd_not_conserv_CK]
diam_free_ext_CKIdbNd_CK [lemma, in Conservativity.CK_Idb_Nd_not_conserv_CK]
Diam_distrib_list_disj [lemma, in GHC.properties]
Diam_rule [lemma, in GHC.properties]
diam_free_strict_ext_CKwCDNd_CK [lemma, in Conservativity.CK_wCD_Nd_not_conserv_CK]
diam_free_ext_CKwCDNd_CK [lemma, in Conservativity.CK_wCD_Nd_not_conserv_CK]
difference_include [lemma, in Sequent.Environments]
difference_singleton [lemma, in Sequent.Environments]
diff_not_in [lemma, in Sequent.Environments]
diff_mult [lemma, in Sequent.Environments]

E

E [definition, in Sequent.G4WK.WKPropQuantifiers]
E [definition, in Sequent.G4CK.CKPropQuantifiers]
EA [definition, in Sequent.G4WK.WKPropQuantifiers]
EA [definition, in Sequent.G4CK.CKPropQuantifiers]
EA_vars [lemma, in Sequent.G4WK.WKPropQuantifiers]
EA_cong [lemma, in Sequent.G4WK.WKPropQuantifiers]
EA_vars [lemma, in Sequent.G4CK.CKPropQuantifiers]
EA_cong [lemma, in Sequent.G4CK.CKPropQuantifiers]
Ef [definition, in Sequent.G4WK.WKPropQuantifiers]
Ef [definition, in Sequent.G4CK.CKPropQuantifiers]
EFQ [lemma, in GHC.properties]
elements_open_boxes_order [lemma, in Sequent.G4WK.WKOrder]
elements_elem_of [lemma, in Sequent.G4WK.WKOrder]
elements_list_to_set_disj [lemma, in Sequent.Environments]
elements_setminus [lemma, in Sequent.Environments]
elements_open_boxes [lemma, in Sequent.Environments]
elements_env_add [lemma, in Sequent.Environments]
elements_open_boxes_order [lemma, in Sequent.G4CK.CKOrder]
elements_elem_of [lemma, in Sequent.G4CK.CKOrder]
elem_of_list_In_1 [lemma, in Sequent.G4WK.WKOrder]
elem_of_open_boxes [lemma, in Sequent.Environments]
elem_of_list_In_1 [lemma, in Sequent.G4CK.CKOrder]
empty [definition, in Sequent.Environments]
emptyweakR [lemma, in Sequent.G4WK.WKSequentProps]
entail_correct [lemma, in Sequent.G4WK.WKPropQuantifiers]
entail_correct [lemma, in Sequent.G4CK.CKPropQuantifiers]
enum [library]
env [definition, in Sequent.Environments]
Environments [library]
env_order_le_lt_trans [lemma, in Sequent.G4WK.WKOrder]
env_order_lt_le_trans [lemma, in Sequent.G4WK.WKOrder]
env_order_refl_add' [lemma, in Sequent.G4WK.WKOrder]
env_order_refl_add [lemma, in Sequent.G4WK.WKOrder]
env_order_cancel_right [lemma, in Sequent.G4WK.WKOrder]
env_order_4 [lemma, in Sequent.G4WK.WKOrder]
env_order_3 [lemma, in Sequent.G4WK.WKOrder]
env_order_2 [lemma, in Sequent.G4WK.WKOrder]
env_order_1' [lemma, in Sequent.G4WK.WKOrder]
env_order_0' [lemma, in Sequent.G4WK.WKOrder]
env_order_0 [lemma, in Sequent.G4WK.WKOrder]
env_order_disj_union_compat_strong_left [lemma, in Sequent.G4WK.WKOrder]
env_order_disj_union_compat_strong_right [lemma, in Sequent.G4WK.WKOrder]
env_order_refl_disj_union_compat [lemma, in Sequent.G4WK.WKOrder]
env_order_disj_union_compat [lemma, in Sequent.G4WK.WKOrder]
env_order_disj_union_compat_right [lemma, in Sequent.G4WK.WKOrder]
env_order_disj_union_compat_left [lemma, in Sequent.G4WK.WKOrder]
env_order_add_compat [lemma, in Sequent.G4WK.WKOrder]
env_order_compat' [lemma, in Sequent.G4WK.WKOrder]
env_order_compat [lemma, in Sequent.G4WK.WKOrder]
env_order_1 [lemma, in Sequent.G4WK.WKOrder]
env_order_equiv_left_compat [lemma, in Sequent.G4WK.WKOrder]
env_order_equiv_right_compat [lemma, in Sequent.G4WK.WKOrder]
env_order_trans [instance, in Sequent.G4WK.WKOrder]
env_order_self [lemma, in Sequent.G4WK.WKOrder]
env_order_refl_trans [lemma, in Sequent.G4WK.WKOrder]
env_order_env_order_refl [lemma, in Sequent.G4WK.WKOrder]
env_order_refl [definition, in Sequent.G4WK.WKOrder]
env_order_singleton [lemma, in Sequent.G4WK.WKOrder]
env_weight_singleton [lemma, in Sequent.G4WK.WKOrder]
env_order [definition, in Sequent.G4WK.WKOrder]
env_weight_add [lemma, in Sequent.G4WK.WKOrder]
env_weight_disj_union [lemma, in Sequent.G4WK.WKOrder]
env_weight [definition, in Sequent.G4WK.WKOrder]
env_equiv_eq [lemma, in Sequent.Environments]
env_add_inv' [lemma, in Sequent.Environments]
env_add_inv [lemma, in Sequent.Environments]
env_add_comm [lemma, in Sequent.Environments]
env_in_add [lemma, in Sequent.Environments]
env_add_remove [lemma, in Sequent.Environments]
env_replace [lemma, in Sequent.Environments]
env_order_le_lt_trans [lemma, in Sequent.G4CK.CKOrder]
env_order_lt_le_trans [lemma, in Sequent.G4CK.CKOrder]
env_order_refl_add' [lemma, in Sequent.G4CK.CKOrder]
env_order_refl_add [lemma, in Sequent.G4CK.CKOrder]
env_order_cancel_right [lemma, in Sequent.G4CK.CKOrder]
env_order_4 [lemma, in Sequent.G4CK.CKOrder]
env_order_3 [lemma, in Sequent.G4CK.CKOrder]
env_order_2 [lemma, in Sequent.G4CK.CKOrder]
env_order_1' [lemma, in Sequent.G4CK.CKOrder]
env_order_0' [lemma, in Sequent.G4CK.CKOrder]
env_order_0 [lemma, in Sequent.G4CK.CKOrder]
env_order_disj_union_compat_strong_left [lemma, in Sequent.G4CK.CKOrder]
env_order_disj_union_compat_strong_right [lemma, in Sequent.G4CK.CKOrder]
env_order_refl_disj_union_compat [lemma, in Sequent.G4CK.CKOrder]
env_order_disj_union_compat [lemma, in Sequent.G4CK.CKOrder]
env_order_disj_union_compat_right [lemma, in Sequent.G4CK.CKOrder]
env_order_disj_union_compat_left [lemma, in Sequent.G4CK.CKOrder]
env_order_add_compat [lemma, in Sequent.G4CK.CKOrder]
env_order_compat' [lemma, in Sequent.G4CK.CKOrder]
env_order_compat [lemma, in Sequent.G4CK.CKOrder]
env_order_1 [lemma, in Sequent.G4CK.CKOrder]
env_order_equiv_left_compat [lemma, in Sequent.G4CK.CKOrder]
env_order_equiv_right_compat [lemma, in Sequent.G4CK.CKOrder]
env_order_trans [instance, in Sequent.G4CK.CKOrder]
env_order_self [lemma, in Sequent.G4CK.CKOrder]
env_order_refl_trans [lemma, in Sequent.G4CK.CKOrder]
env_order_env_order_refl [lemma, in Sequent.G4CK.CKOrder]
env_order_refl [definition, in Sequent.G4CK.CKOrder]
env_order_singleton [lemma, in Sequent.G4CK.CKOrder]
env_weight_singleton [lemma, in Sequent.G4CK.CKOrder]
env_order [definition, in Sequent.G4CK.CKOrder]
env_weight_add [lemma, in Sequent.G4CK.CKOrder]
env_weight_disj_union [lemma, in Sequent.G4CK.CKOrder]
env_weight [definition, in Sequent.G4CK.CKOrder]
equiv_assoc [instance, in Sequent.Environments]
equiv_disj_union_compat_l [lemma, in Sequent.Environments]
equiv_disj_union_compat_r [lemma, in Sequent.Environments]
eq_dec_form [lemma, in Syntax.im_syntax]
ExFalso [constructor, in Sequent.G4WK.WKSequents]
exfalso [lemma, in Sequent.G4CK.CKSequentProps]
exfalso [lemma, in Sequent.G4WK.WKSequentProps]
ExFalso [constructor, in Sequent.G4CK.CKSequents]
exists_dec [definition, in Sequent.G4WK.WKDecisionProcedure]
exists_dec [definition, in Sequent.G4CK.CKDecisionProcedure]
Expl [lemma, in Kripke.kripke_sem]
expl [projection, in Kripke.kripke_sem]
Explosion [lemma, in GHC.properties]
extCKH_finite [lemma, in GHC.logic]
extCKH_struct [lemma, in GHC.logic]
extCKH_comp [lemma, in GHC.logic]
extCKH_monot [lemma, in GHC.logic]
extCKH_prv_sind [definition, in GHC.CKH]
extCKH_prv_ind [definition, in GHC.CKH]
extCKH_prv [inductive, in GHC.CKH]
extCKH_Imp_list_Detachment_Deduction_Theorem [lemma, in GHC.properties]
extCKH_Deduction_Theorem [lemma, in GHC.properties]
extCKH_Detachment_Theorem [lemma, in GHC.properties]
E_of_empty [lemma, in Sequent.G4WK.WKPropQuantifiers]
E_left [lemma, in Sequent.G4WK.WKPropQuantifiers]
e_rule_12_vars [lemma, in Sequent.G4WK.WKPropQuantifiers]
e_rule_9_vars [lemma, in Sequent.G4WK.WKPropQuantifiers]
e_rule_vars [lemma, in Sequent.G4WK.WKPropQuantifiers]
e_rule_12_cong_strong [lemma, in Sequent.G4WK.WKPropQuantifiers]
e_rule_9_cong_strong [lemma, in Sequent.G4WK.WKPropQuantifiers]
e_rule_cong_strong [lemma, in Sequent.G4WK.WKPropQuantifiers]
e_rules_cong [lemma, in Sequent.G4WK.WKPropQuantifiers]
e_rule_12 [definition, in Sequent.G4WK.WKPropQuantifiers]
e_rule_9 [definition, in Sequent.G4WK.WKPropQuantifiers]
e_rule [definition, in Sequent.G4WK.WKPropQuantifiers]
E_of_empty [lemma, in Sequent.G4CK.CKPropQuantifiers]
E_left [lemma, in Sequent.G4CK.CKPropQuantifiers]
e_rule_12_vars [lemma, in Sequent.G4CK.CKPropQuantifiers]
e_rule_9_vars [lemma, in Sequent.G4CK.CKPropQuantifiers]
e_rule_vars [lemma, in Sequent.G4CK.CKPropQuantifiers]
e_rule_12_cong_strong [lemma, in Sequent.G4CK.CKPropQuantifiers]
e_rule_9_cong_strong [lemma, in Sequent.G4CK.CKPropQuantifiers]
e_rule_cong_strong [lemma, in Sequent.G4CK.CKPropQuantifiers]
e_rules_cong [lemma, in Sequent.G4CK.CKPropQuantifiers]
e_rule_12 [definition, in Sequent.G4CK.CKPropQuantifiers]
e_rule_9 [definition, in Sequent.G4CK.CKPropQuantifiers]
e_rule [definition, in Sequent.G4CK.CKPropQuantifiers]
E12_left [lemma, in Sequent.G4WK.WKPropQuantifiers]
E12_left [lemma, in Sequent.G4CK.CKPropQuantifiers]
E9_left [lemma, in Sequent.G4WK.WKPropQuantifiers]
E9_left [lemma, in Sequent.G4CK.CKPropQuantifiers]

F

FIKH_prv [definition, in GHC.CKH]
filter_disj_union [lemma, in Sequent.Environments]
fomula_top [instance, in Sequent.syntax_facts]
fomula_bottom [instance, in Sequent.syntax_facts]
forall_list_conj [lemma, in GHC.properties]
forall_list_disj [lemma, in GHC.properties]
forces [definition, in Kripke.kripke_sem]
form [inductive, in Syntax.im_syntax]
forming_CdNd_model.M [variable, in Conservativity.CK_Cd_Nd_conserv_CK]
forming_CdNd_model [section, in Conservativity.CK_Cd_Nd_conserv_CK]
forming_CdIdb_model.M [variable, in Conservativity.CK_Cd_Idb_conserv_CK]
forming_CdIdb_model [section, in Conservativity.CK_Cd_Idb_conserv_CK]
form_index_inj [lemma, in GHC.enum]
form_enum_index [lemma, in GHC.enum]
form_index [definition, in GHC.enum]
form_index' [definition, in GHC.enum]
form_enum_sur [lemma, in GHC.enum]
form_enum [definition, in GHC.enum]
form_order [definition, in Sequent.syntax_facts]
form_count [instance, in Sequent.syntax_facts]
form_to_gen_tree [definition, in Sequent.syntax_facts]
form_eq_dec [instance, in Sequent.syntax_facts]
form_sind [definition, in Syntax.im_syntax]
form_rec [definition, in Syntax.im_syntax]
form_ind [definition, in Syntax.im_syntax]
form_rect [definition, in Syntax.im_syntax]
fra [projection, in Kripke.kripke_sem]
frame [record, in Kripke.kripke_sem]
fvalid [definition, in Kripke.kripke_sem]

G

GeneralEnvironments [section, in Sequent.Environments]
generalised_contraction [lemma, in Sequent.G4CK.CKSequentProps]
generalised_axiom [lemma, in Sequent.G4CK.CKSequentProps]
generalised_weakeningR [lemma, in Sequent.G4CK.CKSequentProps]
generalised_weakeningL [lemma, in Sequent.G4CK.CKSequentProps]
generalised_contraction [lemma, in Sequent.G4WK.WKSequentProps]
generalised_axiom [lemma, in Sequent.G4WK.WKSequentProps]
generalised_weakeningR [lemma, in Sequent.G4WK.WKSequentProps]
generalised_weakeningL [lemma, in Sequent.G4WK.WKSequentProps]
general_soundness.corresp_AdAx_FraP [variable, in Soundness.general_soundness]
general_soundness.FraP [variable, in Soundness.general_soundness]
general_soundness.AdAx [variable, in Soundness.general_soundness]
general_soundness [section, in Soundness.general_soundness]
General_Lind_pair.Lindenbaum_lemma [section, in GHC.Lindenbaum_lem_pair]
General_Lind_pair.PrimeProps [section, in GHC.Lindenbaum_lem_pair]
General_Lind_pair.Prime [section, in GHC.Lindenbaum_lem_pair]
General_Lind_pair.Pair [section, in GHC.Lindenbaum_lem_pair]
General_Lind_pair.AdAx [variable, in GHC.Lindenbaum_lem_pair]
General_Lind_pair [section, in GHC.Lindenbaum_lem_pair]
general_seg_completeness.CF_ClassF [variable, in Complseg.general_seg_completeness]
general_seg_completeness.ClassF_AdAx [variable, in Complseg.general_seg_completeness]
general_seg_completeness.ClassF [variable, in Complseg.general_seg_completeness]
general_seg_completeness.segment_prf_irrel [variable, in Complseg.general_seg_completeness]
general_seg_completeness.AdAx [variable, in Complseg.general_seg_completeness]
general_seg_completeness.LEM [variable, in Complseg.general_seg_completeness]
general_seg_completeness [section, in Complseg.general_seg_completeness]
general_segAB_completeness.CF_ClassF [variable, in ComplsegAB.general_segAB_completeness]
general_segAB_completeness.ClassF_AdAx [variable, in ComplsegAB.general_segAB_completeness]
general_segAB_completeness.ClassF [variable, in ComplsegAB.general_segAB_completeness]
general_segAB_completeness.ABsegment_prf_irrel [variable, in ComplsegAB.general_segAB_completeness]
general_segAB_completeness.AdAx [variable, in ComplsegAB.general_segAB_completeness]
general_segAB_completeness [section, in ComplsegAB.general_segAB_completeness]
general_th_completeness.CF_ClassF [variable, in Complth.general_th_completeness]
general_th_completeness.ClassF_AdAx [variable, in Complth.general_th_completeness]
general_th_completeness.ClassF [variable, in Complth.general_th_completeness]
general_th_completeness.cworld_prf_irrel [variable, in Complth.general_th_completeness]
general_th_completeness.AdAx [variable, in Complth.general_th_completeness]
general_th_completeness [section, in Complth.general_th_completeness]
General_Lind.Lindenbaum_lemma [section, in GHC.Lindenbaum_lem]
General_Lind.PrimeProps [section, in GHC.Lindenbaum_lem]
General_Lind.Prime [section, in GHC.Lindenbaum_lem]
General_Lind.prelims [section, in GHC.Lindenbaum_lem]
General_Lind.Sets_of_forms [section, in GHC.Lindenbaum_lem]
General_Lind.AdAx [variable, in GHC.Lindenbaum_lem]
General_Lind [section, in GHC.Lindenbaum_lem]
general_segP_completeness.CF_ClassF [variable, in ComplsegP.general_segP_completeness]
general_segP_completeness.ClassF_AdAx [variable, in ComplsegP.general_segP_completeness]
general_segP_completeness.ClassF [variable, in ComplsegP.general_segP_completeness]
general_segP_completeness.Psegment_prf_irrel [variable, in ComplsegP.general_segP_completeness]
general_segP_completeness.AdAx [variable, in ComplsegP.general_segP_completeness]
general_segP_completeness [section, in ComplsegP.general_segP_completeness]
general_soundness [library]
general_segP_completeness [library]
general_segAB_completeness [library]
general_th_completeness [library]
general_seg_completeness [library]
gen_tree_to_form [definition, in Sequent.syntax_facts]
gmultiset_elements_list_to_set_disj_perm [lemma, in Sequent.Environments]
gmultiset_elements_list_to_set_disj [lemma, in Sequent.Environments]
gmultiset_rec [lemma, in Sequent.Environments]
gmultiset_choose_or_empty [lemma, in Sequent.Environments]
G4CK_compl_CKH [lemma, in Sequent.G4CK.CKSoundComplete]
G4CK_sound_CKH [lemma, in Sequent.G4CK.CKSoundComplete]
G4WK_compl_WKH [lemma, in Sequent.G4WK.WKSoundComplete]
G4WK_sound_CKH [lemma, in Sequent.G4WK.WKSoundComplete]

H

head [projection, in Complseg.general_seg_completeness]
head [projection, in ComplsegAB.general_segAB_completeness]
head [projection, in ComplsegP.general_segP_completeness]
height [definition, in Sequent.G4CK.CKSequentProps]
height [definition, in Sequent.G4WK.WKSequentProps]
height_0 [lemma, in Sequent.G4CK.CKSequentProps]
height_0 [lemma, in Sequent.G4WK.WKSequentProps]

I

IAxioms [inductive, in GHC.CKH]
IAxioms_sind [definition, in GHC.CKH]
IAxioms_ind [definition, in GHC.CKH]
IA1 [constructor, in GHC.CKH]
IA2 [constructor, in GHC.CKH]
IA3 [constructor, in GHC.CKH]
IA4 [constructor, in GHC.CKH]
IA5 [constructor, in GHC.CKH]
IA6 [constructor, in GHC.CKH]
IA7 [constructor, in GHC.CKH]
IA8 [constructor, in GHC.CKH]
IA9 [constructor, in GHC.CKH]
Id [constructor, in GHC.CKH]
Idb [section, in Kripke.correspondence]
Idb [definition, in GHC.CKH]
IdbNdb_frame [definition, in Soundness.CK_Idb_Ndb_soundness]
IdbNd_frame [definition, in Soundness.CK_Idb_Nd_soundness]
Idb_frame [definition, in Kripke.correspondence]
IdL_list_disj [lemma, in GHC.properties]
IdL_list_disj_obj [lemma, in GHC.properties]
idowncone [definition, in Kripke.correspondence]
IdR_list_disj [lemma, in GHC.properties]
IdR_list_disj_obj [lemma, in GHC.properties]
IKH_prv [definition, in GHC.CKH]
IK_Soundness [lemma, in Soundness.IK_soundness]
IK_soundness [section, in Soundness.IK_soundness]
IK_not_conserv_CKIdbNd [section, in Conservativity.CK_Idb_Nd_not_conserv_CK]
IK_not_conserv_CK [section, in Conservativity.CK_Idb_Nd_not_conserv_CK]
IK_Strong_Completeness [lemma, in Complth.IK_th_completeness]
IK_completeness [section, in Complth.IK_th_completeness]
IK_soundness [library]
IK_th_completeness [library]
Imp [constructor, in Syntax.im_syntax]
ImpBox [constructor, in Sequent.G4WK.WKSequents]
ImpBox [constructor, in Sequent.G4CK.CKSequents]
ImpBox_dup [lemma, in Sequent.G4CK.CKSequentProps]
ImpBox_dup [lemma, in Sequent.G4WK.WKSequentProps]
ImpDiam [constructor, in Sequent.G4WK.WKSequents]
ImpDiam [constructor, in Sequent.G4CK.CKSequents]
ImpL [lemma, in Sequent.G4CK.CKSequentProps]
ImpL [lemma, in Sequent.G4WK.WKSequentProps]
ImpLAnd [constructor, in Sequent.G4WK.WKSequents]
ImpLAnd [constructor, in Sequent.G4CK.CKSequents]
ImpLAnd_rev [lemma, in Sequent.G4CK.CKSequentProps]
ImpLAnd_rev [lemma, in Sequent.G4WK.WKSequentProps]
ImpLBox_prev [lemma, in Sequent.G4CK.CKSequentProps]
ImpLBox_prev [lemma, in Sequent.G4WK.WKSequentProps]
ImpLDiam_prev [lemma, in Sequent.G4CK.CKSequentProps]
ImpLDiam_prev [lemma, in Sequent.G4WK.WKSequentProps]
ImpLImp [constructor, in Sequent.G4WK.WKSequents]
ImpLImp [constructor, in Sequent.G4CK.CKSequents]
ImpLImp_dup [lemma, in Sequent.G4CK.CKSequentProps]
ImpLImp_prev [lemma, in Sequent.G4CK.CKSequentProps]
ImpLImp_dup [lemma, in Sequent.G4WK.WKSequentProps]
ImpLImp_prev [lemma, in Sequent.G4WK.WKSequentProps]
ImpLOr [constructor, in Sequent.G4WK.WKSequents]
ImpLOr [constructor, in Sequent.G4CK.CKSequents]
ImpLOr_rev [lemma, in Sequent.G4CK.CKSequentProps]
ImpLOr_rev [lemma, in Sequent.G4WK.WKSequentProps]
ImpLVar [constructor, in Sequent.G4WK.WKSequents]
ImpLVar [constructor, in Sequent.G4CK.CKSequents]
ImpLVar_rev [lemma, in Sequent.G4CK.CKSequentProps]
ImpLVar_rev [lemma, in Sequent.G4WK.WKSequentProps]
ImpR [constructor, in Sequent.G4WK.WKSequents]
ImpR [constructor, in Sequent.G4CK.CKSequents]
ImpR_rev [lemma, in Sequent.G4CK.CKSequentProps]
ImpR_rev [lemma, in Sequent.G4WK.WKSequentProps]
imp_cut [lemma, in Sequent.G4CK.CKSequentProps]
imp_cut [lemma, in Sequent.G4WK.WKSequentProps]
Imp_list_Imp [lemma, in GHC.properties]
Imp_And [lemma, in GHC.properties]
Imp_trans [lemma, in GHC.properties]
Imp_trans_help427 [lemma, in GHC.properties]
Imp_trans_help410 [lemma, in GHC.properties]
Imp_trans_help170 [lemma, in GHC.properties]
Imp_trans_help54 [lemma, in GHC.properties]
Imp_trans_help37 [lemma, in GHC.properties]
Imp_trans_help35 [lemma, in GHC.properties]
Imp_trans_help14 [lemma, in GHC.properties]
Imp_trans_help9 [lemma, in GHC.properties]
Imp_trans_help8 [lemma, in GHC.properties]
Imp_trans_help7 [lemma, in GHC.properties]
imp_Id_gen [lemma, in GHC.properties]
im_syntax [library]
in_app_orT [lemma, in Sequent.syntax_facts]
In_form_dec [lemma, in Syntax.im_syntax]
In_open_boxes_t [lemma, in Sequent.Environments]
in_l_open_boxes [lemma, in Sequent.Environments]
in_in_rm [lemma, in Sequent.Environments]
in_rm [lemma, in Sequent.Environments]
in_difference [lemma, in Sequent.Environments]
in_map2_ext [lemma, in Sequent.Environments]
in_map_ext [lemma, in Sequent.Environments]
in_map_empty [lemma, in Sequent.Environments]
in_map2_in [lemma, in Sequent.Environments]
in_map_in [lemma, in Sequent.Environments]
in_subset [definition, in Sequent.Environments]
in_in_map2 [lemma, in Sequent.Environments]
in_in_map [lemma, in Sequent.Environments]
in_map2 [definition, in Sequent.Environments]
in_map2_aux [definition, in Sequent.Environments]
in_map [definition, in Sequent.Environments]
in_map_aux [definition, in Sequent.Environments]
In_Box_list_In_list [lemma, in GHC.properties]
In_list_In_Box_list [lemma, in GHC.properties]
In_remove [lemma, in GHC.properties]
ireachable [projection, in Kripke.kripke_sem]
ireach_expl [projection, in Kripke.kripke_sem]
ireach_tran [projection, in Kripke.kripke_sem]
ireach_refl [projection, in Kripke.kripke_sem]
irreducible [definition, in Sequent.Environments]
irreflexive_form_order [instance, in Sequent.syntax_facts]
is_Ndb [definition, in Complth.CK_Cd_Idb_Ndb_th_completeness]
is_Ndb [definition, in ComplsegP.CK_Idb_Ndb_segP_completeness]
is_box_weight_open_box [lemma, in Sequent.G4CK.CKSequentProps]
is_box_weight_open_box [lemma, in Sequent.G4WK.WKSequentProps]
is_Nd [definition, in Complseg.WK_seg_completeness]
is_Nd [definition, in ComplsegP.CK_Idb_Nd_segP_completeness]
is_not_box_open_box [lemma, in Sequent.Environments]
is_box [definition, in Sequent.Environments]
is_diam_implication_b [definition, in Sequent.Environments]
is_diam_implication [definition, in Sequent.Environments]
is_negation [definition, in Sequent.Environments]
is_implication [definition, in Sequent.Environments]
is_double_negation [definition, in Sequent.Environments]
is_Nd [definition, in ComplsegAB.CK_Cd_Nd_segAB_completeness]
is_Ndb [definition, in Complseg.CK_Ndb_seg_completeness]
is_Ndb [definition, in ComplsegAB.CK_Cd_Ndb_segAB_completeness]
is_Nd [definition, in Complth.IK_th_completeness]
iupcone [definition, in Kripke.correspondence]

K

Kb [constructor, in GHC.CKH]
Kd [constructor, in GHC.CKH]
kripke_sem [section, in Kripke.kripke_sem]
kripke_sem [library]
kripke_export [library]
K_rule [lemma, in GHC.properties]
K_list_Imp [lemma, in GHC.properties]

L

LEM [axiom, in ComplsegP.CK_Idb_Ndb_segP_completeness]
LEM [axiom, in Kripke.correspondence]
LEM [axiom, in ComplsegAB.general_segAB_completeness]
LEM [axiom, in ComplsegP.CK_Idb_Nd_segP_completeness]
LEM [axiom, in Complth.general_th_completeness]
LEM [axiom, in ComplsegP.general_segP_completeness]
LEM_prime [lemma, in GHC.classical_facts]
Lindenbaum [lemma, in GHC.Lindenbaum_lem]
Lindenbaum_pair [lemma, in GHC.Lindenbaum_lem_pair]
Lindenbaum_segment [lemma, in Complseg.general_seg_completeness]
Lindenbaum_ABsegment [lemma, in ComplsegAB.general_segAB_completeness]
Lindenbaum_cworld [lemma, in Complth.general_th_completeness]
Lindenbaum_Psegment_Diam [lemma, in ComplsegP.general_segP_completeness]
Lindenbaum_Psegment [lemma, in ComplsegP.general_segP_completeness]
Lindenbaum_lem_pair [library]
Lindenbaum_lem [library]
Lind_theory_extens [lemma, in GHC.Lindenbaum_lem]
Lind_theory [definition, in GHC.Lindenbaum_lem]
Listfilter_Permutation [lemma, in Sequent.Environments]
listform_opt_add2 [definition, in Sequent.G4WK.WKOrder]
list_disjR [lemma, in Sequent.G4CK.CKSequentProps]
list_disjL [lemma, in Sequent.G4CK.CKSequentProps]
list_conjL [lemma, in Sequent.G4CK.CKSequentProps]
list_conjR [lemma, in Sequent.G4CK.CKSequentProps]
list_split_union [lemma, in GHC.classical_facts]
list_Diam_map_repr [lemma, in Syntax.im_syntax]
list_Box_map_repr [lemma, in Syntax.im_syntax]
list_disj_map_Box [lemma, in Syntax.im_syntax]
list_disj [definition, in Syntax.im_syntax]
list_conj_map_Diam [lemma, in Syntax.im_syntax]
list_conj [definition, in Syntax.im_syntax]
list_Imp [definition, in Syntax.im_syntax]
list_disjR [lemma, in Sequent.G4WK.WKSequentProps]
list_disjL [lemma, in Sequent.G4WK.WKSequentProps]
list_conjL [lemma, in Sequent.G4WK.WKSequentProps]
list_conjR [lemma, in Sequent.G4WK.WKSequentProps]
list_filter_order [lemma, in Sequent.G4WK.WKOrder]
list_to_set_disj_open_boxes [lemma, in Sequent.Environments]
list_to_set_disj_rm [lemma, in Sequent.Environments]
list_to_set_disj_env_add [lemma, in Sequent.Environments]
list_filter_order [lemma, in Sequent.G4CK.CKOrder]
list_conj_Diam [lemma, in GHC.properties]
list_conj_Diam_obj [lemma, in GHC.properties]
list_disj_Box [lemma, in GHC.properties]
list_disj_Box_obj [lemma, in GHC.properties]
loc_conseq [definition, in Kripke.kripke_sem]
logic [library]
logic_props.AdAx_subst_clos [variable, in GHC.logic]
logic_props.AdAx [variable, in GHC.logic]
logic_props [section, in GHC.logic]
L_enum_exhaustive [lemma, in GHC.enum]
L_enum_cumulative [lemma, in GHC.enum]
L_enum [definition, in GHC.enum]
l_open_boxes_env_order [lemma, in Sequent.G4WK.WKOrder]
l_open_boxes_perm [lemma, in Sequent.Environments]
l_open_boxes_open_boxes_perm [lemma, in Sequent.Environments]
l_open_boxes_in [lemma, in Sequent.Environments]
l_open_boxes_app [lemma, in Sequent.Environments]
l_open_boxes_rm [lemma, in Sequent.Environments]
l_open_boxes [definition, in Sequent.Environments]
l_open_boxes_env_order [lemma, in Sequent.G4CK.CKOrder]

M

MAxioms [inductive, in GHC.CKH]
MAxioms_sind [definition, in GHC.CKH]
MAxioms_ind [definition, in GHC.CKH]
mdowncone [definition, in Kripke.correspondence]
Modal [section, in Sequent.Environments]
model [record, in Kripke.kripke_sem]
model_forces_iff_CdNd_model_forces [lemma, in Conservativity.CK_Cd_Nd_conserv_CK]
model_forces_iff_CdIdb_model_forces [lemma, in Conservativity.CK_Cd_Idb_conserv_CK]
monotL_Or [lemma, in GHC.properties]
monotR_Or [lemma, in GHC.properties]
monot_Or2 [lemma, in GHC.properties]
more_AdAx_more_prv [lemma, in GHC.properties]
MP [constructor, in GHC.CKH]
mreachable [projection, in Kripke.kripke_sem]
mreach_expl [projection, in Kripke.kripke_sem]
multeq_meq [lemma, in Sequent.Environments]
mupcone [definition, in Kripke.correspondence]
mvalid [definition, in Kripke.kripke_sem]

N

Natural_Deduction.AdAx [variable, in GHC.properties]
Natural_Deduction [section, in GHC.properties]
Nd [section, in Kripke.correspondence]
Nd [definition, in GHC.CKH]
Ndb [section, in Kripke.correspondence]
Ndb [definition, in GHC.CKH]
Ndb_frame [definition, in Kripke.correspondence]
Nd_frame [definition, in Kripke.correspondence]
ND_OrE [lemma, in GHC.properties]
ND_OrI2 [lemma, in GHC.properties]
ND_OrI1 [lemma, in GHC.properties]
ND_AndE2 [lemma, in GHC.properties]
ND_AndE1 [lemma, in GHC.properties]
ND_AndI [lemma, in GHC.properties]
ND_BotE [lemma, in GHC.properties]
Nec [constructor, in GHC.CKH]
Neg [definition, in Syntax.im_syntax]
negboxbot_negneg_box_prv [lemma, in Conservativity.CK_Idb_Ndb_not_conserv_CK]
negboxbot_negneg_box [section, in Conservativity.CK_Idb_Ndb_not_conserv_CK]
negneg_box_prv [lemma, in GHC.properties]
nLind_theory_extens_le [lemma, in GHC.Lindenbaum_lem]
nLind_theory_extens [lemma, in GHC.Lindenbaum_lem]
nLind_theory [definition, in GHC.Lindenbaum_lem]
NoAdAx [definition, in Complseg.CK_seg_completeness]
NoAdAxCd [definition, in ComplsegAB.CK_Cd_segAB_completeness]
NoAdAxCdIdb [definition, in Complth.CK_Cd_Idb_th_completeness]
NoAdAxIdb [definition, in ComplsegP.CK_Idb_segP_completeness]
nodes [projection, in Kripke.kripke_sem]
NoDup_remove [lemma, in GHC.properties]
not_In_pair_Lind_theory_deriv [lemma, in GHC.Lindenbaum_lem_pair]
not_In_Lind_theory_deriv [lemma, in GHC.Lindenbaum_lem]
npair_Lind_theory_extens_le [lemma, in GHC.Lindenbaum_lem_pair]
npair_Lind_theory_extens [lemma, in GHC.Lindenbaum_lem_pair]
npair_Lind_theory [definition, in GHC.Lindenbaum_lem_pair]

O

obF [instance, in Conservativity.CK_Idb_Ndb_not_conserv_CK]
obireach [definition, in Conservativity.CK_Idb_Ndb_not_conserv_CK]
obireach_expl [lemma, in Conservativity.CK_Idb_Ndb_not_conserv_CK]
obireach_trans [lemma, in Conservativity.CK_Idb_Ndb_not_conserv_CK]
obireach_refl [lemma, in Conservativity.CK_Idb_Ndb_not_conserv_CK]
obM [instance, in Conservativity.CK_Idb_Ndb_not_conserv_CK]
obmreach [definition, in Conservativity.CK_Idb_Ndb_not_conserv_CK]
obmreach_expl [lemma, in Conservativity.CK_Idb_Ndb_not_conserv_CK]
obM' [instance, in Conservativity.CK_wCD_Nd_not_conserv_CK]
obval [definition, in Conservativity.CK_Idb_Ndb_not_conserv_CK]
obval_expl [lemma, in Conservativity.CK_Idb_Ndb_not_conserv_CK]
obval_persist [lemma, in Conservativity.CK_Idb_Ndb_not_conserv_CK]
obval_expl' [lemma, in Conservativity.CK_wCD_Nd_not_conserv_CK]
obval_persist' [lemma, in Conservativity.CK_wCD_Nd_not_conserv_CK]
obval' [definition, in Conservativity.CK_wCD_Nd_not_conserv_CK]
occurs_in_opt [definition, in Sequent.syntax_facts]
occurs_in [definition, in Sequent.syntax_facts]
occurs_in_list_disj [lemma, in Sequent.Environments]
occurs_in_list_conj [lemma, in Sequent.Environments]
occurs_in_map_l_open_boxes [lemma, in Sequent.Environments]
occurs_in_map_open_box [lemma, in Sequent.Environments]
occurs_in_open_boxes [lemma, in Sequent.Environments]
openboxes_env_order [lemma, in Sequent.G4WK.WKOrder]
openboxes_env_order [lemma, in Sequent.G4CK.CKOrder]
open_boxes_case [lemma, in Sequent.G4CK.CKSequentProps]
open_boxes_case [lemma, in Sequent.G4WK.WKSequentProps]
open_boxes_env_order [lemma, in Sequent.G4WK.WKOrder]
open_boxes_remove_f [lemma, in Sequent.Environments]
open_boxes_remove_t [lemma, in Sequent.Environments]
open_boxes_add_f [lemma, in Sequent.Environments]
open_boxes_add_t [lemma, in Sequent.Environments]
open_boxes_singleton_f [lemma, in Sequent.Environments]
open_boxes_singleton_t [lemma, in Sequent.Environments]
open_boxes_disj_union [lemma, in Sequent.Environments]
open_boxes_empty [lemma, in Sequent.Environments]
open_boxes_open_boxes' [lemma, in Sequent.Environments]
open_boxes' [definition, in Sequent.Environments]
open_boxes [definition, in Sequent.Environments]
open_box [definition, in Sequent.Environments]
open_boxes_Diam_rule [lemma, in Sequent.G4WK.WKSoundComplete]
open_boxes_K_rule [lemma, in Sequent.G4WK.WKSoundComplete]
open_boxes_env_order [lemma, in Sequent.G4CK.CKOrder]
open_boxes_Diam_rule [lemma, in Sequent.G4CK.CKSoundComplete]
open_boxes_K_rule [lemma, in Sequent.G4CK.CKSoundComplete]
opt_weight [definition, in Sequent.G4WK.WKOrder]
opt_to_form [definition, in Sequent.G4WK.WKSoundComplete]
Or [constructor, in Syntax.im_syntax]
OrL [constructor, in Sequent.G4WK.WKSequents]
OrL [constructor, in Sequent.G4CK.CKSequents]
OrL_rev [lemma, in Sequent.G4CK.CKSequentProps]
OrL_rev [lemma, in Sequent.G4WK.WKSequentProps]
OrR_idemp [lemma, in Sequent.G4CK.CKSequentProps]
OrR_idemp [lemma, in Sequent.G4WK.WKSequentProps]
OrR1 [constructor, in Sequent.G4WK.WKSequents]
OrR1 [constructor, in Sequent.G4CK.CKSequents]
OrR1Bot_rev [lemma, in Sequent.G4CK.CKSequentProps]
OrR1Bot_rev [lemma, in Sequent.G4WK.WKSequentProps]
OrR2 [constructor, in Sequent.G4WK.WKSequents]
OrR2 [constructor, in Sequent.G4CK.CKSequents]
OrR2Bot_rev [lemma, in Sequent.G4CK.CKSequentProps]
OrR2Bot_rev [lemma, in Sequent.G4WK.WKSequentProps]
oud [definition, in Sequent.G4WK.WKSequents]

P

pair_Lind_theory_extens [lemma, in GHC.Lindenbaum_lem_pair]
pair_Lind_theory [definition, in GHC.Lindenbaum_lem_pair]
pair_choice_code [definition, in GHC.Lindenbaum_lem_pair]
pair_choice_form [definition, in GHC.Lindenbaum_lem_pair]
pair_extCKH_prv [definition, in GHC.Lindenbaum_lem_pair]
partial_finite [lemma, in GHC.classical_facts]
persist [projection, in Kripke.kripke_sem]
Persistence [lemma, in Kripke.kripke_sem]
pointed_env_order_refl [definition, in Sequent.G4WK.WKOrder]
pointed_env_order_None_L [lemma, in Sequent.G4WK.WKOrder]
pointed_env_order_bot_L [lemma, in Sequent.G4WK.WKOrder]
pointed_env_order_None_R [lemma, in Sequent.G4WK.WKOrder]
pointed_env_order_bot_R [lemma, in Sequent.G4WK.WKOrder]
pointed_env_ms_order [definition, in Sequent.G4WK.WKOrder]
pointed_env_order [definition, in Sequent.G4WK.WKOrder]
pointed_env [definition, in Sequent.G4WK.WKOrder]
pointed_env_order_refl [definition, in Sequent.G4CK.CKOrder]
pointed_env_order_bot_L [lemma, in Sequent.G4CK.CKOrder]
pointed_env_order_bot_R [lemma, in Sequent.G4CK.CKOrder]
pointed_env_ms_order [definition, in Sequent.G4CK.CKOrder]
pointed_env_order [definition, in Sequent.G4CK.CKOrder]
pointed_env [definition, in Sequent.G4CK.CKOrder]
pow5_gt_0 [lemma, in Sequent.G4WK.WKOrder]
pow5_gt_0 [lemma, in Sequent.G4CK.CKOrder]
pq_correct [lemma, in Sequent.G4WK.WKPropQuantifiers]
pq_correct [lemma, in Sequent.G4CK.CKPropQuantifiers]
Prime [projection, in Complth.general_th_completeness]
prime [definition, in GHC.Lindenbaum_lem]
prime_list_disj [lemma, in GHC.Lindenbaum_lem]
properties [library]
proper_Provable [instance, in Sequent.G4WK.WKSequents]
Proper_env_order_refl [instance, in Sequent.G4WK.WKOrder]
Proper_env_order [instance, in Sequent.G4WK.WKOrder]
Proper_env_order_refl_env_weight [instance, in Sequent.G4WK.WKOrder]
Proper_env_weight [instance, in Sequent.G4WK.WKOrder]
proper_rm [instance, in Sequent.G4WK.WKDecisionProcedure]
proper_rm [instance, in Sequent.G4CK.CKDecisionProcedure]
Proper_elements [instance, in Sequent.Environments]
proper_open_boxes [instance, in Sequent.Environments]
proper_open_boxes' [instance, in Sequent.Environments]
proper_difference [instance, in Sequent.Environments]
proper_disj_union [instance, in Sequent.Environments]
proper_elem_of [instance, in Sequent.Environments]
proper_Provable [instance, in Sequent.G4CK.CKSequents]
Proper_env_order_refl [instance, in Sequent.G4CK.CKOrder]
Proper_env_order [instance, in Sequent.G4CK.CKOrder]
Proper_env_order_refl_env_weight [instance, in Sequent.G4CK.CKOrder]
Proper_env_weight [instance, in Sequent.G4CK.CKOrder]
PropQuantDefinition [section, in Sequent.G4WK.WKPropQuantifiers]
PropQuantDefinition [section, in Sequent.G4CK.CKPropQuantifiers]
PropQuantDefinition.p [variable, in Sequent.G4WK.WKPropQuantifiers]
PropQuantDefinition.p [variable, in Sequent.G4CK.CKPropQuantifiers]
□⁻¹ _ [notation, in Sequent.G4WK.WKPropQuantifiers]
□⁻¹ _ [notation, in Sequent.G4CK.CKPropQuantifiers]
Provable [inductive, in Sequent.G4WK.WKSequents]
Provable [inductive, in Sequent.G4CK.CKSequents]
Provable_sind [definition, in Sequent.G4WK.WKSequents]
Provable_rec [definition, in Sequent.G4WK.WKSequents]
Provable_ind [definition, in Sequent.G4WK.WKSequents]
Provable_rect [definition, in Sequent.G4WK.WKSequents]
Provable_dec_of_Prop [lemma, in Sequent.G4WK.WKDecisionProcedure]
Provable_dec [lemma, in Sequent.G4WK.WKDecisionProcedure]
Provable_dec_of_Prop [lemma, in Sequent.G4CK.CKDecisionProcedure]
Provable_dec [lemma, in Sequent.G4CK.CKDecisionProcedure]
Provable_sind [definition, in Sequent.G4CK.CKSequents]
Provable_rec [definition, in Sequent.G4CK.CKSequents]
Provable_ind [definition, in Sequent.G4CK.CKSequents]
Provable_rect [definition, in Sequent.G4CK.CKSequents]
prv_list_left_conj [lemma, in GHC.properties]
prv_Top [lemma, in GHC.properties]
Psegment [record, in ComplsegP.general_segP_completeness]
p_contr [lemma, in Sequent.G4CK.CKSequentProps]
p_contr [lemma, in Sequent.G4WK.WKSequentProps]

Q

QuasiCompleteness [lemma, in Complseg.general_seg_completeness]
QuasiCompleteness [lemma, in ComplsegAB.general_segAB_completeness]
QuasiCompleteness [lemma, in Complth.general_th_completeness]
QuasiCompleteness [lemma, in ComplsegP.general_segP_completeness]
quasi_prime_pair_Lind_theory [lemma, in GHC.Lindenbaum_lem_pair]
quasi_prime_Lind_theory [lemma, in GHC.Lindenbaum_lem]
quasi_prime [definition, in GHC.Lindenbaum_lem]

R

remove_In_env_order [lemma, in Sequent.G4WK.WKOrder]
remove_In_env_order_refl [lemma, in Sequent.G4WK.WKOrder]
remove_env_order [lemma, in Sequent.G4WK.WKOrder]
remove_include [lemma, in Sequent.Environments]
remove_In_env_order [lemma, in Sequent.G4CK.CKOrder]
remove_In_env_order_refl [lemma, in Sequent.G4CK.CKOrder]
remove_env_order [lemma, in Sequent.G4CK.CKOrder]
remove_disj [lemma, in GHC.properties]
rm [definition, in Sequent.Environments]
rm_add [lemma, in Sequent.Environments]
rm_perm [lemma, in Sequent.Environments]
rm_perm_inside [lemma, in Sequent.Environments]
rm_notin [lemma, in Sequent.Environments]
rm_comm [lemma, in Sequent.Environments]

S

segAorB [projection, in ComplsegAB.general_segAB_completeness]
segClosed [projection, in Complseg.general_seg_completeness]
segClosed [projection, in ComplsegAB.general_segAB_completeness]
segClosed [projection, in ComplsegP.general_segP_completeness]
segment [record, in Complseg.general_seg_completeness]
segPrime [projection, in Complseg.general_seg_completeness]
segPrime [projection, in ComplsegAB.general_segAB_completeness]
segPrime [projection, in ComplsegP.general_segP_completeness]
segP_noBot_noDiamBot [projection, in ComplsegP.general_segP_completeness]
segP_noBot_DiamBot [projection, in ComplsegP.general_segP_completeness]
segP_Bot [projection, in ComplsegP.general_segP_completeness]
singleton [instance, in Sequent.Environments]
singletonMS [instance, in Sequent.Environments]
singleton_mult_notin [lemma, in Sequent.Environments]
singleton_mult_in [lemma, in Sequent.Environments]
Soundness [lemma, in Soundness.general_soundness]
Soundness [section, in Sequent.G4WK.WKSoundComplete]
Soundness [section, in Sequent.G4CK.CKSoundComplete]
strong_Cd_weak_Idb_Cd_Idb [lemma, in Kripke.correspondence]
strong_Cd_weak_Idb_frame [definition, in Kripke.correspondence]
strong_impl_suff_Cd [lemma, in Kripke.correspondence]
strong_is_suff_Cd [lemma, in Kripke.correspondence]
strong_Cd_frame [definition, in Kripke.correspondence]
Strong_Completeness [lemma, in Complseg.general_seg_completeness]
Strong_Completeness [lemma, in ComplsegAB.general_segAB_completeness]
Strong_Completeness [lemma, in Complth.general_th_completeness]
Strong_Completeness [lemma, in ComplsegP.general_segP_completeness]
SubAnd [constructor, in Sequent.syntax_facts]
SubBox [constructor, in Sequent.syntax_facts]
SubDiam [constructor, in Sequent.syntax_facts]
SubEq [constructor, in Sequent.syntax_facts]
subform [definition, in Syntax.im_syntax]
subformlist [definition, in Syntax.im_syntax]
subformP [inductive, in Sequent.syntax_facts]
subformP_sind [definition, in Sequent.syntax_facts]
subformP_ind [definition, in Sequent.syntax_facts]
subform_trans [lemma, in Syntax.im_syntax]
subform_id [lemma, in Syntax.im_syntax]
SubImpl [constructor, in Sequent.syntax_facts]
SubOr [constructor, in Sequent.syntax_facts]
subst [definition, in Syntax.im_syntax]
subst_Ax [lemma, in GHC.logic]
SubTheory [definition, in GHC.Lindenbaum_lem]
sufficient_Ndb [lemma, in Kripke.correspondence]
sufficient_Nd [lemma, in Kripke.correspondence]
sufficient_Idb [lemma, in Kripke.correspondence]
sufficient_Cd [lemma, in Kripke.correspondence]
suff_suff_suff_CKCdIdbNdb_Strong_Completeness [lemma, in Complth.CK_Cd_Idb_Ndb_th_completeness]
suff_CKIdbNdb_Strong_Completeness [lemma, in ComplsegP.CK_Idb_Ndb_segP_completeness]
suff_suff_CKIdbNdb_Strong_Completeness [lemma, in ComplsegP.CK_Idb_Ndb_segP_completeness]
suff_impl_Ndb [lemma, in Kripke.correspondence]
suff_Ndb_frame [definition, in Kripke.correspondence]
suff_CdIdb [section, in Kripke.correspondence]
suff_impl_Nd [lemma, in Kripke.correspondence]
suff_Nd_frame [definition, in Kripke.correspondence]
suff_impl_Idb [lemma, in Kripke.correspondence]
suff_Idb_frame [definition, in Kripke.correspondence]
suff_impl_Cd [lemma, in Kripke.correspondence]
suff_Cd_frame [definition, in Kripke.correspondence]
suff_suff_CKCdIdb_Strong_Completeness [lemma, in Complth.CK_Cd_Idb_th_completeness]
suff_CKIdb_Strong_Completeness [lemma, in ComplsegP.CK_Idb_segP_completeness]
suff_CKIdbNd_Strong_Completeness [lemma, in ComplsegP.CK_Idb_Nd_segP_completeness]
suff_suff_CKIdbNd_Strong_Completeness [lemma, in ComplsegP.CK_Idb_Nd_segP_completeness]
suff_CKCd_Strong_Completeness [lemma, in ComplsegAB.CK_Cd_segAB_completeness]
suff_CKCdNd_Strong_Completeness [lemma, in ComplsegAB.CK_Cd_Nd_segAB_completeness]
suff_CKCdNdb_Strong_Completeness [lemma, in ComplsegAB.CK_Cd_Ndb_segAB_completeness]
suff_suff_suff_IK_Strong_Completeness [lemma, in Complth.IK_th_completeness]
syntax_facts [library]

T

tail [projection, in Complseg.general_seg_completeness]
tail [projection, in ComplsegAB.general_segAB_completeness]
tail [projection, in ComplsegP.general_segP_completeness]
tbF [instance, in Conservativity.CK_Idb_Nd_not_conserv_CK]
tbF_Idb_Nd [lemma, in Conservativity.CK_Idb_Nd_not_conserv_CK]
tbireach [definition, in Conservativity.CK_Idb_Nd_not_conserv_CK]
tbireach_expl [lemma, in Conservativity.CK_Idb_Nd_not_conserv_CK]
tbireach_trans [lemma, in Conservativity.CK_Idb_Nd_not_conserv_CK]
tbireach_refl [lemma, in Conservativity.CK_Idb_Nd_not_conserv_CK]
tbM [instance, in Conservativity.CK_Idb_Nd_not_conserv_CK]
tbmreach [definition, in Conservativity.CK_Idb_Nd_not_conserv_CK]
tbmreach_expl [lemma, in Conservativity.CK_Idb_Nd_not_conserv_CK]
tbval [definition, in Conservativity.CK_Idb_Nd_not_conserv_CK]
tbval_expl [lemma, in Conservativity.CK_Idb_Nd_not_conserv_CK]
tbval_persist [lemma, in Conservativity.CK_Idb_Nd_not_conserv_CK]
th [projection, in Complth.general_th_completeness]
theorems_and_meta.Axioms [section, in GHC.properties]
theorems_and_meta.list_of_conjunctions [section, in GHC.properties]
theorems_and_meta.list_of_disjunctions [section, in GHC.properties]
theorems_and_meta.AdAx [variable, in GHC.properties]
theorems_and_meta [section, in GHC.properties]
Theory [definition, in GHC.Lindenbaum_lem]
Theory_AllForm [lemma, in GHC.Lindenbaum_lem]
Thm_irrel [lemma, in GHC.properties]
Top [definition, in Syntax.im_syntax]
TopL_rev [lemma, in Sequent.G4CK.CKSequentProps]
TopL_rev [lemma, in Sequent.G4WK.WKSequentProps]
transitive_form_order [instance, in Sequent.syntax_facts]
truth_lemma [lemma, in Complseg.general_seg_completeness]
truth_lemma [lemma, in ComplsegAB.general_segAB_completeness]
truth_lemma [lemma, in Complth.general_th_completeness]
truth_lemma [lemma, in ComplsegP.general_segP_completeness]

U

UnBox [definition, in Syntax.im_syntax]
Under_pair_Lind_theory [lemma, in GHC.Lindenbaum_lem_pair]
Under_npair_Lind_theory [lemma, in GHC.Lindenbaum_lem_pair]
Under_Lind_theory [lemma, in GHC.Lindenbaum_lem]
Under_nLind_theory [lemma, in GHC.Lindenbaum_lem]
union_difference_R [lemma, in Sequent.Environments]
union_difference_L [lemma, in Sequent.Environments]
union_mult [lemma, in Sequent.Environments]

V

val [projection, in Kripke.kripke_sem]
val_expl [projection, in Kripke.kripke_sem]
Var [constructor, in Syntax.im_syntax]
vars_incl [definition, in Sequent.G4WK.WKPropQuantifiers]
vars_incl [definition, in Sequent.G4CK.CKPropQuantifiers]
var_not_tautology [lemma, in Sequent.G4CK.CKSequentProps]
var_not_tautology [lemma, in Sequent.G4WK.WKSequentProps]
var_not_in_env [definition, in Sequent.Environments]

W

wCD [definition, in GHC.CKH]
wCDb_prv [section, in Conservativity.CK_wCD_Nd_not_conserv_CK]
weakening [lemma, in Sequent.G4CK.CKSequentProps]
weakening [lemma, in Sequent.G4WK.WKSequentProps]
weak_ImpL [lemma, in Sequent.G4CK.CKSequentProps]
weak_Idb_frame [definition, in Kripke.correspondence]
weak_ImpL [lemma, in Sequent.G4WK.WKSequentProps]
weight [definition, in Sequent.syntax_facts]
weight_tautology [lemma, in Sequent.G4CK.CKSequentProps]
weight_open_box [lemma, in Sequent.G4CK.CKSequentProps]
weight_ind [definition, in Sequent.syntax_facts]
weight_pos [lemma, in Sequent.syntax_facts]
weight_tautology [lemma, in Sequent.G4WK.WKSequentProps]
weight_open_box [lemma, in Sequent.G4WK.WKSequentProps]
weight_or_bot [lemma, in Sequent.G4WK.WKOrder]
weight_Diam_1 [lemma, in Sequent.G4WK.WKOrder]
weight_Box_1 [lemma, in Sequent.G4WK.WKOrder]
weight_Arrow_1 [lemma, in Sequent.G4WK.WKOrder]
weight_open_box [lemma, in Sequent.G4WK.WKOrder]
weight_or_bot [lemma, in Sequent.G4CK.CKOrder]
weight_Diam_1 [lemma, in Sequent.G4CK.CKOrder]
weight_Box_1 [lemma, in Sequent.G4CK.CKOrder]
weight_Arrow_1 [lemma, in Sequent.G4CK.CKOrder]
weight_open_box [lemma, in Sequent.G4CK.CKOrder]
wf_pointed_env_ms_order [lemma, in Sequent.G4WK.WKOrder]
wf_pointed_order [lemma, in Sequent.G4WK.WKOrder]
wf_env_order [definition, in Sequent.G4WK.WKOrder]
WF_pointed_env_order [instance, in Sequent.G4WK.WKPropQuantifiers]
wf_pointed_env_ms_order [lemma, in Sequent.G4CK.CKOrder]
wf_pointed_order [lemma, in Sequent.G4CK.CKOrder]
wf_env_order [definition, in Sequent.G4CK.CKOrder]
WF_pointed_env_order [instance, in Sequent.G4CK.CKPropQuantifiers]
WKCut [library]
WKDecisionProcedure [library]
WKH_prv [definition, in GHC.CKH]
WKOrder [library]
WKPropQuantifiers [library]
WKSequentProps [library]
WKSequents [library]
WKSoundComplete [library]
WK_extends_CKNdb [lemma, in Conservativity.CK_Cd_Nd_conserv_CK]
WK_conserv_CK [section, in Conservativity.CK_Cd_Nd_conserv_CK]
WK_Soundness [lemma, in Soundness.WK_soundness]
WK_soundness [section, in Soundness.WK_soundness]
WK_Strong_Completeness [lemma, in Complseg.WK_seg_completeness]
WK_completeness [section, in Complseg.WK_seg_completeness]
WK_uniform_interpolation [lemma, in Sequent.G4WK.WKPropQuantifiers]
WK_seg_completeness [library]
WK_soundness [library]

other

_ • _ (list_scope) [notation, in Sequent.G4WK.WKOrder]
_ • _ (list_scope) [notation, in Sequent.G4CK.CKOrder]
_ ⊢WK _ [notation, in Sequent.G4WK.WKSequents]
_ ⊢ _ [notation, in Sequent.G4WK.WKSequents]
_ ≺f _ [notation, in Sequent.syntax_facts]
_ → _ [notation, in Syntax.im_syntax]
_ ∨ _ [notation, in Syntax.im_syntax]
_ ∧ _ [notation, in Syntax.im_syntax]
_ ≺· _ [notation, in Sequent.G4WK.WKOrder]
_ ≼ _ [notation, in Sequent.G4WK.WKOrder]
_ ≺ _ [notation, in Sequent.G4WK.WKOrder]
_ ⊢? _ [notation, in Sequent.G4WK.WKDecisionProcedure]
_ ⊢? _ [notation, in Sequent.G4CK.CKDecisionProcedure]
_ • _ [notation, in Sequent.Environments]
_ ⊢CK _ [notation, in Sequent.G4CK.CKSequents]
_ ⊢ _ [notation, in Sequent.G4CK.CKSequents]
_ ≺· _ [notation, in Sequent.G4CK.CKOrder]
_ ≼ _ [notation, in Sequent.G4CK.CKOrder]
_ ≺ _ [notation, in Sequent.G4CK.CKOrder]
# _ [notation, in Syntax.im_syntax]
¬ _ [notation, in Syntax.im_syntax]
⊗ _ [notation, in Sequent.Environments]
⊙ _ [notation, in Sequent.Environments]
⊤ [notation, in Syntax.im_syntax]
⊥ [notation, in Syntax.im_syntax]
□ _ [notation, in Syntax.im_syntax]
◊ _ [notation, in Syntax.im_syntax]

---

Notation Index

P

□⁻¹ _ [in Sequent.G4WK.WKPropQuantifiers]
□⁻¹ _ [in Sequent.G4CK.CKPropQuantifiers]

other

_ • _ (list_scope) [in Sequent.G4WK.WKOrder]
_ • _ (list_scope) [in Sequent.G4CK.CKOrder]
_ ⊢WK _ [in Sequent.G4WK.WKSequents]
_ ⊢ _ [in Sequent.G4WK.WKSequents]
_ ≺f _ [in Sequent.syntax_facts]
_ → _ [in Syntax.im_syntax]
_ ∨ _ [in Syntax.im_syntax]
_ ∧ _ [in Syntax.im_syntax]
_ ≺· _ [in Sequent.G4WK.WKOrder]
_ ≼ _ [in Sequent.G4WK.WKOrder]
_ ≺ _ [in Sequent.G4WK.WKOrder]
_ ⊢? _ [in Sequent.G4WK.WKDecisionProcedure]
_ ⊢? _ [in Sequent.G4CK.CKDecisionProcedure]
_ • _ [in Sequent.Environments]
_ ⊢CK _ [in Sequent.G4CK.CKSequents]
_ ⊢ _ [in Sequent.G4CK.CKSequents]
_ ≺· _ [in Sequent.G4CK.CKOrder]
_ ≼ _ [in Sequent.G4CK.CKOrder]
_ ≺ _ [in Sequent.G4CK.CKOrder]
# _ [in Syntax.im_syntax]
¬ _ [in Syntax.im_syntax]
⊗ _ [in Sequent.Environments]
⊙ _ [in Sequent.Environments]
⊤ [in Syntax.im_syntax]
⊥ [in Syntax.im_syntax]
□ _ [in Syntax.im_syntax]
◊ _ [in Syntax.im_syntax]

---

Variable Index

A

Additional_ax.AdAx [in GHC.properties]

C

Classical_facts.AdAx [in GHC.classical_facts]
Classical_facts.LEM [in GHC.classical_facts]
Correctness.p [in Sequent.G4WK.WKPropQuantifiers]
Correctness.p [in Sequent.G4CK.CKPropQuantifiers]

F

forming_CdNd_model.M [in Conservativity.CK_Cd_Nd_conserv_CK]
forming_CdIdb_model.M [in Conservativity.CK_Cd_Idb_conserv_CK]

G

general_soundness.corresp_AdAx_FraP [in Soundness.general_soundness]
general_soundness.FraP [in Soundness.general_soundness]
general_soundness.AdAx [in Soundness.general_soundness]
General_Lind_pair.AdAx [in GHC.Lindenbaum_lem_pair]
general_seg_completeness.CF_ClassF [in Complseg.general_seg_completeness]
general_seg_completeness.ClassF_AdAx [in Complseg.general_seg_completeness]
general_seg_completeness.ClassF [in Complseg.general_seg_completeness]
general_seg_completeness.segment_prf_irrel [in Complseg.general_seg_completeness]
general_seg_completeness.AdAx [in Complseg.general_seg_completeness]
general_seg_completeness.LEM [in Complseg.general_seg_completeness]
general_segAB_completeness.CF_ClassF [in ComplsegAB.general_segAB_completeness]
general_segAB_completeness.ClassF_AdAx [in ComplsegAB.general_segAB_completeness]
general_segAB_completeness.ClassF [in ComplsegAB.general_segAB_completeness]
general_segAB_completeness.ABsegment_prf_irrel [in ComplsegAB.general_segAB_completeness]
general_segAB_completeness.AdAx [in ComplsegAB.general_segAB_completeness]
general_th_completeness.CF_ClassF [in Complth.general_th_completeness]
general_th_completeness.ClassF_AdAx [in Complth.general_th_completeness]
general_th_completeness.ClassF [in Complth.general_th_completeness]
general_th_completeness.cworld_prf_irrel [in Complth.general_th_completeness]
general_th_completeness.AdAx [in Complth.general_th_completeness]
General_Lind.AdAx [in GHC.Lindenbaum_lem]
general_segP_completeness.CF_ClassF [in ComplsegP.general_segP_completeness]
general_segP_completeness.ClassF_AdAx [in ComplsegP.general_segP_completeness]
general_segP_completeness.ClassF [in ComplsegP.general_segP_completeness]
general_segP_completeness.Psegment_prf_irrel [in ComplsegP.general_segP_completeness]
general_segP_completeness.AdAx [in ComplsegP.general_segP_completeness]

L

logic_props.AdAx_subst_clos [in GHC.logic]
logic_props.AdAx [in GHC.logic]

N

Natural_Deduction.AdAx [in GHC.properties]

P

PropQuantDefinition.p [in Sequent.G4WK.WKPropQuantifiers]
PropQuantDefinition.p [in Sequent.G4CK.CKPropQuantifiers]

T

theorems_and_meta.AdAx [in GHC.properties]

---

Library Index

C

CKCut
CKDecisionProcedure
CKH
CKH_export
CKOrder
CKPropQuantifiers
CKSequentProps
CKSequents
CKSoundComplete
CK_Ndb_soundness
CK_Ndb_seg_completeness
CK_Cd_soundness
CK_Idb_segP_completeness
CK_Idb_Nd_not_incl_CK_Cd_Idb_Ndb
CK_Idb_Ndb_not_conserv_CK
CK_Cd_Nd_segAB_completeness
CK_Cd_Ndb_segAB_completeness
CK_Idb_Nd_not_conserv_CK
CK_soundness
CK_Idb_Ndb_segP_completeness
CK_Cd_Idb_Ndb_th_completeness
CK_Cd_segAB_completeness
CK_Cd_Nd_conserv_CK
CK_Cd_Nd_soundness
CK_Cd_Idb_th_completeness
CK_Idb_Nd_segP_completeness
CK_Cd_Idb_soundness
CK_wCD_Nd_not_conserv_CK
CK_Idb_Ndb_soundness
CK_Cd_Idb_conserv_CK
CK_Idb_Nd_soundness
CK_seg_completeness
CK_Idb_soundness
CK_Cd_Ndb_soundness
CK_Cd_Idb_Ndb_soundness
classical_facts
correspondence

E

enum
Environments

G

general_soundness
general_segP_completeness
general_segAB_completeness
general_th_completeness
general_seg_completeness

I

IK_soundness
IK_th_completeness
im_syntax

K

kripke_sem
kripke_export

L

Lindenbaum_lem_pair
Lindenbaum_lem
logic

P

properties

S

syntax_facts

W

WKCut
WKDecisionProcedure
WKOrder
WKPropQuantifiers
WKSequentProps
WKSequents
WKSoundComplete
WK_seg_completeness
WK_soundness

---

Lemma Index

A

absorp_Or1 [in GHC.properties]
additive_cut [in Sequent.G4WK.WKCut]
additive_cut [in Sequent.G4CK.CKCut]
Af_right [in Sequent.G4WK.WKPropQuantifiers]
Af_right [in Sequent.G4CK.CKPropQuantifiers]
AndL_rev [in Sequent.G4CK.CKSequentProps]
AndL_rev [in Sequent.G4WK.WKSequentProps]
AndR_rev [in Sequent.G4CK.CKSequentProps]
AndR_rev [in Sequent.G4WK.WKSequentProps]
AndTopL_rev [in Sequent.G4WK.WKPropQuantifiers]
AndTopL_rev [in Sequent.G4CK.CKPropQuantifiers]
And_Imp [in GHC.properties]
Ax_valid [in Soundness.general_soundness]
A_right [in Sequent.G4WK.WKPropQuantifiers]
a_rule_env_spec [in Sequent.G4WK.WKPropQuantifiers]
a_rule_env17_vars [in Sequent.G4WK.WKPropQuantifiers]
a_rule_form_vars [in Sequent.G4WK.WKPropQuantifiers]
a_rule_env_vars [in Sequent.G4WK.WKPropQuantifiers]
a_rule_env17_cong_strong [in Sequent.G4WK.WKPropQuantifiers]
a_rule_form_cong_strong [in Sequent.G4WK.WKPropQuantifiers]
a_rule_env_cong_strong [in Sequent.G4WK.WKPropQuantifiers]
A_right [in Sequent.G4CK.CKPropQuantifiers]
a_rule_env_spec [in Sequent.G4CK.CKPropQuantifiers]
a_rule_env17_vars [in Sequent.G4CK.CKPropQuantifiers]
a_rule_env_form16_vars [in Sequent.G4CK.CKPropQuantifiers]
a_rule_form_vars [in Sequent.G4CK.CKPropQuantifiers]
a_rule_env_vars [in Sequent.G4CK.CKPropQuantifiers]
a_rule_env_form16_cong_strong [in Sequent.G4CK.CKPropQuantifiers]
a_rule_env17_cong_strong [in Sequent.G4CK.CKPropQuantifiers]
a_rule_form_cong_strong [in Sequent.G4CK.CKPropQuantifiers]
a_rule_env_cong_strong [in Sequent.G4CK.CKPropQuantifiers]
A16_right [in Sequent.G4CK.CKPropQuantifiers]
A17_right [in Sequent.G4WK.WKPropQuantifiers]
A17_right [in Sequent.G4CK.CKPropQuantifiers]

B

bF_suff_Idb [in Conservativity.CK_Idb_Nd_not_incl_CK_Cd_Idb_Ndb]
bF_suff_Ndb [in Conservativity.CK_Idb_Nd_not_incl_CK_Cd_Idb_Ndb]
bF_strong_Cd [in Conservativity.CK_Idb_Nd_not_incl_CK_Cd_Idb_Ndb]
bireach_expl [in Conservativity.CK_Idb_Nd_not_conserv_CK]
bireach_trans [in Conservativity.CK_Idb_Nd_not_conserv_CK]
bireach_refl [in Conservativity.CK_Idb_Nd_not_conserv_CK]
bmreach_expl [in Conservativity.CK_Idb_Nd_not_conserv_CK]
bot_not_tautology [in Sequent.G4CK.CKSequentProps]
bot_not_tautology [in Sequent.G4WK.WKSequentProps]
boxreflect [in ComplsegAB.general_segAB_completeness]
boxreflect [in ComplsegP.general_segP_completeness]
box_bot_not_tautology [in Sequent.G4CK.CKSequentProps]
box_var_not_tautology [in Sequent.G4CK.CKSequentProps]
box_bot_not_tautology [in Sequent.G4WK.WKSequentProps]
box_var_not_tautology [in Sequent.G4WK.WKSequentProps]
Box_distrib_list_Imp [in GHC.properties]
bval_expl [in Conservativity.CK_Idb_Nd_not_conserv_CK]
bval_persist [in Conservativity.CK_Idb_Nd_not_conserv_CK]

C

CdIdbireach_expl [in Conservativity.CK_Cd_Idb_conserv_CK]
CdIdbireach_tran [in Conservativity.CK_Cd_Idb_conserv_CK]
CdIdbireach_refl [in Conservativity.CK_Cd_Idb_conserv_CK]
CdIdbmreach_expl [in Conservativity.CK_Cd_Idb_conserv_CK]
CdIdbpersist [in Conservativity.CK_Cd_Idb_conserv_CK]
CdIdbval_expl [in Conservativity.CK_Cd_Idb_conserv_CK]
CdIdb_frame_former_Idb_frame [in Conservativity.CK_Cd_Idb_conserv_CK]
CdIdb_frame_former_strong_Cd_frame [in Conservativity.CK_Cd_Idb_conserv_CK]
CdNdireach_expl [in Conservativity.CK_Cd_Nd_conserv_CK]
CdNdireach_tran [in Conservativity.CK_Cd_Nd_conserv_CK]
CdNdireach_refl [in Conservativity.CK_Cd_Nd_conserv_CK]
CdNdmreach_expl [in Conservativity.CK_Cd_Nd_conserv_CK]
CdNdpersist [in Conservativity.CK_Cd_Nd_conserv_CK]
CdNdval_expl [in Conservativity.CK_Cd_Nd_conserv_CK]
CdNd_frame_former_Nd_frame [in Conservativity.CK_Cd_Nd_conserv_CK]
CdNd_frame_former_Cd_frame [in Conservativity.CK_Cd_Nd_conserv_CK]
cexpl_diamwitness [in Complseg.general_seg_completeness]
cexpl_boxreflect [in Complseg.general_seg_completeness]
cexpl_segPrime [in Complseg.general_seg_completeness]
cexpl_segClosed [in Complseg.general_seg_completeness]
cexpl_segAorB [in ComplsegAB.general_segAB_completeness]
cexpl_segPrime [in ComplsegAB.general_segAB_completeness]
cexpl_segClosed [in ComplsegAB.general_segAB_completeness]
cexpl_Prime [in Complth.general_th_completeness]
cexpl_Closed [in Complth.general_th_completeness]
cexpl_segP_noBot_noDiamBot [in ComplsegP.general_segP_completeness]
cexpl_segP_noBot_DiamBot [in ComplsegP.general_segP_completeness]
cexpl_segP_Bot [in ComplsegP.general_segP_completeness]
cexpl_segPrime [in ComplsegP.general_segP_completeness]
cexpl_segClosed [in ComplsegP.general_segP_completeness]
CF_Ndb [in Complth.CK_Cd_Idb_Ndb_th_completeness]
CF_suff_Ndb [in Complth.CK_Cd_Idb_Ndb_th_completeness]
CF_Ndb [in ComplsegP.CK_Idb_Ndb_segP_completeness]
CF_suff_Ndb [in ComplsegP.CK_Idb_Ndb_segP_completeness]
CF_Nd [in Complseg.WK_seg_completeness]
CF_Cd [in ComplsegAB.general_segAB_completeness]
CF_suff_Cd [in ComplsegAB.general_segAB_completeness]
CF_Nd [in ComplsegP.CK_Idb_Nd_segP_completeness]
CF_suff_Nd [in ComplsegP.CK_Idb_Nd_segP_completeness]
CF_suff_Idb [in Complth.general_th_completeness]
CF_CdIdb [in Complth.general_th_completeness]
CF_strong_Cd_weak_Idb [in Complth.general_th_completeness]
CF_Nd [in ComplsegAB.CK_Cd_Nd_segAB_completeness]
CF_Ndb [in Complseg.CK_Ndb_seg_completeness]
CF_Ndb [in ComplsegAB.CK_Cd_Ndb_segAB_completeness]
CF_Idb [in ComplsegP.general_segP_completeness]
CF_suff_Idb [in ComplsegP.general_segP_completeness]
CF_Nd [in Complth.IK_th_completeness]
CF_suff_Nd [in Complth.IK_th_completeness]
cireach_expl [in Complseg.general_seg_completeness]
cireach_trans [in Complseg.general_seg_completeness]
cireach_refl [in Complseg.general_seg_completeness]
cireach_expl [in ComplsegAB.general_segAB_completeness]
cireach_trans [in ComplsegAB.general_segAB_completeness]
cireach_refl [in ComplsegAB.general_segAB_completeness]
cireach_expl [in Complth.general_th_completeness]
cireach_trans [in Complth.general_th_completeness]
cireach_refl [in Complth.general_th_completeness]
cireach_expl [in ComplsegP.general_segP_completeness]
cireach_trans [in ComplsegP.general_segP_completeness]
cireach_refl [in ComplsegP.general_segP_completeness]
CKCdIdbNdb_Strong_Completeness [in Complth.CK_Cd_Idb_Ndb_th_completeness]
CKCdIdbNdb_Soundness [in Soundness.CK_Cd_Idb_Ndb_soundness]
CKCdIdb_Soundness [in Soundness.CK_Cd_Idb_soundness]
CKCdIdb_Strong_Completeness [in Complth.CK_Cd_Idb_th_completeness]
CKCdNdb_Soundness [in Soundness.CK_Cd_Ndb_soundness]
CKCdNdb_Strong_Completeness [in ComplsegAB.CK_Cd_Ndb_segAB_completeness]
CKCdNd_extends_CKCdNdb [in Conservativity.CK_Cd_Nd_conserv_CK]
CKCdNd_Soundness [in Soundness.CK_Cd_Nd_soundness]
CKCdNd_Strong_Completeness [in ComplsegAB.CK_Cd_Nd_segAB_completeness]
CKCd_Soundness [in Soundness.CK_Cd_soundness]
CKCd_Strong_Completeness [in ComplsegAB.CK_Cd_segAB_completeness]
CKIdbNdb_Strong_Completeness [in ComplsegP.CK_Idb_Ndb_segP_completeness]
CKIdbNdb_Soundness [in Soundness.CK_Idb_Ndb_soundness]
CKIdbNd_Soundness [in Soundness.CK_Idb_Nd_soundness]
CKIdbNd_Strong_Completeness [in ComplsegP.CK_Idb_Nd_segP_completeness]
CKIdbNd_not_included_CKIdbNdb [in Conservativity.CK_Idb_Nd_not_incl_CK_Cd_Idb_Ndb]
CKIdbNd_not_included_CKCdIdbNdb [in Conservativity.CK_Idb_Nd_not_incl_CK_Cd_Idb_Ndb]
CKIdb_Strong_Completeness [in ComplsegP.CK_Idb_segP_completeness]
CKIdb_Soundness [in Soundness.CK_Idb_soundness]
CKIdb_prv_wCD [in GHC.properties]
CKNdb_Soundness [in Soundness.CK_Ndb_soundness]
CKNdb_Strong_Completeness [in Complseg.CK_Ndb_seg_completeness]
CKwCDNd_prv_wCDb [in Conservativity.CK_wCD_Nd_not_conserv_CK]
CK_Soundness [in Soundness.CK_soundness]
CK_Strong_Completeness [in Complseg.CK_seg_completeness]
CK_uniform_interpolation [in Sequent.G4CK.CKPropQuantifiers]
closeder_pair_Lind_theory [in GHC.Lindenbaum_lem_pair]
closeder_Lind_theory [in GHC.Lindenbaum_lem]
cmreach_expl [in Complseg.general_seg_completeness]
cmreach_expl [in ComplsegAB.general_segAB_completeness]
cmreach_expl [in Complth.general_th_completeness]
cmreach_expl [in ComplsegP.general_segP_completeness]
comm_Or [in GHC.properties]
comm_Or_obj [in GHC.properties]
comm_And_obj [in GHC.properties]
Consist_pair_Lind_theory [in GHC.Lindenbaum_lem_pair]
Consist_npair_Lind_theory [in GHC.Lindenbaum_lem_pair]
Consist_Lind_theory [in GHC.Lindenbaum_lem]
Consist_nLind_theory [in GHC.Lindenbaum_lem]
contraction [in Sequent.G4CK.CKSequentProps]
contraction [in Sequent.G4WK.WKSequentProps]
Contr_Bot [in GHC.properties]
correspond_Ndb [in Kripke.correspondence]
correspond_Nd [in Kripke.correspondence]
correspond_Idb [in Kripke.correspondence]
correspond_Cd [in Kripke.correspondence]
cut [in Sequent.G4WK.WKCut]
cut [in Sequent.G4CK.CKCut]
cval_expl [in Complseg.general_seg_completeness]
cval_persist [in Complseg.general_seg_completeness]
cval_expl [in ComplsegAB.general_segAB_completeness]
cval_persist [in ComplsegAB.general_segAB_completeness]
cval_expl [in Complth.general_th_completeness]
cval_persist [in Complth.general_th_completeness]
cval_expl [in ComplsegP.general_segP_completeness]
cval_persist [in ComplsegP.general_segP_completeness]

D

decide_in [in Sequent.Environments]
der_pair_Lind_theory_npair_Lind_theory [in GHC.Lindenbaum_lem_pair]
der_npair_Lind_theory_mpair_Lind_theory_le [in GHC.Lindenbaum_lem_pair]
der_Lind_theory_nLind_theory [in GHC.Lindenbaum_lem]
der_nLind_theory_mLind_theory_le [in GHC.Lindenbaum_lem]
diamimp_partition [in Sequent.Environments]
diamwitness [in ComplsegAB.general_segAB_completeness]
diamwitness [in ComplsegP.general_segP_completeness]
diam_free_eq_CKNdb_CK [in Conservativity.CK_Cd_Nd_conserv_CK]
diam_free_eq_WK_CK [in Conservativity.CK_Cd_Nd_conserv_CK]
diam_free_eq_CKCd_CK [in Conservativity.CK_Cd_Nd_conserv_CK]
diam_free_eq_CKCdNdb_CK [in Conservativity.CK_Cd_Nd_conserv_CK]
diam_free_eq_CKCdNd_CK [in Conservativity.CK_Cd_Nd_conserv_CK]
diam_bot_not_tautology [in Sequent.G4CK.CKSequentProps]
diam_var_not_tautology [in Sequent.G4CK.CKSequentProps]
Diam_existence [in Complseg.general_seg_completeness]
diam_bot_not_tautology [in Sequent.G4WK.WKSequentProps]
diam_var_not_tautology [in Sequent.G4WK.WKSequentProps]
diam_free_eq_CKIdb_CK [in Conservativity.CK_Cd_Idb_conserv_CK]
diam_free_eq_CKCdIdb_CK [in Conservativity.CK_Cd_Idb_conserv_CK]
diam_free_strict_ext_CKIdbNdb_CK [in Conservativity.CK_Idb_Ndb_not_conserv_CK]
diam_free_ext_CKIdbNdb_CK [in Conservativity.CK_Idb_Ndb_not_conserv_CK]
diam_free_strict_ext_IK_CKIdbNd [in Conservativity.CK_Idb_Nd_not_conserv_CK]
diam_free_strict_ext_IK_CK [in Conservativity.CK_Idb_Nd_not_conserv_CK]
diam_free_ext_IK_CK [in Conservativity.CK_Idb_Nd_not_conserv_CK]
diam_free_strict_ext_CKIdbNd_CK [in Conservativity.CK_Idb_Nd_not_conserv_CK]
diam_free_ext_CKIdbNd_CK [in Conservativity.CK_Idb_Nd_not_conserv_CK]
Diam_distrib_list_disj [in GHC.properties]
Diam_rule [in GHC.properties]
diam_free_strict_ext_CKwCDNd_CK [in Conservativity.CK_wCD_Nd_not_conserv_CK]
diam_free_ext_CKwCDNd_CK [in Conservativity.CK_wCD_Nd_not_conserv_CK]
difference_include [in Sequent.Environments]
difference_singleton [in Sequent.Environments]
diff_not_in [in Sequent.Environments]
diff_mult [in Sequent.Environments]

E

EA_vars [in Sequent.G4WK.WKPropQuantifiers]
EA_cong [in Sequent.G4WK.WKPropQuantifiers]
EA_vars [in Sequent.G4CK.CKPropQuantifiers]
EA_cong [in Sequent.G4CK.CKPropQuantifiers]
EFQ [in GHC.properties]
elements_open_boxes_order [in Sequent.G4WK.WKOrder]
elements_elem_of [in Sequent.G4WK.WKOrder]
elements_list_to_set_disj [in Sequent.Environments]
elements_setminus [in Sequent.Environments]
elements_open_boxes [in Sequent.Environments]
elements_env_add [in Sequent.Environments]
elements_open_boxes_order [in Sequent.G4CK.CKOrder]
elements_elem_of [in Sequent.G4CK.CKOrder]
elem_of_list_In_1 [in Sequent.G4WK.WKOrder]
elem_of_open_boxes [in Sequent.Environments]
elem_of_list_In_1 [in Sequent.G4CK.CKOrder]
emptyweakR [in Sequent.G4WK.WKSequentProps]
entail_correct [in Sequent.G4WK.WKPropQuantifiers]
entail_correct [in Sequent.G4CK.CKPropQuantifiers]
env_order_le_lt_trans [in Sequent.G4WK.WKOrder]
env_order_lt_le_trans [in Sequent.G4WK.WKOrder]
env_order_refl_add' [in Sequent.G4WK.WKOrder]
env_order_refl_add [in Sequent.G4WK.WKOrder]
env_order_cancel_right [in Sequent.G4WK.WKOrder]
env_order_4 [in Sequent.G4WK.WKOrder]
env_order_3 [in Sequent.G4WK.WKOrder]
env_order_2 [in Sequent.G4WK.WKOrder]
env_order_1' [in Sequent.G4WK.WKOrder]
env_order_0' [in Sequent.G4WK.WKOrder]
env_order_0 [in Sequent.G4WK.WKOrder]
env_order_disj_union_compat_strong_left [in Sequent.G4WK.WKOrder]
env_order_disj_union_compat_strong_right [in Sequent.G4WK.WKOrder]
env_order_refl_disj_union_compat [in Sequent.G4WK.WKOrder]
env_order_disj_union_compat [in Sequent.G4WK.WKOrder]
env_order_disj_union_compat_right [in Sequent.G4WK.WKOrder]
env_order_disj_union_compat_left [in Sequent.G4WK.WKOrder]
env_order_add_compat [in Sequent.G4WK.WKOrder]
env_order_compat' [in Sequent.G4WK.WKOrder]
env_order_compat [in Sequent.G4WK.WKOrder]
env_order_1 [in Sequent.G4WK.WKOrder]
env_order_equiv_left_compat [in Sequent.G4WK.WKOrder]
env_order_equiv_right_compat [in Sequent.G4WK.WKOrder]
env_order_self [in Sequent.G4WK.WKOrder]
env_order_refl_trans [in Sequent.G4WK.WKOrder]
env_order_env_order_refl [in Sequent.G4WK.WKOrder]
env_order_singleton [in Sequent.G4WK.WKOrder]
env_weight_singleton [in Sequent.G4WK.WKOrder]
env_weight_add [in Sequent.G4WK.WKOrder]
env_weight_disj_union [in Sequent.G4WK.WKOrder]
env_equiv_eq [in Sequent.Environments]
env_add_inv' [in Sequent.Environments]
env_add_inv [in Sequent.Environments]
env_add_comm [in Sequent.Environments]
env_in_add [in Sequent.Environments]
env_add_remove [in Sequent.Environments]
env_replace [in Sequent.Environments]
env_order_le_lt_trans [in Sequent.G4CK.CKOrder]
env_order_lt_le_trans [in Sequent.G4CK.CKOrder]
env_order_refl_add' [in Sequent.G4CK.CKOrder]
env_order_refl_add [in Sequent.G4CK.CKOrder]
env_order_cancel_right [in Sequent.G4CK.CKOrder]
env_order_4 [in Sequent.G4CK.CKOrder]
env_order_3 [in Sequent.G4CK.CKOrder]
env_order_2 [in Sequent.G4CK.CKOrder]
env_order_1' [in Sequent.G4CK.CKOrder]
env_order_0' [in Sequent.G4CK.CKOrder]
env_order_0 [in Sequent.G4CK.CKOrder]
env_order_disj_union_compat_strong_left [in Sequent.G4CK.CKOrder]
env_order_disj_union_compat_strong_right [in Sequent.G4CK.CKOrder]
env_order_refl_disj_union_compat [in Sequent.G4CK.CKOrder]
env_order_disj_union_compat [in Sequent.G4CK.CKOrder]
env_order_disj_union_compat_right [in Sequent.G4CK.CKOrder]
env_order_disj_union_compat_left [in Sequent.G4CK.CKOrder]
env_order_add_compat [in Sequent.G4CK.CKOrder]
env_order_compat' [in Sequent.G4CK.CKOrder]
env_order_compat [in Sequent.G4CK.CKOrder]
env_order_1 [in Sequent.G4CK.CKOrder]
env_order_equiv_left_compat [in Sequent.G4CK.CKOrder]
env_order_equiv_right_compat [in Sequent.G4CK.CKOrder]
env_order_self [in Sequent.G4CK.CKOrder]
env_order_refl_trans [in Sequent.G4CK.CKOrder]
env_order_env_order_refl [in Sequent.G4CK.CKOrder]
env_order_singleton [in Sequent.G4CK.CKOrder]
env_weight_singleton [in Sequent.G4CK.CKOrder]
env_weight_add [in Sequent.G4CK.CKOrder]
env_weight_disj_union [in Sequent.G4CK.CKOrder]
equiv_disj_union_compat_l [in Sequent.Environments]
equiv_disj_union_compat_r [in Sequent.Environments]
eq_dec_form [in Syntax.im_syntax]
exfalso [in Sequent.G4CK.CKSequentProps]
exfalso [in Sequent.G4WK.WKSequentProps]
Expl [in Kripke.kripke_sem]
Explosion [in GHC.properties]
extCKH_finite [in GHC.logic]
extCKH_struct [in GHC.logic]
extCKH_comp [in GHC.logic]
extCKH_monot [in GHC.logic]
extCKH_Imp_list_Detachment_Deduction_Theorem [in GHC.properties]
extCKH_Deduction_Theorem [in GHC.properties]
extCKH_Detachment_Theorem [in GHC.properties]
E_of_empty [in Sequent.G4WK.WKPropQuantifiers]
E_left [in Sequent.G4WK.WKPropQuantifiers]
e_rule_12_vars [in Sequent.G4WK.WKPropQuantifiers]
e_rule_9_vars [in Sequent.G4WK.WKPropQuantifiers]
e_rule_vars [in Sequent.G4WK.WKPropQuantifiers]
e_rule_12_cong_strong [in Sequent.G4WK.WKPropQuantifiers]
e_rule_9_cong_strong [in Sequent.G4WK.WKPropQuantifiers]
e_rule_cong_strong [in Sequent.G4WK.WKPropQuantifiers]
e_rules_cong [in Sequent.G4WK.WKPropQuantifiers]
E_of_empty [in Sequent.G4CK.CKPropQuantifiers]
E_left [in Sequent.G4CK.CKPropQuantifiers]
e_rule_12_vars [in Sequent.G4CK.CKPropQuantifiers]
e_rule_9_vars [in Sequent.G4CK.CKPropQuantifiers]
e_rule_vars [in Sequent.G4CK.CKPropQuantifiers]
e_rule_12_cong_strong [in Sequent.G4CK.CKPropQuantifiers]
e_rule_9_cong_strong [in Sequent.G4CK.CKPropQuantifiers]
e_rule_cong_strong [in Sequent.G4CK.CKPropQuantifiers]
e_rules_cong [in Sequent.G4CK.CKPropQuantifiers]
E12_left [in Sequent.G4WK.WKPropQuantifiers]
E12_left [in Sequent.G4CK.CKPropQuantifiers]
E9_left [in Sequent.G4WK.WKPropQuantifiers]
E9_left [in Sequent.G4CK.CKPropQuantifiers]

F

filter_disj_union [in Sequent.Environments]
forall_list_conj [in GHC.properties]
forall_list_disj [in GHC.properties]
form_index_inj [in GHC.enum]
form_enum_index [in GHC.enum]
form_enum_sur [in GHC.enum]

G

generalised_contraction [in Sequent.G4CK.CKSequentProps]
generalised_axiom [in Sequent.G4CK.CKSequentProps]
generalised_weakeningR [in Sequent.G4CK.CKSequentProps]
generalised_weakeningL [in Sequent.G4CK.CKSequentProps]
generalised_contraction [in Sequent.G4WK.WKSequentProps]
generalised_axiom [in Sequent.G4WK.WKSequentProps]
generalised_weakeningR [in Sequent.G4WK.WKSequentProps]
generalised_weakeningL [in Sequent.G4WK.WKSequentProps]
gmultiset_elements_list_to_set_disj_perm [in Sequent.Environments]
gmultiset_elements_list_to_set_disj [in Sequent.Environments]
gmultiset_rec [in Sequent.Environments]
gmultiset_choose_or_empty [in Sequent.Environments]
G4CK_compl_CKH [in Sequent.G4CK.CKSoundComplete]
G4CK_sound_CKH [in Sequent.G4CK.CKSoundComplete]
G4WK_compl_WKH [in Sequent.G4WK.WKSoundComplete]
G4WK_sound_CKH [in Sequent.G4WK.WKSoundComplete]

H

height_0 [in Sequent.G4CK.CKSequentProps]
height_0 [in Sequent.G4WK.WKSequentProps]

I

IdL_list_disj [in GHC.properties]
IdL_list_disj_obj [in GHC.properties]
IdR_list_disj [in GHC.properties]
IdR_list_disj_obj [in GHC.properties]
IK_Soundness [in Soundness.IK_soundness]
IK_Strong_Completeness [in Complth.IK_th_completeness]
ImpBox_dup [in Sequent.G4CK.CKSequentProps]
ImpBox_dup [in Sequent.G4WK.WKSequentProps]
ImpL [in Sequent.G4CK.CKSequentProps]
ImpL [in Sequent.G4WK.WKSequentProps]
ImpLAnd_rev [in Sequent.G4CK.CKSequentProps]
ImpLAnd_rev [in Sequent.G4WK.WKSequentProps]
ImpLBox_prev [in Sequent.G4CK.CKSequentProps]
ImpLBox_prev [in Sequent.G4WK.WKSequentProps]
ImpLDiam_prev [in Sequent.G4CK.CKSequentProps]
ImpLDiam_prev [in Sequent.G4WK.WKSequentProps]
ImpLImp_dup [in Sequent.G4CK.CKSequentProps]
ImpLImp_prev [in Sequent.G4CK.CKSequentProps]
ImpLImp_dup [in Sequent.G4WK.WKSequentProps]
ImpLImp_prev [in Sequent.G4WK.WKSequentProps]
ImpLOr_rev [in Sequent.G4CK.CKSequentProps]
ImpLOr_rev [in Sequent.G4WK.WKSequentProps]
ImpLVar_rev [in Sequent.G4CK.CKSequentProps]
ImpLVar_rev [in Sequent.G4WK.WKSequentProps]
ImpR_rev [in Sequent.G4CK.CKSequentProps]
ImpR_rev [in Sequent.G4WK.WKSequentProps]
imp_cut [in Sequent.G4CK.CKSequentProps]
imp_cut [in Sequent.G4WK.WKSequentProps]
Imp_list_Imp [in GHC.properties]
Imp_And [in GHC.properties]
Imp_trans [in GHC.properties]
Imp_trans_help427 [in GHC.properties]
Imp_trans_help410 [in GHC.properties]
Imp_trans_help170 [in GHC.properties]
Imp_trans_help54 [in GHC.properties]
Imp_trans_help37 [in GHC.properties]
Imp_trans_help35 [in GHC.properties]
Imp_trans_help14 [in GHC.properties]
Imp_trans_help9 [in GHC.properties]
Imp_trans_help8 [in GHC.properties]
Imp_trans_help7 [in GHC.properties]
imp_Id_gen [in GHC.properties]
in_app_orT [in Sequent.syntax_facts]
In_form_dec [in Syntax.im_syntax]
In_open_boxes_t [in Sequent.Environments]
in_l_open_boxes [in Sequent.Environments]
in_in_rm [in Sequent.Environments]
in_rm [in Sequent.Environments]
in_difference [in Sequent.Environments]
in_map2_ext [in Sequent.Environments]
in_map_ext [in Sequent.Environments]
in_map_empty [in Sequent.Environments]
in_map2_in [in Sequent.Environments]
in_map_in [in Sequent.Environments]
in_in_map2 [in Sequent.Environments]
in_in_map [in Sequent.Environments]
In_Box_list_In_list [in GHC.properties]
In_list_In_Box_list [in GHC.properties]
In_remove [in GHC.properties]
is_box_weight_open_box [in Sequent.G4CK.CKSequentProps]
is_box_weight_open_box [in Sequent.G4WK.WKSequentProps]
is_not_box_open_box [in Sequent.Environments]

K

K_rule [in GHC.properties]
K_list_Imp [in GHC.properties]

L

LEM_prime [in GHC.classical_facts]
Lindenbaum [in GHC.Lindenbaum_lem]
Lindenbaum_pair [in GHC.Lindenbaum_lem_pair]
Lindenbaum_segment [in Complseg.general_seg_completeness]
Lindenbaum_ABsegment [in ComplsegAB.general_segAB_completeness]
Lindenbaum_cworld [in Complth.general_th_completeness]
Lindenbaum_Psegment_Diam [in ComplsegP.general_segP_completeness]
Lindenbaum_Psegment [in ComplsegP.general_segP_completeness]
Lind_theory_extens [in GHC.Lindenbaum_lem]
Listfilter_Permutation [in Sequent.Environments]
list_disjR [in Sequent.G4CK.CKSequentProps]
list_disjL [in Sequent.G4CK.CKSequentProps]
list_conjL [in Sequent.G4CK.CKSequentProps]
list_conjR [in Sequent.G4CK.CKSequentProps]
list_split_union [in GHC.classical_facts]
list_Diam_map_repr [in Syntax.im_syntax]
list_Box_map_repr [in Syntax.im_syntax]
list_disj_map_Box [in Syntax.im_syntax]
list_conj_map_Diam [in Syntax.im_syntax]
list_disjR [in Sequent.G4WK.WKSequentProps]
list_disjL [in Sequent.G4WK.WKSequentProps]
list_conjL [in Sequent.G4WK.WKSequentProps]
list_conjR [in Sequent.G4WK.WKSequentProps]
list_filter_order [in Sequent.G4WK.WKOrder]
list_to_set_disj_open_boxes [in Sequent.Environments]
list_to_set_disj_rm [in Sequent.Environments]
list_to_set_disj_env_add [in Sequent.Environments]
list_filter_order [in Sequent.G4CK.CKOrder]
list_conj_Diam [in GHC.properties]
list_conj_Diam_obj [in GHC.properties]
list_disj_Box [in GHC.properties]
list_disj_Box_obj [in GHC.properties]
L_enum_exhaustive [in GHC.enum]
L_enum_cumulative [in GHC.enum]
l_open_boxes_env_order [in Sequent.G4WK.WKOrder]
l_open_boxes_perm [in Sequent.Environments]
l_open_boxes_open_boxes_perm [in Sequent.Environments]
l_open_boxes_in [in Sequent.Environments]
l_open_boxes_app [in Sequent.Environments]
l_open_boxes_rm [in Sequent.Environments]
l_open_boxes_env_order [in Sequent.G4CK.CKOrder]

M

model_forces_iff_CdNd_model_forces [in Conservativity.CK_Cd_Nd_conserv_CK]
model_forces_iff_CdIdb_model_forces [in Conservativity.CK_Cd_Idb_conserv_CK]
monotL_Or [in GHC.properties]
monotR_Or [in GHC.properties]
monot_Or2 [in GHC.properties]
more_AdAx_more_prv [in GHC.properties]
multeq_meq [in Sequent.Environments]

N

ND_OrE [in GHC.properties]
ND_OrI2 [in GHC.properties]
ND_OrI1 [in GHC.properties]
ND_AndE2 [in GHC.properties]
ND_AndE1 [in GHC.properties]
ND_AndI [in GHC.properties]
ND_BotE [in GHC.properties]
negboxbot_negneg_box_prv [in Conservativity.CK_Idb_Ndb_not_conserv_CK]
negneg_box_prv [in GHC.properties]
nLind_theory_extens_le [in GHC.Lindenbaum_lem]
nLind_theory_extens [in GHC.Lindenbaum_lem]
NoDup_remove [in GHC.properties]
not_In_pair_Lind_theory_deriv [in GHC.Lindenbaum_lem_pair]
not_In_Lind_theory_deriv [in GHC.Lindenbaum_lem]
npair_Lind_theory_extens_le [in GHC.Lindenbaum_lem_pair]
npair_Lind_theory_extens [in GHC.Lindenbaum_lem_pair]

O

obireach_expl [in Conservativity.CK_Idb_Ndb_not_conserv_CK]
obireach_trans [in Conservativity.CK_Idb_Ndb_not_conserv_CK]
obireach_refl [in Conservativity.CK_Idb_Ndb_not_conserv_CK]
obmreach_expl [in Conservativity.CK_Idb_Ndb_not_conserv_CK]
obval_expl [in Conservativity.CK_Idb_Ndb_not_conserv_CK]
obval_persist [in Conservativity.CK_Idb_Ndb_not_conserv_CK]
obval_expl' [in Conservativity.CK_wCD_Nd_not_conserv_CK]
obval_persist' [in Conservativity.CK_wCD_Nd_not_conserv_CK]
occurs_in_list_disj [in Sequent.Environments]
occurs_in_list_conj [in Sequent.Environments]
occurs_in_map_l_open_boxes [in Sequent.Environments]
occurs_in_map_open_box [in Sequent.Environments]
occurs_in_open_boxes [in Sequent.Environments]
openboxes_env_order [in Sequent.G4WK.WKOrder]
openboxes_env_order [in Sequent.G4CK.CKOrder]
open_boxes_case [in Sequent.G4CK.CKSequentProps]
open_boxes_case [in Sequent.G4WK.WKSequentProps]
open_boxes_env_order [in Sequent.G4WK.WKOrder]
open_boxes_remove_f [in Sequent.Environments]
open_boxes_remove_t [in Sequent.Environments]
open_boxes_add_f [in Sequent.Environments]
open_boxes_add_t [in Sequent.Environments]
open_boxes_singleton_f [in Sequent.Environments]
open_boxes_singleton_t [in Sequent.Environments]
open_boxes_disj_union [in Sequent.Environments]
open_boxes_empty [in Sequent.Environments]
open_boxes_open_boxes' [in Sequent.Environments]
open_boxes_Diam_rule [in Sequent.G4WK.WKSoundComplete]
open_boxes_K_rule [in Sequent.G4WK.WKSoundComplete]
open_boxes_env_order [in Sequent.G4CK.CKOrder]
open_boxes_Diam_rule [in Sequent.G4CK.CKSoundComplete]
open_boxes_K_rule [in Sequent.G4CK.CKSoundComplete]
OrL_rev [in Sequent.G4CK.CKSequentProps]
OrL_rev [in Sequent.G4WK.WKSequentProps]
OrR_idemp [in Sequent.G4CK.CKSequentProps]
OrR_idemp [in Sequent.G4WK.WKSequentProps]
OrR1Bot_rev [in Sequent.G4CK.CKSequentProps]
OrR1Bot_rev [in Sequent.G4WK.WKSequentProps]
OrR2Bot_rev [in Sequent.G4CK.CKSequentProps]
OrR2Bot_rev [in Sequent.G4WK.WKSequentProps]

P

pair_Lind_theory_extens [in GHC.Lindenbaum_lem_pair]
partial_finite [in GHC.classical_facts]
Persistence [in Kripke.kripke_sem]
pointed_env_order_None_L [in Sequent.G4WK.WKOrder]
pointed_env_order_bot_L [in Sequent.G4WK.WKOrder]
pointed_env_order_None_R [in Sequent.G4WK.WKOrder]
pointed_env_order_bot_R [in Sequent.G4WK.WKOrder]
pointed_env_order_bot_L [in Sequent.G4CK.CKOrder]
pointed_env_order_bot_R [in Sequent.G4CK.CKOrder]
pow5_gt_0 [in Sequent.G4WK.WKOrder]
pow5_gt_0 [in Sequent.G4CK.CKOrder]
pq_correct [in Sequent.G4WK.WKPropQuantifiers]
pq_correct [in Sequent.G4CK.CKPropQuantifiers]
prime_list_disj [in GHC.Lindenbaum_lem]
Provable_dec_of_Prop [in Sequent.G4WK.WKDecisionProcedure]
Provable_dec [in Sequent.G4WK.WKDecisionProcedure]
Provable_dec_of_Prop [in Sequent.G4CK.CKDecisionProcedure]
Provable_dec [in Sequent.G4CK.CKDecisionProcedure]
prv_list_left_conj [in GHC.properties]
prv_Top [in GHC.properties]
p_contr [in Sequent.G4CK.CKSequentProps]
p_contr [in Sequent.G4WK.WKSequentProps]

Q

QuasiCompleteness [in Complseg.general_seg_completeness]
QuasiCompleteness [in ComplsegAB.general_segAB_completeness]
QuasiCompleteness [in Complth.general_th_completeness]
QuasiCompleteness [in ComplsegP.general_segP_completeness]
quasi_prime_pair_Lind_theory [in GHC.Lindenbaum_lem_pair]
quasi_prime_Lind_theory [in GHC.Lindenbaum_lem]

R

remove_In_env_order [in Sequent.G4WK.WKOrder]
remove_In_env_order_refl [in Sequent.G4WK.WKOrder]
remove_env_order [in Sequent.G4WK.WKOrder]
remove_include [in Sequent.Environments]
remove_In_env_order [in Sequent.G4CK.CKOrder]
remove_In_env_order_refl [in Sequent.G4CK.CKOrder]
remove_env_order [in Sequent.G4CK.CKOrder]
remove_disj [in GHC.properties]
rm_add [in Sequent.Environments]
rm_perm [in Sequent.Environments]
rm_perm_inside [in Sequent.Environments]
rm_notin [in Sequent.Environments]
rm_comm [in Sequent.Environments]

S

singleton_mult_notin [in Sequent.Environments]
singleton_mult_in [in Sequent.Environments]
Soundness [in Soundness.general_soundness]
strong_Cd_weak_Idb_Cd_Idb [in Kripke.correspondence]
strong_impl_suff_Cd [in Kripke.correspondence]
strong_is_suff_Cd [in Kripke.correspondence]
Strong_Completeness [in Complseg.general_seg_completeness]
Strong_Completeness [in ComplsegAB.general_segAB_completeness]
Strong_Completeness [in Complth.general_th_completeness]
Strong_Completeness [in ComplsegP.general_segP_completeness]
subform_trans [in Syntax.im_syntax]
subform_id [in Syntax.im_syntax]
subst_Ax [in GHC.logic]
sufficient_Ndb [in Kripke.correspondence]
sufficient_Nd [in Kripke.correspondence]
sufficient_Idb [in Kripke.correspondence]
sufficient_Cd [in Kripke.correspondence]
suff_suff_suff_CKCdIdbNdb_Strong_Completeness [in Complth.CK_Cd_Idb_Ndb_th_completeness]
suff_CKIdbNdb_Strong_Completeness [in ComplsegP.CK_Idb_Ndb_segP_completeness]
suff_suff_CKIdbNdb_Strong_Completeness [in ComplsegP.CK_Idb_Ndb_segP_completeness]
suff_impl_Ndb [in Kripke.correspondence]
suff_impl_Nd [in Kripke.correspondence]
suff_impl_Idb [in Kripke.correspondence]
suff_impl_Cd [in Kripke.correspondence]
suff_suff_CKCdIdb_Strong_Completeness [in Complth.CK_Cd_Idb_th_completeness]
suff_CKIdb_Strong_Completeness [in ComplsegP.CK_Idb_segP_completeness]
suff_CKIdbNd_Strong_Completeness [in ComplsegP.CK_Idb_Nd_segP_completeness]
suff_suff_CKIdbNd_Strong_Completeness [in ComplsegP.CK_Idb_Nd_segP_completeness]
suff_CKCd_Strong_Completeness [in ComplsegAB.CK_Cd_segAB_completeness]
suff_CKCdNd_Strong_Completeness [in ComplsegAB.CK_Cd_Nd_segAB_completeness]
suff_CKCdNdb_Strong_Completeness [in ComplsegAB.CK_Cd_Ndb_segAB_completeness]
suff_suff_suff_IK_Strong_Completeness [in Complth.IK_th_completeness]

T

tbF_Idb_Nd [in Conservativity.CK_Idb_Nd_not_conserv_CK]
tbireach_expl [in Conservativity.CK_Idb_Nd_not_conserv_CK]
tbireach_trans [in Conservativity.CK_Idb_Nd_not_conserv_CK]
tbireach_refl [in Conservativity.CK_Idb_Nd_not_conserv_CK]
tbmreach_expl [in Conservativity.CK_Idb_Nd_not_conserv_CK]
tbval_expl [in Conservativity.CK_Idb_Nd_not_conserv_CK]
tbval_persist [in Conservativity.CK_Idb_Nd_not_conserv_CK]
Theory_AllForm [in GHC.Lindenbaum_lem]
Thm_irrel [in GHC.properties]
TopL_rev [in Sequent.G4CK.CKSequentProps]
TopL_rev [in Sequent.G4WK.WKSequentProps]
truth_lemma [in Complseg.general_seg_completeness]
truth_lemma [in ComplsegAB.general_segAB_completeness]
truth_lemma [in Complth.general_th_completeness]
truth_lemma [in ComplsegP.general_segP_completeness]

U

Under_pair_Lind_theory [in GHC.Lindenbaum_lem_pair]
Under_npair_Lind_theory [in GHC.Lindenbaum_lem_pair]
Under_Lind_theory [in GHC.Lindenbaum_lem]
Under_nLind_theory [in GHC.Lindenbaum_lem]
union_difference_R [in Sequent.Environments]
union_difference_L [in Sequent.Environments]
union_mult [in Sequent.Environments]

V

var_not_tautology [in Sequent.G4CK.CKSequentProps]
var_not_tautology [in Sequent.G4WK.WKSequentProps]

W

weakening [in Sequent.G4CK.CKSequentProps]
weakening [in Sequent.G4WK.WKSequentProps]
weak_ImpL [in Sequent.G4CK.CKSequentProps]
weak_ImpL [in Sequent.G4WK.WKSequentProps]
weight_tautology [in Sequent.G4CK.CKSequentProps]
weight_open_box [in Sequent.G4CK.CKSequentProps]
weight_pos [in Sequent.syntax_facts]
weight_tautology [in Sequent.G4WK.WKSequentProps]
weight_open_box [in Sequent.G4WK.WKSequentProps]
weight_or_bot [in Sequent.G4WK.WKOrder]
weight_Diam_1 [in Sequent.G4WK.WKOrder]
weight_Box_1 [in Sequent.G4WK.WKOrder]
weight_Arrow_1 [in Sequent.G4WK.WKOrder]
weight_open_box [in Sequent.G4WK.WKOrder]
weight_or_bot [in Sequent.G4CK.CKOrder]
weight_Diam_1 [in Sequent.G4CK.CKOrder]
weight_Box_1 [in Sequent.G4CK.CKOrder]
weight_Arrow_1 [in Sequent.G4CK.CKOrder]
weight_open_box [in Sequent.G4CK.CKOrder]
wf_pointed_env_ms_order [in Sequent.G4WK.WKOrder]
wf_pointed_order [in Sequent.G4WK.WKOrder]
wf_pointed_env_ms_order [in Sequent.G4CK.CKOrder]
wf_pointed_order [in Sequent.G4CK.CKOrder]
WK_extends_CKNdb [in Conservativity.CK_Cd_Nd_conserv_CK]
WK_Soundness [in Soundness.WK_soundness]
WK_Strong_Completeness [in Complseg.WK_seg_completeness]
WK_uniform_interpolation [in Sequent.G4WK.WKPropQuantifiers]

---

Axiom Index

L

LEM [in ComplsegP.CK_Idb_Ndb_segP_completeness]
LEM [in Kripke.correspondence]
LEM [in ComplsegAB.general_segAB_completeness]
LEM [in ComplsegP.CK_Idb_Nd_segP_completeness]
LEM [in Complth.general_th_completeness]
LEM [in ComplsegP.general_segP_completeness]

---

Constructor Index

A

And [in Syntax.im_syntax]
AndL [in Sequent.G4WK.WKSequents]
AndL [in Sequent.G4CK.CKSequents]
AndR [in Sequent.G4WK.WKSequents]
AndR [in Sequent.G4CK.CKSequents]
Atom [in Sequent.G4WK.WKSequents]
Atom [in Sequent.G4CK.CKSequents]
Ax [in GHC.CKH]

B

Bot [in Syntax.im_syntax]
Box [in Syntax.im_syntax]
BoxR [in Sequent.G4WK.WKSequents]
BoxR [in Sequent.G4CK.CKSequents]

D

Diam [in Syntax.im_syntax]
DiamL [in Sequent.G4WK.WKSequents]
DiamL [in Sequent.G4CK.CKSequents]

E

ExFalso [in Sequent.G4WK.WKSequents]
ExFalso [in Sequent.G4CK.CKSequents]

I

IA1 [in GHC.CKH]
IA2 [in GHC.CKH]
IA3 [in GHC.CKH]
IA4 [in GHC.CKH]
IA5 [in GHC.CKH]
IA6 [in GHC.CKH]
IA7 [in GHC.CKH]
IA8 [in GHC.CKH]
IA9 [in GHC.CKH]
Id [in GHC.CKH]
Imp [in Syntax.im_syntax]
ImpBox [in Sequent.G4WK.WKSequents]
ImpBox [in Sequent.G4CK.CKSequents]
ImpDiam [in Sequent.G4WK.WKSequents]
ImpDiam [in Sequent.G4CK.CKSequents]
ImpLAnd [in Sequent.G4WK.WKSequents]
ImpLAnd [in Sequent.G4CK.CKSequents]
ImpLImp [in Sequent.G4WK.WKSequents]
ImpLImp [in Sequent.G4CK.CKSequents]
ImpLOr [in Sequent.G4WK.WKSequents]
ImpLOr [in Sequent.G4CK.CKSequents]
ImpLVar [in Sequent.G4WK.WKSequents]
ImpLVar [in Sequent.G4CK.CKSequents]
ImpR [in Sequent.G4WK.WKSequents]
ImpR [in Sequent.G4CK.CKSequents]

K

Kb [in GHC.CKH]
Kd [in GHC.CKH]

M

MP [in GHC.CKH]

N

Nec [in GHC.CKH]

O

Or [in Syntax.im_syntax]
OrL [in Sequent.G4WK.WKSequents]
OrL [in Sequent.G4CK.CKSequents]
OrR1 [in Sequent.G4WK.WKSequents]
OrR1 [in Sequent.G4CK.CKSequents]
OrR2 [in Sequent.G4WK.WKSequents]
OrR2 [in Sequent.G4CK.CKSequents]

S

SubAnd [in Sequent.syntax_facts]
SubBox [in Sequent.syntax_facts]
SubDiam [in Sequent.syntax_facts]
SubEq [in Sequent.syntax_facts]
SubImpl [in Sequent.syntax_facts]
SubOr [in Sequent.syntax_facts]

V

Var [in Syntax.im_syntax]

---

Inductive Index

E

extCKH_prv [in GHC.CKH]

F

form [in Syntax.im_syntax]

I

IAxioms [in GHC.CKH]

M

MAxioms [in GHC.CKH]

P

Provable [in Sequent.G4WK.WKSequents]
Provable [in Sequent.G4CK.CKSequents]

S

subformP [in Sequent.syntax_facts]

---

Projection Index

B

boxreflect [in Complseg.general_seg_completeness]

C

Closed [in Complth.general_th_completeness]

D

diamwitness [in Complseg.general_seg_completeness]

E

expl [in Kripke.kripke_sem]

F

fra [in Kripke.kripke_sem]

H

head [in Complseg.general_seg_completeness]
head [in ComplsegAB.general_segAB_completeness]
head [in ComplsegP.general_segP_completeness]

I

ireachable [in Kripke.kripke_sem]
ireach_expl [in Kripke.kripke_sem]
ireach_tran [in Kripke.kripke_sem]
ireach_refl [in Kripke.kripke_sem]

M

mreachable [in Kripke.kripke_sem]
mreach_expl [in Kripke.kripke_sem]

N

nodes [in Kripke.kripke_sem]

P

persist [in Kripke.kripke_sem]
Prime [in Complth.general_th_completeness]

S

segAorB [in ComplsegAB.general_segAB_completeness]
segClosed [in Complseg.general_seg_completeness]
segClosed [in ComplsegAB.general_segAB_completeness]
segClosed [in ComplsegP.general_segP_completeness]
segPrime [in Complseg.general_seg_completeness]
segPrime [in ComplsegAB.general_segAB_completeness]
segPrime [in ComplsegP.general_segP_completeness]
segP_noBot_noDiamBot [in ComplsegP.general_segP_completeness]
segP_noBot_DiamBot [in ComplsegP.general_segP_completeness]
segP_Bot [in ComplsegP.general_segP_completeness]

T

tail [in Complseg.general_seg_completeness]
tail [in ComplsegAB.general_segAB_completeness]
tail [in ComplsegP.general_segP_completeness]
th [in Complth.general_th_completeness]

V

val [in Kripke.kripke_sem]
val_expl [in Kripke.kripke_sem]

---

Section Index

A

Additional_ax [in GHC.properties]

C

Cd [in Kripke.correspondence]
CKCdIdb_conserv_CK [in Conservativity.CK_Cd_Idb_conserv_CK]
CKCdNdb_conserv_CK [in Conservativity.CK_Cd_Nd_conserv_CK]
CKCdNd_conserv_CK [in Conservativity.CK_Cd_Nd_conserv_CK]
CKCd_conserv_CK [in Conservativity.CK_Cd_Nd_conserv_CK]
CKIdbNdb_not_conserv_CK [in Conservativity.CK_Idb_Ndb_not_conserv_CK]
CKIdbNd_not_conserv_CK [in Conservativity.CK_Idb_Nd_not_conserv_CK]
CKIdbNd_not_incl_CKIdbNdb [in Conservativity.CK_Idb_Nd_not_incl_CK_Cd_Idb_Ndb]
CKIdbNd_not_incl_CKCdIdbNdb [in Conservativity.CK_Idb_Nd_not_incl_CK_Cd_Idb_Ndb]
CKIdb_conserv_CK [in Conservativity.CK_Cd_Idb_conserv_CK]
CKNdb_conserv_CK [in Conservativity.CK_Cd_Nd_conserv_CK]
CKNdb_completeness [in Complseg.CK_Ndb_seg_completeness]
CKwCDNd_not_conserv_CK [in Conservativity.CK_wCD_Nd_not_conserv_CK]
CK_Cd_Ndb_soundness [in Soundness.CK_Cd_Ndb_soundness]
CK_Cd_Idb_Ndb_completeness [in Complth.CK_Cd_Idb_Ndb_th_completeness]
CK_Cd_soundness [in Soundness.CK_Cd_soundness]
CK_Idb_Ndb_completeness [in ComplsegP.CK_Idb_Ndb_segP_completeness]
CK_Cd_Idb_soundness [in Soundness.CK_Cd_Idb_soundness]
CK_Ndb_soundness [in Soundness.CK_Ndb_soundness]
CK_Cd_Idb_completeness [in Complth.CK_Cd_Idb_th_completeness]
CK_Idb_completeness [in ComplsegP.CK_Idb_segP_completeness]
CK_Idb_Nd_soundness [in Soundness.CK_Idb_Nd_soundness]
CK_soundness [in Soundness.CK_soundness]
CK_Cd_Nd_soundness [in Soundness.CK_Cd_Nd_soundness]
CK_Idb_Nd_completeness [in ComplsegP.CK_Idb_Nd_segP_completeness]
CK_Idb_Ndb_soundness [in Soundness.CK_Idb_Ndb_soundness]
CK_Cd_completeness [in ComplsegAB.CK_Cd_segAB_completeness]
CK_Idb_soundness [in Soundness.CK_Idb_soundness]
CK_Cd_Nd_completeness [in ComplsegAB.CK_Cd_Nd_segAB_completeness]
CK_completeness [in Complseg.CK_seg_completeness]
CK_Cd_Ndb_completeness [in ComplsegAB.CK_Cd_Ndb_segAB_completeness]
CK_Cd_Idb_Ndb_soundness [in Soundness.CK_Cd_Idb_Ndb_soundness]
Classical_facts [in GHC.classical_facts]
Completeness [in Sequent.G4WK.WKSoundComplete]
Completeness [in Sequent.G4CK.CKSoundComplete]
Correctness [in Sequent.G4WK.WKPropQuantifiers]
Correctness [in Sequent.G4CK.CKPropQuantifiers]
Correctness.EntailmentCorrect [in Sequent.G4WK.WKPropQuantifiers]
Correctness.EntailmentCorrect [in Sequent.G4CK.CKPropQuantifiers]
Correctness.PropQuantCorrect [in Sequent.G4WK.WKPropQuantifiers]
Correctness.PropQuantCorrect [in Sequent.G4CK.CKPropQuantifiers]
Correctness.VariablesCorrect [in Sequent.G4WK.WKPropQuantifiers]
Correctness.VariablesCorrect [in Sequent.G4CK.CKPropQuantifiers]
CountablyManyFormulas [in Sequent.syntax_facts]

F

forming_CdNd_model [in Conservativity.CK_Cd_Nd_conserv_CK]
forming_CdIdb_model [in Conservativity.CK_Cd_Idb_conserv_CK]

G

GeneralEnvironments [in Sequent.Environments]
general_soundness [in Soundness.general_soundness]
General_Lind_pair.Lindenbaum_lemma [in GHC.Lindenbaum_lem_pair]
General_Lind_pair.PrimeProps [in GHC.Lindenbaum_lem_pair]
General_Lind_pair.Prime [in GHC.Lindenbaum_lem_pair]
General_Lind_pair.Pair [in GHC.Lindenbaum_lem_pair]
General_Lind_pair [in GHC.Lindenbaum_lem_pair]
general_seg_completeness [in Complseg.general_seg_completeness]
general_segAB_completeness [in ComplsegAB.general_segAB_completeness]
general_th_completeness [in Complth.general_th_completeness]
General_Lind.Lindenbaum_lemma [in GHC.Lindenbaum_lem]
General_Lind.PrimeProps [in GHC.Lindenbaum_lem]
General_Lind.Prime [in GHC.Lindenbaum_lem]
General_Lind.prelims [in GHC.Lindenbaum_lem]
General_Lind.Sets_of_forms [in GHC.Lindenbaum_lem]
General_Lind [in GHC.Lindenbaum_lem]
general_segP_completeness [in ComplsegP.general_segP_completeness]

I

Idb [in Kripke.correspondence]
IK_soundness [in Soundness.IK_soundness]
IK_not_conserv_CKIdbNd [in Conservativity.CK_Idb_Nd_not_conserv_CK]
IK_not_conserv_CK [in Conservativity.CK_Idb_Nd_not_conserv_CK]
IK_completeness [in Complth.IK_th_completeness]

K

kripke_sem [in Kripke.kripke_sem]

L

logic_props [in GHC.logic]

M

Modal [in Sequent.Environments]

N

Natural_Deduction [in GHC.properties]
Nd [in Kripke.correspondence]
Ndb [in Kripke.correspondence]
negboxbot_negneg_box [in Conservativity.CK_Idb_Ndb_not_conserv_CK]

P

PropQuantDefinition [in Sequent.G4WK.WKPropQuantifiers]
PropQuantDefinition [in Sequent.G4CK.CKPropQuantifiers]

S

Soundness [in Sequent.G4WK.WKSoundComplete]
Soundness [in Sequent.G4CK.CKSoundComplete]
suff_CdIdb [in Kripke.correspondence]

T

theorems_and_meta.Axioms [in GHC.properties]
theorems_and_meta.list_of_conjunctions [in GHC.properties]
theorems_and_meta.list_of_disjunctions [in GHC.properties]
theorems_and_meta [in GHC.properties]

W

wCDb_prv [in Conservativity.CK_wCD_Nd_not_conserv_CK]
WK_conserv_CK [in Conservativity.CK_Cd_Nd_conserv_CK]
WK_soundness [in Soundness.WK_soundness]
WK_completeness [in Complseg.WK_seg_completeness]

---

Instance Index

B

bF [in Conservativity.CK_Idb_Nd_not_conserv_CK]
bM [in Conservativity.CK_Idb_Nd_not_conserv_CK]

C

CdIdb_model_former [in Conservativity.CK_Cd_Idb_conserv_CK]
CdIdb_frame_former [in Conservativity.CK_Cd_Idb_conserv_CK]
CdNd_model_former [in Conservativity.CK_Cd_Nd_conserv_CK]
CdNd_frame_former [in Conservativity.CK_Cd_Nd_conserv_CK]
cexpl [in Complseg.general_seg_completeness]
cexpl [in ComplsegAB.general_segAB_completeness]
cexpl [in Complth.general_th_completeness]
cexpl [in ComplsegP.general_segP_completeness]
CF [in Complseg.general_seg_completeness]
CF [in ComplsegAB.general_segAB_completeness]
CF [in Complth.general_th_completeness]
CF [in ComplsegP.general_segP_completeness]
CM [in Complseg.general_seg_completeness]
CM [in ComplsegAB.general_segAB_completeness]
CM [in Complth.general_th_completeness]
CM [in ComplsegP.general_segP_completeness]

D

decidable_is_diam_implication [in Sequent.Environments]
decidable_is_negation [in Sequent.Environments]
decidable_is_implication [in Sequent.Environments]
decidable_is_double_negation [in Sequent.Environments]

E

env_order_trans [in Sequent.G4WK.WKOrder]
env_order_trans [in Sequent.G4CK.CKOrder]
equiv_assoc [in Sequent.Environments]

F

fomula_top [in Sequent.syntax_facts]
fomula_bottom [in Sequent.syntax_facts]
form_count [in Sequent.syntax_facts]
form_eq_dec [in Sequent.syntax_facts]

I

irreflexive_form_order [in Sequent.syntax_facts]

O

obF [in Conservativity.CK_Idb_Ndb_not_conserv_CK]
obM [in Conservativity.CK_Idb_Ndb_not_conserv_CK]
obM' [in Conservativity.CK_wCD_Nd_not_conserv_CK]

P

proper_Provable [in Sequent.G4WK.WKSequents]
Proper_env_order_refl [in Sequent.G4WK.WKOrder]
Proper_env_order [in Sequent.G4WK.WKOrder]
Proper_env_order_refl_env_weight [in Sequent.G4WK.WKOrder]
Proper_env_weight [in Sequent.G4WK.WKOrder]
proper_rm [in Sequent.G4WK.WKDecisionProcedure]
proper_rm [in Sequent.G4CK.CKDecisionProcedure]
Proper_elements [in Sequent.Environments]
proper_open_boxes [in Sequent.Environments]
proper_open_boxes' [in Sequent.Environments]
proper_difference [in Sequent.Environments]
proper_disj_union [in Sequent.Environments]
proper_elem_of [in Sequent.Environments]
proper_Provable [in Sequent.G4CK.CKSequents]
Proper_env_order_refl [in Sequent.G4CK.CKOrder]
Proper_env_order [in Sequent.G4CK.CKOrder]
Proper_env_order_refl_env_weight [in Sequent.G4CK.CKOrder]
Proper_env_weight [in Sequent.G4CK.CKOrder]

S

singleton [in Sequent.Environments]
singletonMS [in Sequent.Environments]

T

tbF [in Conservativity.CK_Idb_Nd_not_conserv_CK]
tbM [in Conservativity.CK_Idb_Nd_not_conserv_CK]
transitive_form_order [in Sequent.syntax_facts]

W

WF_pointed_env_order [in Sequent.G4WK.WKPropQuantifiers]
WF_pointed_env_order [in Sequent.G4CK.CKPropQuantifiers]

---

Definition Index

A

A [in Sequent.G4WK.WKPropQuantifiers]
A [in Sequent.G4CK.CKPropQuantifiers]
AdAxCd [in ComplsegAB.general_segAB_completeness]
AdAxCd [in GHC.properties]
AdAxCdIdb [in Complth.general_th_completeness]
AdAxIdb [in ComplsegP.general_segP_completeness]
Af [in Sequent.G4WK.WKPropQuantifiers]
Af [in Sequent.G4CK.CKPropQuantifiers]
AllForm [in GHC.Lindenbaum_lem]
Axioms [in GHC.CKH]
a_rule_form [in Sequent.G4WK.WKPropQuantifiers]
a_rule_env17 [in Sequent.G4WK.WKPropQuantifiers]
a_rule_env [in Sequent.G4WK.WKPropQuantifiers]
a_rule_form [in Sequent.G4CK.CKPropQuantifiers]
a_rule_env17 [in Sequent.G4CK.CKPropQuantifiers]
a_rule_env_form16 [in Sequent.G4CK.CKPropQuantifiers]
a_rule_env [in Sequent.G4CK.CKPropQuantifiers]

B

bireach [in Conservativity.CK_Idb_Nd_not_conserv_CK]
bmreach [in Conservativity.CK_Idb_Nd_not_conserv_CK]
Box_list [in Syntax.im_syntax]
bval [in Conservativity.CK_Idb_Nd_not_conserv_CK]

C

Cd [in GHC.CKH]
CdIdbireach [in Conservativity.CK_Cd_Idb_conserv_CK]
CdIdbmreach [in Conservativity.CK_Cd_Idb_conserv_CK]
CdIdbNb_frame [in Soundness.IK_soundness]
CdIdbNdb_frame [in Soundness.CK_Cd_Idb_Ndb_soundness]
CdIdbval [in Conservativity.CK_Cd_Idb_conserv_CK]
CdIdb_frame [in Soundness.CK_Cd_Idb_soundness]
CdNdb_frame [in Soundness.CK_Cd_Ndb_soundness]
CdNdireach [in Conservativity.CK_Cd_Nd_conserv_CK]
CdNdmreach [in Conservativity.CK_Cd_Nd_conserv_CK]
CdNdval [in Conservativity.CK_Cd_Nd_conserv_CK]
CdNd_frame [in Soundness.CK_Cd_Nd_soundness]
Cd_frame [in Kripke.correspondence]
choice_code [in GHC.Lindenbaum_lem]
choice_form [in GHC.Lindenbaum_lem]
cireach [in Complseg.general_seg_completeness]
cireach [in ComplsegAB.general_segAB_completeness]
cireach [in Complth.general_th_completeness]
cireach [in ComplsegP.general_segP_completeness]
CKCdH_prv [in GHC.CKH]
CKCdIdbH_prv [in GHC.CKH]
CKCdIdbNdbH_prv [in GHC.CKH]
CKCdNdbH_prv [in GHC.CKH]
CKCdNdH_prv [in GHC.CKH]
CKCdwCDH_prv [in GHC.CKH]
CKH_prv [in GHC.CKH]
CKIdbH_prv [in GHC.CKH]
CKIdbNdbH_prv [in GHC.CKH]
CKIdbNdH_prv [in GHC.CKH]
CKNdbH_prv [in GHC.CKH]
CKwCDH_prv [in GHC.CKH]
CKwCDNdH_prv [in GHC.CKH]
closed [in GHC.Lindenbaum_lem]
cmreach [in Complseg.general_seg_completeness]
cmreach [in ComplsegAB.general_segAB_completeness]
cmreach [in Complth.general_th_completeness]
cmreach [in ComplsegP.general_segP_completeness]
cval [in Complseg.general_seg_completeness]
cval [in ComplsegAB.general_segAB_completeness]
cval [in Complth.general_th_completeness]
cval [in ComplsegP.general_segP_completeness]

D

diam_free [in Syntax.im_syntax]

E

E [in Sequent.G4WK.WKPropQuantifiers]
E [in Sequent.G4CK.CKPropQuantifiers]
EA [in Sequent.G4WK.WKPropQuantifiers]
EA [in Sequent.G4CK.CKPropQuantifiers]
Ef [in Sequent.G4WK.WKPropQuantifiers]
Ef [in Sequent.G4CK.CKPropQuantifiers]
empty [in Sequent.Environments]
env [in Sequent.Environments]
env_order_refl [in Sequent.G4WK.WKOrder]
env_order [in Sequent.G4WK.WKOrder]
env_weight [in Sequent.G4WK.WKOrder]
env_order_refl [in Sequent.G4CK.CKOrder]
env_order [in Sequent.G4CK.CKOrder]
env_weight [in Sequent.G4CK.CKOrder]
exists_dec [in Sequent.G4WK.WKDecisionProcedure]
exists_dec [in Sequent.G4CK.CKDecisionProcedure]
extCKH_prv_sind [in GHC.CKH]
extCKH_prv_ind [in GHC.CKH]
e_rule_12 [in Sequent.G4WK.WKPropQuantifiers]
e_rule_9 [in Sequent.G4WK.WKPropQuantifiers]
e_rule [in Sequent.G4WK.WKPropQuantifiers]
e_rule_12 [in Sequent.G4CK.CKPropQuantifiers]
e_rule_9 [in Sequent.G4CK.CKPropQuantifiers]
e_rule [in Sequent.G4CK.CKPropQuantifiers]

F

FIKH_prv [in GHC.CKH]
forces [in Kripke.kripke_sem]
form_index [in GHC.enum]
form_index' [in GHC.enum]
form_enum [in GHC.enum]
form_order [in Sequent.syntax_facts]
form_to_gen_tree [in Sequent.syntax_facts]
form_sind [in Syntax.im_syntax]
form_rec [in Syntax.im_syntax]
form_ind [in Syntax.im_syntax]
form_rect [in Syntax.im_syntax]
fvalid [in Kripke.kripke_sem]

G

gen_tree_to_form [in Sequent.syntax_facts]

H

height [in Sequent.G4CK.CKSequentProps]
height [in Sequent.G4WK.WKSequentProps]

I

IAxioms_sind [in GHC.CKH]
IAxioms_ind [in GHC.CKH]
Idb [in GHC.CKH]
IdbNdb_frame [in Soundness.CK_Idb_Ndb_soundness]
IdbNd_frame [in Soundness.CK_Idb_Nd_soundness]
Idb_frame [in Kripke.correspondence]
idowncone [in Kripke.correspondence]
IKH_prv [in GHC.CKH]
in_subset [in Sequent.Environments]
in_map2 [in Sequent.Environments]
in_map2_aux [in Sequent.Environments]
in_map [in Sequent.Environments]
in_map_aux [in Sequent.Environments]
irreducible [in Sequent.Environments]
is_Ndb [in Complth.CK_Cd_Idb_Ndb_th_completeness]
is_Ndb [in ComplsegP.CK_Idb_Ndb_segP_completeness]
is_Nd [in Complseg.WK_seg_completeness]
is_Nd [in ComplsegP.CK_Idb_Nd_segP_completeness]
is_box [in Sequent.Environments]
is_diam_implication_b [in Sequent.Environments]
is_diam_implication [in Sequent.Environments]
is_negation [in Sequent.Environments]
is_implication [in Sequent.Environments]
is_double_negation [in Sequent.Environments]
is_Nd [in ComplsegAB.CK_Cd_Nd_segAB_completeness]
is_Ndb [in Complseg.CK_Ndb_seg_completeness]
is_Ndb [in ComplsegAB.CK_Cd_Ndb_segAB_completeness]
is_Nd [in Complth.IK_th_completeness]
iupcone [in Kripke.correspondence]

L

Lind_theory [in GHC.Lindenbaum_lem]
listform_opt_add2 [in Sequent.G4WK.WKOrder]
list_disj [in Syntax.im_syntax]
list_conj [in Syntax.im_syntax]
list_Imp [in Syntax.im_syntax]
loc_conseq [in Kripke.kripke_sem]
L_enum [in GHC.enum]
l_open_boxes [in Sequent.Environments]

M

MAxioms_sind [in GHC.CKH]
MAxioms_ind [in GHC.CKH]
mdowncone [in Kripke.correspondence]
mupcone [in Kripke.correspondence]
mvalid [in Kripke.kripke_sem]

N

Nd [in GHC.CKH]
Ndb [in GHC.CKH]
Ndb_frame [in Kripke.correspondence]
Nd_frame [in Kripke.correspondence]
Neg [in Syntax.im_syntax]
nLind_theory [in GHC.Lindenbaum_lem]
NoAdAx [in Complseg.CK_seg_completeness]
NoAdAxCd [in ComplsegAB.CK_Cd_segAB_completeness]
NoAdAxCdIdb [in Complth.CK_Cd_Idb_th_completeness]
NoAdAxIdb [in ComplsegP.CK_Idb_segP_completeness]
npair_Lind_theory [in GHC.Lindenbaum_lem_pair]

O

obireach [in Conservativity.CK_Idb_Ndb_not_conserv_CK]
obmreach [in Conservativity.CK_Idb_Ndb_not_conserv_CK]
obval [in Conservativity.CK_Idb_Ndb_not_conserv_CK]
obval' [in Conservativity.CK_wCD_Nd_not_conserv_CK]
occurs_in_opt [in Sequent.syntax_facts]
occurs_in [in Sequent.syntax_facts]
open_boxes' [in Sequent.Environments]
open_boxes [in Sequent.Environments]
open_box [in Sequent.Environments]
opt_weight [in Sequent.G4WK.WKOrder]
opt_to_form [in Sequent.G4WK.WKSoundComplete]
oud [in Sequent.G4WK.WKSequents]

P

pair_Lind_theory [in GHC.Lindenbaum_lem_pair]
pair_choice_code [in GHC.Lindenbaum_lem_pair]
pair_choice_form [in GHC.Lindenbaum_lem_pair]
pair_extCKH_prv [in GHC.Lindenbaum_lem_pair]
pointed_env_order_refl [in Sequent.G4WK.WKOrder]
pointed_env_ms_order [in Sequent.G4WK.WKOrder]
pointed_env_order [in Sequent.G4WK.WKOrder]
pointed_env [in Sequent.G4WK.WKOrder]
pointed_env_order_refl [in Sequent.G4CK.CKOrder]
pointed_env_ms_order [in Sequent.G4CK.CKOrder]
pointed_env_order [in Sequent.G4CK.CKOrder]
pointed_env [in Sequent.G4CK.CKOrder]
prime [in GHC.Lindenbaum_lem]
Provable_sind [in Sequent.G4WK.WKSequents]
Provable_rec [in Sequent.G4WK.WKSequents]
Provable_ind [in Sequent.G4WK.WKSequents]
Provable_rect [in Sequent.G4WK.WKSequents]
Provable_sind [in Sequent.G4CK.CKSequents]
Provable_rec [in Sequent.G4CK.CKSequents]
Provable_ind [in Sequent.G4CK.CKSequents]
Provable_rect [in Sequent.G4CK.CKSequents]

Q

quasi_prime [in GHC.Lindenbaum_lem]

R

rm [in Sequent.Environments]

S

strong_Cd_weak_Idb_frame [in Kripke.correspondence]
strong_Cd_frame [in Kripke.correspondence]
subform [in Syntax.im_syntax]
subformlist [in Syntax.im_syntax]
subformP_sind [in Sequent.syntax_facts]
subformP_ind [in Sequent.syntax_facts]
subst [in Syntax.im_syntax]
SubTheory [in GHC.Lindenbaum_lem]
suff_Ndb_frame [in Kripke.correspondence]
suff_Nd_frame [in Kripke.correspondence]
suff_Idb_frame [in Kripke.correspondence]
suff_Cd_frame [in Kripke.correspondence]

T

tbireach [in Conservativity.CK_Idb_Nd_not_conserv_CK]
tbmreach [in Conservativity.CK_Idb_Nd_not_conserv_CK]
tbval [in Conservativity.CK_Idb_Nd_not_conserv_CK]
Theory [in GHC.Lindenbaum_lem]
Top [in Syntax.im_syntax]

U

UnBox [in Syntax.im_syntax]

V

vars_incl [in Sequent.G4WK.WKPropQuantifiers]
vars_incl [in Sequent.G4CK.CKPropQuantifiers]
var_not_in_env [in Sequent.Environments]

W

wCD [in GHC.CKH]
weak_Idb_frame [in Kripke.correspondence]
weight [in Sequent.syntax_facts]
weight_ind [in Sequent.syntax_facts]
wf_env_order [in Sequent.G4WK.WKOrder]
wf_env_order [in Sequent.G4CK.CKOrder]
WKH_prv [in GHC.CKH]

---

Record Index

A

ABsegment [in ComplsegAB.general_segAB_completeness]

C

cworld [in Complth.general_th_completeness]

F

frame [in Kripke.kripke_sem]

M

model [in Kripke.kripke_sem]

P

Psegment [in ComplsegP.general_segP_completeness]

S

segment [in Complseg.general_seg_completeness]

---

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

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

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

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

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

(642 entries)

Axiom Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(6 entries)

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

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

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

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

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

(218 entries)

Record Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(6 entries)