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

[PVS-Help] datatype for index-and



Hello every one:

I have a smaple theory:

index_and: THEORY
 BEGIN
  Data: DATATYPE   BEGIN
    a(b: bool): a?
    AND(a1, a2: Data): and?
 END Data
  f: VAR Data  
 |=(f): RECURSIVE bool =
   CASES f OF a(b): b, AND(a1, a2): |= (a1) AND |=
(a2) ENDCASES     MEASURE id BY <<
 END index_and

But i want to use the datatype "Data" to represent a 
form of  

N : posnat  
f: [below[N]-> Data]
f(0) and f(1) and ... and f(N-1) 


I have established many theoires based on "Data", so I
do not change this datatype defintion.

Is it possible to use an conversion function or an
rewriting rule for that?

thank you in advance.

Q.G .XU.

2006-04-13


	

	
		
___________________________________________________________ 
雅虎1G免费邮箱百分百防垃圾信 
http://cn.mail.yahoo.com/