[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

A question



Dear PVS users:
  I do not know how to prove the following goal:

  |-------
{1}    length(append(l1!1, l2!1)) = length(l1!1) + length(l2!1)

where l1!1, l2!1 are of type list[int].

Did anyone know how to prove it? Many thanks.

-- Jei-Wen Teng