| 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 | (873 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 | (89 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (15 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 | (406 entries) |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1 entry) |
| 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 | (41 entries) |
| Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (72 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 | (10 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 | (13 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 | (36 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 | (176 entries) |
| Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (14 entries) |
Global Index
A
_ @⨂ _ [notation, in ImpAlg.TensorAlgebras]λ⨂ _ [notation, in ImpAlg.TensorAlgebras]
¬ _ [notation, in ImpAlg.TensorAlgebras]
About_TensorAlg [section, in ImpAlg.TensorAlgebras]
About_TensorStruct [section, in ImpAlg.TensorAlgebras]
_ + _ [notation, in ImpAlg.ParAlgebras]
_ ⊢ _ [notation, in ImpAlg.ParAlgebras]
About_ParAlg [section, in ImpAlg.ParAlgebras]
abs [definition, in ImpAlg.ImplicativeStructures]
absurd [lemma, in ImpAlg.ParAlgebras]
absurd_aux [lemma, in ImpAlg.ParAlgebras]
absurd_aux_ter [lemma, in ImpAlg.ParAlgebras]
abs_mon [lemma, in ImpAlg.ImplicativeStructures]
adequacy [lemma, in ImpAlg.Adequacy]
Adequacy [section, in ImpAlg.Adequacy]
Adequacy [library]
adequacy_empty [lemma, in ImpAlg.Adequacy]
λ- _ (ia_scope) [notation, in ImpAlg.Adequacy]
_ @ _ (ia_scope) [notation, in ImpAlg.Adequacy]
_ ^t _ [notation, in ImpAlg.Adequacy]
_ ^tc _ [notation, in ImpAlg.Adequacy]
_ ^t^ _ [notation, in ImpAlg.Adequacy]
_ ^v _ [notation, in ImpAlg.Adequacy]
_ ^c _ [notation, in ImpAlg.Adequacy]
_ ^^ _ [notation, in ImpAlg.Adequacy]
{ _ ~t> _ } _ [notation, in ImpAlg.Adequacy]
{ _ ~> _ } _ [notation, in ImpAlg.Adequacy]
adjunction [lemma, in ImpAlg.ImplicativeStructures]
antiapp [definition, in ImpAlg.TensorAlgebras]
anti_mon [definition, in ImpAlg.Lattices]
app [definition, in ImpAlg.ImplicativeStructures]
app_CHA [lemma, in ImpAlg.HeytingAlgebras]
app_closed [lemma, in ImpAlg.ImplicativeAlgebras]
app_CBA [lemma, in ImpAlg.BooleanAlgebras]
app_closure [definition, in ImpAlg.ImplicativeStructures]
app_min [lemma, in ImpAlg.ImplicativeStructures]
app_eta [lemma, in ImpAlg.ImplicativeStructures]
app_beta [lemma, in ImpAlg.ImplicativeStructures]
app_mon [lemma, in ImpAlg.ImplicativeStructures]
app_mon_r [lemma, in ImpAlg.ImplicativeStructures]
app_mon_l [lemma, in ImpAlg.ImplicativeStructures]
app_closed [lemma, in ImpAlg.ParAlgebras]
arrow [projection, in ImpAlg.ImplicativeStructures]
arrowtop [definition, in ImpAlg.Dummies]
arrow_tsep_psep [lemma, in ImpAlg.TensorAlgebras]
arrow_entails_mon [lemma, in ImpAlg.ImplicativeAlgebras]
arrow_entails_mon_l [lemma, in ImpAlg.ImplicativeAlgebras]
arrow_entails_mon_r [lemma, in ImpAlg.ImplicativeAlgebras]
arrow_r [definition, in ImpAlg.Dummies]
arrow_bot [lemma, in ImpAlg.ImplicativeStructures]
arrow_prenex [lemma, in ImpAlg.ImplicativeStructures]
arrow_mon [lemma, in ImpAlg.ImplicativeStructures]
arrow_meet [projection, in ImpAlg.ImplicativeStructures]
arrow_mon_r [projection, in ImpAlg.ImplicativeStructures]
arrow_mon_l [projection, in ImpAlg.ImplicativeStructures]
arrow_set_Proper [instance, in ImpAlg.ImplicativeStructures]
arrow_set [definition, in ImpAlg.ImplicativeStructures]
arrow_set_r [definition, in ImpAlg.ImplicativeStructures]
arrow_set_l [definition, in ImpAlg.ImplicativeStructures]
arrow_precomp_par_assoc [lemma, in ImpAlg.ParAlgebras]
arrow_pneg [lemma, in ImpAlg.ParAlgebras]
arrow_swap_psep [lemma, in ImpAlg.ParAlgebras]
arrow_meet_r_aux [lemma, in ImpAlg.ParAlgebras]
arrow_meet_r [lemma, in ImpAlg.ParAlgebras]
B
B [definition, in ImpAlg.Combinators]BA_TS5 [lemma, in ImpAlg.BooleanAlgebras]
BA_TS4 [lemma, in ImpAlg.BooleanAlgebras]
BA_TS3 [lemma, in ImpAlg.BooleanAlgebras]
BA_TS2 [lemma, in ImpAlg.BooleanAlgebras]
BA_TS1 [lemma, in ImpAlg.BooleanAlgebras]
BA_PS5 [lemma, in ImpAlg.BooleanAlgebras]
BA_PS4 [lemma, in ImpAlg.BooleanAlgebras]
BA_PS3 [lemma, in ImpAlg.BooleanAlgebras]
BA_PS2 [lemma, in ImpAlg.BooleanAlgebras]
BA_PS1 [lemma, in ImpAlg.BooleanAlgebras]
BA_cc [lemma, in ImpAlg.BooleanAlgebras]
BA_S [lemma, in ImpAlg.BooleanAlgebras]
BA_K [lemma, in ImpAlg.BooleanAlgebras]
BA_HA [instance, in ImpAlg.BooleanAlgebras]
betarule [lemma, in ImpAlg.ImplicativeStructures]
beta_red [lemma, in ImpAlg.ImplicativeStructures]
BooleanAlgebra [record, in ImpAlg.BooleanAlgebras]
BooleanAlgebras [library]
bot [projection, in ImpAlg.Lattices]
bot_min [projection, in ImpAlg.Lattices]
bot_meet [lemma, in ImpAlg.BooleanAlgebras]
BoundedLattice [record, in ImpAlg.Lattices]
box [definition, in ImpAlg.LTensor]
box [definition, in ImpAlg.LPar]
by_refl [lemma, in ImpAlg.Lattices]
C
case [definition, in ImpAlg.ImplicativeAlgebras]CBA_TA [instance, in ImpAlg.BooleanAlgebras]
CBA_TS [instance, in ImpAlg.BooleanAlgebras]
CBA_PA [instance, in ImpAlg.BooleanAlgebras]
CBA_PS [instance, in ImpAlg.BooleanAlgebras]
CBA_IA [instance, in ImpAlg.BooleanAlgebras]
CBA_IS [instance, in ImpAlg.BooleanAlgebras]
CBA_CHA [instance, in ImpAlg.BooleanAlgebras]
CBL [instance, in ImpAlg.Lattices]
cc [definition, in ImpAlg.Adequacy]
cc_polymorph [lemma, in ImpAlg.Lambda]
CHA_IS [instance, in ImpAlg.HeytingAlgebras]
closed [definition, in ImpAlg.Combinators]
closed_typ [definition, in ImpAlg.Combinators]
closed_typ [definition, in ImpAlg.ImplicativeAlgebras]
codom [definition, in ImpAlg.Combinators]
codom [definition, in ImpAlg.ImplicativeAlgebras]
codom [definition, in ImpAlg.Lambda]
codom_concat [lemma, in ImpAlg.Lambda]
codom_push [lemma, in ImpAlg.Lambda]
codom_single [lemma, in ImpAlg.Lambda]
codom_empty [lemma, in ImpAlg.Lambda]
combinator [inductive, in ImpAlg.Combinators]
combinatorLambda [lemma, in ImpAlg.Combinators]
Combinators [section, in ImpAlg.Combinators]
Combinators [library]
combinatorSK [lemma, in ImpAlg.Combinators]
$ _ [notation, in ImpAlg.Combinators]
[ _ ] _ [notation, in ImpAlg.Combinators]
λ+ _ [notation, in ImpAlg.Combinators]
combinator_trm_translated [lemma, in ImpAlg.Combinators]
combinator_translated [lemma, in ImpAlg.Combinators]
comb_app [constructor, in ImpAlg.Combinators]
comb_Id [constructor, in ImpAlg.Combinators]
comb_K [constructor, in ImpAlg.Combinators]
comb_S [constructor, in ImpAlg.Combinators]
compat_append [definition, in ImpAlg.Lambda]
CompleteBooleanAlgebra [record, in ImpAlg.BooleanAlgebras]
CompleteHeytingAlgebra [record, in ImpAlg.HeytingAlgebras]
CompleteLattice [record, in ImpAlg.Lattices]
consistent [projection, in ImpAlg.Lattices]
contraposition_r [lemma, in ImpAlg.ImplicativeAlgebras]
contraposition_l [lemma, in ImpAlg.ImplicativeAlgebras]
cord [definition, in ImpAlg.LTensor]
cord [definition, in ImpAlg.LPar]
cord_join [lemma, in ImpAlg.LTensor]
cord_meet [lemma, in ImpAlg.LTensor]
cord_subset [lemma, in ImpAlg.LTensor]
cord_mon [lemma, in ImpAlg.LTensor]
cord_preOrder [instance, in ImpAlg.LTensor]
cord_Transitive [instance, in ImpAlg.LTensor]
cord_Reflexive [instance, in ImpAlg.LTensor]
cord_join [lemma, in ImpAlg.LPar]
cord_meet [lemma, in ImpAlg.LPar]
cord_subset [lemma, in ImpAlg.LPar]
cord_mon [lemma, in ImpAlg.LPar]
cord_preOrder [instance, in ImpAlg.LPar]
cord_Transitive [instance, in ImpAlg.LPar]
cord_Reflexive [instance, in ImpAlg.LPar]
C6_p [lemma, in ImpAlg.ParAlgebras]
C7 [lemma, in ImpAlg.ParAlgebras]
D
Definitions [section, in ImpAlg.Lambda]_ |= _ : _ [notation, in ImpAlg.Lambda]
_ ^t _ [notation, in ImpAlg.Lambda]
_ ^tc _ [notation, in ImpAlg.Lambda]
_ ^t^ _ [notation, in ImpAlg.Lambda]
_ ^v _ [notation, in ImpAlg.Lambda]
_ ^c _ [notation, in ImpAlg.Lambda]
_ ^^ _ [notation, in ImpAlg.Lambda]
{ _ ~t> _ } _ [notation, in ImpAlg.Lambda]
{ _ ~> _ } _ [notation, in ImpAlg.Lambda]
dn [lemma, in ImpAlg.ImplicativeAlgebras]
dne [lemma, in ImpAlg.ImplicativeAlgebras]
dne [lemma, in ImpAlg.ParAlgebras]
dne_entails [lemma, in ImpAlg.ParAlgebras]
dni [lemma, in ImpAlg.ImplicativeAlgebras]
dni [lemma, in ImpAlg.ParAlgebras]
dni_entails [lemma, in ImpAlg.ParAlgebras]
double_meet_elim [lemma, in ImpAlg.Lattices]
double_meet [lemma, in ImpAlg.Lattices]
double_neg [lemma, in ImpAlg.BooleanAlgebras]
Dummies [library]
Dummy [section, in ImpAlg.Dummies]
dummy_tensor [instance, in ImpAlg.Dummies]
dummy_par [instance, in ImpAlg.Dummies]
dummy_top_abs [lemma, in ImpAlg.Dummies]
dummy_top_app [lemma, in ImpAlg.Dummies]
dummy_imp_top [instance, in ImpAlg.Dummies]
dummy_imp_r [instance, in ImpAlg.Dummies]
E
Easy [definition, in ImpAlg.Combinators]emptyset [definition, in ImpAlg.Ens]
empty_fv_typ_subst [lemma, in ImpAlg.Adequacy]
empty_fv_trm_subst [lemma, in ImpAlg.Adequacy]
Ens [definition, in ImpAlg.Ens]
Ens [library]
entails [definition, in ImpAlg.ImplicativeAlgebras]
entails [definition, in ImpAlg.ParAlgebras]
entails_half_adj [lemma, in ImpAlg.ImplicativeAlgebras]
entails_trans [lemma, in ImpAlg.ImplicativeAlgebras]
entails_refl [lemma, in ImpAlg.ImplicativeAlgebras]
env [definition, in ImpAlg.Combinators]
env [definition, in ImpAlg.ImplicativeAlgebras]
env [definition, in ImpAlg.Lambda]
equivalence [definition, in ImpAlg.ImplicativeAlgebras]
equivalence [definition, in ImpAlg.ParAlgebras]
equiv_sep [lemma, in ImpAlg.ImplicativeAlgebras]
eta [definition, in ImpAlg.TensorAlgebras]
eta [definition, in ImpAlg.ImplicativeStructures]
etarule [lemma, in ImpAlg.ImplicativeStructures]
exfalso_S [lemma, in ImpAlg.ImplicativeAlgebras]
existst [definition, in ImpAlg.ImplicativeAlgebras]
extra_hyp_ter [lemma, in ImpAlg.ParAlgebras]
extra_hyp [lemma, in ImpAlg.ParAlgebras]
ex_term [definition, in ImpAlg.ImplicativeAlgebras]
ex_falso [lemma, in ImpAlg.ParAlgebras]
F
fn_typ_type [lemma, in ImpAlg.Lambda]fn_typ_type_aux [lemma, in ImpAlg.Lambda]
fn_typ_fall [lemma, in ImpAlg.Lambda]
fn_typ_fall_aux [lemma, in ImpAlg.Lambda]
fn_typ_fall_Aux [lemma, in ImpAlg.Lambda]
fn_typ_arrow [lemma, in ImpAlg.Lambda]
fn_typ_fall_bvar [lemma, in ImpAlg.Lambda]
fn_typ [definition, in ImpAlg.Lambda]
fn_typ_aux [definition, in ImpAlg.Lambda]
forallt [definition, in ImpAlg.ImplicativeAlgebras]
from_list_nil_inv [lemma, in ImpAlg.Lambda]
from_list_append [lemma, in ImpAlg.Lambda]
fv_typ [definition, in ImpAlg.Combinators]
fv_trm [definition, in ImpAlg.Combinators]
fv_typ [definition, in ImpAlg.ImplicativeAlgebras]
fv_trm [definition, in ImpAlg.ImplicativeAlgebras]
fv_open_trm [lemma, in ImpAlg.Lambda]
fv_typ [definition, in ImpAlg.Lambda]
fv_trm [definition, in ImpAlg.Lambda]
fv_typ_subst [lemma, in ImpAlg.Adequacy]
G
geq_S_S [lemma, in ImpAlg.Lambda]geq_1_S [lemma, in ImpAlg.Lambda]
glb [definition, in ImpAlg.Lattices]
glb_elim_intro [lemma, in ImpAlg.Lattices]
glb_unique [lemma, in ImpAlg.Lattices]
H
half_pmodus_ponens [lemma, in ImpAlg.ParAlgebras]ha_adjunction [lemma, in ImpAlg.ImplicativeAlgebras]
HeytingAlgebra [record, in ImpAlg.HeytingAlgebras]
HeytingAlgebras [library]
I
IA [section, in ImpAlg.ImplicativeAlgebras]_ ⊕ _ [notation, in ImpAlg.ImplicativeAlgebras]
_ × _ [notation, in ImpAlg.ImplicativeAlgebras]
_ ≈ _ [notation, in ImpAlg.ImplicativeAlgebras]
_ ⊢ _ [notation, in ImpAlg.ImplicativeAlgebras]
$ _ [notation, in ImpAlg.ImplicativeAlgebras]
[ _ ] _ [notation, in ImpAlg.ImplicativeAlgebras]
[∀] _ [notation, in ImpAlg.ImplicativeAlgebras]
[∃] _ [notation, in ImpAlg.ImplicativeAlgebras]
¬ _ [notation, in ImpAlg.ImplicativeAlgebras]
λ+ _ [notation, in ImpAlg.ImplicativeAlgebras]
Id [definition, in ImpAlg.Combinators]
Idum [definition, in ImpAlg.Dummies]
Id_SK [lemma, in ImpAlg.Combinators]
II_neq_I [lemma, in ImpAlg.Dummies]
image_set [definition, in ImpAlg.Lattices]
imp [projection, in ImpAlg.HeytingAlgebras]
Impcc [lemma, in ImpAlg.ParAlgebras]
ImpK [lemma, in ImpAlg.ParAlgebras]
ImplicativeAlgebra [record, in ImpAlg.ImplicativeAlgebras]
ImplicativeAlgebras [library]
ImplicativeStructure [record, in ImpAlg.ImplicativeStructures]
ImplicativeStructures [library]
ImpS [lemma, in ImpAlg.ParAlgebras]
imp_meet [lemma, in ImpAlg.HeytingAlgebras]
imp_is_join [lemma, in ImpAlg.HeytingAlgebras]
imp_mon_r [lemma, in ImpAlg.HeytingAlgebras]
imp_mon_l [lemma, in ImpAlg.HeytingAlgebras]
imp_adj [lemma, in ImpAlg.HeytingAlgebras]
imp_lub [lemma, in ImpAlg.HeytingAlgebras]
imp_intro [lemma, in ImpAlg.HeytingAlgebras]
imp_self [lemma, in ImpAlg.HeytingAlgebras]
imp_elim [lemma, in ImpAlg.HeytingAlgebras]
imp_sup [projection, in ImpAlg.HeytingAlgebras]
imp_bot_pneg [lemma, in ImpAlg.ParAlgebras]
inf [definition, in ImpAlg.Lattices]
inf_comm [lemma, in ImpAlg.Lattices]
inf_comm_aux [lemma, in ImpAlg.Lattices]
inf_elim_trans [lemma, in ImpAlg.Lattices]
inf_pneg [lemma, in ImpAlg.ParAlgebras]
inj1 [definition, in ImpAlg.ImplicativeAlgebras]
inj2 [definition, in ImpAlg.ImplicativeAlgebras]
in_revsep [lemma, in ImpAlg.TensorAlgebras]
in_pre_pneg [lemma, in ImpAlg.TensorAlgebras]
in_list [definition, in ImpAlg.Lambda]
IS [definition, in ImpAlg.ParAlgebras]
I_neq_SKK_dum [lemma, in ImpAlg.Dummies]
J
join [projection, in ImpAlg.Lattices]join_set_Proper [instance, in ImpAlg.Lattices]
join_same_set [lemma, in ImpAlg.Lattices]
join_subset [lemma, in ImpAlg.Lattices]
join_elim_trans [lemma, in ImpAlg.Lattices]
join_family [definition, in ImpAlg.Lattices]
join_set_lub [lemma, in ImpAlg.Lattices]
join_emptyset [lemma, in ImpAlg.Lattices]
join_intro [projection, in ImpAlg.Lattices]
join_elim [projection, in ImpAlg.Lattices]
join_set [projection, in ImpAlg.Lattices]
join_top_r [lemma, in ImpAlg.Lattices]
join_top_l [lemma, in ImpAlg.Lattices]
join_bot_r [lemma, in ImpAlg.Lattices]
join_bot_l [lemma, in ImpAlg.Lattices]
join_meet_completeness [lemma, in ImpAlg.Lattices]
join_complete [definition, in ImpAlg.Lattices]
join_mon_r [lemma, in ImpAlg.Lattices]
join_mon_l [lemma, in ImpAlg.Lattices]
join_lub [lemma, in ImpAlg.Lattices]
join_ub_r [lemma, in ImpAlg.Lattices]
join_ub_l [lemma, in ImpAlg.Lattices]
join_consistent [lemma, in ImpAlg.Lattices]
join_idempotent [projection, in ImpAlg.Lattices]
join_absorptive [projection, in ImpAlg.Lattices]
join_associative [projection, in ImpAlg.Lattices]
join_commutative [projection, in ImpAlg.Lattices]
join_neg_l [lemma, in ImpAlg.BooleanAlgebras]
join_distributive_l [lemma, in ImpAlg.BooleanAlgebras]
join_meet_set [lemma, in ImpAlg.BooleanAlgebras]
join_neg [projection, in ImpAlg.BooleanAlgebras]
join_distributive [projection, in ImpAlg.BooleanAlgebras]
join3_neg3 [lemma, in ImpAlg.BooleanAlgebras]
join3_neg1 [lemma, in ImpAlg.BooleanAlgebras]
K
K [definition, in ImpAlg.Combinators]Kdum [definition, in ImpAlg.Dummies]
L
Lambda [library]lambdaB [definition, in ImpAlg.Combinators]
lambdaEasy [definition, in ImpAlg.Combinators]
lambdaId [definition, in ImpAlg.Combinators]
lambdaK [definition, in ImpAlg.Combinators]
lambdaS [definition, in ImpAlg.Combinators]
lambdaSK [axiom, in ImpAlg.Combinators]
lambdaW [definition, in ImpAlg.Combinators]
lambda_B [lemma, in ImpAlg.Combinators]
lambda_Easy [lemma, in ImpAlg.Combinators]
lambda_W [lemma, in ImpAlg.Combinators]
lambda_S [lemma, in ImpAlg.Combinators]
lambda_K [lemma, in ImpAlg.Combinators]
lambda_Id [lemma, in ImpAlg.Combinators]
Lattice [record, in ImpAlg.Lattices]
Lattices [library]
lb [definition, in ImpAlg.Lattices]
LPar [library]
µ{[],}. _ [notation, in ImpAlg.LPar]
µ{}. _ [notation, in ImpAlg.LPar]
µ[]. _ [notation, in ImpAlg.LPar]
µ-. _ [notation, in ImpAlg.LPar]
[ _ ] [notation, in ImpAlg.LPar]
{ _ , _ } [notation, in ImpAlg.LPar]
µ+. _ [notation, in ImpAlg.LPar]
_ ◃ _ [notation, in ImpAlg.LPar]
< _ | _ > [notation, in ImpAlg.LPar]
_ ∈(≤) [notation, in ImpAlg.LPar]
LPar_Encoding [section, in ImpAlg.LPar]
LTensor [section, in ImpAlg.LTensor]
LTensor [library]
_ ◃ _ (lt_scope) [notation, in ImpAlg.LTensor]
_ ∈(≤) [notation, in ImpAlg.LTensor]
< _ | _ > [notation, in ImpAlg.LTensor]
[ _ ] [notation, in ImpAlg.LTensor]
{ _ , _ } [notation, in ImpAlg.LTensor]
¬ _ [notation, in ImpAlg.LTensor]
µ+. _ [notation, in ImpAlg.LTensor]
µ-. _ [notation, in ImpAlg.LTensor]
µ[]. _ [notation, in ImpAlg.LTensor]
µ{}. _ [notation, in ImpAlg.LTensor]
lub [definition, in ImpAlg.Lattices]
lub_elim_intro [lemma, in ImpAlg.Lattices]
lub_unique [lemma, in ImpAlg.Lattices]
M
map_pred_S [lemma, in ImpAlg.Lambda]map_pred_append [lemma, in ImpAlg.Lambda]
map_pred_cons [lemma, in ImpAlg.Lambda]
map_pred [definition, in ImpAlg.Lambda]
meet [projection, in ImpAlg.Lattices]
meet_set_Proper [instance, in ImpAlg.Lattices]
meet_same_set [lemma, in ImpAlg.Lattices]
meet_same_set_le [lemma, in ImpAlg.Lattices]
meet_subset [lemma, in ImpAlg.Lattices]
meet_fam_intro [lemma, in ImpAlg.Lattices]
meet_fam_elim [lemma, in ImpAlg.Lattices]
meet_comm [lemma, in ImpAlg.Lattices]
meet_comm_aux [lemma, in ImpAlg.Lattices]
meet_elim_trans [lemma, in ImpAlg.Lattices]
meet_family [definition, in ImpAlg.Lattices]
meet_set_glb [lemma, in ImpAlg.Lattices]
meet_emptyset [lemma, in ImpAlg.Lattices]
meet_intro [projection, in ImpAlg.Lattices]
meet_elim [projection, in ImpAlg.Lattices]
meet_set [projection, in ImpAlg.Lattices]
meet_top_r [lemma, in ImpAlg.Lattices]
meet_top_l [lemma, in ImpAlg.Lattices]
meet_bot_r [lemma, in ImpAlg.Lattices]
meet_bot_l [lemma, in ImpAlg.Lattices]
meet_join_completeness [lemma, in ImpAlg.Lattices]
meet_complete [definition, in ImpAlg.Lattices]
meet_mon_r [lemma, in ImpAlg.Lattices]
meet_mon_l [lemma, in ImpAlg.Lattices]
meet_glb [lemma, in ImpAlg.Lattices]
meet_lb_r [lemma, in ImpAlg.Lattices]
meet_lb_l [lemma, in ImpAlg.Lattices]
meet_join [lemma, in ImpAlg.Lattices]
meet_idempotent [projection, in ImpAlg.Lattices]
meet_absorptive [projection, in ImpAlg.Lattices]
meet_associative [projection, in ImpAlg.Lattices]
meet_commutative [projection, in ImpAlg.Lattices]
meet_distributive_l [lemma, in ImpAlg.BooleanAlgebras]
meet_join_set [lemma, in ImpAlg.BooleanAlgebras]
meet_neg [projection, in ImpAlg.BooleanAlgebras]
meet_distributive [projection, in ImpAlg.BooleanAlgebras]
min [definition, in ImpAlg.Lattices]
modus_ponens_revsep [lemma, in ImpAlg.TensorAlgebras]
modus_ponens_later [lemma, in ImpAlg.ImplicativeAlgebras]
modus_ponens [projection, in ImpAlg.ImplicativeAlgebras]
modus_ponens_parrow [lemma, in ImpAlg.ParAlgebras]
mod_ponens [lemma, in ImpAlg.ImplicativeAlgebras]
mod_pon_app [lemma, in ImpAlg.ImplicativeStructures]
mod_pon_closure [definition, in ImpAlg.ImplicativeStructures]
mod_pon_cong [lemma, in ImpAlg.ParAlgebras]
mod_pon_inf_ter [lemma, in ImpAlg.ParAlgebras]
mod_pon_inf [lemma, in ImpAlg.ParAlgebras]
mod_pon_app [lemma, in ImpAlg.ParAlgebras]
mun [definition, in ImpAlg.LTensor]
mun [definition, in ImpAlg.LPar]
mun_beta [lemma, in ImpAlg.LTensor]
mun_eta [lemma, in ImpAlg.LTensor]
mun_mon [lemma, in ImpAlg.LTensor]
mun_beta [lemma, in ImpAlg.LPar]
mun_eta [lemma, in ImpAlg.LPar]
mun_mon [lemma, in ImpAlg.LPar]
mup [definition, in ImpAlg.LTensor]
mup [definition, in ImpAlg.LPar]
mup_eta [lemma, in ImpAlg.LTensor]
mup_beta [lemma, in ImpAlg.LTensor]
mup_mon [lemma, in ImpAlg.LTensor]
mup_eta [lemma, in ImpAlg.LPar]
mup_beta [lemma, in ImpAlg.LPar]
mup_mon [lemma, in ImpAlg.LPar]
mu_neg_beta [lemma, in ImpAlg.LTensor]
mu_pair_beta [lemma, in ImpAlg.LTensor]
mu_neg_eta [lemma, in ImpAlg.LTensor]
mu_pair_eta [lemma, in ImpAlg.LTensor]
mu_neg_mon [lemma, in ImpAlg.LTensor]
mu_pair_mon [lemma, in ImpAlg.LTensor]
mu_neg [definition, in ImpAlg.LTensor]
mu_pair [definition, in ImpAlg.LTensor]
mu_abs_char [lemma, in ImpAlg.LPar]
mu_abs [definition, in ImpAlg.LPar]
mu_neg_beta [lemma, in ImpAlg.LPar]
mu_pair_beta [lemma, in ImpAlg.LPar]
mu_neg_eta [lemma, in ImpAlg.LPar]
mu_pair_eta [lemma, in ImpAlg.LPar]
mu_neg_mon [lemma, in ImpAlg.LPar]
mu_pair_mon [lemma, in ImpAlg.LPar]
mu_neg [definition, in ImpAlg.LPar]
mu_pair [definition, in ImpAlg.LPar]
N
neg [definition, in ImpAlg.Combinators]neg [definition, in ImpAlg.ImplicativeAlgebras]
neg [projection, in ImpAlg.BooleanAlgebras]
negbot [definition, in ImpAlg.Dummies]
negtop [definition, in ImpAlg.Dummies]
neg_join_set [lemma, in ImpAlg.BooleanAlgebras]
neg_meet_set [lemma, in ImpAlg.BooleanAlgebras]
neg_mon [lemma, in ImpAlg.BooleanAlgebras]
neg_meet [lemma, in ImpAlg.BooleanAlgebras]
neg_join [lemma, in ImpAlg.BooleanAlgebras]
neg_bot [lemma, in ImpAlg.BooleanAlgebras]
neg_top [lemma, in ImpAlg.BooleanAlgebras]
neg_complement [lemma, in ImpAlg.BooleanAlgebras]
O
ok [definition, in ImpAlg.LTensor]ok [definition, in ImpAlg.LPar]
ok_Reflexive [instance, in ImpAlg.LTensor]
ok_Reflexive [instance, in ImpAlg.LPar]
open_typ_com_ct [lemma, in ImpAlg.Lambda]
open_typ_com_ff [lemma, in ImpAlg.Lambda]
open_typ_com_cc [lemma, in ImpAlg.Lambda]
open_typ_com_cf [lemma, in ImpAlg.Lambda]
open_typ_type [lemma, in ImpAlg.Lambda]
open_typ_fn [lemma, in ImpAlg.Lambda]
open_typ_fvar [definition, in ImpAlg.Lambda]
open_typ [definition, in ImpAlg.Lambda]
open_rec_typ [definition, in ImpAlg.Lambda]
open_trm_def [lemma, in ImpAlg.Lambda]
open_trm_var [definition, in ImpAlg.Lambda]
open_trm [definition, in ImpAlg.Lambda]
open_rec_trm [definition, in ImpAlg.Lambda]
or [definition, in ImpAlg.ParAlgebras]
ord [projection, in ImpAlg.Lattices]
Order [record, in ImpAlg.Lattices]
ord_Antisymmetric [instance, in ImpAlg.Lattices]
ord_Transitive [instance, in ImpAlg.Lattices]
ord_Reflexive [instance, in ImpAlg.Lattices]
ord_trans [projection, in ImpAlg.Lattices]
ord_antisym [projection, in ImpAlg.Lattices]
ord_refl [projection, in ImpAlg.Lattices]
or_par [lemma, in ImpAlg.ParAlgebras]
or_par_gen [lemma, in ImpAlg.ParAlgebras]
P
pair [definition, in ImpAlg.ImplicativeAlgebras]pairing [definition, in ImpAlg.LTensor]
pairing [definition, in ImpAlg.LPar]
par [projection, in ImpAlg.ParAlgebras]
ParAlgebra [record, in ImpAlg.ParAlgebras]
ParAlgebras [library]
ParAlgebra_is_ImpAlgebra [lemma, in ImpAlg.Theorems]
parrow [definition, in ImpAlg.ParAlgebras]
parrow_meet [lemma, in ImpAlg.ParAlgebras]
parrow_mon [lemma, in ImpAlg.ParAlgebras]
parrow_mon_r [lemma, in ImpAlg.ParAlgebras]
parrow_mon_l [lemma, in ImpAlg.ParAlgebras]
ParStructure [record, in ImpAlg.ParAlgebras]
ParStructure_is_ImplicativeStructure [lemma, in ImpAlg.Theorems]
partop [definition, in ImpAlg.Dummies]
par_or [lemma, in ImpAlg.ParAlgebras]
par_or_gen [lemma, in ImpAlg.ParAlgebras]
par_swap_psep [lemma, in ImpAlg.ParAlgebras]
par_assoc_psep [lemma, in ImpAlg.ParAlgebras]
par_comm_psep [lemma, in ImpAlg.ParAlgebras]
par_assoc_r [lemma, in ImpAlg.ParAlgebras]
par_assoc_l [definition, in ImpAlg.ParAlgebras]
par_meet_f_r [lemma, in ImpAlg.ParAlgebras]
par_top_r [lemma, in ImpAlg.ParAlgebras]
par_top_l [lemma, in ImpAlg.ParAlgebras]
par_mon_r [lemma, in ImpAlg.ParAlgebras]
par_mon_l [lemma, in ImpAlg.ParAlgebras]
par_meet_r [projection, in ImpAlg.ParAlgebras]
par_meet_l [projection, in ImpAlg.ParAlgebras]
par_mon [projection, in ImpAlg.ParAlgebras]
par_set_l_Proper [instance, in ImpAlg.ParAlgebras]
par_set_r_Proper [instance, in ImpAlg.ParAlgebras]
par_set [definition, in ImpAlg.ParAlgebras]
par_set_l [definition, in ImpAlg.ParAlgebras]
par_set_r [definition, in ImpAlg.ParAlgebras]
PA_TA [instance, in ImpAlg.TensorAlgebras]
PA_IA [instance, in ImpAlg.ParAlgebras]
Pcc [definition, in ImpAlg.ParAlgebras]
PC6 [definition, in ImpAlg.ParAlgebras]
PC6_ter [definition, in ImpAlg.ParAlgebras]
PC7 [definition, in ImpAlg.ParAlgebras]
PI [definition, in ImpAlg.ParAlgebras]
PK [definition, in ImpAlg.ParAlgebras]
pmodus_ponens [projection, in ImpAlg.ParAlgebras]
pneg [projection, in ImpAlg.ParAlgebras]
pneg_imp_bot [lemma, in ImpAlg.ParAlgebras]
pneg_arrow [lemma, in ImpAlg.ParAlgebras]
pneg_top [lemma, in ImpAlg.ParAlgebras]
pneg_meet [projection, in ImpAlg.ParAlgebras]
pneg_mon [projection, in ImpAlg.ParAlgebras]
preimage [definition, in ImpAlg.Lattices]
preimage_set [definition, in ImpAlg.Lattices]
pre_pneg_set [definition, in ImpAlg.TensorAlgebras]
pre_pneg [definition, in ImpAlg.TensorAlgebras]
pre_upclosed_rev [lemma, in ImpAlg.Lattices]
pre_comp_arr_bi [lemma, in ImpAlg.ParAlgebras]
prodt [definition, in ImpAlg.ImplicativeAlgebras]
prodt_intro [lemma, in ImpAlg.ImplicativeAlgebras]
prodt_r [lemma, in ImpAlg.ImplicativeAlgebras]
prodt_l [lemma, in ImpAlg.ImplicativeAlgebras]
proj1 [definition, in ImpAlg.ImplicativeAlgebras]
proj2 [definition, in ImpAlg.ImplicativeAlgebras]
PS [definition, in ImpAlg.ParAlgebras]
psep [projection, in ImpAlg.ParAlgebras]
psep_Impcc [lemma, in ImpAlg.ParAlgebras]
psep_ImpS [lemma, in ImpAlg.ParAlgebras]
psep_ImpK [lemma, in ImpAlg.ParAlgebras]
psep_cc [lemma, in ImpAlg.ParAlgebras]
psep_S [lemma, in ImpAlg.ParAlgebras]
psep_K [lemma, in ImpAlg.ParAlgebras]
psep_PS4_r [lemma, in ImpAlg.ParAlgebras]
psep_PS2_l [lemma, in ImpAlg.ParAlgebras]
psep_PI [lemma, in ImpAlg.ParAlgebras]
psep_C7 [lemma, in ImpAlg.ParAlgebras]
psep_PC6_ter [lemma, in ImpAlg.ParAlgebras]
psep_PC6 [lemma, in ImpAlg.ParAlgebras]
psep_PS5 [projection, in ImpAlg.ParAlgebras]
psep_PS4 [projection, in ImpAlg.ParAlgebras]
psep_PS3 [projection, in ImpAlg.ParAlgebras]
psep_PS2 [projection, in ImpAlg.ParAlgebras]
psep_PS1 [projection, in ImpAlg.ParAlgebras]
Pswap_l [definition, in ImpAlg.ParAlgebras]
Pswap_r [definition, in ImpAlg.ParAlgebras]
PS_TS [instance, in ImpAlg.TensorAlgebras]
ps_mod_pon_closure [definition, in ImpAlg.ParAlgebras]
ps_app_closure [definition, in ImpAlg.ParAlgebras]
ps_upwards_closure [definition, in ImpAlg.ParAlgebras]
ps_adjunction [lemma, in ImpAlg.ParAlgebras]
ps_app_min [lemma, in ImpAlg.ParAlgebras]
ps_etarule [lemma, in ImpAlg.ParAlgebras]
ps_betarule [lemma, in ImpAlg.ParAlgebras]
ps_abs_mon [lemma, in ImpAlg.ParAlgebras]
ps_app_mon [lemma, in ImpAlg.ParAlgebras]
PS_IS [instance, in ImpAlg.ParAlgebras]
PS1 [definition, in ImpAlg.ParAlgebras]
PS1_lpar [lemma, in ImpAlg.LPar]
PS2 [definition, in ImpAlg.ParAlgebras]
PS2_lpar [lemma, in ImpAlg.LPar]
PS2_lpar_aux [lemma, in ImpAlg.LPar]
PS2_l [definition, in ImpAlg.ParAlgebras]
PS3 [definition, in ImpAlg.ParAlgebras]
PS3_lpar [lemma, in ImpAlg.LPar]
PS4 [definition, in ImpAlg.ParAlgebras]
PS4_lpar_aux [lemma, in ImpAlg.LPar]
PS4_r [definition, in ImpAlg.ParAlgebras]
PS5 [definition, in ImpAlg.ParAlgebras]
PS5_lpar [lemma, in ImpAlg.LPar]
pup_closed [projection, in ImpAlg.ParAlgebras]
R
realize [inductive, in ImpAlg.Adequacy]realizer_later [lemma, in ImpAlg.ImplicativeAlgebras]
realize_update [lemma, in ImpAlg.Adequacy]
realize_inv [lemma, in ImpAlg.Adequacy]
real_push [constructor, in ImpAlg.Adequacy]
real_empty [constructor, in ImpAlg.Adequacy]
reductio_ad_absurdum [lemma, in ImpAlg.ParAlgebras]
remove [definition, in ImpAlg.Lambda]
remove_pred_0 [lemma, in ImpAlg.Lambda]
remove_pred [lemma, in ImpAlg.Lambda]
remove_comm [lemma, in ImpAlg.Lambda]
remove_0_def [lemma, in ImpAlg.Lambda]
remove_append [lemma, in ImpAlg.Lambda]
remove_0_incl [lemma, in ImpAlg.Lambda]
remove_0_cons_0 [lemma, in ImpAlg.Lambda]
remove_0 [definition, in ImpAlg.Lambda]
rev [definition, in ImpAlg.Lattices]
RevBooleanAlgebra [definition, in ImpAlg.BooleanAlgebras]
RevBoundedLattice [definition, in ImpAlg.Lattices]
RevCompleteBooleanAlgebra [definition, in ImpAlg.BooleanAlgebras]
RevCompleteLattice [definition, in ImpAlg.Lattices]
reverse [definition, in ImpAlg.Lattices]
ReverseParAlg [section, in ImpAlg.TensorAlgebras]
_ ◃ _ (ia_scope) [notation, in ImpAlg.TensorAlgebras]
¬⁻¹ _ (ia_scope) [notation, in ImpAlg.TensorAlgebras]
_ ⨂↦ _ [notation, in ImpAlg.TensorAlgebras]
_ ⨂ _ [notation, in ImpAlg.TensorAlgebras]
ReversePS [section, in ImpAlg.TensorAlgebras]
ReverseTS [section, in ImpAlg.TensorAlgebras]
¬ _ [notation, in ImpAlg.TensorAlgebras]
RevLattice [definition, in ImpAlg.Lattices]
RevOrd [definition, in ImpAlg.Lattices]
revsep [definition, in ImpAlg.TensorAlgebras]
revsep_TS5 [lemma, in ImpAlg.TensorAlgebras]
revsep_TS4 [lemma, in ImpAlg.TensorAlgebras]
revsep_TS3 [lemma, in ImpAlg.TensorAlgebras]
revsep_TS2 [lemma, in ImpAlg.TensorAlgebras]
revsep_TS1 [lemma, in ImpAlg.TensorAlgebras]
rev_pneg_meet [lemma, in ImpAlg.TensorAlgebras]
rev_par_meet_r [lemma, in ImpAlg.TensorAlgebras]
rev_par_meet_l [lemma, in ImpAlg.TensorAlgebras]
rev_pneg_mon [lemma, in ImpAlg.TensorAlgebras]
rev_par_mon [lemma, in ImpAlg.TensorAlgebras]
rev_tneg_join [lemma, in ImpAlg.TensorAlgebras]
rev_tensor_join_r [lemma, in ImpAlg.TensorAlgebras]
rev_tensor_join_l [lemma, in ImpAlg.TensorAlgebras]
rev_tneg_mon [lemma, in ImpAlg.TensorAlgebras]
rev_tensor_mon [lemma, in ImpAlg.TensorAlgebras]
rev_consistent [lemma, in ImpAlg.Lattices]
rev_trans [lemma, in ImpAlg.Lattices]
rev_antisym [lemma, in ImpAlg.Lattices]
rev_refl [lemma, in ImpAlg.Lattices]
Rev_TensorStructure_is_ParStructure [lemma, in ImpAlg.Theorems]
Rev_ParAlgebra_is_TensorAlgebra [lemma, in ImpAlg.Theorems]
Rev_ParStructure_is_TensorStructure [lemma, in ImpAlg.Theorems]
S
S [definition, in ImpAlg.Combinators]same_set_Equiv [instance, in ImpAlg.Ens]
same_set_trans [lemma, in ImpAlg.Ens]
same_set_sym [lemma, in ImpAlg.Ens]
same_set_refl [lemma, in ImpAlg.Ens]
same_set [definition, in ImpAlg.Ens]
Sdum [definition, in ImpAlg.Dummies]
semi_adjunction [lemma, in ImpAlg.TensorAlgebras]
separator [projection, in ImpAlg.ImplicativeAlgebras]
sep_Easy [lemma, in ImpAlg.ImplicativeAlgebras]
sep_W [lemma, in ImpAlg.ImplicativeAlgebras]
sep_typ [lemma, in ImpAlg.ImplicativeAlgebras]
sep_term [lemma, in ImpAlg.ImplicativeAlgebras]
sep_SK [lemma, in ImpAlg.ImplicativeAlgebras]
sep_comb [lemma, in ImpAlg.ImplicativeAlgebras]
sep_Id [lemma, in ImpAlg.ImplicativeAlgebras]
sep_cc [projection, in ImpAlg.ImplicativeAlgebras]
sep_S [projection, in ImpAlg.ImplicativeAlgebras]
sep_K [projection, in ImpAlg.ImplicativeAlgebras]
size [definition, in ImpAlg.Lambda]
size_typ_arrow [lemma, in ImpAlg.Lambda]
size_typ_plus_S [lemma, in ImpAlg.Lambda]
size_typ_S [lemma, in ImpAlg.Lambda]
size_typ_open_f [lemma, in ImpAlg.Lambda]
size_typ_open [lemma, in ImpAlg.Lambda]
size_typ_le_1 [lemma, in ImpAlg.Lambda]
size_typ_ind [lemma, in ImpAlg.Lambda]
size_typ_ind_gen [lemma, in ImpAlg.Lambda]
size_typ_induction [lemma, in ImpAlg.Lambda]
size_typ_not_0 [lemma, in ImpAlg.Lambda]
size_typ [definition, in ImpAlg.Lambda]
size_open [lemma, in ImpAlg.Lambda]
size_le_1 [lemma, in ImpAlg.Lambda]
size_ind [lemma, in ImpAlg.Lambda]
size_ind_gen [lemma, in ImpAlg.Lambda]
size_induction [lemma, in ImpAlg.Lambda]
size_not_0 [lemma, in ImpAlg.Lambda]
subset [definition, in ImpAlg.Ens]
subset_trans [lemma, in ImpAlg.Lambda]
substitution [definition, in ImpAlg.Adequacy]
subst_trm_update [lemma, in ImpAlg.Adequacy]
subst_trm_update_open [lemma, in ImpAlg.Adequacy]
subst_typ_update [lemma, in ImpAlg.Adequacy]
subst_typ_var [lemma, in ImpAlg.Adequacy]
subst_typ [definition, in ImpAlg.Adequacy]
subst_trm [definition, in ImpAlg.Adequacy]
subtyping [lemma, in ImpAlg.ImplicativeAlgebras]
Succ [definition, in ImpAlg.Combinators]
sumt [definition, in ImpAlg.ImplicativeAlgebras]
sumt_elim [lemma, in ImpAlg.ImplicativeAlgebras]
sumt_r [lemma, in ImpAlg.ImplicativeAlgebras]
sumt_l [lemma, in ImpAlg.ImplicativeAlgebras]
sup [definition, in ImpAlg.Lattices]
swap_imp [lemma, in ImpAlg.ParAlgebras]
swap_l [lemma, in ImpAlg.ParAlgebras]
swap_r [lemma, in ImpAlg.ParAlgebras]
S1_p [lemma, in ImpAlg.ParAlgebras]
S2_p [lemma, in ImpAlg.ParAlgebras]
S3_p [lemma, in ImpAlg.ParAlgebras]
S4_p [lemma, in ImpAlg.ParAlgebras]
S6_gen [lemma, in ImpAlg.ParAlgebras]
T
tarr [definition, in ImpAlg.TensorAlgebras]tarrow [definition, in ImpAlg.TensorAlgebras]
tens [definition, in ImpAlg.TensorAlgebras]
tensor [projection, in ImpAlg.TensorAlgebras]
TensorAlgebra [record, in ImpAlg.TensorAlgebras]
TensorAlgebras [library]
tensorbot [definition, in ImpAlg.Dummies]
TensorStructure [record, in ImpAlg.TensorAlgebras]
tensor_bot_r [lemma, in ImpAlg.TensorAlgebras]
tensor_bot_l [lemma, in ImpAlg.TensorAlgebras]
tensor_mon_r [lemma, in ImpAlg.TensorAlgebras]
tensor_mon_l [lemma, in ImpAlg.TensorAlgebras]
tensor_join_r [projection, in ImpAlg.TensorAlgebras]
tensor_join_l [projection, in ImpAlg.TensorAlgebras]
tensor_mon [projection, in ImpAlg.TensorAlgebras]
tensor_set [definition, in ImpAlg.TensorAlgebras]
tensor_set_r [definition, in ImpAlg.TensorAlgebras]
tensor_set_l [definition, in ImpAlg.TensorAlgebras]
term [inductive, in ImpAlg.Lambda]
termSK [inductive, in ImpAlg.Combinators]
termSK_app [constructor, in ImpAlg.Combinators]
term_K [constructor, in ImpAlg.Combinators]
term_S [constructor, in ImpAlg.Combinators]
term_cc [constructor, in ImpAlg.Lambda]
term_app [constructor, in ImpAlg.Lambda]
term_abs [constructor, in ImpAlg.Lambda]
term_var [constructor, in ImpAlg.Lambda]
Theorems [library]
tmodus_ponens [projection, in ImpAlg.TensorAlgebras]
tneg [projection, in ImpAlg.TensorAlgebras]
tneg_bot [lemma, in ImpAlg.TensorAlgebras]
tneg_join [projection, in ImpAlg.TensorAlgebras]
tneg_mon [projection, in ImpAlg.TensorAlgebras]
top [projection, in ImpAlg.Lattices]
top_max [projection, in ImpAlg.Lattices]
top_join [lemma, in ImpAlg.BooleanAlgebras]
translated [inductive, in ImpAlg.Adequacy]
translated_Easy [lemma, in ImpAlg.Combinators]
translated_W [lemma, in ImpAlg.Combinators]
translated_S [lemma, in ImpAlg.Combinators]
translated_K [lemma, in ImpAlg.Combinators]
translated_Id [lemma, in ImpAlg.Combinators]
translated_peirce [lemma, in ImpAlg.Adequacy]
translated_typ_unique [lemma, in ImpAlg.Adequacy]
translated_unique [lemma, in ImpAlg.Adequacy]
translated_typ [inductive, in ImpAlg.Adequacy]
trans_typ_open [lemma, in ImpAlg.Adequacy]
trans_typ_update [lemma, in ImpAlg.Adequacy]
trans_correct [lemma, in ImpAlg.Adequacy]
trans_typ_var [lemma, in ImpAlg.Adequacy]
trans_typ_arrow [lemma, in ImpAlg.Adequacy]
trans_typ_fold [lemma, in ImpAlg.Adequacy]
trans_typ_fioul [lemma, in ImpAlg.Adequacy]
trans_typ_fall [lemma, in ImpAlg.Adequacy]
trans_typ [definition, in ImpAlg.Adequacy]
trans_typ_aux [definition, in ImpAlg.Adequacy]
trm [inductive, in ImpAlg.Lambda]
trm_cc [constructor, in ImpAlg.Lambda]
trm_app [constructor, in ImpAlg.Lambda]
trm_abs [constructor, in ImpAlg.Lambda]
trm_cvar [constructor, in ImpAlg.Lambda]
trm_fvar [constructor, in ImpAlg.Lambda]
trm_bvar [constructor, in ImpAlg.Lambda]
true_S [lemma, in ImpAlg.ImplicativeAlgebras]
tr_typ_fall [constructor, in ImpAlg.Adequacy]
tr_typ_arrow [constructor, in ImpAlg.Adequacy]
tr_typ_var [constructor, in ImpAlg.Adequacy]
tr_cc [constructor, in ImpAlg.Adequacy]
tr_app [constructor, in ImpAlg.Adequacy]
tr_abs [constructor, in ImpAlg.Adequacy]
tr_var [constructor, in ImpAlg.Adequacy]
TS [definition, in ImpAlg.TensorAlgebras]
tsep [projection, in ImpAlg.TensorAlgebras]
tsep_TS5 [projection, in ImpAlg.TensorAlgebras]
tsep_TS4 [projection, in ImpAlg.TensorAlgebras]
tsep_TS3 [projection, in ImpAlg.TensorAlgebras]
tsep_TS2 [projection, in ImpAlg.TensorAlgebras]
tsep_TS1 [projection, in ImpAlg.TensorAlgebras]
ts_half_adjunction [lemma, in ImpAlg.TensorAlgebras]
ts_app [definition, in ImpAlg.TensorAlgebras]
ts_abs [definition, in ImpAlg.TensorAlgebras]
TS_PS [instance, in ImpAlg.TensorAlgebras]
TS1 [definition, in ImpAlg.TensorAlgebras]
TS2 [definition, in ImpAlg.TensorAlgebras]
TS3 [definition, in ImpAlg.TensorAlgebras]
TS4 [definition, in ImpAlg.TensorAlgebras]
TS5 [definition, in ImpAlg.TensorAlgebras]
tup_closed [projection, in ImpAlg.TensorAlgebras]
typ [inductive, in ImpAlg.Lambda]
type [inductive, in ImpAlg.Lambda]
type_case [lemma, in ImpAlg.ImplicativeAlgebras]
type_inj2 [lemma, in ImpAlg.ImplicativeAlgebras]
type_inj1 [lemma, in ImpAlg.ImplicativeAlgebras]
type_proj2 [lemma, in ImpAlg.ImplicativeAlgebras]
type_proj1 [lemma, in ImpAlg.ImplicativeAlgebras]
type_pair [lemma, in ImpAlg.ImplicativeAlgebras]
type_ex_elim [lemma, in ImpAlg.ImplicativeAlgebras]
type_ex_intro [lemma, in ImpAlg.ImplicativeAlgebras]
type_fa_elim [lemma, in ImpAlg.ImplicativeAlgebras]
type_fa_intro [lemma, in ImpAlg.ImplicativeAlgebras]
type_subst [lemma, in ImpAlg.Lambda]
type_peirce [lemma, in ImpAlg.Lambda]
type_arrow [constructor, in ImpAlg.Lambda]
type_fall [constructor, in ImpAlg.Lambda]
type_cvar [constructor, in ImpAlg.Lambda]
type_fvar [constructor, in ImpAlg.Lambda]
typing_empty_closed [lemma, in ImpAlg.Combinators]
typing_fv_trm [lemma, in ImpAlg.Lambda]
typing_fv_trm_aux [lemma, in ImpAlg.Lambda]
typing_term [lemma, in ImpAlg.Lambda]
typing_type [lemma, in ImpAlg.Lambda]
typing_cc [constructor, in ImpAlg.Lambda]
typing_fallE [constructor, in ImpAlg.Lambda]
typing_fallI [constructor, in ImpAlg.Lambda]
typing_app [constructor, in ImpAlg.Lambda]
typing_abs [constructor, in ImpAlg.Lambda]
typing_prf_var [constructor, in ImpAlg.Lambda]
typing_trm [inductive, in ImpAlg.Lambda]
typing_subst_trm [lemma, in ImpAlg.Adequacy]
typ_eq_subst [lemma, in ImpAlg.Lambda]
typ_peirce [definition, in ImpAlg.Lambda]
typ_arrow [constructor, in ImpAlg.Lambda]
typ_fall [constructor, in ImpAlg.Lambda]
typ_cvar [constructor, in ImpAlg.Lambda]
typ_fvar [constructor, in ImpAlg.Lambda]
typ_bvar [constructor, in ImpAlg.Lambda]
U
ub [definition, in ImpAlg.Lattices]union_empty [lemma, in ImpAlg.Lambda]
update [definition, in ImpAlg.Adequacy]
upwards_closure [definition, in ImpAlg.ImplicativeStructures]
up_closed_tsep [lemma, in ImpAlg.TensorAlgebras]
up_closed [projection, in ImpAlg.ImplicativeAlgebras]
up_closed_set [definition, in ImpAlg.Lattices]
W
W [definition, in ImpAlg.Combinators]other
_ ⋁ _ (ia_scope) [notation, in ImpAlg.Lattices]_ ⋀ _ (ia_scope) [notation, in ImpAlg.Lattices]
_ ≤ _ (ia_scope) [notation, in ImpAlg.Lattices]
_ ≤ _ (ia_scope) [notation, in ImpAlg.Lattices]
λ- _ (ia_scope) [notation, in ImpAlg.ImplicativeStructures]
_ ↪ _ (ia_scope) [notation, in ImpAlg.ImplicativeStructures]
_ ↦ _ (ia_scope) [notation, in ImpAlg.ImplicativeStructures]
_ ∈ʆ (pa_scope) [notation, in ImpAlg.ParAlgebras]
_ ⅋↦ _ (pa_scope) [notation, in ImpAlg.ParAlgebras]
¬ _ (pa_scope) [notation, in ImpAlg.ParAlgebras]
_ ⅋ _ (pa_scope) [notation, in ImpAlg.ParAlgebras]
_ ∈ʆ (ta_scope) [notation, in ImpAlg.TensorAlgebras]
_ ⨂↦ _ (ta_scope) [notation, in ImpAlg.TensorAlgebras]
_ ⨂ _ (ta_scope) [notation, in ImpAlg.TensorAlgebras]
_ ◃ _ [notation, in ImpAlg.TensorAlgebras]
_ @ _ [notation, in ImpAlg.ImplicativeAlgebras]
_ ∈ʆ [notation, in ImpAlg.ImplicativeAlgebras]
_ ≅ _ [notation, in ImpAlg.Ens]
_ @ _ [notation, in ImpAlg.ImplicativeStructures]
∩ _ [notation, in ImpAlg.Lattices]
⊓ [notation, in ImpAlg.Lattices]
⊔ [notation, in ImpAlg.Lattices]
⊤ [notation, in ImpAlg.Lattices]
⊥ [notation, in ImpAlg.Lattices]
⋂[ _ ] _ [notation, in ImpAlg.Lattices]
¬ _ [notation, in ImpAlg.BooleanAlgebras]
λ- _ [notation, in ImpAlg.ImplicativeAlgebras]
Notation Index
A
_ @⨂ _ [in ImpAlg.TensorAlgebras]λ⨂ _ [in ImpAlg.TensorAlgebras]
¬ _ [in ImpAlg.TensorAlgebras]
_ + _ [in ImpAlg.ParAlgebras]
_ ⊢ _ [in ImpAlg.ParAlgebras]
λ- _ (ia_scope) [in ImpAlg.Adequacy]
_ @ _ (ia_scope) [in ImpAlg.Adequacy]
_ ^t _ [in ImpAlg.Adequacy]
_ ^tc _ [in ImpAlg.Adequacy]
_ ^t^ _ [in ImpAlg.Adequacy]
_ ^v _ [in ImpAlg.Adequacy]
_ ^c _ [in ImpAlg.Adequacy]
_ ^^ _ [in ImpAlg.Adequacy]
{ _ ~t> _ } _ [in ImpAlg.Adequacy]
{ _ ~> _ } _ [in ImpAlg.Adequacy]
C
$ _ [in ImpAlg.Combinators][ _ ] _ [in ImpAlg.Combinators]
λ+ _ [in ImpAlg.Combinators]
D
_ |= _ : _ [in ImpAlg.Lambda]_ ^t _ [in ImpAlg.Lambda]
_ ^tc _ [in ImpAlg.Lambda]
_ ^t^ _ [in ImpAlg.Lambda]
_ ^v _ [in ImpAlg.Lambda]
_ ^c _ [in ImpAlg.Lambda]
_ ^^ _ [in ImpAlg.Lambda]
{ _ ~t> _ } _ [in ImpAlg.Lambda]
{ _ ~> _ } _ [in ImpAlg.Lambda]
I
_ ⊕ _ [in ImpAlg.ImplicativeAlgebras]_ × _ [in ImpAlg.ImplicativeAlgebras]
_ ≈ _ [in ImpAlg.ImplicativeAlgebras]
_ ⊢ _ [in ImpAlg.ImplicativeAlgebras]
$ _ [in ImpAlg.ImplicativeAlgebras]
[ _ ] _ [in ImpAlg.ImplicativeAlgebras]
[∀] _ [in ImpAlg.ImplicativeAlgebras]
[∃] _ [in ImpAlg.ImplicativeAlgebras]
¬ _ [in ImpAlg.ImplicativeAlgebras]
λ+ _ [in ImpAlg.ImplicativeAlgebras]
L
µ{[],}. _ [in ImpAlg.LPar]µ{}. _ [in ImpAlg.LPar]
µ[]. _ [in ImpAlg.LPar]
µ-. _ [in ImpAlg.LPar]
[ _ ] [in ImpAlg.LPar]
{ _ , _ } [in ImpAlg.LPar]
µ+. _ [in ImpAlg.LPar]
_ ◃ _ [in ImpAlg.LPar]
< _ | _ > [in ImpAlg.LPar]
_ ∈(≤) [in ImpAlg.LPar]
_ ◃ _ (lt_scope) [in ImpAlg.LTensor]
_ ∈(≤) [in ImpAlg.LTensor]
< _ | _ > [in ImpAlg.LTensor]
[ _ ] [in ImpAlg.LTensor]
{ _ , _ } [in ImpAlg.LTensor]
¬ _ [in ImpAlg.LTensor]
µ+. _ [in ImpAlg.LTensor]
µ-. _ [in ImpAlg.LTensor]
µ[]. _ [in ImpAlg.LTensor]
µ{}. _ [in ImpAlg.LTensor]
R
_ ◃ _ (ia_scope) [in ImpAlg.TensorAlgebras]¬⁻¹ _ (ia_scope) [in ImpAlg.TensorAlgebras]
_ ⨂↦ _ [in ImpAlg.TensorAlgebras]
_ ⨂ _ [in ImpAlg.TensorAlgebras]
¬ _ [in ImpAlg.TensorAlgebras]
other
_ ⋁ _ (ia_scope) [in ImpAlg.Lattices]_ ⋀ _ (ia_scope) [in ImpAlg.Lattices]
_ ≤ _ (ia_scope) [in ImpAlg.Lattices]
_ ≤ _ (ia_scope) [in ImpAlg.Lattices]
λ- _ (ia_scope) [in ImpAlg.ImplicativeStructures]
_ ↪ _ (ia_scope) [in ImpAlg.ImplicativeStructures]
_ ↦ _ (ia_scope) [in ImpAlg.ImplicativeStructures]
_ ∈ʆ (pa_scope) [in ImpAlg.ParAlgebras]
_ ⅋↦ _ (pa_scope) [in ImpAlg.ParAlgebras]
¬ _ (pa_scope) [in ImpAlg.ParAlgebras]
_ ⅋ _ (pa_scope) [in ImpAlg.ParAlgebras]
_ ∈ʆ (ta_scope) [in ImpAlg.TensorAlgebras]
_ ⨂↦ _ (ta_scope) [in ImpAlg.TensorAlgebras]
_ ⨂ _ (ta_scope) [in ImpAlg.TensorAlgebras]
_ ◃ _ [in ImpAlg.TensorAlgebras]
_ @ _ [in ImpAlg.ImplicativeAlgebras]
_ ∈ʆ [in ImpAlg.ImplicativeAlgebras]
_ ≅ _ [in ImpAlg.Ens]
_ @ _ [in ImpAlg.ImplicativeStructures]
∩ _ [in ImpAlg.Lattices]
⊓ [in ImpAlg.Lattices]
⊔ [in ImpAlg.Lattices]
⊤ [in ImpAlg.Lattices]
⊥ [in ImpAlg.Lattices]
⋂[ _ ] _ [in ImpAlg.Lattices]
¬ _ [in ImpAlg.BooleanAlgebras]
λ- _ [in ImpAlg.ImplicativeAlgebras]
Library Index
A
AdequacyB
BooleanAlgebrasC
CombinatorsD
DummiesE
EnsH
HeytingAlgebrasI
ImplicativeAlgebrasImplicativeStructures
L
LambdaLattices
LPar
LTensor
P
ParAlgebrasT
TensorAlgebrasTheorems
Lemma Index
A
absurd [in ImpAlg.ParAlgebras]absurd_aux [in ImpAlg.ParAlgebras]
absurd_aux_ter [in ImpAlg.ParAlgebras]
abs_mon [in ImpAlg.ImplicativeStructures]
adequacy [in ImpAlg.Adequacy]
adequacy_empty [in ImpAlg.Adequacy]
adjunction [in ImpAlg.ImplicativeStructures]
app_CHA [in ImpAlg.HeytingAlgebras]
app_closed [in ImpAlg.ImplicativeAlgebras]
app_CBA [in ImpAlg.BooleanAlgebras]
app_min [in ImpAlg.ImplicativeStructures]
app_eta [in ImpAlg.ImplicativeStructures]
app_beta [in ImpAlg.ImplicativeStructures]
app_mon [in ImpAlg.ImplicativeStructures]
app_mon_r [in ImpAlg.ImplicativeStructures]
app_mon_l [in ImpAlg.ImplicativeStructures]
app_closed [in ImpAlg.ParAlgebras]
arrow_tsep_psep [in ImpAlg.TensorAlgebras]
arrow_entails_mon [in ImpAlg.ImplicativeAlgebras]
arrow_entails_mon_l [in ImpAlg.ImplicativeAlgebras]
arrow_entails_mon_r [in ImpAlg.ImplicativeAlgebras]
arrow_bot [in ImpAlg.ImplicativeStructures]
arrow_prenex [in ImpAlg.ImplicativeStructures]
arrow_mon [in ImpAlg.ImplicativeStructures]
arrow_precomp_par_assoc [in ImpAlg.ParAlgebras]
arrow_pneg [in ImpAlg.ParAlgebras]
arrow_swap_psep [in ImpAlg.ParAlgebras]
arrow_meet_r_aux [in ImpAlg.ParAlgebras]
arrow_meet_r [in ImpAlg.ParAlgebras]
B
BA_TS5 [in ImpAlg.BooleanAlgebras]BA_TS4 [in ImpAlg.BooleanAlgebras]
BA_TS3 [in ImpAlg.BooleanAlgebras]
BA_TS2 [in ImpAlg.BooleanAlgebras]
BA_TS1 [in ImpAlg.BooleanAlgebras]
BA_PS5 [in ImpAlg.BooleanAlgebras]
BA_PS4 [in ImpAlg.BooleanAlgebras]
BA_PS3 [in ImpAlg.BooleanAlgebras]
BA_PS2 [in ImpAlg.BooleanAlgebras]
BA_PS1 [in ImpAlg.BooleanAlgebras]
BA_cc [in ImpAlg.BooleanAlgebras]
BA_S [in ImpAlg.BooleanAlgebras]
BA_K [in ImpAlg.BooleanAlgebras]
betarule [in ImpAlg.ImplicativeStructures]
beta_red [in ImpAlg.ImplicativeStructures]
bot_meet [in ImpAlg.BooleanAlgebras]
by_refl [in ImpAlg.Lattices]
C
cc_polymorph [in ImpAlg.Lambda]codom_concat [in ImpAlg.Lambda]
codom_push [in ImpAlg.Lambda]
codom_single [in ImpAlg.Lambda]
codom_empty [in ImpAlg.Lambda]
combinatorLambda [in ImpAlg.Combinators]
combinatorSK [in ImpAlg.Combinators]
combinator_trm_translated [in ImpAlg.Combinators]
combinator_translated [in ImpAlg.Combinators]
contraposition_r [in ImpAlg.ImplicativeAlgebras]
contraposition_l [in ImpAlg.ImplicativeAlgebras]
cord_join [in ImpAlg.LTensor]
cord_meet [in ImpAlg.LTensor]
cord_subset [in ImpAlg.LTensor]
cord_mon [in ImpAlg.LTensor]
cord_join [in ImpAlg.LPar]
cord_meet [in ImpAlg.LPar]
cord_subset [in ImpAlg.LPar]
cord_mon [in ImpAlg.LPar]
C6_p [in ImpAlg.ParAlgebras]
C7 [in ImpAlg.ParAlgebras]
D
dn [in ImpAlg.ImplicativeAlgebras]dne [in ImpAlg.ImplicativeAlgebras]
dne [in ImpAlg.ParAlgebras]
dne_entails [in ImpAlg.ParAlgebras]
dni [in ImpAlg.ImplicativeAlgebras]
dni [in ImpAlg.ParAlgebras]
dni_entails [in ImpAlg.ParAlgebras]
double_meet_elim [in ImpAlg.Lattices]
double_meet [in ImpAlg.Lattices]
double_neg [in ImpAlg.BooleanAlgebras]
dummy_top_abs [in ImpAlg.Dummies]
dummy_top_app [in ImpAlg.Dummies]
E
empty_fv_typ_subst [in ImpAlg.Adequacy]empty_fv_trm_subst [in ImpAlg.Adequacy]
entails_half_adj [in ImpAlg.ImplicativeAlgebras]
entails_trans [in ImpAlg.ImplicativeAlgebras]
entails_refl [in ImpAlg.ImplicativeAlgebras]
equiv_sep [in ImpAlg.ImplicativeAlgebras]
etarule [in ImpAlg.ImplicativeStructures]
exfalso_S [in ImpAlg.ImplicativeAlgebras]
extra_hyp_ter [in ImpAlg.ParAlgebras]
extra_hyp [in ImpAlg.ParAlgebras]
ex_falso [in ImpAlg.ParAlgebras]
F
fn_typ_type [in ImpAlg.Lambda]fn_typ_type_aux [in ImpAlg.Lambda]
fn_typ_fall [in ImpAlg.Lambda]
fn_typ_fall_aux [in ImpAlg.Lambda]
fn_typ_fall_Aux [in ImpAlg.Lambda]
fn_typ_arrow [in ImpAlg.Lambda]
fn_typ_fall_bvar [in ImpAlg.Lambda]
from_list_nil_inv [in ImpAlg.Lambda]
from_list_append [in ImpAlg.Lambda]
fv_open_trm [in ImpAlg.Lambda]
fv_typ_subst [in ImpAlg.Adequacy]
G
geq_S_S [in ImpAlg.Lambda]geq_1_S [in ImpAlg.Lambda]
glb_elim_intro [in ImpAlg.Lattices]
glb_unique [in ImpAlg.Lattices]
H
half_pmodus_ponens [in ImpAlg.ParAlgebras]ha_adjunction [in ImpAlg.ImplicativeAlgebras]
I
Id_SK [in ImpAlg.Combinators]II_neq_I [in ImpAlg.Dummies]
Impcc [in ImpAlg.ParAlgebras]
ImpK [in ImpAlg.ParAlgebras]
ImpS [in ImpAlg.ParAlgebras]
imp_meet [in ImpAlg.HeytingAlgebras]
imp_is_join [in ImpAlg.HeytingAlgebras]
imp_mon_r [in ImpAlg.HeytingAlgebras]
imp_mon_l [in ImpAlg.HeytingAlgebras]
imp_adj [in ImpAlg.HeytingAlgebras]
imp_lub [in ImpAlg.HeytingAlgebras]
imp_intro [in ImpAlg.HeytingAlgebras]
imp_self [in ImpAlg.HeytingAlgebras]
imp_elim [in ImpAlg.HeytingAlgebras]
imp_bot_pneg [in ImpAlg.ParAlgebras]
inf_comm [in ImpAlg.Lattices]
inf_comm_aux [in ImpAlg.Lattices]
inf_elim_trans [in ImpAlg.Lattices]
inf_pneg [in ImpAlg.ParAlgebras]
in_revsep [in ImpAlg.TensorAlgebras]
in_pre_pneg [in ImpAlg.TensorAlgebras]
I_neq_SKK_dum [in ImpAlg.Dummies]
J
join_same_set [in ImpAlg.Lattices]join_subset [in ImpAlg.Lattices]
join_elim_trans [in ImpAlg.Lattices]
join_set_lub [in ImpAlg.Lattices]
join_emptyset [in ImpAlg.Lattices]
join_top_r [in ImpAlg.Lattices]
join_top_l [in ImpAlg.Lattices]
join_bot_r [in ImpAlg.Lattices]
join_bot_l [in ImpAlg.Lattices]
join_meet_completeness [in ImpAlg.Lattices]
join_mon_r [in ImpAlg.Lattices]
join_mon_l [in ImpAlg.Lattices]
join_lub [in ImpAlg.Lattices]
join_ub_r [in ImpAlg.Lattices]
join_ub_l [in ImpAlg.Lattices]
join_consistent [in ImpAlg.Lattices]
join_neg_l [in ImpAlg.BooleanAlgebras]
join_distributive_l [in ImpAlg.BooleanAlgebras]
join_meet_set [in ImpAlg.BooleanAlgebras]
join3_neg3 [in ImpAlg.BooleanAlgebras]
join3_neg1 [in ImpAlg.BooleanAlgebras]
L
lambda_B [in ImpAlg.Combinators]lambda_Easy [in ImpAlg.Combinators]
lambda_W [in ImpAlg.Combinators]
lambda_S [in ImpAlg.Combinators]
lambda_K [in ImpAlg.Combinators]
lambda_Id [in ImpAlg.Combinators]
lub_elim_intro [in ImpAlg.Lattices]
lub_unique [in ImpAlg.Lattices]
M
map_pred_S [in ImpAlg.Lambda]map_pred_append [in ImpAlg.Lambda]
map_pred_cons [in ImpAlg.Lambda]
meet_same_set [in ImpAlg.Lattices]
meet_same_set_le [in ImpAlg.Lattices]
meet_subset [in ImpAlg.Lattices]
meet_fam_intro [in ImpAlg.Lattices]
meet_fam_elim [in ImpAlg.Lattices]
meet_comm [in ImpAlg.Lattices]
meet_comm_aux [in ImpAlg.Lattices]
meet_elim_trans [in ImpAlg.Lattices]
meet_set_glb [in ImpAlg.Lattices]
meet_emptyset [in ImpAlg.Lattices]
meet_top_r [in ImpAlg.Lattices]
meet_top_l [in ImpAlg.Lattices]
meet_bot_r [in ImpAlg.Lattices]
meet_bot_l [in ImpAlg.Lattices]
meet_join_completeness [in ImpAlg.Lattices]
meet_mon_r [in ImpAlg.Lattices]
meet_mon_l [in ImpAlg.Lattices]
meet_glb [in ImpAlg.Lattices]
meet_lb_r [in ImpAlg.Lattices]
meet_lb_l [in ImpAlg.Lattices]
meet_join [in ImpAlg.Lattices]
meet_distributive_l [in ImpAlg.BooleanAlgebras]
meet_join_set [in ImpAlg.BooleanAlgebras]
modus_ponens_revsep [in ImpAlg.TensorAlgebras]
modus_ponens_later [in ImpAlg.ImplicativeAlgebras]
modus_ponens_parrow [in ImpAlg.ParAlgebras]
mod_ponens [in ImpAlg.ImplicativeAlgebras]
mod_pon_app [in ImpAlg.ImplicativeStructures]
mod_pon_cong [in ImpAlg.ParAlgebras]
mod_pon_inf_ter [in ImpAlg.ParAlgebras]
mod_pon_inf [in ImpAlg.ParAlgebras]
mod_pon_app [in ImpAlg.ParAlgebras]
mun_beta [in ImpAlg.LTensor]
mun_eta [in ImpAlg.LTensor]
mun_mon [in ImpAlg.LTensor]
mun_beta [in ImpAlg.LPar]
mun_eta [in ImpAlg.LPar]
mun_mon [in ImpAlg.LPar]
mup_eta [in ImpAlg.LTensor]
mup_beta [in ImpAlg.LTensor]
mup_mon [in ImpAlg.LTensor]
mup_eta [in ImpAlg.LPar]
mup_beta [in ImpAlg.LPar]
mup_mon [in ImpAlg.LPar]
mu_neg_beta [in ImpAlg.LTensor]
mu_pair_beta [in ImpAlg.LTensor]
mu_neg_eta [in ImpAlg.LTensor]
mu_pair_eta [in ImpAlg.LTensor]
mu_neg_mon [in ImpAlg.LTensor]
mu_pair_mon [in ImpAlg.LTensor]
mu_abs_char [in ImpAlg.LPar]
mu_neg_beta [in ImpAlg.LPar]
mu_pair_beta [in ImpAlg.LPar]
mu_neg_eta [in ImpAlg.LPar]
mu_pair_eta [in ImpAlg.LPar]
mu_neg_mon [in ImpAlg.LPar]
mu_pair_mon [in ImpAlg.LPar]
N
neg_join_set [in ImpAlg.BooleanAlgebras]neg_meet_set [in ImpAlg.BooleanAlgebras]
neg_mon [in ImpAlg.BooleanAlgebras]
neg_meet [in ImpAlg.BooleanAlgebras]
neg_join [in ImpAlg.BooleanAlgebras]
neg_bot [in ImpAlg.BooleanAlgebras]
neg_top [in ImpAlg.BooleanAlgebras]
neg_complement [in ImpAlg.BooleanAlgebras]
O
open_typ_com_ct [in ImpAlg.Lambda]open_typ_com_ff [in ImpAlg.Lambda]
open_typ_com_cc [in ImpAlg.Lambda]
open_typ_com_cf [in ImpAlg.Lambda]
open_typ_type [in ImpAlg.Lambda]
open_typ_fn [in ImpAlg.Lambda]
open_trm_def [in ImpAlg.Lambda]
or_par [in ImpAlg.ParAlgebras]
or_par_gen [in ImpAlg.ParAlgebras]
P
ParAlgebra_is_ImpAlgebra [in ImpAlg.Theorems]parrow_meet [in ImpAlg.ParAlgebras]
parrow_mon [in ImpAlg.ParAlgebras]
parrow_mon_r [in ImpAlg.ParAlgebras]
parrow_mon_l [in ImpAlg.ParAlgebras]
ParStructure_is_ImplicativeStructure [in ImpAlg.Theorems]
par_or [in ImpAlg.ParAlgebras]
par_or_gen [in ImpAlg.ParAlgebras]
par_swap_psep [in ImpAlg.ParAlgebras]
par_assoc_psep [in ImpAlg.ParAlgebras]
par_comm_psep [in ImpAlg.ParAlgebras]
par_assoc_r [in ImpAlg.ParAlgebras]
par_meet_f_r [in ImpAlg.ParAlgebras]
par_top_r [in ImpAlg.ParAlgebras]
par_top_l [in ImpAlg.ParAlgebras]
par_mon_r [in ImpAlg.ParAlgebras]
par_mon_l [in ImpAlg.ParAlgebras]
pneg_imp_bot [in ImpAlg.ParAlgebras]
pneg_arrow [in ImpAlg.ParAlgebras]
pneg_top [in ImpAlg.ParAlgebras]
pre_upclosed_rev [in ImpAlg.Lattices]
pre_comp_arr_bi [in ImpAlg.ParAlgebras]
prodt_intro [in ImpAlg.ImplicativeAlgebras]
prodt_r [in ImpAlg.ImplicativeAlgebras]
prodt_l [in ImpAlg.ImplicativeAlgebras]
psep_Impcc [in ImpAlg.ParAlgebras]
psep_ImpS [in ImpAlg.ParAlgebras]
psep_ImpK [in ImpAlg.ParAlgebras]
psep_cc [in ImpAlg.ParAlgebras]
psep_S [in ImpAlg.ParAlgebras]
psep_K [in ImpAlg.ParAlgebras]
psep_PS4_r [in ImpAlg.ParAlgebras]
psep_PS2_l [in ImpAlg.ParAlgebras]
psep_PI [in ImpAlg.ParAlgebras]
psep_C7 [in ImpAlg.ParAlgebras]
psep_PC6_ter [in ImpAlg.ParAlgebras]
psep_PC6 [in ImpAlg.ParAlgebras]
ps_adjunction [in ImpAlg.ParAlgebras]
ps_app_min [in ImpAlg.ParAlgebras]
ps_etarule [in ImpAlg.ParAlgebras]
ps_betarule [in ImpAlg.ParAlgebras]
ps_abs_mon [in ImpAlg.ParAlgebras]
ps_app_mon [in ImpAlg.ParAlgebras]
PS1_lpar [in ImpAlg.LPar]
PS2_lpar [in ImpAlg.LPar]
PS2_lpar_aux [in ImpAlg.LPar]
PS3_lpar [in ImpAlg.LPar]
PS4_lpar_aux [in ImpAlg.LPar]
PS5_lpar [in ImpAlg.LPar]
R
realizer_later [in ImpAlg.ImplicativeAlgebras]realize_update [in ImpAlg.Adequacy]
realize_inv [in ImpAlg.Adequacy]
reductio_ad_absurdum [in ImpAlg.ParAlgebras]
remove_pred_0 [in ImpAlg.Lambda]
remove_pred [in ImpAlg.Lambda]
remove_comm [in ImpAlg.Lambda]
remove_0_def [in ImpAlg.Lambda]
remove_append [in ImpAlg.Lambda]
remove_0_incl [in ImpAlg.Lambda]
remove_0_cons_0 [in ImpAlg.Lambda]
revsep_TS5 [in ImpAlg.TensorAlgebras]
revsep_TS4 [in ImpAlg.TensorAlgebras]
revsep_TS3 [in ImpAlg.TensorAlgebras]
revsep_TS2 [in ImpAlg.TensorAlgebras]
revsep_TS1 [in ImpAlg.TensorAlgebras]
rev_pneg_meet [in ImpAlg.TensorAlgebras]
rev_par_meet_r [in ImpAlg.TensorAlgebras]
rev_par_meet_l [in ImpAlg.TensorAlgebras]
rev_pneg_mon [in ImpAlg.TensorAlgebras]
rev_par_mon [in ImpAlg.TensorAlgebras]
rev_tneg_join [in ImpAlg.TensorAlgebras]
rev_tensor_join_r [in ImpAlg.TensorAlgebras]
rev_tensor_join_l [in ImpAlg.TensorAlgebras]
rev_tneg_mon [in ImpAlg.TensorAlgebras]
rev_tensor_mon [in ImpAlg.TensorAlgebras]
rev_consistent [in ImpAlg.Lattices]
rev_trans [in ImpAlg.Lattices]
rev_antisym [in ImpAlg.Lattices]
rev_refl [in ImpAlg.Lattices]
Rev_TensorStructure_is_ParStructure [in ImpAlg.Theorems]
Rev_ParAlgebra_is_TensorAlgebra [in ImpAlg.Theorems]
Rev_ParStructure_is_TensorStructure [in ImpAlg.Theorems]
S
same_set_trans [in ImpAlg.Ens]same_set_sym [in ImpAlg.Ens]
same_set_refl [in ImpAlg.Ens]
semi_adjunction [in ImpAlg.TensorAlgebras]
sep_Easy [in ImpAlg.ImplicativeAlgebras]
sep_W [in ImpAlg.ImplicativeAlgebras]
sep_typ [in ImpAlg.ImplicativeAlgebras]
sep_term [in ImpAlg.ImplicativeAlgebras]
sep_SK [in ImpAlg.ImplicativeAlgebras]
sep_comb [in ImpAlg.ImplicativeAlgebras]
sep_Id [in ImpAlg.ImplicativeAlgebras]
size_typ_arrow [in ImpAlg.Lambda]
size_typ_plus_S [in ImpAlg.Lambda]
size_typ_S [in ImpAlg.Lambda]
size_typ_open_f [in ImpAlg.Lambda]
size_typ_open [in ImpAlg.Lambda]
size_typ_le_1 [in ImpAlg.Lambda]
size_typ_ind [in ImpAlg.Lambda]
size_typ_ind_gen [in ImpAlg.Lambda]
size_typ_induction [in ImpAlg.Lambda]
size_typ_not_0 [in ImpAlg.Lambda]
size_open [in ImpAlg.Lambda]
size_le_1 [in ImpAlg.Lambda]
size_ind [in ImpAlg.Lambda]
size_ind_gen [in ImpAlg.Lambda]
size_induction [in ImpAlg.Lambda]
size_not_0 [in ImpAlg.Lambda]
subset_trans [in ImpAlg.Lambda]
subst_trm_update [in ImpAlg.Adequacy]
subst_trm_update_open [in ImpAlg.Adequacy]
subst_typ_update [in ImpAlg.Adequacy]
subst_typ_var [in ImpAlg.Adequacy]
subtyping [in ImpAlg.ImplicativeAlgebras]
sumt_elim [in ImpAlg.ImplicativeAlgebras]
sumt_r [in ImpAlg.ImplicativeAlgebras]
sumt_l [in ImpAlg.ImplicativeAlgebras]
swap_imp [in ImpAlg.ParAlgebras]
swap_l [in ImpAlg.ParAlgebras]
swap_r [in ImpAlg.ParAlgebras]
S1_p [in ImpAlg.ParAlgebras]
S2_p [in ImpAlg.ParAlgebras]
S3_p [in ImpAlg.ParAlgebras]
S4_p [in ImpAlg.ParAlgebras]
S6_gen [in ImpAlg.ParAlgebras]
T
tensor_bot_r [in ImpAlg.TensorAlgebras]tensor_bot_l [in ImpAlg.TensorAlgebras]
tensor_mon_r [in ImpAlg.TensorAlgebras]
tensor_mon_l [in ImpAlg.TensorAlgebras]
tneg_bot [in ImpAlg.TensorAlgebras]
top_join [in ImpAlg.BooleanAlgebras]
translated_Easy [in ImpAlg.Combinators]
translated_W [in ImpAlg.Combinators]
translated_S [in ImpAlg.Combinators]
translated_K [in ImpAlg.Combinators]
translated_Id [in ImpAlg.Combinators]
translated_peirce [in ImpAlg.Adequacy]
translated_typ_unique [in ImpAlg.Adequacy]
translated_unique [in ImpAlg.Adequacy]
trans_typ_open [in ImpAlg.Adequacy]
trans_typ_update [in ImpAlg.Adequacy]
trans_correct [in ImpAlg.Adequacy]
trans_typ_var [in ImpAlg.Adequacy]
trans_typ_arrow [in ImpAlg.Adequacy]
trans_typ_fold [in ImpAlg.Adequacy]
trans_typ_fioul [in ImpAlg.Adequacy]
trans_typ_fall [in ImpAlg.Adequacy]
true_S [in ImpAlg.ImplicativeAlgebras]
ts_half_adjunction [in ImpAlg.TensorAlgebras]
type_case [in ImpAlg.ImplicativeAlgebras]
type_inj2 [in ImpAlg.ImplicativeAlgebras]
type_inj1 [in ImpAlg.ImplicativeAlgebras]
type_proj2 [in ImpAlg.ImplicativeAlgebras]
type_proj1 [in ImpAlg.ImplicativeAlgebras]
type_pair [in ImpAlg.ImplicativeAlgebras]
type_ex_elim [in ImpAlg.ImplicativeAlgebras]
type_ex_intro [in ImpAlg.ImplicativeAlgebras]
type_fa_elim [in ImpAlg.ImplicativeAlgebras]
type_fa_intro [in ImpAlg.ImplicativeAlgebras]
type_subst [in ImpAlg.Lambda]
type_peirce [in ImpAlg.Lambda]
typing_empty_closed [in ImpAlg.Combinators]
typing_fv_trm [in ImpAlg.Lambda]
typing_fv_trm_aux [in ImpAlg.Lambda]
typing_term [in ImpAlg.Lambda]
typing_type [in ImpAlg.Lambda]
typing_subst_trm [in ImpAlg.Adequacy]
typ_eq_subst [in ImpAlg.Lambda]
U
union_empty [in ImpAlg.Lambda]up_closed_tsep [in ImpAlg.TensorAlgebras]
Axiom Index
L
lambdaSK [in ImpAlg.Combinators]Constructor Index
C
comb_app [in ImpAlg.Combinators]comb_Id [in ImpAlg.Combinators]
comb_K [in ImpAlg.Combinators]
comb_S [in ImpAlg.Combinators]
R
real_push [in ImpAlg.Adequacy]real_empty [in ImpAlg.Adequacy]
T
termSK_app [in ImpAlg.Combinators]term_K [in ImpAlg.Combinators]
term_S [in ImpAlg.Combinators]
term_cc [in ImpAlg.Lambda]
term_app [in ImpAlg.Lambda]
term_abs [in ImpAlg.Lambda]
term_var [in ImpAlg.Lambda]
trm_cc [in ImpAlg.Lambda]
trm_app [in ImpAlg.Lambda]
trm_abs [in ImpAlg.Lambda]
trm_cvar [in ImpAlg.Lambda]
trm_fvar [in ImpAlg.Lambda]
trm_bvar [in ImpAlg.Lambda]
tr_typ_fall [in ImpAlg.Adequacy]
tr_typ_arrow [in ImpAlg.Adequacy]
tr_typ_var [in ImpAlg.Adequacy]
tr_cc [in ImpAlg.Adequacy]
tr_app [in ImpAlg.Adequacy]
tr_abs [in ImpAlg.Adequacy]
tr_var [in ImpAlg.Adequacy]
type_arrow [in ImpAlg.Lambda]
type_fall [in ImpAlg.Lambda]
type_cvar [in ImpAlg.Lambda]
type_fvar [in ImpAlg.Lambda]
typing_cc [in ImpAlg.Lambda]
typing_fallE [in ImpAlg.Lambda]
typing_fallI [in ImpAlg.Lambda]
typing_app [in ImpAlg.Lambda]
typing_abs [in ImpAlg.Lambda]
typing_prf_var [in ImpAlg.Lambda]
typ_arrow [in ImpAlg.Lambda]
typ_fall [in ImpAlg.Lambda]
typ_cvar [in ImpAlg.Lambda]
typ_fvar [in ImpAlg.Lambda]
typ_bvar [in ImpAlg.Lambda]
Projection Index
A
arrow [in ImpAlg.ImplicativeStructures]arrow_meet [in ImpAlg.ImplicativeStructures]
arrow_mon_r [in ImpAlg.ImplicativeStructures]
arrow_mon_l [in ImpAlg.ImplicativeStructures]
B
bot [in ImpAlg.Lattices]bot_min [in ImpAlg.Lattices]
C
consistent [in ImpAlg.Lattices]I
imp [in ImpAlg.HeytingAlgebras]imp_sup [in ImpAlg.HeytingAlgebras]
J
join [in ImpAlg.Lattices]join_intro [in ImpAlg.Lattices]
join_elim [in ImpAlg.Lattices]
join_set [in ImpAlg.Lattices]
join_idempotent [in ImpAlg.Lattices]
join_absorptive [in ImpAlg.Lattices]
join_associative [in ImpAlg.Lattices]
join_commutative [in ImpAlg.Lattices]
join_neg [in ImpAlg.BooleanAlgebras]
join_distributive [in ImpAlg.BooleanAlgebras]
M
meet [in ImpAlg.Lattices]meet_intro [in ImpAlg.Lattices]
meet_elim [in ImpAlg.Lattices]
meet_set [in ImpAlg.Lattices]
meet_idempotent [in ImpAlg.Lattices]
meet_absorptive [in ImpAlg.Lattices]
meet_associative [in ImpAlg.Lattices]
meet_commutative [in ImpAlg.Lattices]
meet_neg [in ImpAlg.BooleanAlgebras]
meet_distributive [in ImpAlg.BooleanAlgebras]
modus_ponens [in ImpAlg.ImplicativeAlgebras]
N
neg [in ImpAlg.BooleanAlgebras]O
ord [in ImpAlg.Lattices]ord_trans [in ImpAlg.Lattices]
ord_antisym [in ImpAlg.Lattices]
ord_refl [in ImpAlg.Lattices]
P
par [in ImpAlg.ParAlgebras]par_meet_r [in ImpAlg.ParAlgebras]
par_meet_l [in ImpAlg.ParAlgebras]
par_mon [in ImpAlg.ParAlgebras]
pmodus_ponens [in ImpAlg.ParAlgebras]
pneg [in ImpAlg.ParAlgebras]
pneg_meet [in ImpAlg.ParAlgebras]
pneg_mon [in ImpAlg.ParAlgebras]
psep [in ImpAlg.ParAlgebras]
psep_PS5 [in ImpAlg.ParAlgebras]
psep_PS4 [in ImpAlg.ParAlgebras]
psep_PS3 [in ImpAlg.ParAlgebras]
psep_PS2 [in ImpAlg.ParAlgebras]
psep_PS1 [in ImpAlg.ParAlgebras]
pup_closed [in ImpAlg.ParAlgebras]
S
separator [in ImpAlg.ImplicativeAlgebras]sep_cc [in ImpAlg.ImplicativeAlgebras]
sep_S [in ImpAlg.ImplicativeAlgebras]
sep_K [in ImpAlg.ImplicativeAlgebras]
T
tensor [in ImpAlg.TensorAlgebras]tensor_join_r [in ImpAlg.TensorAlgebras]
tensor_join_l [in ImpAlg.TensorAlgebras]
tensor_mon [in ImpAlg.TensorAlgebras]
tmodus_ponens [in ImpAlg.TensorAlgebras]
tneg [in ImpAlg.TensorAlgebras]
tneg_join [in ImpAlg.TensorAlgebras]
tneg_mon [in ImpAlg.TensorAlgebras]
top [in ImpAlg.Lattices]
top_max [in ImpAlg.Lattices]
tsep [in ImpAlg.TensorAlgebras]
tsep_TS5 [in ImpAlg.TensorAlgebras]
tsep_TS4 [in ImpAlg.TensorAlgebras]
tsep_TS3 [in ImpAlg.TensorAlgebras]
tsep_TS2 [in ImpAlg.TensorAlgebras]
tsep_TS1 [in ImpAlg.TensorAlgebras]
tup_closed [in ImpAlg.TensorAlgebras]
U
up_closed [in ImpAlg.ImplicativeAlgebras]Inductive Index
C
combinator [in ImpAlg.Combinators]R
realize [in ImpAlg.Adequacy]T
term [in ImpAlg.Lambda]termSK [in ImpAlg.Combinators]
translated [in ImpAlg.Adequacy]
translated_typ [in ImpAlg.Adequacy]
trm [in ImpAlg.Lambda]
typ [in ImpAlg.Lambda]
type [in ImpAlg.Lambda]
typing_trm [in ImpAlg.Lambda]
Section Index
A
About_TensorAlg [in ImpAlg.TensorAlgebras]About_TensorStruct [in ImpAlg.TensorAlgebras]
About_ParAlg [in ImpAlg.ParAlgebras]
Adequacy [in ImpAlg.Adequacy]
C
Combinators [in ImpAlg.Combinators]D
Definitions [in ImpAlg.Lambda]Dummy [in ImpAlg.Dummies]
I
IA [in ImpAlg.ImplicativeAlgebras]L
LPar_Encoding [in ImpAlg.LPar]LTensor [in ImpAlg.LTensor]
R
ReverseParAlg [in ImpAlg.TensorAlgebras]ReversePS [in ImpAlg.TensorAlgebras]
ReverseTS [in ImpAlg.TensorAlgebras]
Instance Index
A
arrow_set_Proper [in ImpAlg.ImplicativeStructures]B
BA_HA [in ImpAlg.BooleanAlgebras]C
CBA_TA [in ImpAlg.BooleanAlgebras]CBA_TS [in ImpAlg.BooleanAlgebras]
CBA_PA [in ImpAlg.BooleanAlgebras]
CBA_PS [in ImpAlg.BooleanAlgebras]
CBA_IA [in ImpAlg.BooleanAlgebras]
CBA_IS [in ImpAlg.BooleanAlgebras]
CBA_CHA [in ImpAlg.BooleanAlgebras]
CBL [in ImpAlg.Lattices]
CHA_IS [in ImpAlg.HeytingAlgebras]
cord_preOrder [in ImpAlg.LTensor]
cord_Transitive [in ImpAlg.LTensor]
cord_Reflexive [in ImpAlg.LTensor]
cord_preOrder [in ImpAlg.LPar]
cord_Transitive [in ImpAlg.LPar]
cord_Reflexive [in ImpAlg.LPar]
D
dummy_tensor [in ImpAlg.Dummies]dummy_par [in ImpAlg.Dummies]
dummy_imp_top [in ImpAlg.Dummies]
dummy_imp_r [in ImpAlg.Dummies]
J
join_set_Proper [in ImpAlg.Lattices]M
meet_set_Proper [in ImpAlg.Lattices]O
ok_Reflexive [in ImpAlg.LTensor]ok_Reflexive [in ImpAlg.LPar]
ord_Antisymmetric [in ImpAlg.Lattices]
ord_Transitive [in ImpAlg.Lattices]
ord_Reflexive [in ImpAlg.Lattices]
P
par_set_l_Proper [in ImpAlg.ParAlgebras]par_set_r_Proper [in ImpAlg.ParAlgebras]
PA_TA [in ImpAlg.TensorAlgebras]
PA_IA [in ImpAlg.ParAlgebras]
PS_TS [in ImpAlg.TensorAlgebras]
PS_IS [in ImpAlg.ParAlgebras]
S
same_set_Equiv [in ImpAlg.Ens]T
TS_PS [in ImpAlg.TensorAlgebras]Definition Index
A
abs [in ImpAlg.ImplicativeStructures]antiapp [in ImpAlg.TensorAlgebras]
anti_mon [in ImpAlg.Lattices]
app [in ImpAlg.ImplicativeStructures]
app_closure [in ImpAlg.ImplicativeStructures]
arrowtop [in ImpAlg.Dummies]
arrow_r [in ImpAlg.Dummies]
arrow_set [in ImpAlg.ImplicativeStructures]
arrow_set_r [in ImpAlg.ImplicativeStructures]
arrow_set_l [in ImpAlg.ImplicativeStructures]
B
B [in ImpAlg.Combinators]box [in ImpAlg.LTensor]
box [in ImpAlg.LPar]
C
case [in ImpAlg.ImplicativeAlgebras]cc [in ImpAlg.Adequacy]
closed [in ImpAlg.Combinators]
closed_typ [in ImpAlg.Combinators]
closed_typ [in ImpAlg.ImplicativeAlgebras]
codom [in ImpAlg.Combinators]
codom [in ImpAlg.ImplicativeAlgebras]
codom [in ImpAlg.Lambda]
compat_append [in ImpAlg.Lambda]
cord [in ImpAlg.LTensor]
cord [in ImpAlg.LPar]
E
Easy [in ImpAlg.Combinators]emptyset [in ImpAlg.Ens]
Ens [in ImpAlg.Ens]
entails [in ImpAlg.ImplicativeAlgebras]
entails [in ImpAlg.ParAlgebras]
env [in ImpAlg.Combinators]
env [in ImpAlg.ImplicativeAlgebras]
env [in ImpAlg.Lambda]
equivalence [in ImpAlg.ImplicativeAlgebras]
equivalence [in ImpAlg.ParAlgebras]
eta [in ImpAlg.TensorAlgebras]
eta [in ImpAlg.ImplicativeStructures]
existst [in ImpAlg.ImplicativeAlgebras]
ex_term [in ImpAlg.ImplicativeAlgebras]
F
fn_typ [in ImpAlg.Lambda]fn_typ_aux [in ImpAlg.Lambda]
forallt [in ImpAlg.ImplicativeAlgebras]
fv_typ [in ImpAlg.Combinators]
fv_trm [in ImpAlg.Combinators]
fv_typ [in ImpAlg.ImplicativeAlgebras]
fv_trm [in ImpAlg.ImplicativeAlgebras]
fv_typ [in ImpAlg.Lambda]
fv_trm [in ImpAlg.Lambda]
G
glb [in ImpAlg.Lattices]I
Id [in ImpAlg.Combinators]Idum [in ImpAlg.Dummies]
image_set [in ImpAlg.Lattices]
inf [in ImpAlg.Lattices]
inj1 [in ImpAlg.ImplicativeAlgebras]
inj2 [in ImpAlg.ImplicativeAlgebras]
in_list [in ImpAlg.Lambda]
IS [in ImpAlg.ParAlgebras]
J
join_family [in ImpAlg.Lattices]join_complete [in ImpAlg.Lattices]
K
K [in ImpAlg.Combinators]Kdum [in ImpAlg.Dummies]
L
lambdaB [in ImpAlg.Combinators]lambdaEasy [in ImpAlg.Combinators]
lambdaId [in ImpAlg.Combinators]
lambdaK [in ImpAlg.Combinators]
lambdaS [in ImpAlg.Combinators]
lambdaW [in ImpAlg.Combinators]
lb [in ImpAlg.Lattices]
lub [in ImpAlg.Lattices]
M
map_pred [in ImpAlg.Lambda]meet_family [in ImpAlg.Lattices]
meet_complete [in ImpAlg.Lattices]
min [in ImpAlg.Lattices]
mod_pon_closure [in ImpAlg.ImplicativeStructures]
mun [in ImpAlg.LTensor]
mun [in ImpAlg.LPar]
mup [in ImpAlg.LTensor]
mup [in ImpAlg.LPar]
mu_neg [in ImpAlg.LTensor]
mu_pair [in ImpAlg.LTensor]
mu_abs [in ImpAlg.LPar]
mu_neg [in ImpAlg.LPar]
mu_pair [in ImpAlg.LPar]
N
neg [in ImpAlg.Combinators]neg [in ImpAlg.ImplicativeAlgebras]
negbot [in ImpAlg.Dummies]
negtop [in ImpAlg.Dummies]
O
ok [in ImpAlg.LTensor]ok [in ImpAlg.LPar]
open_typ_fvar [in ImpAlg.Lambda]
open_typ [in ImpAlg.Lambda]
open_rec_typ [in ImpAlg.Lambda]
open_trm_var [in ImpAlg.Lambda]
open_trm [in ImpAlg.Lambda]
open_rec_trm [in ImpAlg.Lambda]
or [in ImpAlg.ParAlgebras]
P
pair [in ImpAlg.ImplicativeAlgebras]pairing [in ImpAlg.LTensor]
pairing [in ImpAlg.LPar]
parrow [in ImpAlg.ParAlgebras]
partop [in ImpAlg.Dummies]
par_assoc_l [in ImpAlg.ParAlgebras]
par_set [in ImpAlg.ParAlgebras]
par_set_l [in ImpAlg.ParAlgebras]
par_set_r [in ImpAlg.ParAlgebras]
Pcc [in ImpAlg.ParAlgebras]
PC6 [in ImpAlg.ParAlgebras]
PC6_ter [in ImpAlg.ParAlgebras]
PC7 [in ImpAlg.ParAlgebras]
PI [in ImpAlg.ParAlgebras]
PK [in ImpAlg.ParAlgebras]
preimage [in ImpAlg.Lattices]
preimage_set [in ImpAlg.Lattices]
pre_pneg_set [in ImpAlg.TensorAlgebras]
pre_pneg [in ImpAlg.TensorAlgebras]
prodt [in ImpAlg.ImplicativeAlgebras]
proj1 [in ImpAlg.ImplicativeAlgebras]
proj2 [in ImpAlg.ImplicativeAlgebras]
PS [in ImpAlg.ParAlgebras]
Pswap_l [in ImpAlg.ParAlgebras]
Pswap_r [in ImpAlg.ParAlgebras]
ps_mod_pon_closure [in ImpAlg.ParAlgebras]
ps_app_closure [in ImpAlg.ParAlgebras]
ps_upwards_closure [in ImpAlg.ParAlgebras]
PS1 [in ImpAlg.ParAlgebras]
PS2 [in ImpAlg.ParAlgebras]
PS2_l [in ImpAlg.ParAlgebras]
PS3 [in ImpAlg.ParAlgebras]
PS4 [in ImpAlg.ParAlgebras]
PS4_r [in ImpAlg.ParAlgebras]
PS5 [in ImpAlg.ParAlgebras]
R
remove [in ImpAlg.Lambda]remove_0 [in ImpAlg.Lambda]
rev [in ImpAlg.Lattices]
RevBooleanAlgebra [in ImpAlg.BooleanAlgebras]
RevBoundedLattice [in ImpAlg.Lattices]
RevCompleteBooleanAlgebra [in ImpAlg.BooleanAlgebras]
RevCompleteLattice [in ImpAlg.Lattices]
reverse [in ImpAlg.Lattices]
RevLattice [in ImpAlg.Lattices]
RevOrd [in ImpAlg.Lattices]
revsep [in ImpAlg.TensorAlgebras]
S
S [in ImpAlg.Combinators]same_set [in ImpAlg.Ens]
Sdum [in ImpAlg.Dummies]
size [in ImpAlg.Lambda]
size_typ [in ImpAlg.Lambda]
subset [in ImpAlg.Ens]
substitution [in ImpAlg.Adequacy]
subst_typ [in ImpAlg.Adequacy]
subst_trm [in ImpAlg.Adequacy]
Succ [in ImpAlg.Combinators]
sumt [in ImpAlg.ImplicativeAlgebras]
sup [in ImpAlg.Lattices]
T
tarr [in ImpAlg.TensorAlgebras]tarrow [in ImpAlg.TensorAlgebras]
tens [in ImpAlg.TensorAlgebras]
tensorbot [in ImpAlg.Dummies]
tensor_set [in ImpAlg.TensorAlgebras]
tensor_set_r [in ImpAlg.TensorAlgebras]
tensor_set_l [in ImpAlg.TensorAlgebras]
trans_typ [in ImpAlg.Adequacy]
trans_typ_aux [in ImpAlg.Adequacy]
TS [in ImpAlg.TensorAlgebras]
ts_app [in ImpAlg.TensorAlgebras]
ts_abs [in ImpAlg.TensorAlgebras]
TS1 [in ImpAlg.TensorAlgebras]
TS2 [in ImpAlg.TensorAlgebras]
TS3 [in ImpAlg.TensorAlgebras]
TS4 [in ImpAlg.TensorAlgebras]
TS5 [in ImpAlg.TensorAlgebras]
typ_peirce [in ImpAlg.Lambda]
U
ub [in ImpAlg.Lattices]update [in ImpAlg.Adequacy]
upwards_closure [in ImpAlg.ImplicativeStructures]
up_closed_set [in ImpAlg.Lattices]
W
W [in ImpAlg.Combinators]Record Index
B
BooleanAlgebra [in ImpAlg.BooleanAlgebras]BoundedLattice [in ImpAlg.Lattices]
C
CompleteBooleanAlgebra [in ImpAlg.BooleanAlgebras]CompleteHeytingAlgebra [in ImpAlg.HeytingAlgebras]
CompleteLattice [in ImpAlg.Lattices]
H
HeytingAlgebra [in ImpAlg.HeytingAlgebras]I
ImplicativeAlgebra [in ImpAlg.ImplicativeAlgebras]ImplicativeStructure [in ImpAlg.ImplicativeStructures]
L
Lattice [in ImpAlg.Lattices]O
Order [in ImpAlg.Lattices]P
ParAlgebra [in ImpAlg.ParAlgebras]ParStructure [in ImpAlg.ParAlgebras]
T
TensorAlgebra [in ImpAlg.TensorAlgebras]TensorStructure [in ImpAlg.TensorAlgebras]
| 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 | (873 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 | (89 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (15 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 | (406 entries) |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1 entry) |
| 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 | (41 entries) |
| Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (72 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 | (10 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 | (13 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 | (36 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 | (176 entries) |
| Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (14 entries) |