perms_2 Theory

Defines several equivalence relations on lists, including `is a permutation of', `is a permutation of up to', and `is equivalent to, up to'.

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

Listing


Last modified February 24th, 1995

Paul Jackson / jackson@cs.cornell.edu