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

[PVS-Help] How to define a step for splitting without generatingredundant TCCs

Dear all,

I am trying to define a PVS strategy for splitting a sequent of the

X |- A and B

into the two subgoals:

X    |- A
X, A |- B

This is straightforwardly accomplished by (case "not A") and
simplifying the resulting sequents. However, doing so introduces
redundant TCCs for A, which I would like to avoid. Is there some way
of using more primitive proof functions, maybe from PVS lisp, to
achieve the same but bypassing the TCC generation?

Johannes Eriksson

Johannes W. E. Eriksson, M.Sc.
Ph.D. Student / Turku Centre For Computer Science (TUCS)
Åbo Akademi University / Department of Information Technologies
e-mail: joheriks@abo.fi  www: http://www.abo.fi/~joheriks