list_2 Theory

Summary of Definitions

Typed Definitions

eq_list *9

dset_list *4

mem_f *3

mon_reduce *2

mon_for *1

mon_htfor *1

lapp_imon *8

lapp_mon *10

bexists *1

ball *1

mem *1

remove1 *5

bpermr *7

count *1

dislist *1

diff *4

lmin *1

lmax *1

bsublist *1

bsuplist *1

distinct *1

Main Theorems

assert_of_eq_list *18

list_in_mem_f_list *8

mon_reduce_append *4

mon_reduce_eq_itop *16

mon_for_append *6

select_reject_permr *15

mon_reduce_functionality_wrt_permr *7

map_permr_func *13

map_functionality *3

mon_for_functionality_wrt_permr *13

length_mon_for_char *2

length_functionality_wrt_permr *3

mon_for_map *4

mon_for_of_id *6

mon_for_of_op *5

mon_for_swap *6

mon_for_when_swap *6

mon_for_when_none *13

mon_for_when_unique *26

lapp_fact *3

dist_hom_over_mon_for *4

ball_functionality_wrt_permr *2

bexists_iff_exists_nth *24

bnot_thru_exists *4

mem_iff_mem_f *5

mem_functionality_wrt_permr *3

bexists_char *19

ball_char *14

mem_iff_exists *5

cons_permr_mem *6

cons_remove1_permr *10

not_mem_remove1 *7

remove1_functionality_wrt_permr *7

assert_of_bpermr *21

null_functionality_wrt_permr *8

count_functionality *3

count_bounds *6

mem_iff_count_nzero *10

permr_iff_eq_counts *28

permr_iff_eq_counts_a *2

count_append *4

mem_append *6

mem_map *6

count_remove1 *17

count_diff *9

mem_diff *10

diff_functionality_wrt_permr *7

count_lmin *3

mem_lmin *8

lmin_functionality_wrt_permr *7

lmin_com *4

lmin_assoc *4

count_lmax *3

mem_lmax *8

lmax_functionality_wrt_permr *7

lmax_com *4

lmax_assoc *4

count_bsublist *12

count_bsublist_a *3

mem_bsublist_imp *5

mem_bsublist *10

bsublist_weakening *4

bsublist_transitivity *3

bsublist_functionality_wrt_permr *5

bsublist_functionality_wrt_bsublist *7

bsublist_append_diff *9

ball_respects_bsublist *7

ball_functionality_wrt_bimplies *10

distinct_iff_counts_le_one *19