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

(705 entries)

Notation Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(10 entries)

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

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

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

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

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

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

(5 entries)

Section Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

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

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

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

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]
AllForm [definition, in GHC.Lindenbaum_lem]
And [constructor, in Syntax.im_syntax]
And_Imp [lemma, in GHC.properties]
Ax [constructor, in GHC.CKH]
Axioms [definition, in GHC.CKH]
Ax_valid [lemma, in Soundness.general_soundness]

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]
Box [constructor, in Syntax.im_syntax]
boxreflect [lemma, in ComplsegAB.general_segAB_completeness]
boxreflect [projection, in Complseg.general_seg_completeness]
boxreflect [lemma, in ComplsegP.general_segP_completeness]
Box_list [definition, in Syntax.im_syntax]
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_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]
CdIdb_frame [definition, in Soundness.CK_Cd_Idb_soundness]
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 ComplsegAB.general_segAB_completeness]
cexpl [instance, in Complth.general_th_completeness]
cexpl [instance, in Complseg.general_seg_completeness]
cexpl [instance, in ComplsegP.general_segP_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_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_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 ComplsegAB.general_segAB_completeness]
CF [instance, in Complth.general_th_completeness]
CF [instance, in Complseg.general_seg_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 ComplsegAB.general_segAB_completeness]
cireach [definition, in Complth.general_th_completeness]
cireach [definition, in Complseg.general_seg_completeness]
cireach [definition, in ComplsegP.general_segP_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 Complseg.general_seg_completeness]
cireach_trans [lemma, in Complseg.general_seg_completeness]
cireach_refl [lemma, in Complseg.general_seg_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_conserv_CK [section, in Conservativity.CK_Cd_Idb_conserv_CK]
CKCdIdb_Soundness [lemma, in Soundness.CK_Cd_Idb_soundness]
CKCdIdb_Strong_Completeness [lemma, in Complth.CK_Cd_Idb_th_completeness]
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]
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_Strong_Completeness [lemma, in ComplsegP.CK_Idb_Nd_segP_completeness]
CKIdbNd_Soundness [lemma, in Soundness.CK_Idb_Nd_soundness]
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_conserv_CK [section, in Conservativity.CK_Cd_Idb_conserv_CK]
CKIdb_Soundness [lemma, in Soundness.CK_Idb_soundness]
CKIdb_Strong_Completeness [lemma, in ComplsegP.CK_Idb_segP_completeness]
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]
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_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_Cd_Idb_completeness [section, in Complth.CK_Cd_Idb_th_completeness]
CK_Idb_soundness [section, in Soundness.CK_Idb_soundness]
CK_Cd_Nd_completeness [section, in ComplsegAB.CK_Cd_Nd_segAB_completeness]
CK_Idb_completeness [section, in ComplsegP.CK_Idb_segP_completeness]
CK_Strong_Completeness [lemma, in Complseg.CK_seg_completeness]
CK_completeness [section, in Complseg.CK_seg_completeness]
CK_Idb_Nd_soundness [section, in Soundness.CK_Idb_Nd_soundness]
CK_Cd_Ndb_completeness [section, in ComplsegAB.CK_Cd_Ndb_segAB_completeness]
CK_Soundness [lemma, in Soundness.CK_soundness]
CK_soundness [section, in Soundness.CK_soundness]
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 ComplsegAB.general_segAB_completeness]
CM [instance, in Complth.general_th_completeness]
CM [instance, in Complseg.general_seg_completeness]
CM [instance, in ComplsegP.general_segP_completeness]
cmreach [definition, in ComplsegAB.general_segAB_completeness]
cmreach [definition, in Complth.general_th_completeness]
cmreach [definition, in Complseg.general_seg_completeness]
cmreach [definition, in ComplsegP.general_segP_completeness]
cmreach_expl [lemma, in ComplsegAB.general_segAB_completeness]
cmreach_expl [lemma, in Complth.general_th_completeness]
cmreach_expl [lemma, in Complseg.general_seg_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]
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]
Contr_Bot [lemma, in GHC.properties]
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 [library]
cval [definition, in ComplsegAB.general_segAB_completeness]
cval [definition, in Complth.general_th_completeness]
cval [definition, in Complseg.general_seg_completeness]
cval [definition, in ComplsegP.general_segP_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 Complseg.general_seg_completeness]
cval_persist [lemma, in Complseg.general_seg_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

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]
diamwitness [lemma, in ComplsegAB.general_segAB_completeness]
diamwitness [projection, in Complseg.general_seg_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_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 [definition, in Syntax.im_syntax]
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_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_existence [lemma, in Complseg.general_seg_completeness]
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]

