| 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 | (913 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 | (684 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:151 [binder, in Pqf.PropQuantifiers]
d:154 [binder, in Pqf.PropQuantifiers]
d:157 [binder, in Pqf.PropQuantifiers]
d:160 [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:102 [binder, in Pqf.PropQuantifiers]
EA0:114 [binder, in Pqf.PropQuantifiers]
EA0:132 [binder, in Pqf.PropQuantifiers]
EA0:21 [binder, in Pqf.PropQuantifiers]
EA0:36 [binder, in Pqf.PropQuantifiers]
EA0:6 [binder, in Pqf.PropQuantifiers]
EA0:88 [binder, in Pqf.PropQuantifiers]
EA1:55 [binder, in Pqf.PropQuantifiers]
EA1:63 [binder, in Pqf.PropQuantifiers]
EA1:69 [binder, in Pqf.PropQuantifiers]
EA2:56 [binder, in Pqf.PropQuantifiers]
EA2:64 [binder, in Pqf.PropQuantifiers]
EA2:70 [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:152 [binder, in Pqf.PropQuantifiers]
f:153 [binder, in Pqf.Environments]
f:155 [binder, in Pqf.PropQuantifiers]
f:158 [binder, in Pqf.PropQuantifiers]
f:161 [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:108 [binder, in Pqf.PropQuantifiers]
HEA0:120 [binder, in Pqf.PropQuantifiers]
HEA0:94 [binder, in Pqf.PropQuantifiers]
HEA:136 [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]
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:130 [binder, in Pqf.PropQuantifiers]
Hin:137 [binder, in Pqf.Environments]
Hin:142 [binder, in Pqf.Environments]
Hin:147 [binder, in Pqf.Environments]
Hin:179 [binder, in Pqf.PropQuantifiers]
Hin:187 [binder, in Pqf.PropQuantifiers]
Hin:23 [binder, in Pqf.PropQuantifiers]
Hin:54 [binder, in Pqf.PropQuantifiers]
Hin:62 [binder, in Pqf.PropQuantifiers]
Hin:8 [binder, in Pqf.PropQuantifiers]
Hin:84 [binder, in Pqf.PropQuantifiers]
Hin:98 [binder, in Pqf.PropQuantifiers]
Hi:126 [binder, in Pqf.Environments]
Hpe:101 [binder, in Pqf.PropQuantifiers]
Hpe:105 [binder, in Pqf.PropQuantifiers]
Hpe:113 [binder, in Pqf.PropQuantifiers]
Hpe:117 [binder, in Pqf.PropQuantifiers]
Hpe:135 [binder, in Pqf.PropQuantifiers]
Hpe:139 [binder, in Pqf.PropQuantifiers]
Hpe:142 [binder, in Pqf.PropQuantifiers]
Hpe:145 [binder, in Pqf.PropQuantifiers]
Hpe:148 [binder, in Pqf.PropQuantifiers]
Hpe:20 [binder, in Pqf.PropQuantifiers]
Hpe:35 [binder, in Pqf.PropQuantifiers]
Hpe:5 [binder, in Pqf.PropQuantifiers]
Hpe:58 [binder, in Pqf.PropQuantifiers]
Hpe:66 [binder, in Pqf.PropQuantifiers]
Hpe:72 [binder, in Pqf.PropQuantifiers]
Hpe:87 [binder, in Pqf.PropQuantifiers]
Hpe:91 [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:202 [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:100 [binder, in Pqf.PropQuantifiers]
pe:104 [binder, in Pqf.PropQuantifiers]
pe:112 [binder, in Pqf.PropQuantifiers]
pe:116 [binder, in Pqf.PropQuantifiers]
pe:131 [binder, in Pqf.PropQuantifiers]
pe:180 [binder, in Pqf.PropQuantifiers]
pe:181 [binder, in Pqf.PropQuantifiers]
pe:182 [binder, in Pqf.PropQuantifiers]
pe:188 [binder, in Pqf.PropQuantifiers]
pe:189 [binder, in Pqf.PropQuantifiers]
pe:19 [binder, in Pqf.PropQuantifiers]
pe:190 [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:57 [binder, in Pqf.PropQuantifiers]
pe:65 [binder, in Pqf.PropQuantifiers]
pe:71 [binder, in Pqf.PropQuantifiers]
pe:75 [binder, in Pqf.PropQuantifiers]
pe:76 [binder, in Pqf.PropQuantifiers]
pe:77 [binder, in Pqf.PropQuantifiers]
pe:86 [binder, in Pqf.PropQuantifiers]
pe:90 [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:199 [binder, in Pqf.PropQuantifiers]
p:204 [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:205 [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:103 [binder, in Pqf.PropQuantifiers]
x:11 [binder, in Pqf.Environments]
x:115 [binder, in Pqf.PropQuantifiers]
x:124 [binder, in Pqf.PropQuantifiers]
x:14 [binder, in Pqf.Environments]
x:153 [binder, in Pqf.PropQuantifiers]
x:156 [binder, in Pqf.PropQuantifiers]
x:159 [binder, in Pqf.PropQuantifiers]
x:162 [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:203 [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:89 [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:166 [binder, in Pqf.PropQuantifiers]
Γ0:168 [binder, in Pqf.PropQuantifiers]
Γ0:170 [binder, in Pqf.PropQuantifiers]
Γ0:172 [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]
Γ:174 [binder, in Pqf.PropQuantifiers]
Γ:178 [binder, in Pqf.SequentProps]
Γ:180 [binder, in Pqf.Environments]
Γ:183 [binder, in Pqf.PropQuantifiers]
Γ:184 [binder, in Pqf.Environments]
Γ:187 [binder, in Pqf.Environments]
Γ:191 [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:137 [binder, in Pqf.PropQuantifiers]
Δ0:140 [binder, in Pqf.PropQuantifiers]
Δ0:143 [binder, in Pqf.PropQuantifiers]
Δ0:146 [binder, in Pqf.PropQuantifiers]
Δ:110 [binder, in Pqf.PropQuantifiers]
Δ:122 [binder, in Pqf.PropQuantifiers]
Δ:127 [binder, in Pqf.PropQuantifiers]
Δ:133 [binder, in Pqf.PropQuantifiers]
Δ:148 [binder, in Pqf.SequentProps]
Δ:149 [binder, in Pqf.PropQuantifiers]
Δ:152 [binder, in Pqf.Environments]
Δ:161 [binder, in Pqf.Environments]
Δ:161 [binder, in Pqf.SequentProps]
Δ:163 [binder, in Pqf.Environments]
Δ:164 [binder, in Pqf.PropQuantifiers]
Δ:166 [binder, in Pqf.Environments]
Δ:166 [binder, in Pqf.SequentProps]
Δ:168 [binder, in Pqf.Environments]
Δ:17 [binder, in Pqf.PropQuantifiers]
Δ:171 [binder, in Pqf.Environments]
Δ:173 [binder, in Pqf.SequentProps]
Δ:174 [binder, in Pqf.Environments]
Δ:176 [binder, in Pqf.PropQuantifiers]
Δ:177 [binder, in Pqf.Environments]
Δ:179 [binder, in Pqf.SequentProps]
Δ:184 [binder, in Pqf.PropQuantifiers]
Δ:192 [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]
Δ:59 [binder, in Pqf.PropQuantifiers]
Δ:67 [binder, in Pqf.PropQuantifiers]
Δ:73 [binder, in Pqf.PropQuantifiers]
Δ:78 [binder, in Pqf.PropQuantifiers]
Δ:80 [binder, in Pqf.PropQuantifiers]
Δ:82 [binder, in Pqf.PropQuantifiers]
Δ:9 [binder, in Pqf.PropQuantifiers]
Δ:96 [binder, in Pqf.PropQuantifiers]
θ':196 [binder, in Pqf.Environments]
θ:101 [binder, in Pqf.SequentProps]
θ:105 [binder, in Pqf.SequentProps]
θ:106 [binder, in Pqf.PropQuantifiers]
θ:107 [binder, in Pqf.PropQuantifiers]
θ:109 [binder, in Pqf.PropQuantifiers]
θ:110 [binder, in Pqf.SequentProps]
θ:118 [binder, in Pqf.PropQuantifiers]
θ:119 [binder, in Pqf.PropQuantifiers]
θ:120 [binder, in Pqf.SequentProps]
θ:121 [binder, in Pqf.PropQuantifiers]
θ:124 [binder, in Pqf.SequentProps]
θ:125 [binder, in Pqf.PropQuantifiers]
θ:126 [binder, in Pqf.PropQuantifiers]
θ:128 [binder, in Pqf.PropQuantifiers]
θ:128 [binder, in Pqf.SequentProps]
θ:13 [binder, in Pqf.Sequents]
θ:132 [binder, in Pqf.SequentProps]
θ: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.PropQuantifiers]
θ:175 [binder, in Pqf.SequentProps]
θ:181 [binder, in Pqf.SequentProps]
θ:182 [binder, in Pqf.SequentProps]
θ:195 [binder, in Pqf.Environments]
θ:20 [binder, in Pqf.SequentProps]
θ:208 [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]
θ:61 [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.PropQuantifiers]
θ:83 [binder, in Pqf.SequentProps]
θ:87 [binder, in Pqf.SequentProps]
θ:91 [binder, in Pqf.SequentProps]
θ:92 [binder, in Pqf.PropQuantifiers]
θ:93 [binder, in Pqf.PropQuantifiers]
θ:95 [binder, in Pqf.PropQuantifiers]
θ:96 [binder, in Pqf.SequentProps]
θ:97 [binder, in Pqf.PropQuantifiers]
φ':1 [binder, in Pqf.SequentProps]
φ':178 [binder, in Pqf.PropQuantifiers]
φ':186 [binder, in Pqf.PropQuantifiers]
φ0:167 [binder, in Pqf.PropQuantifiers]
φ0:169 [binder, in Pqf.PropQuantifiers]
φ0:171 [binder, in Pqf.PropQuantifiers]
φ0:173 [binder, in Pqf.PropQuantifiers]
φ0:194 [binder, in Pqf.PropQuantifiers]
φ0:195 [binder, in Pqf.PropQuantifiers]
φ0:196 [binder, in Pqf.PropQuantifiers]
φ0:197 [binder, in Pqf.PropQuantifiers]
φ0:198 [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]
φ:177 [binder, in Pqf.PropQuantifiers]
φ:178 [binder, in Pqf.Environments]
φ:18 [binder, in Pqf.Sequents]
φ:18 [binder, in Pqf.SequentProps]
φ:180 [binder, in Pqf.SequentProps]
φ:182 [binder, in Pqf.Environments]
φ:185 [binder, in Pqf.PropQuantifiers]
φ:186 [binder, in Pqf.Environments]
φ:200 [binder, in Pqf.PropQuantifiers]
φ:200 [binder, in Pqf.Environments]
φ:201 [binder, in Pqf.PropQuantifiers]
φ:204 [binder, in Pqf.Environments]
φ: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]
φ: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]
ψ:207 [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]
ϕ':163 [binder, in Pqf.PropQuantifiers]
ϕ0:138 [binder, in Pqf.PropQuantifiers]
ϕ0:141 [binder, in Pqf.PropQuantifiers]
ϕ0:144 [binder, in Pqf.PropQuantifiers]
ϕ0:147 [binder, in Pqf.PropQuantifiers]
ϕ:111 [binder, in Pqf.PropQuantifiers]
ϕ:123 [binder, in Pqf.PropQuantifiers]
ϕ:129 [binder, in Pqf.PropQuantifiers]
ϕ:134 [binder, in Pqf.PropQuantifiers]
ϕ:150 [binder, in Pqf.PropQuantifiers]
ϕ:165 [binder, in Pqf.PropQuantifiers]
ϕ:169 [binder, in Pqf.Environments]
ϕ:176 [binder, in Pqf.Environments]
ϕ:18 [binder, in Pqf.PropQuantifiers]
ϕ:193 [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]
ϕ:60 [binder, in Pqf.PropQuantifiers]
ϕ:68 [binder, in Pqf.PropQuantifiers]
ϕ:74 [binder, in Pqf.PropQuantifiers]
ϕ:79 [binder, in Pqf.PropQuantifiers]
ϕ:81 [binder, in Pqf.PropQuantifiers]
ϕ:85 [binder, in Pqf.PropQuantifiers]
ϕ:99 [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:151 [in Pqf.PropQuantifiers]d:154 [in Pqf.PropQuantifiers]
d:157 [in Pqf.PropQuantifiers]
d:160 [in Pqf.PropQuantifiers]
E
EA0:102 [in Pqf.PropQuantifiers]EA0:114 [in Pqf.PropQuantifiers]
EA0:132 [in Pqf.PropQuantifiers]
EA0:21 [in Pqf.PropQuantifiers]
EA0:36 [in Pqf.PropQuantifiers]
EA0:6 [in Pqf.PropQuantifiers]
EA0:88 [in Pqf.PropQuantifiers]
EA1:55 [in Pqf.PropQuantifiers]
EA1:63 [in Pqf.PropQuantifiers]
EA1:69 [in Pqf.PropQuantifiers]
EA2:56 [in Pqf.PropQuantifiers]
EA2:64 [in Pqf.PropQuantifiers]
EA2:70 [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:152 [in Pqf.PropQuantifiers]
f:153 [in Pqf.Environments]
f:155 [in Pqf.PropQuantifiers]
f:158 [in Pqf.PropQuantifiers]
f:161 [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:108 [in Pqf.PropQuantifiers]
HEA0:120 [in Pqf.PropQuantifiers]
HEA0:94 [in Pqf.PropQuantifiers]
HEA:136 [in Pqf.PropQuantifiers]
Hin':138 [in Pqf.Environments]
Hin':143 [in Pqf.Environments]
Hin':148 [in Pqf.Environments]
Hin:115 [in Pqf.Environments]
Hin:119 [in Pqf.Environments]
Hin:123 [in Pqf.Environments]
Hin:128 [in Pqf.Environments]
Hin:130 [in Pqf.PropQuantifiers]
Hin:137 [in Pqf.Environments]
Hin:142 [in Pqf.Environments]
Hin:147 [in Pqf.Environments]
Hin:179 [in Pqf.PropQuantifiers]
Hin:187 [in Pqf.PropQuantifiers]
Hin:23 [in Pqf.PropQuantifiers]
Hin:54 [in Pqf.PropQuantifiers]
Hin:62 [in Pqf.PropQuantifiers]
Hin:8 [in Pqf.PropQuantifiers]
Hin:84 [in Pqf.PropQuantifiers]
Hin:98 [in Pqf.PropQuantifiers]
Hi:126 [in Pqf.Environments]
Hpe:101 [in Pqf.PropQuantifiers]
Hpe:105 [in Pqf.PropQuantifiers]
Hpe:113 [in Pqf.PropQuantifiers]
Hpe:117 [in Pqf.PropQuantifiers]
Hpe:135 [in Pqf.PropQuantifiers]
Hpe:139 [in Pqf.PropQuantifiers]
Hpe:142 [in Pqf.PropQuantifiers]
Hpe:145 [in Pqf.PropQuantifiers]
Hpe:148 [in Pqf.PropQuantifiers]
Hpe:20 [in Pqf.PropQuantifiers]
Hpe:35 [in Pqf.PropQuantifiers]
Hpe:5 [in Pqf.PropQuantifiers]
Hpe:58 [in Pqf.PropQuantifiers]
Hpe:66 [in Pqf.PropQuantifiers]
Hpe:72 [in Pqf.PropQuantifiers]
Hpe:87 [in Pqf.PropQuantifiers]
Hpe:91 [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:202 [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:100 [in Pqf.PropQuantifiers]
pe:104 [in Pqf.PropQuantifiers]
pe:112 [in Pqf.PropQuantifiers]
pe:116 [in Pqf.PropQuantifiers]
pe:131 [in Pqf.PropQuantifiers]
pe:180 [in Pqf.PropQuantifiers]
pe:181 [in Pqf.PropQuantifiers]
pe:182 [in Pqf.PropQuantifiers]
pe:188 [in Pqf.PropQuantifiers]
pe:189 [in Pqf.PropQuantifiers]
pe:19 [in Pqf.PropQuantifiers]
pe:190 [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:57 [in Pqf.PropQuantifiers]
pe:65 [in Pqf.PropQuantifiers]
pe:71 [in Pqf.PropQuantifiers]
pe:75 [in Pqf.PropQuantifiers]
pe:76 [in Pqf.PropQuantifiers]
pe:77 [in Pqf.PropQuantifiers]
pe:86 [in Pqf.PropQuantifiers]
pe:90 [in Pqf.PropQuantifiers]
P:189 [in Pqf.Environments]
p:199 [in Pqf.PropQuantifiers]
p:204 [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:205 [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:103 [in Pqf.PropQuantifiers]
x:11 [in Pqf.Environments]
x:115 [in Pqf.PropQuantifiers]
x:124 [in Pqf.PropQuantifiers]
x:14 [in Pqf.Environments]
x:153 [in Pqf.PropQuantifiers]
x:156 [in Pqf.PropQuantifiers]
x:159 [in Pqf.PropQuantifiers]
x:162 [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:203 [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:89 [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:166 [in Pqf.PropQuantifiers]
Γ0:168 [in Pqf.PropQuantifiers]
Γ0:170 [in Pqf.PropQuantifiers]
Γ0:172 [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]
Γ:174 [in Pqf.PropQuantifiers]
Γ:178 [in Pqf.SequentProps]
Γ:180 [in Pqf.Environments]
Γ:183 [in Pqf.PropQuantifiers]
Γ:184 [in Pqf.Environments]
Γ:187 [in Pqf.Environments]
Γ:191 [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:137 [in Pqf.PropQuantifiers]
Δ0:140 [in Pqf.PropQuantifiers]
Δ0:143 [in Pqf.PropQuantifiers]
Δ0:146 [in Pqf.PropQuantifiers]
Δ:110 [in Pqf.PropQuantifiers]
Δ:122 [in Pqf.PropQuantifiers]
Δ:127 [in Pqf.PropQuantifiers]
Δ:133 [in Pqf.PropQuantifiers]
Δ:148 [in Pqf.SequentProps]
Δ:149 [in Pqf.PropQuantifiers]
Δ:152 [in Pqf.Environments]
Δ:161 [in Pqf.Environments]
Δ:161 [in Pqf.SequentProps]
Δ:163 [in Pqf.Environments]
Δ:164 [in Pqf.PropQuantifiers]
Δ:166 [in Pqf.Environments]
Δ:166 [in Pqf.SequentProps]
Δ:168 [in Pqf.Environments]
Δ:17 [in Pqf.PropQuantifiers]
Δ:171 [in Pqf.Environments]
Δ:173 [in Pqf.SequentProps]
Δ:174 [in Pqf.Environments]
Δ:176 [in Pqf.PropQuantifiers]
Δ:177 [in Pqf.Environments]
Δ:179 [in Pqf.SequentProps]
Δ:184 [in Pqf.PropQuantifiers]
Δ:192 [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]
Δ:59 [in Pqf.PropQuantifiers]
Δ:67 [in Pqf.PropQuantifiers]
Δ:73 [in Pqf.PropQuantifiers]
Δ:78 [in Pqf.PropQuantifiers]
Δ:80 [in Pqf.PropQuantifiers]
Δ:82 [in Pqf.PropQuantifiers]
Δ:9 [in Pqf.PropQuantifiers]
Δ:96 [in Pqf.PropQuantifiers]
θ':196 [in Pqf.Environments]
θ:101 [in Pqf.SequentProps]
θ:105 [in Pqf.SequentProps]
θ:106 [in Pqf.PropQuantifiers]
θ:107 [in Pqf.PropQuantifiers]
θ:109 [in Pqf.PropQuantifiers]
θ:110 [in Pqf.SequentProps]
θ:118 [in Pqf.PropQuantifiers]
θ:119 [in Pqf.PropQuantifiers]
θ:120 [in Pqf.SequentProps]
θ:121 [in Pqf.PropQuantifiers]
θ:124 [in Pqf.SequentProps]
θ:125 [in Pqf.PropQuantifiers]
θ:126 [in Pqf.PropQuantifiers]
θ:128 [in Pqf.PropQuantifiers]
θ:128 [in Pqf.SequentProps]
θ:13 [in Pqf.Sequents]
θ:132 [in Pqf.SequentProps]
θ: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.PropQuantifiers]
θ:175 [in Pqf.SequentProps]
θ:181 [in Pqf.SequentProps]
θ:182 [in Pqf.SequentProps]
θ:195 [in Pqf.Environments]
θ:20 [in Pqf.SequentProps]
θ:208 [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]
θ:61 [in Pqf.PropQuantifiers]
θ:7 [in Pqf.PropQuantifiers]
θ:70 [in Pqf.SequentProps]
θ:73 [in Pqf.SequentProps]
θ:76 [in Pqf.SequentProps]
θ:83 [in Pqf.PropQuantifiers]
θ:83 [in Pqf.SequentProps]
θ:87 [in Pqf.SequentProps]
θ:91 [in Pqf.SequentProps]
θ:92 [in Pqf.PropQuantifiers]
θ:93 [in Pqf.PropQuantifiers]
θ:95 [in Pqf.PropQuantifiers]
θ:96 [in Pqf.SequentProps]
θ:97 [in Pqf.PropQuantifiers]
φ':1 [in Pqf.SequentProps]
φ':178 [in Pqf.PropQuantifiers]
φ':186 [in Pqf.PropQuantifiers]
φ0:167 [in Pqf.PropQuantifiers]
φ0:169 [in Pqf.PropQuantifiers]
φ0:171 [in Pqf.PropQuantifiers]
φ0:173 [in Pqf.PropQuantifiers]
φ0:194 [in Pqf.PropQuantifiers]
φ0:195 [in Pqf.PropQuantifiers]
φ0:196 [in Pqf.PropQuantifiers]
φ0:197 [in Pqf.PropQuantifiers]
φ0:198 [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]
φ:177 [in Pqf.PropQuantifiers]
φ:178 [in Pqf.Environments]
φ:18 [in Pqf.Sequents]
φ:18 [in Pqf.SequentProps]
φ:180 [in Pqf.SequentProps]
φ:182 [in Pqf.Environments]
φ:185 [in Pqf.PropQuantifiers]
φ:186 [in Pqf.Environments]
φ:200 [in Pqf.PropQuantifiers]
φ:200 [in Pqf.Environments]
φ:201 [in Pqf.PropQuantifiers]
φ:204 [in Pqf.Environments]
φ:206 [in Pqf.PropQuantifiers]
φ:206 [in Pqf.Environments]
φ:209 [in Pqf.Environments]
φ:21 [in Pqf.Formulas]
φ:21 [in Pqf.Sequents]
φ: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]
ψ:207 [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]
ϕ':163 [in Pqf.PropQuantifiers]
ϕ0:138 [in Pqf.PropQuantifiers]
ϕ0:141 [in Pqf.PropQuantifiers]
ϕ0:144 [in Pqf.PropQuantifiers]
ϕ0:147 [in Pqf.PropQuantifiers]
ϕ:111 [in Pqf.PropQuantifiers]
ϕ:123 [in Pqf.PropQuantifiers]
ϕ:129 [in Pqf.PropQuantifiers]
ϕ:134 [in Pqf.PropQuantifiers]
ϕ:150 [in Pqf.PropQuantifiers]
ϕ:165 [in Pqf.PropQuantifiers]
ϕ:169 [in Pqf.Environments]
ϕ:176 [in Pqf.Environments]
ϕ:18 [in Pqf.PropQuantifiers]
ϕ:193 [in Pqf.PropQuantifiers]
ϕ:228 [in Pqf.Environments]
ϕ:231 [in Pqf.Environments]
ϕ:3 [in Pqf.PropQuantifiers]
ϕ:33 [in Pqf.PropQuantifiers]
ϕ:52 [in Pqf.PropQuantifiers]
ϕ:60 [in Pqf.PropQuantifiers]
ϕ:68 [in Pqf.PropQuantifiers]
ϕ:74 [in Pqf.PropQuantifiers]
ϕ:79 [in Pqf.PropQuantifiers]
ϕ:81 [in Pqf.PropQuantifiers]
ϕ:85 [in Pqf.PropQuantifiers]
ϕ:99 [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
EnvironmentsF
FormulasP
PropQuantifiersS
SequentPropsSequents
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 | (913 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 | (684 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) |