# Re: [PVS-Help] How to define a step for splitting withoutgenerating redundant TCCs

```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
>
>

--
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

```

• Follow-Ups: