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

*To*: <pvs-help@csl.sri.com>*Subject*: need helps!!!*From*: "Kun Wei" <k.wei@eim.surrey.ac.uk>*Date*: Thu, 20 Mar 2003 02:06:10 -0000 (GMT)*Importance*: Normal*Sender*: pvs-help-owner@csl.sri.com

Hi, every PVS users, I am a new beginer of PVS. I met problems when I tried to prove a simple theory. It is (x+1)(x+1) can be divisible by 4(x is odd nat). I desinged the pvs script. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% division:THEORY BEGIN i,j:VAR nat odd_nat?(i):bool=exists j: i=2*j+1 odd_nat:TYPE=(odd_nat?) division_4:THEOREM (FORALL x:odd_nat:(exists y:nat: (x+1)*(x+1)=4*y)) END division %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% Ok, I use "induct "x"" to prove this theorem. The prover generates three subgoals. For the first one and the second,I've finished. But I got the problems in the third subgoal. Because the induction method is we assume the j is right,then we reason (j+1) is right also. but in this case, I was dealing with odd number, the increment is two instead of one. So I don't know hwo to prove that. Hope to get any help form the users. Thanks! Kun

- Prev by Date:
**Re: LISP code for ground evaluation?** - Next by Date:
**Re: need helps!!!** - Prev by thread:
**Assembly program verification in PVS** - Next by thread:
**Re: need helps!!!** - Index(es):