[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [PVS-Help] Proving theorems when induction is required onmultiple parameters
Could you send me your specs, so I have a more concrete idea of what the
Prasanna Kumar <firstname.lastname@example.org> wrote:
> 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