[PVS-Help] how to induct?

[maqian <applehopedream@xxxxxxx>]

Hello,

   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!

---

09年新晋3D主流网游《天下贰》，网易六年亿资打造