perms_1 Theory


Summary of Definitions


Typed Definitions

perm_sig *1
perm_f *1
perm_b *1
perm *1
mk_perm *1 *3

id_perm *9
inv_perm *8
comp_perm *16
perm_igrp *14

sym_grp *
swap *1
tswap *1
txpose_perm *6
rev_permf *2
rev_perm *5
app_permf *3
app_perm *9
conj_perm *2
extend_permf *5
extend_perm *12
restrict_perm *61

Main Theorems

mk_perm_eta_rw *8
perm_assoc *7
perm_ident *14
perm_inverse *19
perm_grp_inv_assoc *1
perm_grp_inv_id *1
perm_grp_inv_inv *1
perm_grp_inv_thru_op *1
perm_grp_inverse *1
perm_mon_ident *1
perm_mon_assoc *1
swap_order_2 *15
swap_sym *5
swap_id *6
swap_eval_1 *3
tswap_eval_1 *6
tswap_eval_2 *6
tswap_eval_3 *6
swap_eval_2 *3
swap_eval_3 *3
triple_swap *7
txpose_perm_inv *4
txpose_perm_order_2 *10
txpose_perm_sym *10
txpose_perm_id *10
triple_txpose_perm *12
rev_permf_order_2 *3
app_permf_id *4
app_permf_comp *10
extend_permf_over_id *6
extend_permf_over_comp *9
extend_permf_over_swap *9
extend_perm_over_id *11
extend_perm_over_comp *12
extend_perm_over_txpose *18
extend_restrict_perm_cancel *20
restrict_perm_using_txpose *22
extend_perm_over_itcomp *10
trivial_nat1_fun *7
zero_sym_grp *9
trivial_sym_grp *8
sym_grp_is_swaps *39
sym_grp_is_swaps_a *33
perm_induction *14
perm_induction_a *19
perm_induction_b *12
mon_itop_txpose_invar *7
mon_itop_perm_invar *7

Listing


Last modified February 24th, 1995

Paul Jackson / jackson@cs.cornell.edu