[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?
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: email@example.com www: http://www.abo.fi/~joheriks