perms_2 Theory

The permutation relations were defined in terms of permutation functions. This turned out to be rather awkward. Would have been much easier to start with computable notions of when one list is a permutation of another (see list_2 for details).

Various properties of these relations were proven.

Summary of Definitions

Typed Definitions

permr *9

tl_perm *57

perm_morph *9

permr_upto *1

lequiv *1

Main Theorems

permr_suptyping *9

not_permr_cons_nil *3

permr_nil_is_nil *6

permr_weakening *14

permr_inversion *26

permr_transitivity *17

permr_equiv_rel *5

cons_functionality_wrt_permr *19

permr_functionality_wrt_permr *13

perm_b_to_f *7

perm_f_b_cancel *6

perm_b_f_cancel *6

perm_f_inj *7

perm_b_inj *8

permr_hd_cancel *35

hd_two_swap_permr *19

cons_cons_permr *4

append_functionality_wrt_permr *21

append_comm_1 *6

append_comm *11

permr_upto_inversion *18

permr_upto_transitivity *15

permr_upto_weakening *9

permr_upto_equiv_rel *7

permr_upto_functionality_wrt_permr_upto *4

cons_functionality_wrt_lequiv *11

permr_upto_split *30

cons_functionality_wrt_permr_upto *8