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

*To*: pvs-help <pvs-help@csl.sri.com>*Subject*: [PVS-Help] How to use the induction command in such a case?*From*: "K.Wei" <K.Wei@surrey.ac.uk>*Date*: Tue, 17 Jan 2006 21:45:37 -0000*List-Help*: <mailto:pvs-help-request@csl.sri.com?subject=help>*List-Id*: PVS-Help <pvs-help.csl.sri.com>*List-Post*: <mailto:pvs-help@csl.sri.com>*List-Subscribe*: <http://lists.csl.sri.com/mailman/listinfo/pvs-help>,<mailto:pvs-help-request@csl.sri.com?subject=subscribe>*List-Unsubscribe*: <http://lists.csl.sri.com/mailman/listinfo/pvs-help>,<mailto:pvs-help-request@csl.sri.com?subject=unsubscribe>*Sender*: pvs-help-bounces+archive=csl.sri.com@csl.sri.com*Thread-Index*: AcYbr1owxRvFfKERTZu5/Uhj8/9YOQ==*Thread-Topic*: 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

- Prev by Date:
**Re: [PVS-Help] Records and quantifying over fields** - Next by Date:
**Re: [PVS-Help] How to use the induction command in such a case?** - Prev by thread:
**[PVS-Help] Expressing cube root in PVS** - Next by thread:
**Re: [PVS-Help] How to use the induction command in such a case?** - Index(es):