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