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

[PVS-Help] how to induct?

   when I use PVS to prove some lemmas ,I come across a problem on induction? I only know the induction way used in PVS  is like this :
1. base :P(0)
2. P(j-1) implies P(j)
But I want to prove both at the even state and odd state ,and they are different.How can I induct?
Thank you for advanced!
Best regards!