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

```Perhaps I'm misunderstanding your question, but why not just have and l0
that proves what you want about a(x), and use that lemma to prove l1?

jerome

Johannes Eriksson wrote:
> Hi again,
>
> I will try to make my problem a little more concrete. Say I have a
> formula like:
>
> l1: theorem a(x) and c
>
> Additionally, assume that the application a(x) produces a complex TCC
> which require some interactive theorem proving to discharge. Given
> that, I would like to define a strategy split the root sequent:
>
> |- a(x) and c
>
> into just the two branches:
>
>      |- a(x)
> a(x) |- c
>
> i.e., without having to reprove the TCC from a(x), which I have to if
> I use "case". How hints on how I can do it?  I know that the TCC can
> be invoked as a lemma, e.g.  (use l1_TCC1), but I want to avoid that
> since the strategy should work independently of the formula name.
>
> Regards,
> Johannes
>
>
> * Johannes Eriksson [Thu, Nov 19, 2009 at 03:59:48PM +0200]:
>> Dear all,
>>
>> I am trying to define a PVS strategy for splitting a sequent of the
>> form:
>>
>> 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?
>>
>> Regards,
>> 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
>>
>>
>

```