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