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