[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
RE: [PVS-Help] An easy pvs question
Thanks, but "induct" will only work on consequences but antecedents. That
...|- 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.
(FORALL m: m<t => s(m)=s(m+1) )
From: Butler, Ricky W. (LARC-D320) [mailto:r.w.butler@xxxxxxxx]
Sent: 2008Äê5ÔÂ5ÈÕ 21:06
Subject: RE: [PVS-Help] An easy pvs question
I would try induction on "m". PVS "induct" command.
> -----Original Message-----
> From: pvs-help-bounces+r.w.butler=larc.nasa.gov@xxxxxxxxxxx
> help-bounces+r.w.butler=larc.nasa.gov@xxxxxxxxxxx] On Behalf Of
> Sent: Sunday, May 04, 2008 7:22 AM
> To: pvs-help@xxxxxxxxxxx
> Subject: [PVS-Help] An easy pvs question
> when I was trying to prove some lemma,I encountered this:
> [-1] FORALL m: m < N - 1 => s(m) = s(1 + m)
>  s(N - 2) = s(0)
> It seems easy,but I can not find suitable rule to prove it. Please
> me, thanks.