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

Strange problems



Maybe someone could help me out with this. I am developing a deep
embedding of the DisCo (http://disco.cs.tut.fi) specification
language. While trying to verify some properties of the DisCo
language based on the embedding, I ran into the following sequent
which PVS does not recognize to be provable:

action_superposition.3.1.1.1.1 :  

[-1]  sem(variable_assignments(role_of_object(ob!1, ra!1, roles(a!1)),
                               append(new_fields(ref!1), fields(a!1)),
                               append(new_assignments(ref!1), body(a!1))),
          ra!1, b!1)
  |-------
[1]   sem(variable_assignments(role_of_object(ob!1, ra!1, roles(a!1)),
                               append(new_fields(ref!1), fields(a!1)),
                               append(new_assignments(ref!1), body(a!1))),
          ra!1, b!1)

I use subtypes in the specification, and I suspect this has something
to do with that, but I have not been able to figure out what goes
wrong here. At least the typepred command does not do anything useful,
since it only adds antecedents into the sequent.

The dump file is available at http://www.cs.tut.fi/~pk/tmp/dump and
the relevant PVS file is superposition.pvs.

Any help would be greatly appreciated.
--
pertti