[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[PVS-Help] How to use the induction command in such a case?
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
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
else College(i,j-1) || PandF(i,j) endif
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.