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

Re: [PVS-Help] Proving theorems when induction is required onmultiple parameters



Hi Prasanna,

Could you send me your specs, so I have a more concrete idea of what the
problem is?

Thanks,
Sam Owre

Prasanna Kumar <k.prasannakumar@gmail.com> wrote:

> Hi,
>  I am a newbie to PVS and was trying to prove some basic properties on lists. I
> am facing a problem in trying to prove append(take(n,l),drop(n,l)) = l.
>  If I use induction on n I get subgoals which have a condition on l being null
> and if I induct on l then I get a condition where n >= 0 is present in one of
> the goals. 
>  Please let me know if there is anything different I should be doing.
> 
> Thanks in advance.
> - Prasanna