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

[PVS-Help] Proving theorems when induction is required on multipleparameters

 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