# gen_algebra_1 Theory

Various general-purpose definitions and theorems for the algebra theories are introduced.

A few unary predicates are defined.

Much of the theory concerns common properties of binary relations. Two developments are given, differing in whether relations with or without arguments are considered more fundamental.

Definitions are given for common properties (e.g. commutativity, associativity) of algebraic operators.

## Typed Definitions

p_subset *1
p_equiv *1
detach *1
detach_fun *1
refl *1
sym *1
trans *1
equiv_rel *1
preorder *1
symmetrize *1
eqfun_p *1
anti_sym *1
st_anti_sym *1
connex *1
order *1
linorder *1
strict_part *1
irrefl *1
binrel_eqv *1
binrel_le *1
ab_binrel *1
binrel_ap *1
dec_binrel *1
xxrefl *1
xxsym *1
xxtrans *1
xxsymmetrize *1
xxirrefl *1
xxanti_sym *1
xxst_anti_sym *1
xxconnex *1
xxorder *1
xxlinorder *1
refl_cl *1
sym_cl *1
s_part *1
qprop *3
ident *1
assoc *2
comm *1
inverse *2
bilinear *1
bilinear_p *1
action_p *1
dist_1op_2op_lr *1
fun_thru_1op *1
fun_thru_2op *1
cancel *1
monot *1
monotone *1
rels_iso *1

## Main Theorems

exists_det_fun *36
exists_det_fun_a *1
dec_alt_char *15
dec_alt_char_a *16
refl_functionality_wrt_iff *3
sym_functionality_wrt_iff *4
trans_functionality_wrt_iff *3
trans_rel_self_functionality *3
equiv_rel_subtyping *5
symmetrized_preorder *6
equiv_rel_iff *4
equiv_rel_functionality_wrt_iff *9
equiv_rel_self_functionality *12
squash_thru_equiv_rel *8
sq_stable__eqfun_p *2
eqfun_p_subtyping *6
anti_sym_functionality_wrt_iff *4
connex_functionality_wrt_iff *3
connex_functionality_wrt_implies *6
connex_iff_trichot *7
order_functionality_wrt_iff *4
linorder_functionality_wrt_iff *2
sq_stable__refl *1
sq_stable__sym *1
sq_stable__trans *1
sq_stable__anti_sym *1
sq_stable__connex *1
strict_part_irrefl *3
order_split *10
trans_imp_sp_trans *4
trans_imp_sp_trans_a *5
trans_imp_sp_trans_b *4
linorder_le_neg *5
linorder_lt_neg *5
binrel_eqv_transitivity *2
binrel_le_antisymmetry *3
binrel_eqv_weakening *3
binrel_eqv_inversion *2
binrel_eqv_functionality_wrt_breqv *5
binrel_le_transitivity *2
binrel_le_weakening *2
ab_binrel_functionality *3
binrel_ap_functionality_wrt_breqv *3
xxrefl_functionality_wrt_breqv *3
xxsym_functionality_wrt_breqv *4
xxtrans_functionality_wrt_breqv *4
xxanti_sym_functionality_wrt_breqv *4
xxconnex_functionality_wrt_breqv *4
xxorder_functionality_wrt_breqv *4
xxorder_eq_order *3
s_part_functionality_wrt_breqv *3
s_part_char *1
xxorder_split *4
xxtrans_imp_sp_trans *5
refl_cl_is_order *14
irrefl_trans_imp_sasym *4
xxconnex_iff_trichot *4
xxconnex_iff_trichot_a *7
rel_le_refl_cl_sp *7
refl_cl_sp_le_rel *4
refl_cl_sp_cancel *3
rel_le_sp_refl_cl *8
sp_refl_cl_le_rel *5
sp_refl_cl_cancel *2
quot_elim *7
all_quot_elim *10
sq_stable__ident *2
sq_stable__assoc *3
sq_stable__comm *2
sq_stable__inverse *2
sq_stable__bilinear *2
bilinear_comm_elim *4
sq_stable__bilinear_p *1
sq_stable__action_p *1
sq_stable__dist_1op_2op_lr *1
sq_stable__fun_thru_1op *1
sq_stable__fun_thru_2op *1
sq_stable__cancel *1
sq_stable__monot *1
monot_functionality *2
assoc_shift *4
comm_shift *4
cancel_shift *5
eqfun_p_shift *5
sym_shift *2
trans_shift *3
connex_shift *2
anti_sym_shift *2
refl_shift *2
monot_shift *3