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