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

[PVS-Help] How to continue this proof?



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