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

Re: A question

>   I do not know how to prove the following goal:
>   |-------
> {1}    length(append(l1!1, l2!1)) = length(l1!1) + length(l2!1)

There is a lemma for this in the prelude (Use M-x vpf to view the PVS
prelude file), so you can prove it with:

	(use "length_append[int]")

or you can prove it directly by using:

        (generalize "l1!1" "l_1")
	(induct-and-simplify "l_1")


Dr Dave Stringer-Calvert, Software Engineer, Computer Science Laboratory
SRI International, 333 Ravenswood Avenue, Menlo Park, CA 94025-3493, USA
Phone: (650) 859-3291 Fax: (650) 859-2844 David.Stringer-Calvert@sri.com