E

EFQ [lemma, in GHC.properties]
enum [library]
Environments [library]
eq_dec_form [lemma, in Syntax.im_syntax]
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]

F

FIKH_prv [definition, in GHC.CKH]
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

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_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_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_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_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_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]

H

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

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_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]
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_form_dec [lemma, in Syntax.im_syntax]
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]
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_Nd [definition, in Complseg.WK_seg_completeness]
is_Nd [definition, in ComplsegP.CK_Idb_Nd_segP_completeness]
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 ComplsegAB.general_segAB_completeness]
LEM [axiom, in ComplsegP.CK_Idb_Nd_segP_completeness]
LEM [axiom, in Kripke.correspondence]
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_ABsegment [lemma, in ComplsegAB.general_segAB_completeness]
Lindenbaum_pair [lemma, in GHC.Lindenbaum_lem_pair]
Lindenbaum_cworld [lemma, in Complth.general_th_completeness]
Lindenbaum_segment [lemma, in Complseg.general_seg_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]
list_split_union [lemma, in GHC.classical_facts]
list_Imp [definition, in Syntax.im_syntax]
list_Diam_map_repr [lemma, in GHC.properties]
list_Box_map_repr [lemma, in GHC.properties]
list_conj_Diam [lemma, in GHC.properties]
list_conj_Diam_obj [lemma, in GHC.properties]
list_conj_map_Diam [lemma, in GHC.properties]
list_conj [definition, in GHC.properties]
list_disj_Box [lemma, in GHC.properties]
list_disj_Box_obj [lemma, in GHC.properties]
list_disj_map_Box [lemma, in GHC.properties]
list_disj [definition, 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]

M

MAxioms [inductive, in GHC.CKH]
MAxioms_sind [definition, in GHC.CKH]
MAxioms_ind [definition, in GHC.CKH]
mdowncone [definition, in Kripke.correspondence]
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]
mupcone [definition, in Kripke.correspondence]
mvalid [definition, in Kripke.kripke_sem]

N

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]
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 [definition, in Sequent.syntax_facts]
Optimizations [library]
Or [constructor, in Syntax.im_syntax]
Order [library]

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]
Prime [projection, in Complth.general_th_completeness]
prime [definition, in GHC.Lindenbaum_lem]
prime_list_disj [lemma, in GHC.Lindenbaum_lem]
properties [library]
PropQuantifiers [library]
prv_list_left_conj [lemma, in GHC.properties]
prv_Top [lemma, in GHC.properties]
Psegment [record, in ComplsegP.general_segP_completeness]

Q

QuasiCompleteness [lemma, in ComplsegAB.general_segAB_completeness]
QuasiCompleteness [lemma, in Complth.general_th_completeness]
QuasiCompleteness [lemma, in Complseg.general_seg_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_disj [lemma, in GHC.properties]

S

segAorB [projection, in ComplsegAB.general_segAB_completeness]
segClosed [projection, in ComplsegAB.general_segAB_completeness]
segClosed [projection, in Complseg.general_seg_completeness]
segClosed [projection, in ComplsegP.general_segP_completeness]
segment [record, in Complseg.general_seg_completeness]
segPrime [projection, in ComplsegAB.general_segAB_completeness]
segPrime [projection, in Complseg.general_seg_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]
SequentProps [library]
Sequents [library]
Simplifications [library]
Simp_env [library]
Soundness [lemma, in Soundness.general_soundness]
Strong_Completeness [lemma, in ComplsegAB.general_segAB_completeness]
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 Complth.general_th_completeness]
Strong_Completeness [lemma, in Complseg.general_seg_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_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_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_CKCd_Strong_Completeness [lemma, in ComplsegAB.CK_Cd_segAB_completeness]
suff_suff_CKCdIdb_Strong_Completeness [lemma, in Complth.CK_Cd_Idb_th_completeness]
suff_CKCdNd_Strong_Completeness [lemma, in ComplsegAB.CK_Cd_Nd_segAB_completeness]
suff_CKIdb_Strong_Completeness [lemma, in ComplsegP.CK_Idb_segP_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 ComplsegAB.general_segAB_completeness]
tail [projection, in Complseg.general_seg_completeness]
tail [projection, in ComplsegP.general_segP_completeness]
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]
transitive_form_order [instance, in Sequent.syntax_facts]
truth_lemma [lemma, in ComplsegAB.general_segAB_completeness]
truth_lemma [lemma, in Complth.general_th_completeness]
truth_lemma [lemma, in Complseg.general_seg_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]

