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

Re: [PVS-Help] How to continue this proof?



Sjaak,

What do you get when you issue the command C-u M-x show-expanded-sequent?
My wild guest is that the two inject functions don't have the same type.

Cesar


On 10/19/12 10:24 AM, "Sjaak Smetsers" <s.smetsers@xxxxxxxxxxxxx> wrote:

>Especially when dealing with lists, I now end then get stuck in a
>situation like this:
> 
>[-1]  length[list[T]]
>          (map(LAMBDA (l2: list[T]): cons(cons1_var!1, l2),
>               inject(x!1)(cons2_var!1)))
>       = 1 + length[T](cons2_var!1)
>  |-------
>[1]   1 +
>       length[list[T]]
>           (map(LAMBDA (l2: list[T]): cons(cons1_var!1, l2),
>                inject(x!1)(cons2_var!1)))
>       = 2 + length[T](cons2_var!1)
> 
>I don¹t understand why PVS is not able to derive 1 from -1. It seems as
>if it considers the applications of map as different, but I do not see
>why. But more annoyingly, there seems to way to continue. How should I
>proceed? E.g. if I type (name-replace STUPIDTHING ³map(LAMBDA (l2:
>list[T]): cons(cons1_var!1, l2), inject(x!1)(cons2_var!1))²) it will
>replace just one of the map expressions by  STUPIDTHING.
> 
>Sjaak
> 
>