RE: [PVS-Help] An easy pvs question

["Mao Lingzhao" <maolzh@xxxxxxxxx>]

Thanks, but "induct"  will only work on consequences but antecedents. That
is 

...|- FORALL m ....

Can be inducted by m.

I've solved in another way by defining another lemma and then apply to it,
maybe there is a more convenient way to solve it.

  all_same :LEMMA
  (FORALL m: m<t => s(m)=s(m+1) )
  IMPLIES   (s(t)=s(0))


Lingzhao

-----Original Message-----
From: Butler, Ricky W. (LARC-D320) [mailto:r.w.butler@xxxxxxxx] 
Sent: 2008Äê5ÔÂ5ÈÕ 21:06
To: lingzhao
Subject: RE: [PVS-Help] An easy pvs question

I would try induction on "m".  PVS "induct" command.

Rick

> -----Original Message-----
> From: pvs-help-bounces+r.w.butler=larc.nasa.gov@xxxxxxxxxxx
[mailto:pvs-
> help-bounces+r.w.butler=larc.nasa.gov@xxxxxxxxxxx] On Behalf Of
lingzhao
> Sent: Sunday, May 04, 2008 7:22 AM
> To: pvs-help@xxxxxxxxxxx
> Subject: [PVS-Help] An easy pvs question
> 
> Hi,
> 
>    when I was trying to prove some lemma,I encountered this:
> 
> [-1]  FORALL m: m < N - 1 => s(m) = s(1 + m)
>   |-------
> [1]   s(N - 2) = s(0)
> 
> Rule?
> 
> 
> It seems easy,but I can not find suitable rule to prove it. Please
help
> me, thanks.