V

val [projection, in Kripke.kripke_sem]
val_expl [projection, in Kripke.kripke_sem]
Var [constructor, in Syntax.im_syntax]

W

wCD [definition, in GHC.CKH]
wCDb_prv [section, in Conservativity.CK_wCD_Nd_not_conserv_CK]
weak_Idb_frame [definition, in Kripke.correspondence]
weight [definition, in Sequent.syntax_facts]
weight_ind [definition, in Sequent.syntax_facts]
weight_pos [lemma, in Sequent.syntax_facts]
WKH_prv [definition, in GHC.CKH]
WK_extends_CKNdb [lemma, in Conservativity.CK_Cd_Nd_conserv_CK]
WK_conserv_CK [section, in Conservativity.CK_Cd_Nd_conserv_CK]
WK_Strong_Completeness [lemma, in Complseg.WK_seg_completeness]
WK_completeness [section, in Complseg.WK_seg_completeness]
WK_Soundness [lemma, in Soundness.WK_soundness]
WK_soundness [section, in Soundness.WK_soundness]
WK_seg_completeness [library]
WK_soundness [library]

other

_ ≺f _ [notation, in Sequent.syntax_facts]
_ → _ [notation, in Syntax.im_syntax]
_ ∨ _ [notation, in Syntax.im_syntax]
_ ∧ _ [notation, in Syntax.im_syntax]
# _ [notation, in Syntax.im_syntax]
¬ _ [notation, in Syntax.im_syntax]
⊤ [notation, in Syntax.im_syntax]
⊥ [notation, in Syntax.im_syntax]
□ _ [notation, in Syntax.im_syntax]
◊ _ [notation, in Syntax.im_syntax]

---

Notation Index

other

_ ≺f _ [in Sequent.syntax_facts]
_ → _ [in Syntax.im_syntax]
_ ∨ _ [in Syntax.im_syntax]
_ ∧ _ [in Syntax.im_syntax]
# _ [in Syntax.im_syntax]
¬ _ [in Syntax.im_syntax]
⊤ [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]

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_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_Lind_pair.AdAx [in GHC.Lindenbaum_lem_pair]
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_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_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]

T

theorems_and_meta.AdAx [in GHC.properties]

---

Library Index

C

CKH
CKH_export
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
Cut

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

O

Optimizations
Order

P

properties
PropQuantifiers

S

SequentProps
Sequents
Simplifications
Simp_env
syntax_facts

W

WK_seg_completeness
WK_soundness

---

Lemma Index

A

absorp_Or1 [in GHC.properties]
And_Imp [in GHC.properties]
Ax_valid [in Soundness.general_soundness]

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]
boxreflect [in ComplsegAB.general_segAB_completeness]
boxreflect [in ComplsegP.general_segP_completeness]
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_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_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_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 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 Complseg.general_seg_completeness]
cireach_trans [in Complseg.general_seg_completeness]
cireach_refl [in Complseg.general_seg_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_Strong_Completeness [in ComplsegP.CK_Idb_Nd_segP_completeness]
CKIdbNd_Soundness [in Soundness.CK_Idb_Nd_soundness]
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_Soundness [in Soundness.CK_Idb_soundness]
CKIdb_Strong_Completeness [in ComplsegP.CK_Idb_segP_completeness]
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_Strong_Completeness [in Complseg.CK_seg_completeness]
CK_Soundness [in Soundness.CK_soundness]
closeder_pair_Lind_theory [in GHC.Lindenbaum_lem_pair]
closeder_Lind_theory [in GHC.Lindenbaum_lem]
cmreach_expl [in ComplsegAB.general_segAB_completeness]
cmreach_expl [in Complth.general_th_completeness]
cmreach_expl [in Complseg.general_seg_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]
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]
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 Complseg.general_seg_completeness]
cval_persist [in Complseg.general_seg_completeness]
cval_expl [in ComplsegP.general_segP_completeness]
cval_persist [in ComplsegP.general_segP_completeness]

D

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]
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_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_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_existence [in Complseg.general_seg_completeness]
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]

