# [PVS-Help] (PVS novice) A doubt regarding lemma rewrites

```Hi--

I am using PVS to do  certain simple things for me. Right now I want to use
PVS to build a library for redundant arithmetic systems like Carry-Save and
Borrow-Save arithmetic. i am also sending the entire PVS theory.

I have a few expressions

CSVec2nat -- conversion from CS to natural
CSvec2nat_Proj(csnumber,upper,lower) - a projection of a certain CS number
indexed between u and l
CSFraction -- CSVec2nat(CSProjection(csnumber,i,0)/2^(i+1)  the fractional
value of the projection
i = upper index

CSVec2nat_Proj_bd_Correct -- Lemma  1 which shows that the CSVec2Nat(CSProj)
< 2^(u-l+2)
This has been proved using PVS

CSFraction_UBound -- Lemma 2which shows that CSFraction < 2

This is true because CSVec2Nat(CSProj) < 2^(u-l+2)

The fractional value  CSFraction is  CSVec2Nat(CSProj)/2^(i+1) <
2^(i-0+2)/2^(i+1)

which is  CSFraction < 2

this is clearly due to Lemma 1.
Proving Lemma 1 was no problem at all but I am struggling in the proof of
Lemma 2.I dont see a way to use Lemma 1 to prove Lemma 2 even though Lemma 1
is nothing but a division of 2^(i+1) on both sides.

Can someone provide some tips on how to do this?This is not for a class,
just for messing around with PVS so do feel free to mail in your
suggestions.

--------------------------------------------------------------------------------------------------------------

Here is the PVS theory

csnumber :THEORY

BEGIN

IMPORTING bitvectors@top
n: VAR nat
l: VAR nat
u: VAR nat
i: VAR nat

CSVec(n): TYPE = [#C:bvec[n],S:bvec[n]#]

CSVec2nat(n: nat,csv: CSVec(n)): nat = bv2nat(csv`C) + bv2nat(csv`S)

CSVProj(n:nat,csv: CSVec(n),u:below(n), l:below(u)): CSVec(u-l+1) =
(# C := csv`C^(u,l),S
:= csv`S^(u,l)#)

CSDigitVal(n:nat,i:below(n),csv:CSVec(n)): nat =

b2n(csv`C(i))+b2n(csv`S(i))

bv22CSVec(n: nat,s:bvec[n],c:bvec[n]): CSVec(n) = (#C:= c, S:= s#)

CSVec2nat_correct: LEMMA
FORALL(s,c: bvec[n]): LET csv = bv22CSVec(n,s,c) IN
CSVec2nat(n,csv) = bv2nat(s) + bv2nat(c)

CSVec2Nat_BdCorrect: LEMMA
FORALL(csv: CSVec(n)):
LET i = CSVec2nat(n,csv) IN
i < exp2(n+1)

CSVec2Nat_Proj_BdCorrect: LEMMA
FORALL(n:nat,u:below(n),l:below(u),csv:
CSVec(n)):
LET csvproj = CSVProj(n,csv,u,l),
i  = CSVec2nat(u-l+1,csvproj) IN
i < exp2(u-l+2)

%%%% FRACTION RANGES %%%%

CSFraction(n: nat,i: below(n),csv: CSVec(n)): real =
LET csvproj =
CSVProj(n,csv,i,0) IN

CSVec2nat(i,csvproj)/exp2(i+1)

CSFraction_LBound: LEMMA FORALL(n: nat,i: below(n),csv: CSVec(n)):
LET j = CSFraction(n,i,csv) IN
j >= 0

CSFraction_UBound: LEMMA FORALL(n:nat,i: below(n), csv: CSVec(n)):
LET j = CSFraction(n,i,csv) IN
j < 2

END csnumber

---
http://engr.smu.edu/~nikhil

_________________________________________________________________
MSN Hotmail now on your Mobile phone.