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

need helps!!!



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