E

EFQ [in GHC.properties]
eq_dec_form [in Syntax.im_syntax]
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]

F

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]

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]
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_form_dec [in Syntax.im_syntax]
In_Box_list_In_list [in GHC.properties]
In_list_In_Box_list [in GHC.properties]
In_remove [in GHC.properties]

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_ABsegment [in ComplsegAB.general_segAB_completeness]
Lindenbaum_pair [in GHC.Lindenbaum_lem_pair]
Lindenbaum_cworld [in Complth.general_th_completeness]
Lindenbaum_segment [in Complseg.general_seg_completeness]
Lindenbaum_Psegment_Diam [in ComplsegP.general_segP_completeness]
Lindenbaum_Psegment [in ComplsegP.general_segP_completeness]
Lind_theory_extens [in GHC.Lindenbaum_lem]
list_split_union [in GHC.classical_facts]
list_Diam_map_repr [in GHC.properties]
list_Box_map_repr [in GHC.properties]
list_conj_Diam [in GHC.properties]
list_conj_Diam_obj [in GHC.properties]
list_conj_map_Diam [in GHC.properties]
list_disj_Box [in GHC.properties]
list_disj_Box_obj [in GHC.properties]
list_disj_map_Box [in GHC.properties]
L_enum_exhaustive [in GHC.enum]
L_enum_cumulative [in GHC.enum]

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]

N

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]

P

pair_Lind_theory_extens [in GHC.Lindenbaum_lem_pair]
partial_finite [in GHC.classical_facts]
Persistence [in Kripke.kripke_sem]
prime_list_disj [in GHC.Lindenbaum_lem]
prv_list_left_conj [in GHC.properties]
prv_Top [in GHC.properties]

Q

QuasiCompleteness [in ComplsegAB.general_segAB_completeness]
QuasiCompleteness [in Complth.general_th_completeness]
QuasiCompleteness [in Complseg.general_seg_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_disj [in GHC.properties]

S

Soundness [in Soundness.general_soundness]
Strong_Completeness [in ComplsegAB.general_segAB_completeness]
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 Complth.general_th_completeness]
Strong_Completeness [in Complseg.general_seg_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_CKIdbNd_Strong_Completeness [in ComplsegP.CK_Idb_Nd_segP_completeness]
suff_suff_CKIdbNd_Strong_Completeness [in ComplsegP.CK_Idb_Nd_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_CKCd_Strong_Completeness [in ComplsegAB.CK_Cd_segAB_completeness]
suff_suff_CKCdIdb_Strong_Completeness [in Complth.CK_Cd_Idb_th_completeness]
suff_CKCdNd_Strong_Completeness [in ComplsegAB.CK_Cd_Nd_segAB_completeness]
suff_CKIdb_Strong_Completeness [in ComplsegP.CK_Idb_segP_completeness]
suff_CKCdNdb_Strong_Completeness [in ComplsegAB.CK_Cd_Ndb_segAB_completeness]
suff_suff_suff_IK_Strong_Completeness [in Complth.IK_th_completeness]

T

Theory_AllForm [in GHC.Lindenbaum_lem]
Thm_irrel [in GHC.properties]
truth_lemma [in ComplsegAB.general_segAB_completeness]
truth_lemma [in Complth.general_th_completeness]
truth_lemma [in Complseg.general_seg_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]

W

weight_pos [in Sequent.syntax_facts]
WK_extends_CKNdb [in Conservativity.CK_Cd_Nd_conserv_CK]
WK_Strong_Completeness [in Complseg.WK_seg_completeness]
WK_Soundness [in Soundness.WK_soundness]

---

Axiom Index

L

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

---

Constructor Index

A

And [in Syntax.im_syntax]
Ax [in GHC.CKH]

B

Bot [in Syntax.im_syntax]
Box [in Syntax.im_syntax]

D

Diam [in Syntax.im_syntax]

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]

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]

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]

---

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 ComplsegAB.general_segAB_completeness]
head [in Complseg.general_seg_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 ComplsegAB.general_segAB_completeness]
segClosed [in Complseg.general_seg_completeness]
segClosed [in ComplsegP.general_segP_completeness]
segPrime [in ComplsegAB.general_segAB_completeness]
segPrime [in Complseg.general_seg_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 ComplsegAB.general_segAB_completeness]
tail [in Complseg.general_seg_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]

---

Inductive Index

E

extCKH_prv [in GHC.CKH]

