This file contains list functions and theorems involving the booleans. These include the boolean valued test for nil, test for membership give a boolean-valued equality over the type of elements of the list, list subtraction, universal and existential extensions of a predicate to a list of values.
** Module lib_list_bool Imports lib_list_basics lib_bool_thms nil_test = ... : {s|Type}(list s)->bool exist_list = ... : {t|Type}(t->bool)->(list t)->bool all_list = ... : {t|Type}(t->bool)->(list t)->bool member = ... : {t|Type}(t->t->bool)->t->(list t)->bool list_eq = ... : {t|Type}(t->t->bool)->(list t)->(list t)->bool del_first = ... : {t|Type}(t->t->bool)->t->(list t)->list t del_all = ... : {t|Type}(t->t->bool)->t->(list t)->list t list_sub = ... : {A|Type}(Type)->(A->bool)->A->(list A)->list A exist_list_append_lem = ... : {t|Type}{P:t->bool}{j,k:list t} Eq (exist_list P (append j k)) (orelse (exist_list P j) (exist_list P k)) member_append_lem = ... : {t|Type}{eq_on_t:t->t->bool}{x:t}{j,k:list t} Eq (member eq_on_t x (append j k)) (orelse (member eq_on_t x j) (member eq_on_t x k)) nil_test_true_equiv_Eq_nil = ... : {t|Type}{l:list t}iff (Eq (nil_test l) true) (Eq l (nil t)) nil_test_false_equiv_Eq_cons = ... : {t|Type}{l:list t} iff (Eq (nil_test l) false) (Ex ([a:t]Ex ([m:list t]Eq l (cons a m)))) nil_test_on_append = ... : {t|Type}{l,m:list t}{a:t}Eq (nil_test (append l (cons a m))) false