Entry	Value
Package Name	list-append-thm
Count	18
Theorems	ALL_APPEND : !p l1 l2. ALL p (APPEND l1 l2) <=> ALL p l1 /\ ALL p l2 APPEND_ASSOC : !l1 l2 l3. APPEND l1 (APPEND l2 l3) = APPEND (APPEND l1 l2) l3 APPEND_EQ_NIL : !l1 l2. APPEND l1 l2 = [] <=> l1 = [] /\ l2 = [] APPEND_LCANCEL : !l l1 l2. APPEND l l1 = APPEND l l2 <=> l1 = l2 APPEND_LCANCEL_IMP : !l l1 l2. APPEND l l1 = APPEND l l2 ==> l1 = l2 APPEND_LINJ : !l1 l1' l2 l2'. LENGTH l1 = LENGTH l1' /\ APPEND l1 l2 = APPEND l1' l2' ==> l1 = l1' APPEND_NIL : !l. APPEND l [] = l APPEND_RCANCEL : !l l1 l2. APPEND l1 l = APPEND l2 l <=> l1 = l2 APPEND_RCANCEL_IMP : !l l1 l2. APPEND l1 l = APPEND l2 l ==> l1 = l2 APPEND_RINJ : !l1 l1' l2 l2'. LENGTH l2 = LENGTH l2' /\ APPEND l1 l2 = APPEND l1' l2' ==> l2 = l2' APPEND_SING : !h t. APPEND [h] t = CONS h t EX_APPEND : !p l1 l2. EX p (APPEND l1 l2) <=> EX p l1 \/ EX p l2 LENGTH_APPEND : !l1 l2. LENGTH (APPEND l1 l2) = LENGTH l1 + LENGTH l2 MEM_APPEND : !l1 l2 x. MEM x (APPEND l1 l2) <=> MEM x l1 \/ MEM x l2 MEM_APPEND_DECOMPOSE_LEFT : !x l. MEM x l <=> (?l1 l2. ~MEM x l1 /\ l = APPEND l1 (CONS x l2)) NULL_APPEND : !l1 l2. NULL (APPEND l1 l2) <=> NULL l1 /\ NULL l2 SET_OF_LIST_APPEND : !l1 l2. set_of_list (APPEND l1 l2) = set_of_list l1 UNION set_of_list l2 null_concat : !l. NULL (concat l) <=> ALL NULL l

Back to main package page