[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.