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



K.Wei writes:
   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
   (i-1).
    
   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[2]")

Bye,

Hendrik