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 (918 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 (17 entries)
Binder 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 (689 entries)
Module Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (5 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 (1 entry)
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 (5 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 (112 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 (21 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 (3 entries)
Section Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (8 entries)
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 (12 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 (45 entries)

Global Index

A

A [definition, in Pqf.PropQuantifiers]
Af [definition, in Pqf.PropQuantifiers]
And [constructor, in Pqf.Formulas]
AndL [constructor, in Pqf.Sequents]
AndL_rev [lemma, in Pqf.SequentProps]
AndR [constructor, in Pqf.Sequents]
AndR_rev [lemma, in Pqf.SequentProps]
assoc_meq_union [instance, in Pqf.Environments]
Atom [constructor, in Pqf.Sequents]
A_right [lemma, in Pqf.PropQuantifiers]
a_rule_env_spec [lemma, in Pqf.PropQuantifiers]
a_rule_form_vars [lemma, in Pqf.PropQuantifiers]
a_rule_env_vars [lemma, in Pqf.PropQuantifiers]
A_eq [definition, in Pqf.PropQuantifiers]
a_rule_form_cong [lemma, in Pqf.PropQuantifiers]
a_rule_env_cong [lemma, in Pqf.PropQuantifiers]
a_rule_form [definition, in Pqf.PropQuantifiers]
a_rule_env [definition, in Pqf.PropQuantifiers]
A:102 [binder, in Pqf.Environments]
A:106 [binder, in Pqf.Environments]
a:107 [binder, in Pqf.Environments]
A:129 [binder, in Pqf.Environments]
a:130 [binder, in Pqf.Environments]
A:14 [binder, in Pqf.PropQuantifiers]
A:149 [binder, in Pqf.Environments]
A:151 [binder, in Pqf.Environments]
A:29 [binder, in Pqf.PropQuantifiers]
a:29 [binder, in Pqf.Environments]
A:42 [binder, in Pqf.PropQuantifiers]
A:94 [binder, in Pqf.Environments]


B

Bot [constructor, in Pqf.Formulas]
b:108 [binder, in Pqf.Environments]
b:131 [binder, in Pqf.Environments]


C

conjunction [definition, in Pqf.Environments]
conjunction_L [lemma, in Pqf.SequentProps]
conjunction_R2 [lemma, in Pqf.SequentProps]
conjunction_R1 [lemma, in Pqf.SequentProps]
contraction [lemma, in Pqf.SequentProps]
CountablyManyFormulas [section, in Pqf.Formulas]


D

decide_in [lemma, in Pqf.Environments]
difference_include [lemma, in Pqf.Environments]
difference_singleton [lemma, in Pqf.Environments]
diff_not_in [lemma, in Pqf.Environments]
disjunction [definition, in Pqf.Environments]
disjunction_R [lemma, in Pqf.SequentProps]
disjunction_L [lemma, in Pqf.SequentProps]
d:156 [binder, in Pqf.PropQuantifiers]
d:159 [binder, in Pqf.PropQuantifiers]
d:162 [binder, in Pqf.PropQuantifiers]
d:165 [binder, in Pqf.PropQuantifiers]


E

E [definition, in Pqf.PropQuantifiers]
EA [definition, in Pqf.PropQuantifiers]
EA_vars [lemma, in Pqf.PropQuantifiers]
EA_eq [lemma, in Pqf.PropQuantifiers]
EA0:107 [binder, in Pqf.PropQuantifiers]
EA0:119 [binder, in Pqf.PropQuantifiers]
EA0:137 [binder, in Pqf.PropQuantifiers]
EA0:21 [binder, in Pqf.PropQuantifiers]
EA0:36 [binder, in Pqf.PropQuantifiers]
EA0:6 [binder, in Pqf.PropQuantifiers]
EA0:93 [binder, in Pqf.PropQuantifiers]
EA1:56 [binder, in Pqf.PropQuantifiers]
EA1:66 [binder, in Pqf.PropQuantifiers]
EA1:73 [binder, in Pqf.PropQuantifiers]
EA2:57 [binder, in Pqf.PropQuantifiers]
EA2:67 [binder, in Pqf.PropQuantifiers]
EA2:74 [binder, in Pqf.PropQuantifiers]
Ef [definition, in Pqf.PropQuantifiers]
entail_correct [lemma, in Pqf.PropQuantifiers]
env [definition, in Pqf.Environments]
Environments [library]
EnvMS [module, in Pqf.Environments]
EnvMS.diff [definition, in Pqf.Environments]
EnvMS.diff_mult [lemma, in Pqf.Environments]
EnvMS.empty [definition, in Pqf.Environments]
EnvMS.empty_mult [lemma, in Pqf.Environments]
EnvMS.gmultiset_choose_or_empty [lemma, in Pqf.Environments]
EnvMS.intersection [definition, in Pqf.Environments]
EnvMS.intersection_mult [lemma, in Pqf.Environments]
EnvMS.meq [definition, in Pqf.Environments]
EnvMS.meq_multeq [lemma, in Pqf.Environments]
EnvMS.mset_ind_type [definition, in Pqf.Environments]
EnvMS.mult [definition, in Pqf.Environments]
EnvMS.multeq_meq [lemma, in Pqf.Environments]
EnvMS.Multiset [definition, in Pqf.Environments]
EnvMS.mult_eqA_compat [lemma, in Pqf.Environments]
EnvMS.Sid [module, in Pqf.Environments]
EnvMS.Sid.Dom [module, in Pqf.Environments]
EnvMS.Sid.Dom.A [definition, in Pqf.Environments]
EnvMS.Sid.Eq [module, in Pqf.Environments]
EnvMS.Sid.eqA_dec [definition, in Pqf.Environments]
EnvMS.singleton [definition, in Pqf.Environments]
EnvMS.singleton_mult_notin [lemma, in Pqf.Environments]
EnvMS.singleton_mult_in [lemma, in Pqf.Environments]
EnvMS.union [definition, in Pqf.Environments]
EnvMS.union_mult [lemma, in Pqf.Environments]
env_order_equiv_right_compat [lemma, in Pqf.Environments]
env_order_add_compat [lemma, in Pqf.Environments]
env_order_cancel_right [lemma, in Pqf.Environments]
env_order_0 [lemma, in Pqf.Environments]
env_order_2 [lemma, in Pqf.Environments]
env_order_1 [lemma, in Pqf.Environments]
env_equiv_eq [lemma, in Pqf.Environments]
env_add_inv' [lemma, in Pqf.Environments]
env_add_inv [lemma, in Pqf.Environments]
env_add_comm [lemma, in Pqf.Environments]
env_in_add [lemma, in Pqf.Environments]
env_order_singleton_compat [lemma, in Pqf.Environments]
env_order_singleton [lemma, in Pqf.Environments]
env_order_trans [instance, in Pqf.Environments]
env_replace [lemma, in Pqf.Environments]
env_order [definition, in Pqf.Environments]
equiv_assoc [instance, in Pqf.Environments]
equiv_disj_union_compat_r [lemma, in Pqf.Environments]
example_multiset [lemma, in Pqf.Environments]
ExFalso [constructor, in Pqf.Sequents]
exfalso [lemma, in Pqf.SequentProps]
E_of_empty [lemma, in Pqf.PropQuantifiers]
E_left [lemma, in Pqf.PropQuantifiers]
E_irr [lemma, in Pqf.PropQuantifiers]
e_rule_vars [lemma, in Pqf.PropQuantifiers]
E_eq [definition, in Pqf.PropQuantifiers]
e_rule_cong [lemma, in Pqf.PropQuantifiers]
e_rule [definition, in Pqf.PropQuantifiers]
E:11 [binder, in Pqf.PropQuantifiers]
E:26 [binder, in Pqf.PropQuantifiers]
E:39 [binder, in Pqf.PropQuantifiers]


F

fomula_bottom [instance, in Pqf.Formulas]
form [inductive, in Pqf.Formulas]
Formulas [library]
form_order [definition, in Pqf.Formulas]
form_count [instance, in Pqf.Formulas]
form_to_gen_tree [definition, in Pqf.Formulas]
form_eq_dec [instance, in Pqf.Formulas]
form_top [instance, in Pqf.Formulas]
f:105 [binder, in Pqf.Environments]
f:112 [binder, in Pqf.Environments]
f:135 [binder, in Pqf.Environments]
f:150 [binder, in Pqf.Environments]
f:153 [binder, in Pqf.Environments]
f:157 [binder, in Pqf.PropQuantifiers]
f:160 [binder, in Pqf.PropQuantifiers]
f:163 [binder, in Pqf.PropQuantifiers]
f:166 [binder, in Pqf.PropQuantifiers]
f:97 [binder, in Pqf.Environments]


G

generalised_contraction [lemma, in Pqf.SequentProps]
generalised_axiom [lemma, in Pqf.SequentProps]
generalised_weakeningR [lemma, in Pqf.SequentProps]
generalised_weakeningL [lemma, in Pqf.SequentProps]
gen_tree_to_form [definition, in Pqf.Formulas]
gmultiset_rec [lemma, in Pqf.Environments]
g:154 [binder, in Pqf.Environments]


H

HD:109 [binder, in Pqf.Environments]
HD:132 [binder, in Pqf.Environments]
HEA0:113 [binder, in Pqf.PropQuantifiers]
HEA0:125 [binder, in Pqf.PropQuantifiers]
HEA0:99 [binder, in Pqf.PropQuantifiers]
HEA:141 [binder, in Pqf.PropQuantifiers]
height [definition, in Pqf.SequentProps]
height_0 [lemma, in Pqf.SequentProps]
Hin':138 [binder, in Pqf.Environments]
Hin':143 [binder, in Pqf.Environments]
Hin':148 [binder, in Pqf.Environments]
Hin1:54 [binder, in Pqf.PropQuantifiers]
Hin1:64 [binder, in Pqf.PropQuantifiers]
Hin2:55 [binder, in Pqf.PropQuantifiers]
Hin2:65 [binder, in Pqf.PropQuantifiers]
Hin:103 [binder, in Pqf.PropQuantifiers]
Hin:115 [binder, in Pqf.Environments]
Hin:119 [binder, in Pqf.Environments]
Hin:123 [binder, in Pqf.Environments]
Hin:128 [binder, in Pqf.Environments]
Hin:135 [binder, in Pqf.PropQuantifiers]
Hin:137 [binder, in Pqf.Environments]
Hin:142 [binder, in Pqf.Environments]
Hin:147 [binder, in Pqf.Environments]
Hin:184 [binder, in Pqf.PropQuantifiers]
Hin:192 [binder, in Pqf.PropQuantifiers]
Hin:23 [binder, in Pqf.PropQuantifiers]
Hin:8 [binder, in Pqf.PropQuantifiers]
Hin:89 [binder, in Pqf.PropQuantifiers]
Hi:126 [binder, in Pqf.Environments]
Hpe':60 [binder, in Pqf.PropQuantifiers]
Hpe':70 [binder, in Pqf.PropQuantifiers]
Hpe':77 [binder, in Pqf.PropQuantifiers]
Hpe:106 [binder, in Pqf.PropQuantifiers]
Hpe:110 [binder, in Pqf.PropQuantifiers]
Hpe:118 [binder, in Pqf.PropQuantifiers]
Hpe:122 [binder, in Pqf.PropQuantifiers]
Hpe:140 [binder, in Pqf.PropQuantifiers]
Hpe:144 [binder, in Pqf.PropQuantifiers]
Hpe:147 [binder, in Pqf.PropQuantifiers]
Hpe:150 [binder, in Pqf.PropQuantifiers]
Hpe:153 [binder, in Pqf.PropQuantifiers]
Hpe:20 [binder, in Pqf.PropQuantifiers]
Hpe:35 [binder, in Pqf.PropQuantifiers]
Hpe:5 [binder, in Pqf.PropQuantifiers]
Hpe:59 [binder, in Pqf.PropQuantifiers]
Hpe:69 [binder, in Pqf.PropQuantifiers]
Hpe:76 [binder, in Pqf.PropQuantifiers]
Hpe:92 [binder, in Pqf.PropQuantifiers]
Hpe:96 [binder, in Pqf.PropQuantifiers]
Hp:60 [binder, in Pqf.SequentProps]
Hp:65 [binder, in Pqf.SequentProps]
H:10 [binder, in Pqf.PropQuantifiers]
H:13 [binder, in Pqf.PropQuantifiers]
H:156 [binder, in Pqf.Environments]
H:25 [binder, in Pqf.PropQuantifiers]
H:28 [binder, in Pqf.PropQuantifiers]
H:38 [binder, in Pqf.PropQuantifiers]
H:41 [binder, in Pqf.PropQuantifiers]
HΓ':117 [binder, in Pqf.Environments]
HΓ':121 [binder, in Pqf.Environments]
HΓ':140 [binder, in Pqf.Environments]
HΓ':145 [binder, in Pqf.Environments]
HΓ':99 [binder, in Pqf.Environments]
HΓ:158 [binder, in Pqf.Environments]
HΓ:160 [binder, in Pqf.Environments]


I

ImpL [lemma, in Pqf.SequentProps]
ImpLAnd [constructor, in Pqf.Sequents]
ImpLAnd_rev [lemma, in Pqf.SequentProps]
Implies [constructor, in Pqf.Formulas]
ImpLImp [constructor, in Pqf.Sequents]
ImpLImp_dup [lemma, in Pqf.SequentProps]
ImpLImp_prev [lemma, in Pqf.SequentProps]
ImpLOr [constructor, in Pqf.Sequents]
ImpLOr_rev [lemma, in Pqf.SequentProps]
ImpLVar [constructor, in Pqf.Sequents]
ImpLVar_rev [lemma, in Pqf.SequentProps]
ImpR [constructor, in Pqf.Sequents]
ImpR_rev [lemma, in Pqf.SequentProps]
imp_cut [lemma, in Pqf.SequentProps]
in_difference [lemma, in Pqf.Environments]
in_map_ext [lemma, in Pqf.Environments]
in_map_empty [lemma, in Pqf.Environments]
in_map_in [lemma, in Pqf.Environments]
in_subset [definition, in Pqf.Environments]
in_in_map [lemma, in Pqf.Environments]
in_map [definition, in Pqf.Environments]
in_map_aux [definition, in Pqf.Environments]
irreducible [definition, in Pqf.Environments]


L

l:207 [binder, in Pqf.PropQuantifiers]
l:78 [binder, in Pqf.Environments]
l:79 [binder, in Pqf.Environments]
l:81 [binder, in Pqf.Environments]
l:88 [binder, in Pqf.Environments]


M

make_impl_weight2 [lemma, in Pqf.Environments]
make_impl_weight [lemma, in Pqf.Environments]
make_impl_spec [lemma, in Pqf.Environments]
make_impl [definition, in Pqf.Environments]
make_disj_spec [lemma, in Pqf.Environments]
make_disj [definition, in Pqf.Environments]
make_conj_spec [lemma, in Pqf.Environments]
make_conj [definition, in Pqf.Environments]
make_disj_complete_R [lemma, in Pqf.SequentProps]
make_disj_sound_R [lemma, in Pqf.SequentProps]
make_conj_complete_R [lemma, in Pqf.SequentProps]
make_conj_sound_R [lemma, in Pqf.SequentProps]
make_conj_complete_L [lemma, in Pqf.SequentProps]
make_conj_sound_L [lemma, in Pqf.SequentProps]
make_disj_complete [lemma, in Pqf.SequentProps]
make_disj_sound_L [lemma, in Pqf.SequentProps]
make_impl_sound_R [lemma, in Pqf.SequentProps]
make_impl_complete_R [lemma, in Pqf.SequentProps]
make_impl_complete_L2 [lemma, in Pqf.SequentProps]
make_impl_complete_L [lemma, in Pqf.SequentProps]
make_impl_sound_L2' [lemma, in Pqf.SequentProps]
make_impl_sound_L2 [lemma, in Pqf.SequentProps]
make_impl_sound_L [lemma, in Pqf.SequentProps]
MO [module, in Pqf.Environments]
M:12 [binder, in Pqf.Environments]
M:15 [binder, in Pqf.Environments]
M:18 [binder, in Pqf.Environments]
M:2 [binder, in Pqf.Environments]
M:28 [binder, in Pqf.Environments]
M:30 [binder, in Pqf.Environments]
M:5 [binder, in Pqf.Environments]
M:8 [binder, in Pqf.Environments]


N

N:13 [binder, in Pqf.Environments]
N:16 [binder, in Pqf.Environments]
N:19 [binder, in Pqf.Environments]
N:6 [binder, in Pqf.Environments]
N:9 [binder, in Pqf.Environments]


O

occurs_in [definition, in Pqf.Formulas]
occurs_in_make_impl2 [lemma, in Pqf.Environments]
occurs_in_make_impl [lemma, in Pqf.Environments]
occurs_in_make_disj [lemma, in Pqf.Environments]
occurs_in_make_conj [lemma, in Pqf.Environments]
Or [constructor, in Pqf.Formulas]
Order [section, in Pqf.Environments]
OrL [constructor, in Pqf.Sequents]
OrL_rev [lemma, in Pqf.SequentProps]
OrR_idemp [lemma, in Pqf.SequentProps]
OrR1 [constructor, in Pqf.Sequents]
OrR1Bot_rev [lemma, in Pqf.SequentProps]
OrR2 [constructor, in Pqf.Sequents]
OrR2Bot_rev [lemma, in Pqf.SequentProps]


P

pe0:12 [binder, in Pqf.PropQuantifiers]
pe0:27 [binder, in Pqf.PropQuantifiers]
pe0:37 [binder, in Pqf.PropQuantifiers]
pe0:40 [binder, in Pqf.PropQuantifiers]
pe1:193 [binder, in Pqf.Environments]
pe2:194 [binder, in Pqf.Environments]
pe:105 [binder, in Pqf.PropQuantifiers]
pe:109 [binder, in Pqf.PropQuantifiers]
pe:117 [binder, in Pqf.PropQuantifiers]
pe:121 [binder, in Pqf.PropQuantifiers]
pe:136 [binder, in Pqf.PropQuantifiers]
pe:185 [binder, in Pqf.PropQuantifiers]
pe:186 [binder, in Pqf.PropQuantifiers]
pe:187 [binder, in Pqf.PropQuantifiers]
pe:19 [binder, in Pqf.PropQuantifiers]
pe:193 [binder, in Pqf.PropQuantifiers]
pe:194 [binder, in Pqf.PropQuantifiers]
pe:195 [binder, in Pqf.PropQuantifiers]
pe:34 [binder, in Pqf.PropQuantifiers]
pe:4 [binder, in Pqf.PropQuantifiers]
pe:44 [binder, in Pqf.PropQuantifiers]
pe:47 [binder, in Pqf.PropQuantifiers]
pe:48 [binder, in Pqf.PropQuantifiers]
pe:58 [binder, in Pqf.PropQuantifiers]
pe:68 [binder, in Pqf.PropQuantifiers]
pe:75 [binder, in Pqf.PropQuantifiers]
pe:80 [binder, in Pqf.PropQuantifiers]
pe:81 [binder, in Pqf.PropQuantifiers]
pe:82 [binder, in Pqf.PropQuantifiers]
pe:91 [binder, in Pqf.PropQuantifiers]
pe:95 [binder, in Pqf.PropQuantifiers]
pitts [lemma, in Pqf.PropQuantifiers]
Pitts [section, in Pqf.PropQuantifiers]
Pitts.Correctness [section, in Pqf.PropQuantifiers]
Pitts.Correctness.EntailmentCorrect [section, in Pqf.PropQuantifiers]
Pitts.Correctness.PropQuantCorrect [section, in Pqf.PropQuantifiers]
Pitts.Correctness.VariablesCorrect [section, in Pqf.PropQuantifiers]
Pitts.p [variable, in Pqf.PropQuantifiers]
Pitts.PropQuantDefinition [section, in Pqf.PropQuantifiers]
pointed_env_order [definition, in Pqf.Environments]
pointed_env [definition, in Pqf.Environments]
pq_correct [lemma, in Pqf.PropQuantifiers]
proper_Provable [instance, in Pqf.Sequents]
proper_disj_union [instance, in Pqf.Environments]
proper_elem_of [instance, in Pqf.Environments]
PropQuantifiers [library]
Provable [inductive, in Pqf.Sequents]
p_contr [lemma, in Pqf.SequentProps]
P:189 [binder, in Pqf.Environments]
p:204 [binder, in Pqf.PropQuantifiers]
p:209 [binder, in Pqf.PropQuantifiers]
P:221 [binder, in Pqf.Environments]
p:232 [binder, in Pqf.Environments]
p:25 [binder, in Pqf.SequentProps]
P:27 [binder, in Pqf.Environments]
p:28 [binder, in Pqf.Sequents]
P:35 [binder, in Pqf.Formulas]
p:4 [binder, in Pqf.Sequents]
p:43 [binder, in Pqf.Environments]


S

SequentProps [library]
Sequents [library]
singleton [instance, in Pqf.Environments]
singletonMS [instance, in Pqf.Environments]
SubAnd [constructor, in Pqf.Formulas]
SubEq [constructor, in Pqf.Formulas]
subform [inductive, in Pqf.Formulas]
SubImpl [constructor, in Pqf.Formulas]
SubOr [constructor, in Pqf.Formulas]


T

TopL_rev [lemma, in Pqf.SequentProps]
t:10 [binder, in Pqf.Formulas]


U

union_difference_R [lemma, in Pqf.Environments]
union_difference_L [lemma, in Pqf.Environments]


V

Var [constructor, in Pqf.Formulas]
variable [definition, in Pqf.Formulas]
variables_disjunction [lemma, in Pqf.Environments]
variables_conjunction [lemma, in Pqf.Environments]
vars_incl [definition, in Pqf.PropQuantifiers]
var_not_in_env [definition, in Pqf.Environments]
V:210 [binder, in Pqf.PropQuantifiers]
v:53 [binder, in Pqf.Environments]
v:62 [binder, in Pqf.Environments]
v:71 [binder, in Pqf.Environments]
v:74 [binder, in Pqf.Environments]


W

weakening [lemma, in Pqf.SequentProps]
weak_ImpL [lemma, in Pqf.SequentProps]
weight [definition, in Pqf.Formulas]
weight_ind [definition, in Pqf.Formulas]
weight_pos [lemma, in Pqf.Formulas]
wf_pointed_order [lemma, in Pqf.Environments]
wf_env_order [definition, in Pqf.Environments]


X

x:1 [binder, in Pqf.Environments]
x:10 [binder, in Pqf.Environments]
x:108 [binder, in Pqf.PropQuantifiers]
x:11 [binder, in Pqf.Environments]
x:120 [binder, in Pqf.PropQuantifiers]
x:129 [binder, in Pqf.PropQuantifiers]
x:14 [binder, in Pqf.Environments]
x:158 [binder, in Pqf.PropQuantifiers]
x:161 [binder, in Pqf.PropQuantifiers]
x:164 [binder, in Pqf.PropQuantifiers]
x:167 [binder, in Pqf.PropQuantifiers]
x:17 [binder, in Pqf.Environments]
x:190 [binder, in Pqf.Environments]
X:191 [binder, in Pqf.Environments]
X:192 [binder, in Pqf.Environments]
x:20 [binder, in Pqf.Environments]
x:208 [binder, in Pqf.PropQuantifiers]
x:21 [binder, in Pqf.Environments]
x:23 [binder, in Pqf.Environments]
x:235 [binder, in Pqf.Environments]
x:236 [binder, in Pqf.Environments]
X:25 [binder, in Pqf.Environments]
x:26 [binder, in Pqf.Environments]
x:3 [binder, in Pqf.Formulas]
x:3 [binder, in Pqf.Environments]
x:33 [binder, in Pqf.Environments]
x:47 [binder, in Pqf.Environments]
x:51 [binder, in Pqf.Environments]
x:54 [binder, in Pqf.Environments]
x:56 [binder, in Pqf.Environments]
x:60 [binder, in Pqf.Environments]
x:63 [binder, in Pqf.Environments]
x:65 [binder, in Pqf.Environments]
x:69 [binder, in Pqf.Environments]
x:7 [binder, in Pqf.Environments]
x:72 [binder, in Pqf.Environments]
x:75 [binder, in Pqf.Environments]
x:80 [binder, in Pqf.Environments]
x:87 [binder, in Pqf.Environments]
x:94 [binder, in Pqf.PropQuantifiers]


Y

y:22 [binder, in Pqf.Environments]
y:24 [binder, in Pqf.Environments]
y:34 [binder, in Pqf.Environments]
y:4 [binder, in Pqf.Environments]
y:48 [binder, in Pqf.Environments]
y:52 [binder, in Pqf.Environments]
y:55 [binder, in Pqf.Environments]
y:57 [binder, in Pqf.Environments]
y:61 [binder, in Pqf.Environments]
y:64 [binder, in Pqf.Environments]
y:66 [binder, in Pqf.Environments]
y:70 [binder, in Pqf.Environments]
y:73 [binder, in Pqf.Environments]
y:76 [binder, in Pqf.Environments]


Z

z:77 [binder, in Pqf.Environments]


other

_ ≺f _ [notation, in Pqf.Formulas]
_ _ ⇔ _ _ [notation, in Pqf.Formulas]
_ → _ [notation, in Pqf.Formulas]
_ ∨ _ [notation, in Pqf.Formulas]
_ ∧ _ [notation, in Pqf.Formulas]
_ ⊢ _ [notation, in Pqf.Sequents]
_ ≺· _ [notation, in Pqf.Environments]
_ ⇢ _ [notation, in Pqf.Environments]
_ ⊻ _ [notation, in Pqf.Environments]
_ ⊼ _ [notation, in Pqf.Environments]
_ • _ [notation, in Pqf.Environments]
_ ≺ _ [notation, in Pqf.Environments]
¬ _ [notation, in Pqf.Formulas]
[notation, in Pqf.Formulas]
[notation, in Pqf.Formulas]
[notation, in Pqf.Environments]
[notation, in Pqf.Environments]
Γ':116 [binder, in Pqf.Environments]
Γ':120 [binder, in Pqf.Environments]
Γ':125 [binder, in Pqf.Environments]
Γ':139 [binder, in Pqf.Environments]
Γ':144 [binder, in Pqf.Environments]
Γ':181 [binder, in Pqf.Environments]
Γ':185 [binder, in Pqf.Environments]
Γ':188 [binder, in Pqf.Environments]
Γ':5 [binder, in Pqf.SequentProps]
Γ':78 [binder, in Pqf.SequentProps]
Γ':8 [binder, in Pqf.SequentProps]
Γ':98 [binder, in Pqf.Environments]
Γ0:171 [binder, in Pqf.PropQuantifiers]
Γ0:173 [binder, in Pqf.PropQuantifiers]
Γ0:175 [binder, in Pqf.PropQuantifiers]
Γ0:177 [binder, in Pqf.PropQuantifiers]
Γ:10 [binder, in Pqf.Sequents]
Γ:10 [binder, in Pqf.SequentProps]
Γ:102 [binder, in Pqf.SequentProps]
Γ:103 [binder, in Pqf.Environments]
Γ:106 [binder, in Pqf.SequentProps]
Γ:110 [binder, in Pqf.Environments]
Γ:111 [binder, in Pqf.SequentProps]
Γ:114 [binder, in Pqf.SequentProps]
Γ:117 [binder, in Pqf.SequentProps]
Γ:121 [binder, in Pqf.SequentProps]
Γ:124 [binder, in Pqf.Environments]
Γ:125 [binder, in Pqf.SequentProps]
Γ:129 [binder, in Pqf.SequentProps]
Γ:13 [binder, in Pqf.SequentProps]
Γ:133 [binder, in Pqf.Environments]
Γ:133 [binder, in Pqf.SequentProps]
Γ:136 [binder, in Pqf.SequentProps]
Γ:139 [binder, in Pqf.SequentProps]
Γ:14 [binder, in Pqf.Sequents]
Γ:141 [binder, in Pqf.SequentProps]
Γ:144 [binder, in Pqf.SequentProps]
Γ:147 [binder, in Pqf.SequentProps]
Γ:157 [binder, in Pqf.Environments]
Γ:159 [binder, in Pqf.Environments]
Γ:160 [binder, in Pqf.SequentProps]
Γ:165 [binder, in Pqf.SequentProps]
Γ:17 [binder, in Pqf.Sequents]
Γ:17 [binder, in Pqf.SequentProps]
Γ:172 [binder, in Pqf.SequentProps]
Γ:178 [binder, in Pqf.SequentProps]
Γ:179 [binder, in Pqf.PropQuantifiers]
Γ:180 [binder, in Pqf.Environments]
Γ:184 [binder, in Pqf.Environments]
Γ:187 [binder, in Pqf.Environments]
Γ:188 [binder, in Pqf.PropQuantifiers]
Γ:196 [binder, in Pqf.PropQuantifiers]
Γ:2 [binder, in Pqf.SequentProps]
Γ:20 [binder, in Pqf.Sequents]
Γ:21 [binder, in Pqf.SequentProps]
Γ:222 [binder, in Pqf.Environments]
Γ:226 [binder, in Pqf.Environments]
Γ:229 [binder, in Pqf.Environments]
Γ:233 [binder, in Pqf.Environments]
Γ:24 [binder, in Pqf.Sequents]
Γ:24 [binder, in Pqf.SequentProps]
Γ:27 [binder, in Pqf.Sequents]
Γ:28 [binder, in Pqf.SequentProps]
Γ:3 [binder, in Pqf.Sequents]
Γ:31 [binder, in Pqf.Sequents]
Γ:31 [binder, in Pqf.Environments]
Γ:33 [binder, in Pqf.SequentProps]
Γ:36 [binder, in Pqf.Sequents]
Γ:37 [binder, in Pqf.Environments]
Γ:38 [binder, in Pqf.SequentProps]
Γ:4 [binder, in Pqf.SequentProps]
Γ:40 [binder, in Pqf.Environments]
Γ:41 [binder, in Pqf.Sequents]
Γ:42 [binder, in Pqf.Environments]
Γ:43 [binder, in Pqf.SequentProps]
Γ:45 [binder, in Pqf.SequentProps]
Γ:47 [binder, in Pqf.SequentProps]
Γ:5 [binder, in Pqf.Sequents]
Γ:50 [binder, in Pqf.SequentProps]
Γ:52 [binder, in Pqf.SequentProps]
Γ:54 [binder, in Pqf.SequentProps]
Γ:58 [binder, in Pqf.SequentProps]
Γ:63 [binder, in Pqf.SequentProps]
Γ:66 [binder, in Pqf.SequentProps]
Γ:7 [binder, in Pqf.Sequents]
Γ:7 [binder, in Pqf.SequentProps]
Γ:71 [binder, in Pqf.SequentProps]
Γ:74 [binder, in Pqf.SequentProps]
Γ:77 [binder, in Pqf.SequentProps]
Γ:80 [binder, in Pqf.SequentProps]
Γ:85 [binder, in Pqf.SequentProps]
Γ:88 [binder, in Pqf.SequentProps]
Γ:92 [binder, in Pqf.SequentProps]
Γ:95 [binder, in Pqf.Environments]
Γ:97 [binder, in Pqf.SequentProps]
Δ'':173 [binder, in Pqf.Environments]
Δ'':215 [binder, in Pqf.Environments]
Δ':15 [binder, in Pqf.PropQuantifiers]
Δ':164 [binder, in Pqf.Environments]
Δ':172 [binder, in Pqf.Environments]
Δ':208 [binder, in Pqf.Environments]
Δ':211 [binder, in Pqf.Environments]
Δ':214 [binder, in Pqf.Environments]
Δ':30 [binder, in Pqf.PropQuantifiers]
Δ0:142 [binder, in Pqf.PropQuantifiers]
Δ0:145 [binder, in Pqf.PropQuantifiers]
Δ0:148 [binder, in Pqf.PropQuantifiers]
Δ0:151 [binder, in Pqf.PropQuantifiers]
Δ:101 [binder, in Pqf.PropQuantifiers]
Δ:115 [binder, in Pqf.PropQuantifiers]
Δ:127 [binder, in Pqf.PropQuantifiers]
Δ:132 [binder, in Pqf.PropQuantifiers]
Δ:138 [binder, in Pqf.PropQuantifiers]
Δ:148 [binder, in Pqf.SequentProps]
Δ:152 [binder, in Pqf.Environments]
Δ:154 [binder, in Pqf.PropQuantifiers]
Δ:161 [binder, in Pqf.Environments]
Δ:161 [binder, in Pqf.SequentProps]
Δ:163 [binder, in Pqf.Environments]
Δ:166 [binder, in Pqf.Environments]
Δ:166 [binder, in Pqf.SequentProps]
Δ:168 [binder, in Pqf.Environments]
Δ:169 [binder, in Pqf.PropQuantifiers]
Δ:17 [binder, in Pqf.PropQuantifiers]
Δ:171 [binder, in Pqf.Environments]
Δ:173 [binder, in Pqf.SequentProps]
Δ:174 [binder, in Pqf.Environments]
Δ:177 [binder, in Pqf.Environments]
Δ:179 [binder, in Pqf.SequentProps]
Δ:181 [binder, in Pqf.PropQuantifiers]
Δ:189 [binder, in Pqf.PropQuantifiers]
Δ:197 [binder, in Pqf.PropQuantifiers]
Δ:197 [binder, in Pqf.Environments]
Δ:198 [binder, in Pqf.Environments]
Δ:2 [binder, in Pqf.PropQuantifiers]
Δ:201 [binder, in Pqf.Environments]
Δ:205 [binder, in Pqf.Environments]
Δ:207 [binder, in Pqf.Environments]
Δ:210 [binder, in Pqf.Environments]
Δ:213 [binder, in Pqf.Environments]
Δ:227 [binder, in Pqf.Environments]
Δ:230 [binder, in Pqf.Environments]
Δ:24 [binder, in Pqf.PropQuantifiers]
Δ:32 [binder, in Pqf.PropQuantifiers]
Δ:32 [binder, in Pqf.Environments]
Δ:46 [binder, in Pqf.PropQuantifiers]
Δ:51 [binder, in Pqf.PropQuantifiers]
Δ:61 [binder, in Pqf.PropQuantifiers]
Δ:71 [binder, in Pqf.PropQuantifiers]
Δ:78 [binder, in Pqf.PropQuantifiers]
Δ:83 [binder, in Pqf.PropQuantifiers]
Δ:85 [binder, in Pqf.PropQuantifiers]
Δ:87 [binder, in Pqf.PropQuantifiers]
Δ:9 [binder, in Pqf.PropQuantifiers]
θ':196 [binder, in Pqf.Environments]
θ:100 [binder, in Pqf.PropQuantifiers]
θ:101 [binder, in Pqf.SequentProps]
θ:102 [binder, in Pqf.PropQuantifiers]
θ:105 [binder, in Pqf.SequentProps]
θ:110 [binder, in Pqf.SequentProps]
θ:111 [binder, in Pqf.PropQuantifiers]
θ:112 [binder, in Pqf.PropQuantifiers]
θ:114 [binder, in Pqf.PropQuantifiers]
θ:120 [binder, in Pqf.SequentProps]
θ:123 [binder, in Pqf.PropQuantifiers]
θ:124 [binder, in Pqf.PropQuantifiers]
θ:124 [binder, in Pqf.SequentProps]
θ:126 [binder, in Pqf.PropQuantifiers]
θ:128 [binder, in Pqf.SequentProps]
θ:13 [binder, in Pqf.Sequents]
θ:130 [binder, in Pqf.PropQuantifiers]
θ:131 [binder, in Pqf.PropQuantifiers]
θ:132 [binder, in Pqf.SequentProps]
θ:133 [binder, in Pqf.PropQuantifiers]
θ:149 [binder, in Pqf.SequentProps]
θ:16 [binder, in Pqf.SequentProps]
θ:163 [binder, in Pqf.SequentProps]
θ:164 [binder, in Pqf.SequentProps]
θ:168 [binder, in Pqf.SequentProps]
θ:170 [binder, in Pqf.SequentProps]
θ:175 [binder, in Pqf.SequentProps]
θ:180 [binder, in Pqf.PropQuantifiers]
θ:181 [binder, in Pqf.SequentProps]
θ:182 [binder, in Pqf.SequentProps]
θ:195 [binder, in Pqf.Environments]
θ:20 [binder, in Pqf.SequentProps]
θ:213 [binder, in Pqf.PropQuantifiers]
θ:22 [binder, in Pqf.PropQuantifiers]
θ:220 [binder, in Pqf.Environments]
θ:23 [binder, in Pqf.Sequents]
θ:23 [binder, in Pqf.SequentProps]
θ:237 [binder, in Pqf.Environments]
θ:238 [binder, in Pqf.Environments]
θ:53 [binder, in Pqf.PropQuantifiers]
θ:57 [binder, in Pqf.SequentProps]
θ:63 [binder, in Pqf.PropQuantifiers]
θ:7 [binder, in Pqf.PropQuantifiers]
θ:70 [binder, in Pqf.SequentProps]
θ:73 [binder, in Pqf.SequentProps]
θ:76 [binder, in Pqf.SequentProps]
θ:83 [binder, in Pqf.SequentProps]
θ:87 [binder, in Pqf.SequentProps]
θ:88 [binder, in Pqf.PropQuantifiers]
θ:91 [binder, in Pqf.SequentProps]
θ:96 [binder, in Pqf.SequentProps]
θ:97 [binder, in Pqf.PropQuantifiers]
θ:98 [binder, in Pqf.PropQuantifiers]
φ':1 [binder, in Pqf.SequentProps]
φ':183 [binder, in Pqf.PropQuantifiers]
φ':191 [binder, in Pqf.PropQuantifiers]
φ0:172 [binder, in Pqf.PropQuantifiers]
φ0:174 [binder, in Pqf.PropQuantifiers]
φ0:176 [binder, in Pqf.PropQuantifiers]
φ0:178 [binder, in Pqf.PropQuantifiers]
φ0:199 [binder, in Pqf.PropQuantifiers]
φ0:200 [binder, in Pqf.PropQuantifiers]
φ0:201 [binder, in Pqf.PropQuantifiers]
φ0:202 [binder, in Pqf.PropQuantifiers]
φ0:203 [binder, in Pqf.PropQuantifiers]
φ0:234 [binder, in Pqf.Environments]
φ1:107 [binder, in Pqf.SequentProps]
φ1:199 [binder, in Pqf.Environments]
φ1:202 [binder, in Pqf.Environments]
φ1:29 [binder, in Pqf.SequentProps]
φ1:32 [binder, in Pqf.Sequents]
φ1:34 [binder, in Pqf.SequentProps]
φ1:37 [binder, in Pqf.Sequents]
φ1:39 [binder, in Pqf.SequentProps]
φ1:42 [binder, in Pqf.Sequents]
φ1:48 [binder, in Pqf.SequentProps]
φ1:67 [binder, in Pqf.SequentProps]
φ1:93 [binder, in Pqf.SequentProps]
φ1:98 [binder, in Pqf.SequentProps]
φ2:108 [binder, in Pqf.SequentProps]
φ2:203 [binder, in Pqf.Environments]
φ2:30 [binder, in Pqf.SequentProps]
φ2:33 [binder, in Pqf.Sequents]
φ2:35 [binder, in Pqf.SequentProps]
φ2:38 [binder, in Pqf.Sequents]
φ2:40 [binder, in Pqf.SequentProps]
φ2:43 [binder, in Pqf.Sequents]
φ2:49 [binder, in Pqf.SequentProps]
φ2:68 [binder, in Pqf.SequentProps]
φ2:94 [binder, in Pqf.SequentProps]
φ2:99 [binder, in Pqf.SequentProps]
φ3:31 [binder, in Pqf.SequentProps]
φ3:34 [binder, in Pqf.Sequents]
φ3:36 [binder, in Pqf.SequentProps]
φ3:39 [binder, in Pqf.Sequents]
φ3:41 [binder, in Pqf.SequentProps]
φ3:44 [binder, in Pqf.Sequents]
φ3:69 [binder, in Pqf.SequentProps]
φ:103 [binder, in Pqf.SequentProps]
φ:104 [binder, in Pqf.Environments]
φ:11 [binder, in Pqf.Sequents]
φ:11 [binder, in Pqf.SequentProps]
φ:111 [binder, in Pqf.Environments]
φ:112 [binder, in Pqf.SequentProps]
φ:115 [binder, in Pqf.SequentProps]
φ:118 [binder, in Pqf.SequentProps]
φ:122 [binder, in Pqf.SequentProps]
φ:126 [binder, in Pqf.SequentProps]
φ:13 [binder, in Pqf.Formulas]
φ:130 [binder, in Pqf.SequentProps]
φ:134 [binder, in Pqf.Environments]
φ:134 [binder, in Pqf.SequentProps]
φ:137 [binder, in Pqf.SequentProps]
φ:14 [binder, in Pqf.SequentProps]
φ:142 [binder, in Pqf.SequentProps]
φ:145 [binder, in Pqf.SequentProps]
φ:15 [binder, in Pqf.Formulas]
φ:15 [binder, in Pqf.Sequents]
φ:150 [binder, in Pqf.SequentProps]
φ:151 [binder, in Pqf.SequentProps]
φ:153 [binder, in Pqf.SequentProps]
φ:155 [binder, in Pqf.Environments]
φ:155 [binder, in Pqf.SequentProps]
φ:157 [binder, in Pqf.SequentProps]
φ:159 [binder, in Pqf.SequentProps]
φ:162 [binder, in Pqf.Environments]
φ:162 [binder, in Pqf.SequentProps]
φ:165 [binder, in Pqf.Environments]
φ:167 [binder, in Pqf.Environments]
φ:167 [binder, in Pqf.SequentProps]
φ:169 [binder, in Pqf.SequentProps]
φ:17 [binder, in Pqf.Formulas]
φ:170 [binder, in Pqf.Environments]
φ:171 [binder, in Pqf.SequentProps]
φ:174 [binder, in Pqf.SequentProps]
φ:175 [binder, in Pqf.Environments]
φ:178 [binder, in Pqf.Environments]
φ:18 [binder, in Pqf.Sequents]
φ:18 [binder, in Pqf.SequentProps]
φ:180 [binder, in Pqf.SequentProps]
φ:182 [binder, in Pqf.PropQuantifiers]
φ:182 [binder, in Pqf.Environments]
φ:186 [binder, in Pqf.Environments]
φ:190 [binder, in Pqf.PropQuantifiers]
φ:200 [binder, in Pqf.Environments]
φ:204 [binder, in Pqf.Environments]
φ:205 [binder, in Pqf.PropQuantifiers]
φ:206 [binder, in Pqf.PropQuantifiers]
φ:206 [binder, in Pqf.Environments]
φ:209 [binder, in Pqf.Environments]
φ:21 [binder, in Pqf.Formulas]
φ:21 [binder, in Pqf.Sequents]
φ:211 [binder, in Pqf.PropQuantifiers]
φ:212 [binder, in Pqf.Environments]
φ:216 [binder, in Pqf.Environments]
φ:218 [binder, in Pqf.Environments]
φ:22 [binder, in Pqf.Formulas]
φ:22 [binder, in Pqf.SequentProps]
φ:223 [binder, in Pqf.Environments]
φ:224 [binder, in Pqf.Environments]
φ:225 [binder, in Pqf.Environments]
φ:25 [binder, in Pqf.Formulas]
φ:25 [binder, in Pqf.Sequents]
φ:26 [binder, in Pqf.SequentProps]
φ:28 [binder, in Pqf.Formulas]
φ:29 [binder, in Pqf.Sequents]
φ:3 [binder, in Pqf.SequentProps]
φ:31 [binder, in Pqf.Formulas]
φ:34 [binder, in Pqf.Formulas]
φ:35 [binder, in Pqf.Environments]
φ:37 [binder, in Pqf.Formulas]
φ:38 [binder, in Pqf.Formulas]
φ:38 [binder, in Pqf.Environments]
φ:39 [binder, in Pqf.Formulas]
φ:4 [binder, in Pqf.Formulas]
φ:41 [binder, in Pqf.Environments]
φ:44 [binder, in Pqf.Environments]
φ:44 [binder, in Pqf.SequentProps]
φ:45 [binder, in Pqf.Environments]
φ:46 [binder, in Pqf.SequentProps]
φ:51 [binder, in Pqf.SequentProps]
φ:53 [binder, in Pqf.SequentProps]
φ:55 [binder, in Pqf.SequentProps]
φ:59 [binder, in Pqf.SequentProps]
φ:6 [binder, in Pqf.Sequents]
φ:6 [binder, in Pqf.SequentProps]
φ:64 [binder, in Pqf.SequentProps]
φ:7 [binder, in Pqf.Formulas]
φ:72 [binder, in Pqf.SequentProps]
φ:79 [binder, in Pqf.SequentProps]
φ:8 [binder, in Pqf.Sequents]
φ:81 [binder, in Pqf.SequentProps]
φ:82 [binder, in Pqf.Environments]
φ:84 [binder, in Pqf.Environments]
φ:84 [binder, in Pqf.SequentProps]
φ:86 [binder, in Pqf.Environments]
φ:89 [binder, in Pqf.Environments]
φ:89 [binder, in Pqf.SequentProps]
φ:9 [binder, in Pqf.SequentProps]
φ:91 [binder, in Pqf.Environments]
φ:93 [binder, in Pqf.Environments]
φ:96 [binder, in Pqf.Environments]
ψ0:114 [binder, in Pqf.Environments]
ψ0:118 [binder, in Pqf.Environments]
ψ0:122 [binder, in Pqf.Environments]
ψ0:127 [binder, in Pqf.Environments]
ψ0:136 [binder, in Pqf.Environments]
ψ0:141 [binder, in Pqf.Environments]
ψ0:146 [binder, in Pqf.Environments]
ψ1:23 [binder, in Pqf.Formulas]
ψ1:26 [binder, in Pqf.Formulas]
ψ1:29 [binder, in Pqf.Formulas]
ψ2:24 [binder, in Pqf.Formulas]
ψ2:27 [binder, in Pqf.Formulas]
ψ2:30 [binder, in Pqf.Formulas]
ψ:100 [binder, in Pqf.SequentProps]
ψ:104 [binder, in Pqf.SequentProps]
ψ:109 [binder, in Pqf.SequentProps]
ψ:113 [binder, in Pqf.Environments]
ψ:113 [binder, in Pqf.SequentProps]
ψ:116 [binder, in Pqf.SequentProps]
ψ:119 [binder, in Pqf.SequentProps]
ψ:12 [binder, in Pqf.Sequents]
ψ:12 [binder, in Pqf.SequentProps]
ψ:123 [binder, in Pqf.SequentProps]
ψ:127 [binder, in Pqf.SequentProps]
ψ:131 [binder, in Pqf.SequentProps]
ψ:135 [binder, in Pqf.SequentProps]
ψ:138 [binder, in Pqf.SequentProps]
ψ:14 [binder, in Pqf.Formulas]
ψ:140 [binder, in Pqf.SequentProps]
ψ:143 [binder, in Pqf.SequentProps]
ψ:146 [binder, in Pqf.SequentProps]
ψ:15 [binder, in Pqf.SequentProps]
ψ:152 [binder, in Pqf.SequentProps]
ψ:154 [binder, in Pqf.SequentProps]
ψ:156 [binder, in Pqf.SequentProps]
ψ:158 [binder, in Pqf.SequentProps]
ψ:16 [binder, in Pqf.Formulas]
ψ:16 [binder, in Pqf.Sequents]
ψ:176 [binder, in Pqf.SequentProps]
ψ:177 [binder, in Pqf.SequentProps]
ψ:179 [binder, in Pqf.Environments]
ψ:18 [binder, in Pqf.Formulas]
ψ:183 [binder, in Pqf.Environments]
ψ:19 [binder, in Pqf.Sequents]
ψ:19 [binder, in Pqf.SequentProps]
ψ:212 [binder, in Pqf.PropQuantifiers]
ψ:217 [binder, in Pqf.Environments]
ψ:219 [binder, in Pqf.Environments]
ψ:22 [binder, in Pqf.Sequents]
ψ:26 [binder, in Pqf.Sequents]
ψ:27 [binder, in Pqf.SequentProps]
ψ:30 [binder, in Pqf.Sequents]
ψ:32 [binder, in Pqf.SequentProps]
ψ:35 [binder, in Pqf.Sequents]
ψ:36 [binder, in Pqf.Formulas]
ψ:36 [binder, in Pqf.Environments]
ψ:37 [binder, in Pqf.SequentProps]
ψ:39 [binder, in Pqf.Environments]
ψ:40 [binder, in Pqf.Formulas]
ψ:40 [binder, in Pqf.Sequents]
ψ:42 [binder, in Pqf.SequentProps]
ψ:45 [binder, in Pqf.Sequents]
ψ:46 [binder, in Pqf.Environments]
ψ:49 [binder, in Pqf.PropQuantifiers]
ψ:50 [binder, in Pqf.PropQuantifiers]
ψ:56 [binder, in Pqf.SequentProps]
ψ:75 [binder, in Pqf.SequentProps]
ψ:82 [binder, in Pqf.SequentProps]
ψ:83 [binder, in Pqf.Environments]
ψ:85 [binder, in Pqf.Environments]
ψ:86 [binder, in Pqf.SequentProps]
ψ:9 [binder, in Pqf.Sequents]
ψ:90 [binder, in Pqf.Environments]
ψ:90 [binder, in Pqf.SequentProps]
ψ:92 [binder, in Pqf.Environments]
ψ:95 [binder, in Pqf.SequentProps]
ϕ':168 [binder, in Pqf.PropQuantifiers]
ϕ0:143 [binder, in Pqf.PropQuantifiers]
ϕ0:146 [binder, in Pqf.PropQuantifiers]
ϕ0:149 [binder, in Pqf.PropQuantifiers]
ϕ0:152 [binder, in Pqf.PropQuantifiers]
ϕ:104 [binder, in Pqf.PropQuantifiers]
ϕ:116 [binder, in Pqf.PropQuantifiers]
ϕ:128 [binder, in Pqf.PropQuantifiers]
ϕ:134 [binder, in Pqf.PropQuantifiers]
ϕ:139 [binder, in Pqf.PropQuantifiers]
ϕ:155 [binder, in Pqf.PropQuantifiers]
ϕ:169 [binder, in Pqf.Environments]
ϕ:170 [binder, in Pqf.PropQuantifiers]
ϕ:176 [binder, in Pqf.Environments]
ϕ:18 [binder, in Pqf.PropQuantifiers]
ϕ:198 [binder, in Pqf.PropQuantifiers]
ϕ:228 [binder, in Pqf.Environments]
ϕ:231 [binder, in Pqf.Environments]
ϕ:3 [binder, in Pqf.PropQuantifiers]
ϕ:33 [binder, in Pqf.PropQuantifiers]
ϕ:52 [binder, in Pqf.PropQuantifiers]
ϕ:62 [binder, in Pqf.PropQuantifiers]
ϕ:72 [binder, in Pqf.PropQuantifiers]
ϕ:79 [binder, in Pqf.PropQuantifiers]
ϕ:84 [binder, in Pqf.PropQuantifiers]
ϕ:86 [binder, in Pqf.PropQuantifiers]
ϕ:90 [binder, in Pqf.PropQuantifiers]



Notation Index

other

_ ≺f _ [in Pqf.Formulas]
_ _ ⇔ _ _ [in Pqf.Formulas]
_ → _ [in Pqf.Formulas]
_ ∨ _ [in Pqf.Formulas]
_ ∧ _ [in Pqf.Formulas]
_ ⊢ _ [in Pqf.Sequents]
_ ≺· _ [in Pqf.Environments]
_ ⇢ _ [in Pqf.Environments]
_ ⊻ _ [in Pqf.Environments]
_ ⊼ _ [in Pqf.Environments]
_ • _ [in Pqf.Environments]
_ ≺ _ [in Pqf.Environments]
¬ _ [in Pqf.Formulas]
[in Pqf.Formulas]
[in Pqf.Formulas]
[in Pqf.Environments]
[in Pqf.Environments]



Binder Index

A

A:102 [in Pqf.Environments]
A:106 [in Pqf.Environments]
a:107 [in Pqf.Environments]
A:129 [in Pqf.Environments]
a:130 [in Pqf.Environments]
A:14 [in Pqf.PropQuantifiers]
A:149 [in Pqf.Environments]
A:151 [in Pqf.Environments]
A:29 [in Pqf.PropQuantifiers]
a:29 [in Pqf.Environments]
A:42 [in Pqf.PropQuantifiers]
A:94 [in Pqf.Environments]


B

b:108 [in Pqf.Environments]
b:131 [in Pqf.Environments]


D

d:156 [in Pqf.PropQuantifiers]
d:159 [in Pqf.PropQuantifiers]
d:162 [in Pqf.PropQuantifiers]
d:165 [in Pqf.PropQuantifiers]


E

EA0:107 [in Pqf.PropQuantifiers]
EA0:119 [in Pqf.PropQuantifiers]
EA0:137 [in Pqf.PropQuantifiers]
EA0:21 [in Pqf.PropQuantifiers]
EA0:36 [in Pqf.PropQuantifiers]
EA0:6 [in Pqf.PropQuantifiers]
EA0:93 [in Pqf.PropQuantifiers]
EA1:56 [in Pqf.PropQuantifiers]
EA1:66 [in Pqf.PropQuantifiers]
EA1:73 [in Pqf.PropQuantifiers]
EA2:57 [in Pqf.PropQuantifiers]
EA2:67 [in Pqf.PropQuantifiers]
EA2:74 [in Pqf.PropQuantifiers]
E:11 [in Pqf.PropQuantifiers]
E:26 [in Pqf.PropQuantifiers]
E:39 [in Pqf.PropQuantifiers]


F

f:105 [in Pqf.Environments]
f:112 [in Pqf.Environments]
f:135 [in Pqf.Environments]
f:150 [in Pqf.Environments]
f:153 [in Pqf.Environments]
f:157 [in Pqf.PropQuantifiers]
f:160 [in Pqf.PropQuantifiers]
f:163 [in Pqf.PropQuantifiers]
f:166 [in Pqf.PropQuantifiers]
f:97 [in Pqf.Environments]


G

g:154 [in Pqf.Environments]


H

HD:109 [in Pqf.Environments]
HD:132 [in Pqf.Environments]
HEA0:113 [in Pqf.PropQuantifiers]
HEA0:125 [in Pqf.PropQuantifiers]
HEA0:99 [in Pqf.PropQuantifiers]
HEA:141 [in Pqf.PropQuantifiers]
Hin':138 [in Pqf.Environments]
Hin':143 [in Pqf.Environments]
Hin':148 [in Pqf.Environments]
Hin1:54 [in Pqf.PropQuantifiers]
Hin1:64 [in Pqf.PropQuantifiers]
Hin2:55 [in Pqf.PropQuantifiers]
Hin2:65 [in Pqf.PropQuantifiers]
Hin:103 [in Pqf.PropQuantifiers]
Hin:115 [in Pqf.Environments]
Hin:119 [in Pqf.Environments]
Hin:123 [in Pqf.Environments]
Hin:128 [in Pqf.Environments]
Hin:135 [in Pqf.PropQuantifiers]
Hin:137 [in Pqf.Environments]
Hin:142 [in Pqf.Environments]
Hin:147 [in Pqf.Environments]
Hin:184 [in Pqf.PropQuantifiers]
Hin:192 [in Pqf.PropQuantifiers]
Hin:23 [in Pqf.PropQuantifiers]
Hin:8 [in Pqf.PropQuantifiers]
Hin:89 [in Pqf.PropQuantifiers]
Hi:126 [in Pqf.Environments]
Hpe':60 [in Pqf.PropQuantifiers]
Hpe':70 [in Pqf.PropQuantifiers]
Hpe':77 [in Pqf.PropQuantifiers]
Hpe:106 [in Pqf.PropQuantifiers]
Hpe:110 [in Pqf.PropQuantifiers]
Hpe:118 [in Pqf.PropQuantifiers]
Hpe:122 [in Pqf.PropQuantifiers]
Hpe:140 [in Pqf.PropQuantifiers]
Hpe:144 [in Pqf.PropQuantifiers]
Hpe:147 [in Pqf.PropQuantifiers]
Hpe:150 [in Pqf.PropQuantifiers]
Hpe:153 [in Pqf.PropQuantifiers]
Hpe:20 [in Pqf.PropQuantifiers]
Hpe:35 [in Pqf.PropQuantifiers]
Hpe:5 [in Pqf.PropQuantifiers]
Hpe:59 [in Pqf.PropQuantifiers]
Hpe:69 [in Pqf.PropQuantifiers]
Hpe:76 [in Pqf.PropQuantifiers]
Hpe:92 [in Pqf.PropQuantifiers]
Hpe:96 [in Pqf.PropQuantifiers]
Hp:60 [in Pqf.SequentProps]
Hp:65 [in Pqf.SequentProps]
H:10 [in Pqf.PropQuantifiers]
H:13 [in Pqf.PropQuantifiers]
H:156 [in Pqf.Environments]
H:25 [in Pqf.PropQuantifiers]
H:28 [in Pqf.PropQuantifiers]
H:38 [in Pqf.PropQuantifiers]
H:41 [in Pqf.PropQuantifiers]
HΓ':117 [in Pqf.Environments]
HΓ':121 [in Pqf.Environments]
HΓ':140 [in Pqf.Environments]
HΓ':145 [in Pqf.Environments]
HΓ':99 [in Pqf.Environments]
HΓ:158 [in Pqf.Environments]
HΓ:160 [in Pqf.Environments]


L

l:207 [in Pqf.PropQuantifiers]
l:78 [in Pqf.Environments]
l:79 [in Pqf.Environments]
l:81 [in Pqf.Environments]
l:88 [in Pqf.Environments]


M

M:12 [in Pqf.Environments]
M:15 [in Pqf.Environments]
M:18 [in Pqf.Environments]
M:2 [in Pqf.Environments]
M:28 [in Pqf.Environments]
M:30 [in Pqf.Environments]
M:5 [in Pqf.Environments]
M:8 [in Pqf.Environments]


N

N:13 [in Pqf.Environments]
N:16 [in Pqf.Environments]
N:19 [in Pqf.Environments]
N:6 [in Pqf.Environments]
N:9 [in Pqf.Environments]


P

pe0:12 [in Pqf.PropQuantifiers]
pe0:27 [in Pqf.PropQuantifiers]
pe0:37 [in Pqf.PropQuantifiers]
pe0:40 [in Pqf.PropQuantifiers]
pe1:193 [in Pqf.Environments]
pe2:194 [in Pqf.Environments]
pe:105 [in Pqf.PropQuantifiers]
pe:109 [in Pqf.PropQuantifiers]
pe:117 [in Pqf.PropQuantifiers]
pe:121 [in Pqf.PropQuantifiers]
pe:136 [in Pqf.PropQuantifiers]
pe:185 [in Pqf.PropQuantifiers]
pe:186 [in Pqf.PropQuantifiers]
pe:187 [in Pqf.PropQuantifiers]
pe:19 [in Pqf.PropQuantifiers]
pe:193 [in Pqf.PropQuantifiers]
pe:194 [in Pqf.PropQuantifiers]
pe:195 [in Pqf.PropQuantifiers]
pe:34 [in Pqf.PropQuantifiers]
pe:4 [in Pqf.PropQuantifiers]
pe:44 [in Pqf.PropQuantifiers]
pe:47 [in Pqf.PropQuantifiers]
pe:48 [in Pqf.PropQuantifiers]
pe:58 [in Pqf.PropQuantifiers]
pe:68 [in Pqf.PropQuantifiers]
pe:75 [in Pqf.PropQuantifiers]
pe:80 [in Pqf.PropQuantifiers]
pe:81 [in Pqf.PropQuantifiers]
pe:82 [in Pqf.PropQuantifiers]
pe:91 [in Pqf.PropQuantifiers]
pe:95 [in Pqf.PropQuantifiers]
P:189 [in Pqf.Environments]
p:204 [in Pqf.PropQuantifiers]
p:209 [in Pqf.PropQuantifiers]
P:221 [in Pqf.Environments]
p:232 [in Pqf.Environments]
p:25 [in Pqf.SequentProps]
P:27 [in Pqf.Environments]
p:28 [in Pqf.Sequents]
P:35 [in Pqf.Formulas]
p:4 [in Pqf.Sequents]
p:43 [in Pqf.Environments]


T

t:10 [in Pqf.Formulas]


V

V:210 [in Pqf.PropQuantifiers]
v:53 [in Pqf.Environments]
v:62 [in Pqf.Environments]
v:71 [in Pqf.Environments]
v:74 [in Pqf.Environments]


X

x:1 [in Pqf.Environments]
x:10 [in Pqf.Environments]
x:108 [in Pqf.PropQuantifiers]
x:11 [in Pqf.Environments]
x:120 [in Pqf.PropQuantifiers]
x:129 [in Pqf.PropQuantifiers]
x:14 [in Pqf.Environments]
x:158 [in Pqf.PropQuantifiers]
x:161 [in Pqf.PropQuantifiers]
x:164 [in Pqf.PropQuantifiers]
x:167 [in Pqf.PropQuantifiers]
x:17 [in Pqf.Environments]
x:190 [in Pqf.Environments]
X:191 [in Pqf.Environments]
X:192 [in Pqf.Environments]
x:20 [in Pqf.Environments]
x:208 [in Pqf.PropQuantifiers]
x:21 [in Pqf.Environments]
x:23 [in Pqf.Environments]
x:235 [in Pqf.Environments]
x:236 [in Pqf.Environments]
X:25 [in Pqf.Environments]
x:26 [in Pqf.Environments]
x:3 [in Pqf.Formulas]
x:3 [in Pqf.Environments]
x:33 [in Pqf.Environments]
x:47 [in Pqf.Environments]
x:51 [in Pqf.Environments]
x:54 [in Pqf.Environments]
x:56 [in Pqf.Environments]
x:60 [in Pqf.Environments]
x:63 [in Pqf.Environments]
x:65 [in Pqf.Environments]
x:69 [in Pqf.Environments]
x:7 [in Pqf.Environments]
x:72 [in Pqf.Environments]
x:75 [in Pqf.Environments]
x:80 [in Pqf.Environments]
x:87 [in Pqf.Environments]
x:94 [in Pqf.PropQuantifiers]


Y

y:22 [in Pqf.Environments]
y:24 [in Pqf.Environments]
y:34 [in Pqf.Environments]
y:4 [in Pqf.Environments]
y:48 [in Pqf.Environments]
y:52 [in Pqf.Environments]
y:55 [in Pqf.Environments]
y:57 [in Pqf.Environments]
y:61 [in Pqf.Environments]
y:64 [in Pqf.Environments]
y:66 [in Pqf.Environments]
y:70 [in Pqf.Environments]
y:73 [in Pqf.Environments]
y:76 [in Pqf.Environments]


Z

z:77 [in Pqf.Environments]


other

Γ':116 [in Pqf.Environments]
Γ':120 [in Pqf.Environments]
Γ':125 [in Pqf.Environments]
Γ':139 [in Pqf.Environments]
Γ':144 [in Pqf.Environments]
Γ':181 [in Pqf.Environments]
Γ':185 [in Pqf.Environments]
Γ':188 [in Pqf.Environments]
Γ':5 [in Pqf.SequentProps]
Γ':78 [in Pqf.SequentProps]
Γ':8 [in Pqf.SequentProps]
Γ':98 [in Pqf.Environments]
Γ0:171 [in Pqf.PropQuantifiers]
Γ0:173 [in Pqf.PropQuantifiers]
Γ0:175 [in Pqf.PropQuantifiers]
Γ0:177 [in Pqf.PropQuantifiers]
Γ:10 [in Pqf.Sequents]
Γ:10 [in Pqf.SequentProps]
Γ:102 [in Pqf.SequentProps]
Γ:103 [in Pqf.Environments]
Γ:106 [in Pqf.SequentProps]
Γ:110 [in Pqf.Environments]
Γ:111 [in Pqf.SequentProps]
Γ:114 [in Pqf.SequentProps]
Γ:117 [in Pqf.SequentProps]
Γ:121 [in Pqf.SequentProps]
Γ:124 [in Pqf.Environments]
Γ:125 [in Pqf.SequentProps]
Γ:129 [in Pqf.SequentProps]
Γ:13 [in Pqf.SequentProps]
Γ:133 [in Pqf.Environments]
Γ:133 [in Pqf.SequentProps]
Γ:136 [in Pqf.SequentProps]
Γ:139 [in Pqf.SequentProps]
Γ:14 [in Pqf.Sequents]
Γ:141 [in Pqf.SequentProps]
Γ:144 [in Pqf.SequentProps]
Γ:147 [in Pqf.SequentProps]
Γ:157 [in Pqf.Environments]
Γ:159 [in Pqf.Environments]
Γ:160 [in Pqf.SequentProps]
Γ:165 [in Pqf.SequentProps]
Γ:17 [in Pqf.Sequents]
Γ:17 [in Pqf.SequentProps]
Γ:172 [in Pqf.SequentProps]
Γ:178 [in Pqf.SequentProps]
Γ:179 [in Pqf.PropQuantifiers]
Γ:180 [in Pqf.Environments]
Γ:184 [in Pqf.Environments]
Γ:187 [in Pqf.Environments]
Γ:188 [in Pqf.PropQuantifiers]
Γ:196 [in Pqf.PropQuantifiers]
Γ:2 [in Pqf.SequentProps]
Γ:20 [in Pqf.Sequents]
Γ:21 [in Pqf.SequentProps]
Γ:222 [in Pqf.Environments]
Γ:226 [in Pqf.Environments]
Γ:229 [in Pqf.Environments]
Γ:233 [in Pqf.Environments]
Γ:24 [in Pqf.Sequents]
Γ:24 [in Pqf.SequentProps]
Γ:27 [in Pqf.Sequents]
Γ:28 [in Pqf.SequentProps]
Γ:3 [in Pqf.Sequents]
Γ:31 [in Pqf.Sequents]
Γ:31 [in Pqf.Environments]
Γ:33 [in Pqf.SequentProps]
Γ:36 [in Pqf.Sequents]
Γ:37 [in Pqf.Environments]
Γ:38 [in Pqf.SequentProps]
Γ:4 [in Pqf.SequentProps]
Γ:40 [in Pqf.Environments]
Γ:41 [in Pqf.Sequents]
Γ:42 [in Pqf.Environments]
Γ:43 [in Pqf.SequentProps]
Γ:45 [in Pqf.SequentProps]
Γ:47 [in Pqf.SequentProps]
Γ:5 [in Pqf.Sequents]
Γ:50 [in Pqf.SequentProps]
Γ:52 [in Pqf.SequentProps]
Γ:54 [in Pqf.SequentProps]
Γ:58 [in Pqf.SequentProps]
Γ:63 [in Pqf.SequentProps]
Γ:66 [in Pqf.SequentProps]
Γ:7 [in Pqf.Sequents]
Γ:7 [in Pqf.SequentProps]
Γ:71 [in Pqf.SequentProps]
Γ:74 [in Pqf.SequentProps]
Γ:77 [in Pqf.SequentProps]
Γ:80 [in Pqf.SequentProps]
Γ:85 [in Pqf.SequentProps]
Γ:88 [in Pqf.SequentProps]
Γ:92 [in Pqf.SequentProps]
Γ:95 [in Pqf.Environments]
Γ:97 [in Pqf.SequentProps]
Δ'':173 [in Pqf.Environments]
Δ'':215 [in Pqf.Environments]
Δ':15 [in Pqf.PropQuantifiers]
Δ':164 [in Pqf.Environments]
Δ':172 [in Pqf.Environments]
Δ':208 [in Pqf.Environments]
Δ':211 [in Pqf.Environments]
Δ':214 [in Pqf.Environments]
Δ':30 [in Pqf.PropQuantifiers]
Δ0:142 [in Pqf.PropQuantifiers]
Δ0:145 [in Pqf.PropQuantifiers]
Δ0:148 [in Pqf.PropQuantifiers]
Δ0:151 [in Pqf.PropQuantifiers]
Δ:101 [in Pqf.PropQuantifiers]
Δ:115 [in Pqf.PropQuantifiers]
Δ:127 [in Pqf.PropQuantifiers]
Δ:132 [in Pqf.PropQuantifiers]
Δ:138 [in Pqf.PropQuantifiers]
Δ:148 [in Pqf.SequentProps]
Δ:152 [in Pqf.Environments]
Δ:154 [in Pqf.PropQuantifiers]
Δ:161 [in Pqf.Environments]
Δ:161 [in Pqf.SequentProps]
Δ:163 [in Pqf.Environments]
Δ:166 [in Pqf.Environments]
Δ:166 [in Pqf.SequentProps]
Δ:168 [in Pqf.Environments]
Δ:169 [in Pqf.PropQuantifiers]
Δ:17 [in Pqf.PropQuantifiers]
Δ:171 [in Pqf.Environments]
Δ:173 [in Pqf.SequentProps]
Δ:174 [in Pqf.Environments]
Δ:177 [in Pqf.Environments]
Δ:179 [in Pqf.SequentProps]
Δ:181 [in Pqf.PropQuantifiers]
Δ:189 [in Pqf.PropQuantifiers]
Δ:197 [in Pqf.PropQuantifiers]
Δ:197 [in Pqf.Environments]
Δ:198 [in Pqf.Environments]
Δ:2 [in Pqf.PropQuantifiers]
Δ:201 [in Pqf.Environments]
Δ:205 [in Pqf.Environments]
Δ:207 [in Pqf.Environments]
Δ:210 [in Pqf.Environments]
Δ:213 [in Pqf.Environments]
Δ:227 [in Pqf.Environments]
Δ:230 [in Pqf.Environments]
Δ:24 [in Pqf.PropQuantifiers]
Δ:32 [in Pqf.PropQuantifiers]
Δ:32 [in Pqf.Environments]
Δ:46 [in Pqf.PropQuantifiers]
Δ:51 [in Pqf.PropQuantifiers]
Δ:61 [in Pqf.PropQuantifiers]
Δ:71 [in Pqf.PropQuantifiers]
Δ:78 [in Pqf.PropQuantifiers]
Δ:83 [in Pqf.PropQuantifiers]
Δ:85 [in Pqf.PropQuantifiers]
Δ:87 [in Pqf.PropQuantifiers]
Δ:9 [in Pqf.PropQuantifiers]
θ':196 [in Pqf.Environments]
θ:100 [in Pqf.PropQuantifiers]
θ:101 [in Pqf.SequentProps]
θ:102 [in Pqf.PropQuantifiers]
θ:105 [in Pqf.SequentProps]
θ:110 [in Pqf.SequentProps]
θ:111 [in Pqf.PropQuantifiers]
θ:112 [in Pqf.PropQuantifiers]
θ:114 [in Pqf.PropQuantifiers]
θ:120 [in Pqf.SequentProps]
θ:123 [in Pqf.PropQuantifiers]
θ:124 [in Pqf.PropQuantifiers]
θ:124 [in Pqf.SequentProps]
θ:126 [in Pqf.PropQuantifiers]
θ:128 [in Pqf.SequentProps]
θ:13 [in Pqf.Sequents]
θ:130 [in Pqf.PropQuantifiers]
θ:131 [in Pqf.PropQuantifiers]
θ:132 [in Pqf.SequentProps]
θ:133 [in Pqf.PropQuantifiers]
θ:149 [in Pqf.SequentProps]
θ:16 [in Pqf.SequentProps]
θ:163 [in Pqf.SequentProps]
θ:164 [in Pqf.SequentProps]
θ:168 [in Pqf.SequentProps]
θ:170 [in Pqf.SequentProps]
θ:175 [in Pqf.SequentProps]
θ:180 [in Pqf.PropQuantifiers]
θ:181 [in Pqf.SequentProps]
θ:182 [in Pqf.SequentProps]
θ:195 [in Pqf.Environments]
θ:20 [in Pqf.SequentProps]
θ:213 [in Pqf.PropQuantifiers]
θ:22 [in Pqf.PropQuantifiers]
θ:220 [in Pqf.Environments]
θ:23 [in Pqf.Sequents]
θ:23 [in Pqf.SequentProps]
θ:237 [in Pqf.Environments]
θ:238 [in Pqf.Environments]
θ:53 [in Pqf.PropQuantifiers]
θ:57 [in Pqf.SequentProps]
θ:63 [in Pqf.PropQuantifiers]
θ:7 [in Pqf.PropQuantifiers]
θ:70 [in Pqf.SequentProps]
θ:73 [in Pqf.SequentProps]
θ:76 [in Pqf.SequentProps]
θ:83 [in Pqf.SequentProps]
θ:87 [in Pqf.SequentProps]
θ:88 [in Pqf.PropQuantifiers]
θ:91 [in Pqf.SequentProps]
θ:96 [in Pqf.SequentProps]
θ:97 [in Pqf.PropQuantifiers]
θ:98 [in Pqf.PropQuantifiers]
φ':1 [in Pqf.SequentProps]
φ':183 [in Pqf.PropQuantifiers]
φ':191 [in Pqf.PropQuantifiers]
φ0:172 [in Pqf.PropQuantifiers]
φ0:174 [in Pqf.PropQuantifiers]
φ0:176 [in Pqf.PropQuantifiers]
φ0:178 [in Pqf.PropQuantifiers]
φ0:199 [in Pqf.PropQuantifiers]
φ0:200 [in Pqf.PropQuantifiers]
φ0:201 [in Pqf.PropQuantifiers]
φ0:202 [in Pqf.PropQuantifiers]
φ0:203 [in Pqf.PropQuantifiers]
φ0:234 [in Pqf.Environments]
φ1:107 [in Pqf.SequentProps]
φ1:199 [in Pqf.Environments]
φ1:202 [in Pqf.Environments]
φ1:29 [in Pqf.SequentProps]
φ1:32 [in Pqf.Sequents]
φ1:34 [in Pqf.SequentProps]
φ1:37 [in Pqf.Sequents]
φ1:39 [in Pqf.SequentProps]
φ1:42 [in Pqf.Sequents]
φ1:48 [in Pqf.SequentProps]
φ1:67 [in Pqf.SequentProps]
φ1:93 [in Pqf.SequentProps]
φ1:98 [in Pqf.SequentProps]
φ2:108 [in Pqf.SequentProps]
φ2:203 [in Pqf.Environments]
φ2:30 [in Pqf.SequentProps]
φ2:33 [in Pqf.Sequents]
φ2:35 [in Pqf.SequentProps]
φ2:38 [in Pqf.Sequents]
φ2:40 [in Pqf.SequentProps]
φ2:43 [in Pqf.Sequents]
φ2:49 [in Pqf.SequentProps]
φ2:68 [in Pqf.SequentProps]
φ2:94 [in Pqf.SequentProps]
φ2:99 [in Pqf.SequentProps]
φ3:31 [in Pqf.SequentProps]
φ3:34 [in Pqf.Sequents]
φ3:36 [in Pqf.SequentProps]
φ3:39 [in Pqf.Sequents]
φ3:41 [in Pqf.SequentProps]
φ3:44 [in Pqf.Sequents]
φ3:69 [in Pqf.SequentProps]
φ:103 [in Pqf.SequentProps]
φ:104 [in Pqf.Environments]
φ:11 [in Pqf.Sequents]
φ:11 [in Pqf.SequentProps]
φ:111 [in Pqf.Environments]
φ:112 [in Pqf.SequentProps]
φ:115 [in Pqf.SequentProps]
φ:118 [in Pqf.SequentProps]
φ:122 [in Pqf.SequentProps]
φ:126 [in Pqf.SequentProps]
φ:13 [in Pqf.Formulas]
φ:130 [in Pqf.SequentProps]
φ:134 [in Pqf.Environments]
φ:134 [in Pqf.SequentProps]
φ:137 [in Pqf.SequentProps]
φ:14 [in Pqf.SequentProps]
φ:142 [in Pqf.SequentProps]
φ:145 [in Pqf.SequentProps]
φ:15 [in Pqf.Formulas]
φ:15 [in Pqf.Sequents]
φ:150 [in Pqf.SequentProps]
φ:151 [in Pqf.SequentProps]
φ:153 [in Pqf.SequentProps]
φ:155 [in Pqf.Environments]
φ:155 [in Pqf.SequentProps]
φ:157 [in Pqf.SequentProps]
φ:159 [in Pqf.SequentProps]
φ:162 [in Pqf.Environments]
φ:162 [in Pqf.SequentProps]
φ:165 [in Pqf.Environments]
φ:167 [in Pqf.Environments]
φ:167 [in Pqf.SequentProps]
φ:169 [in Pqf.SequentProps]
φ:17 [in Pqf.Formulas]
φ:170 [in Pqf.Environments]
φ:171 [in Pqf.SequentProps]
φ:174 [in Pqf.SequentProps]
φ:175 [in Pqf.Environments]
φ:178 [in Pqf.Environments]
φ:18 [in Pqf.Sequents]
φ:18 [in Pqf.SequentProps]
φ:180 [in Pqf.SequentProps]
φ:182 [in Pqf.PropQuantifiers]
φ:182 [in Pqf.Environments]
φ:186 [in Pqf.Environments]
φ:190 [in Pqf.PropQuantifiers]
φ:200 [in Pqf.Environments]
φ:204 [in Pqf.Environments]
φ:205 [in Pqf.PropQuantifiers]
φ:206 [in Pqf.PropQuantifiers]
φ:206 [in Pqf.Environments]
φ:209 [in Pqf.Environments]
φ:21 [in Pqf.Formulas]
φ:21 [in Pqf.Sequents]
φ:211 [in Pqf.PropQuantifiers]
φ:212 [in Pqf.Environments]
φ:216 [in Pqf.Environments]
φ:218 [in Pqf.Environments]
φ:22 [in Pqf.Formulas]
φ:22 [in Pqf.SequentProps]
φ:223 [in Pqf.Environments]
φ:224 [in Pqf.Environments]
φ:225 [in Pqf.Environments]
φ:25 [in Pqf.Formulas]
φ:25 [in Pqf.Sequents]
φ:26 [in Pqf.SequentProps]
φ:28 [in Pqf.Formulas]
φ:29 [in Pqf.Sequents]
φ:3 [in Pqf.SequentProps]
φ:31 [in Pqf.Formulas]
φ:34 [in Pqf.Formulas]
φ:35 [in Pqf.Environments]
φ:37 [in Pqf.Formulas]
φ:38 [in Pqf.Formulas]
φ:38 [in Pqf.Environments]
φ:39 [in Pqf.Formulas]
φ:4 [in Pqf.Formulas]
φ:41 [in Pqf.Environments]
φ:44 [in Pqf.Environments]
φ:44 [in Pqf.SequentProps]
φ:45 [in Pqf.Environments]
φ:46 [in Pqf.SequentProps]
φ:51 [in Pqf.SequentProps]
φ:53 [in Pqf.SequentProps]
φ:55 [in Pqf.SequentProps]
φ:59 [in Pqf.SequentProps]
φ:6 [in Pqf.Sequents]
φ:6 [in Pqf.SequentProps]
φ:64 [in Pqf.SequentProps]
φ:7 [in Pqf.Formulas]
φ:72 [in Pqf.SequentProps]
φ:79 [in Pqf.SequentProps]
φ:8 [in Pqf.Sequents]
φ:81 [in Pqf.SequentProps]
φ:82 [in Pqf.Environments]
φ:84 [in Pqf.Environments]
φ:84 [in Pqf.SequentProps]
φ:86 [in Pqf.Environments]
φ:89 [in Pqf.Environments]
φ:89 [in Pqf.SequentProps]
φ:9 [in Pqf.SequentProps]
φ:91 [in Pqf.Environments]
φ:93 [in Pqf.Environments]
φ:96 [in Pqf.Environments]
ψ0:114 [in Pqf.Environments]
ψ0:118 [in Pqf.Environments]
ψ0:122 [in Pqf.Environments]
ψ0:127 [in Pqf.Environments]
ψ0:136 [in Pqf.Environments]
ψ0:141 [in Pqf.Environments]
ψ0:146 [in Pqf.Environments]
ψ1:23 [in Pqf.Formulas]
ψ1:26 [in Pqf.Formulas]
ψ1:29 [in Pqf.Formulas]
ψ2:24 [in Pqf.Formulas]
ψ2:27 [in Pqf.Formulas]
ψ2:30 [in Pqf.Formulas]
ψ:100 [in Pqf.SequentProps]
ψ:104 [in Pqf.SequentProps]
ψ:109 [in Pqf.SequentProps]
ψ:113 [in Pqf.Environments]
ψ:113 [in Pqf.SequentProps]
ψ:116 [in Pqf.SequentProps]
ψ:119 [in Pqf.SequentProps]
ψ:12 [in Pqf.Sequents]
ψ:12 [in Pqf.SequentProps]
ψ:123 [in Pqf.SequentProps]
ψ:127 [in Pqf.SequentProps]
ψ:131 [in Pqf.SequentProps]
ψ:135 [in Pqf.SequentProps]
ψ:138 [in Pqf.SequentProps]
ψ:14 [in Pqf.Formulas]
ψ:140 [in Pqf.SequentProps]
ψ:143 [in Pqf.SequentProps]
ψ:146 [in Pqf.SequentProps]
ψ:15 [in Pqf.SequentProps]
ψ:152 [in Pqf.SequentProps]
ψ:154 [in Pqf.SequentProps]
ψ:156 [in Pqf.SequentProps]
ψ:158 [in Pqf.SequentProps]
ψ:16 [in Pqf.Formulas]
ψ:16 [in Pqf.Sequents]
ψ:176 [in Pqf.SequentProps]
ψ:177 [in Pqf.SequentProps]
ψ:179 [in Pqf.Environments]
ψ:18 [in Pqf.Formulas]
ψ:183 [in Pqf.Environments]
ψ:19 [in Pqf.Sequents]
ψ:19 [in Pqf.SequentProps]
ψ:212 [in Pqf.PropQuantifiers]
ψ:217 [in Pqf.Environments]
ψ:219 [in Pqf.Environments]
ψ:22 [in Pqf.Sequents]
ψ:26 [in Pqf.Sequents]
ψ:27 [in Pqf.SequentProps]
ψ:30 [in Pqf.Sequents]
ψ:32 [in Pqf.SequentProps]
ψ:35 [in Pqf.Sequents]
ψ:36 [in Pqf.Formulas]
ψ:36 [in Pqf.Environments]
ψ:37 [in Pqf.SequentProps]
ψ:39 [in Pqf.Environments]
ψ:40 [in Pqf.Formulas]
ψ:40 [in Pqf.Sequents]
ψ:42 [in Pqf.SequentProps]
ψ:45 [in Pqf.Sequents]
ψ:46 [in Pqf.Environments]
ψ:49 [in Pqf.PropQuantifiers]
ψ:50 [in Pqf.PropQuantifiers]
ψ:56 [in Pqf.SequentProps]
ψ:75 [in Pqf.SequentProps]
ψ:82 [in Pqf.SequentProps]
ψ:83 [in Pqf.Environments]
ψ:85 [in Pqf.Environments]
ψ:86 [in Pqf.SequentProps]
ψ:9 [in Pqf.Sequents]
ψ:90 [in Pqf.Environments]
ψ:90 [in Pqf.SequentProps]
ψ:92 [in Pqf.Environments]
ψ:95 [in Pqf.SequentProps]
ϕ':168 [in Pqf.PropQuantifiers]
ϕ0:143 [in Pqf.PropQuantifiers]
ϕ0:146 [in Pqf.PropQuantifiers]
ϕ0:149 [in Pqf.PropQuantifiers]
ϕ0:152 [in Pqf.PropQuantifiers]
ϕ:104 [in Pqf.PropQuantifiers]
ϕ:116 [in Pqf.PropQuantifiers]
ϕ:128 [in Pqf.PropQuantifiers]
ϕ:134 [in Pqf.PropQuantifiers]
ϕ:139 [in Pqf.PropQuantifiers]
ϕ:155 [in Pqf.PropQuantifiers]
ϕ:169 [in Pqf.Environments]
ϕ:170 [in Pqf.PropQuantifiers]
ϕ:176 [in Pqf.Environments]
ϕ:18 [in Pqf.PropQuantifiers]
ϕ:198 [in Pqf.PropQuantifiers]
ϕ:228 [in Pqf.Environments]
ϕ:231 [in Pqf.Environments]
ϕ:3 [in Pqf.PropQuantifiers]
ϕ:33 [in Pqf.PropQuantifiers]
ϕ:52 [in Pqf.PropQuantifiers]
ϕ:62 [in Pqf.PropQuantifiers]
ϕ:72 [in Pqf.PropQuantifiers]
ϕ:79 [in Pqf.PropQuantifiers]
ϕ:84 [in Pqf.PropQuantifiers]
ϕ:86 [in Pqf.PropQuantifiers]
ϕ:90 [in Pqf.PropQuantifiers]



Module Index

E

EnvMS [in Pqf.Environments]
EnvMS.Sid [in Pqf.Environments]
EnvMS.Sid.Dom [in Pqf.Environments]
EnvMS.Sid.Eq [in Pqf.Environments]


M

MO [in Pqf.Environments]



Variable Index

P

Pitts.p [in Pqf.PropQuantifiers]



Library Index

E

Environments


F

Formulas


P

PropQuantifiers


S

SequentProps
Sequents



Lemma Index

A

AndL_rev [in Pqf.SequentProps]
AndR_rev [in Pqf.SequentProps]
A_right [in Pqf.PropQuantifiers]
a_rule_env_spec [in Pqf.PropQuantifiers]
a_rule_form_vars [in Pqf.PropQuantifiers]
a_rule_env_vars [in Pqf.PropQuantifiers]
a_rule_form_cong [in Pqf.PropQuantifiers]
a_rule_env_cong [in Pqf.PropQuantifiers]


C

conjunction_L [in Pqf.SequentProps]
conjunction_R2 [in Pqf.SequentProps]
conjunction_R1 [in Pqf.SequentProps]
contraction [in Pqf.SequentProps]


D

decide_in [in Pqf.Environments]
difference_include [in Pqf.Environments]
difference_singleton [in Pqf.Environments]
diff_not_in [in Pqf.Environments]
disjunction_R [in Pqf.SequentProps]
disjunction_L [in Pqf.SequentProps]


E

EA_vars [in Pqf.PropQuantifiers]
EA_eq [in Pqf.PropQuantifiers]
entail_correct [in Pqf.PropQuantifiers]
EnvMS.diff_mult [in Pqf.Environments]
EnvMS.empty_mult [in Pqf.Environments]
EnvMS.gmultiset_choose_or_empty [in Pqf.Environments]
EnvMS.intersection_mult [in Pqf.Environments]
EnvMS.meq_multeq [in Pqf.Environments]
EnvMS.multeq_meq [in Pqf.Environments]
EnvMS.mult_eqA_compat [in Pqf.Environments]
EnvMS.singleton_mult_notin [in Pqf.Environments]
EnvMS.singleton_mult_in [in Pqf.Environments]
EnvMS.union_mult [in Pqf.Environments]
env_order_equiv_right_compat [in Pqf.Environments]
env_order_add_compat [in Pqf.Environments]
env_order_cancel_right [in Pqf.Environments]
env_order_0 [in Pqf.Environments]
env_order_2 [in Pqf.Environments]
env_order_1 [in Pqf.Environments]
env_equiv_eq [in Pqf.Environments]
env_add_inv' [in Pqf.Environments]
env_add_inv [in Pqf.Environments]
env_add_comm [in Pqf.Environments]
env_in_add [in Pqf.Environments]
env_order_singleton_compat [in Pqf.Environments]
env_order_singleton [in Pqf.Environments]
env_replace [in Pqf.Environments]
equiv_disj_union_compat_r [in Pqf.Environments]
example_multiset [in Pqf.Environments]
exfalso [in Pqf.SequentProps]
E_of_empty [in Pqf.PropQuantifiers]
E_left [in Pqf.PropQuantifiers]
E_irr [in Pqf.PropQuantifiers]
e_rule_vars [in Pqf.PropQuantifiers]
e_rule_cong [in Pqf.PropQuantifiers]


G

generalised_contraction [in Pqf.SequentProps]
generalised_axiom [in Pqf.SequentProps]
generalised_weakeningR [in Pqf.SequentProps]
generalised_weakeningL [in Pqf.SequentProps]
gmultiset_rec [in Pqf.Environments]


H

height_0 [in Pqf.SequentProps]


I

ImpL [in Pqf.SequentProps]
ImpLAnd_rev [in Pqf.SequentProps]
ImpLImp_dup [in Pqf.SequentProps]
ImpLImp_prev [in Pqf.SequentProps]
ImpLOr_rev [in Pqf.SequentProps]
ImpLVar_rev [in Pqf.SequentProps]
ImpR_rev [in Pqf.SequentProps]
imp_cut [in Pqf.SequentProps]
in_difference [in Pqf.Environments]
in_map_ext [in Pqf.Environments]
in_map_empty [in Pqf.Environments]
in_map_in [in Pqf.Environments]
in_in_map [in Pqf.Environments]


M

make_impl_weight2 [in Pqf.Environments]
make_impl_weight [in Pqf.Environments]
make_impl_spec [in Pqf.Environments]
make_disj_spec [in Pqf.Environments]
make_conj_spec [in Pqf.Environments]
make_disj_complete_R [in Pqf.SequentProps]
make_disj_sound_R [in Pqf.SequentProps]
make_conj_complete_R [in Pqf.SequentProps]
make_conj_sound_R [in Pqf.SequentProps]
make_conj_complete_L [in Pqf.SequentProps]
make_conj_sound_L [in Pqf.SequentProps]
make_disj_complete [in Pqf.SequentProps]
make_disj_sound_L [in Pqf.SequentProps]
make_impl_sound_R [in Pqf.SequentProps]
make_impl_complete_R [in Pqf.SequentProps]
make_impl_complete_L2 [in Pqf.SequentProps]
make_impl_complete_L [in Pqf.SequentProps]
make_impl_sound_L2' [in Pqf.SequentProps]
make_impl_sound_L2 [in Pqf.SequentProps]
make_impl_sound_L [in Pqf.SequentProps]


O

occurs_in_make_impl2 [in Pqf.Environments]
occurs_in_make_impl [in Pqf.Environments]
occurs_in_make_disj [in Pqf.Environments]
occurs_in_make_conj [in Pqf.Environments]
OrL_rev [in Pqf.SequentProps]
OrR_idemp [in Pqf.SequentProps]
OrR1Bot_rev [in Pqf.SequentProps]
OrR2Bot_rev [in Pqf.SequentProps]


P

pitts [in Pqf.PropQuantifiers]
pq_correct [in Pqf.PropQuantifiers]
p_contr [in Pqf.SequentProps]


T

TopL_rev [in Pqf.SequentProps]


U

union_difference_R [in Pqf.Environments]
union_difference_L [in Pqf.Environments]


V

variables_disjunction [in Pqf.Environments]
variables_conjunction [in Pqf.Environments]


W

weakening [in Pqf.SequentProps]
weak_ImpL [in Pqf.SequentProps]
weight_pos [in Pqf.Formulas]
wf_pointed_order [in Pqf.Environments]



Constructor Index

A

And [in Pqf.Formulas]
AndL [in Pqf.Sequents]
AndR [in Pqf.Sequents]
Atom [in Pqf.Sequents]


B

Bot [in Pqf.Formulas]


E

ExFalso [in Pqf.Sequents]


I

ImpLAnd [in Pqf.Sequents]
Implies [in Pqf.Formulas]
ImpLImp [in Pqf.Sequents]
ImpLOr [in Pqf.Sequents]
ImpLVar [in Pqf.Sequents]
ImpR [in Pqf.Sequents]


O

Or [in Pqf.Formulas]
OrL [in Pqf.Sequents]
OrR1 [in Pqf.Sequents]
OrR2 [in Pqf.Sequents]


S

SubAnd [in Pqf.Formulas]
SubEq [in Pqf.Formulas]
SubImpl [in Pqf.Formulas]
SubOr [in Pqf.Formulas]


V

Var [in Pqf.Formulas]



Inductive Index

F

form [in Pqf.Formulas]


P

Provable [in Pqf.Sequents]


S

subform [in Pqf.Formulas]



Section Index

C

CountablyManyFormulas [in Pqf.Formulas]


O

Order [in Pqf.Environments]


P

Pitts [in Pqf.PropQuantifiers]
Pitts.Correctness [in Pqf.PropQuantifiers]
Pitts.Correctness.EntailmentCorrect [in Pqf.PropQuantifiers]
Pitts.Correctness.PropQuantCorrect [in Pqf.PropQuantifiers]
Pitts.Correctness.VariablesCorrect [in Pqf.PropQuantifiers]
Pitts.PropQuantDefinition [in Pqf.PropQuantifiers]



Instance Index

A

assoc_meq_union [in Pqf.Environments]


E

env_order_trans [in Pqf.Environments]
equiv_assoc [in Pqf.Environments]


F

fomula_bottom [in Pqf.Formulas]
form_count [in Pqf.Formulas]
form_eq_dec [in Pqf.Formulas]
form_top [in Pqf.Formulas]


P

proper_Provable [in Pqf.Sequents]
proper_disj_union [in Pqf.Environments]
proper_elem_of [in Pqf.Environments]


S

singleton [in Pqf.Environments]
singletonMS [in Pqf.Environments]



Definition Index

A

A [in Pqf.PropQuantifiers]
Af [in Pqf.PropQuantifiers]
A_eq [in Pqf.PropQuantifiers]
a_rule_form [in Pqf.PropQuantifiers]
a_rule_env [in Pqf.PropQuantifiers]


C

conjunction [in Pqf.Environments]


D

disjunction [in Pqf.Environments]


E

E [in Pqf.PropQuantifiers]
EA [in Pqf.PropQuantifiers]
Ef [in Pqf.PropQuantifiers]
env [in Pqf.Environments]
EnvMS.diff [in Pqf.Environments]
EnvMS.empty [in Pqf.Environments]
EnvMS.intersection [in Pqf.Environments]
EnvMS.meq [in Pqf.Environments]
EnvMS.mset_ind_type [in Pqf.Environments]
EnvMS.mult [in Pqf.Environments]
EnvMS.Multiset [in Pqf.Environments]
EnvMS.Sid.Dom.A [in Pqf.Environments]
EnvMS.Sid.eqA_dec [in Pqf.Environments]
EnvMS.singleton [in Pqf.Environments]
EnvMS.union [in Pqf.Environments]
env_order [in Pqf.Environments]
E_eq [in Pqf.PropQuantifiers]
e_rule [in Pqf.PropQuantifiers]


F

form_order [in Pqf.Formulas]
form_to_gen_tree [in Pqf.Formulas]


G

gen_tree_to_form [in Pqf.Formulas]


H

height [in Pqf.SequentProps]


I

in_subset [in Pqf.Environments]
in_map [in Pqf.Environments]
in_map_aux [in Pqf.Environments]
irreducible [in Pqf.Environments]


M

make_impl [in Pqf.Environments]
make_disj [in Pqf.Environments]
make_conj [in Pqf.Environments]


O

occurs_in [in Pqf.Formulas]


P

pointed_env_order [in Pqf.Environments]
pointed_env [in Pqf.Environments]


V

variable [in Pqf.Formulas]
vars_incl [in Pqf.PropQuantifiers]
var_not_in_env [in Pqf.Environments]


W

weight [in Pqf.Formulas]
weight_ind [in Pqf.Formulas]
wf_env_order [in Pqf.Environments]



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 (918 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 (17 entries)
Binder 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 (689 entries)
Module Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (5 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 (1 entry)
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 (5 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 (112 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 (21 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 (3 entries)
Section Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (8 entries)
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 (12 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 (45 entries)