a question

[Bin Chen <chenb3@cas.mcmaster.ca>]

Hi,

Could you please help me to solve this problem?

In my PVS file, some definitions are:

term: DATATYPE
  begin
    m(n:int): memory?
    r(n:int): register?
    cons(d:domain):const?
  END term

environment: type =[term -> domain]

memory: type =(memory?)
register: type = (register?)
const: type = (const?)

Now I want to define some lifting functions such that the operations in
"domain" can be applied to "term", i.e., op[domain->domain] becomes
op[term->term]; op[domain,domain->domain] becomes op[term,term->term].

I couldn't work it out. Could anyone please help me?

Thanks a lot.

******************************************
Bin Chen
Department of Computing and Software
McMaster University
1280 Main Street West
Hamilton, Ontario, L8S 4K1
Canada

email: chenb3@cas.mcmaster.ca
phone: (905)525-9140, ext.27406
******************************************