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

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

* Jerome White [Wed, Nov 25, 2009 at 08:40:12PM -0800]:
> 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

Thanks. However, the theories I am dealing with are generated by a
tool in a certain way that I would like to avoid changing at this
point. Hence my interest in achieving this with a strategy.


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