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

[PVS-Help] How to use the induction command in such a case?



Hello all,
 
I have got a very tricky case. I am going to prove a group of components to satisfy a property. The natural approach is to use the induction rule to it. For example, as following, besides the starting point, if
we could prove for any i
 
 College(i,j) sat P implies College(i+1,j) sat P
 
then, College(i,j) sat P in any cases. Here College(i,j) is a recursive definition, as following
 
College(i,j): Recursive process[E] = if j=0 then PandF(i,0)
                                                    else College(i,j-1) || PandF(i,j)   endif
measure j
 
 
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.
 
many thanks,
 
Kun