F

form [in Syntax.im_syntax]

I

IAxioms [in GHC.CKH]

M

MAxioms [in GHC.CKH]

S

subformP [in Sequent.syntax_facts]

---

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_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_Cd_Idb_completeness [in Complth.CK_Cd_Idb_th_completeness]
CK_Idb_soundness [in Soundness.CK_Idb_soundness]
CK_Cd_Nd_completeness [in ComplsegAB.CK_Cd_Nd_segAB_completeness]
CK_Idb_completeness [in ComplsegP.CK_Idb_segP_completeness]
CK_completeness [in Complseg.CK_seg_completeness]
CK_Idb_Nd_soundness [in Soundness.CK_Idb_Nd_soundness]
CK_Cd_Ndb_completeness [in ComplsegAB.CK_Cd_Ndb_segAB_completeness]
CK_soundness [in Soundness.CK_soundness]
CK_Cd_Idb_Ndb_soundness [in Soundness.CK_Cd_Idb_Ndb_soundness]
Classical_facts [in GHC.classical_facts]
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

general_soundness [in Soundness.general_soundness]
general_segAB_completeness [in ComplsegAB.general_segAB_completeness]
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_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_seg_completeness [in Complseg.general_seg_completeness]
general_segP_completeness [in ComplsegP.general_segP_completeness]

I

Idb [in Kripke.correspondence]
IK_soundness [in Soundness.IK_soundness]
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]

N

Nd [in Kripke.correspondence]
Ndb [in Kripke.correspondence]
negboxbot_negneg_box [in Conservativity.CK_Idb_Ndb_not_conserv_CK]

S

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_completeness [in Complseg.WK_seg_completeness]
WK_soundness [in Soundness.WK_soundness]

---

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 ComplsegAB.general_segAB_completeness]
cexpl [in Complth.general_th_completeness]
cexpl [in Complseg.general_seg_completeness]
cexpl [in ComplsegP.general_segP_completeness]
CF [in ComplsegAB.general_segAB_completeness]
CF [in Complth.general_th_completeness]
CF [in Complseg.general_seg_completeness]
CF [in ComplsegP.general_segP_completeness]
CM [in ComplsegAB.general_segAB_completeness]
CM [in Complth.general_th_completeness]
CM [in Complseg.general_seg_completeness]
CM [in ComplsegP.general_segP_completeness]

F

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]

T

transitive_form_order [in Sequent.syntax_facts]

---

Definition Index

A

AdAxCd [in ComplsegAB.general_segAB_completeness]
AdAxCd [in GHC.properties]
AdAxCdIdb [in Complth.general_th_completeness]
AdAxIdb [in ComplsegP.general_segP_completeness]
AllForm [in GHC.Lindenbaum_lem]
Axioms [in GHC.CKH]

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 ComplsegAB.general_segAB_completeness]
cireach [in Complth.general_th_completeness]
cireach [in Complseg.general_seg_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 ComplsegAB.general_segAB_completeness]
cmreach [in Complth.general_th_completeness]
cmreach [in Complseg.general_seg_completeness]
cmreach [in ComplsegP.general_segP_completeness]
cval [in ComplsegAB.general_segAB_completeness]
cval [in Complth.general_th_completeness]
cval [in Complseg.general_seg_completeness]
cval [in ComplsegP.general_segP_completeness]

D

diam_free [in Syntax.im_syntax]

E

extCKH_prv_sind [in GHC.CKH]
extCKH_prv_ind [in GHC.CKH]

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]

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]
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_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]
list_Imp [in Syntax.im_syntax]
list_conj [in GHC.properties]
list_disj [in GHC.properties]
loc_conseq [in Kripke.kripke_sem]
L_enum [in GHC.enum]

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 [in Sequent.syntax_facts]

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]
prime [in GHC.Lindenbaum_lem]

Q

quasi_prime [in GHC.Lindenbaum_lem]

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

Theory [in GHC.Lindenbaum_lem]
Top [in Syntax.im_syntax]

U

UnBox [in Syntax.im_syntax]

W

wCD [in GHC.CKH]
weak_Idb_frame [in Kripke.correspondence]
weight [in Sequent.syntax_facts]
weight_ind [in Sequent.syntax_facts]
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

(705 entries)

Notation Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(10 entries)

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

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

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

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

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

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

(5 entries)

Section Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

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

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

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

Generated by coqdoc and improved with CoqdocJS