[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [PVS-Help] How to use the induction command in such a case?
Subject: [PVS-Help] How to use the induction command in such a case?
The problem is that here i is considered as a natural number
greater than 2 and j is a dependent type which equals to
So may I use the command ' induct "i" ' or ' measure-induct
"y" ("y") 1 ' to prove such a case.
(induct "i") should give you induction on natural numbers. The
base case is trivial because it contains the contradiction i=0
and i > 2. In the induction step you have to make a case
distinction on i = 3 to get you base case.
Alternatively you can use (induct "i" :name "above_induction")