[PVS-Help] nested recusive data types

[Sjaak Smetsers <s.smetsers@xxxxxxxx>]

Hi,

I've the defined the following data type:

TERMS [V,S:TYPE]: DATATYPE
BEGIN
    tvar(id:V): tvar?
    tapp (symb:S,args:list[TERMS]): tapp?
END TERMS

This will cause PVS to generate an TERMS_adt file containing, among other 
things, a map function. If copy this function into my own theory, i'm not 
able to prove the generated termination TCC. The MEASURE of my own map 
function is the standard ordering on terms given by <<. The complete 
definition is

map(f:[V -> W]) (t:TERMS[V,S]) : RECURSIVE TERMS[W,S] =
      CASES t
        OF tvar(tvar1_var): tvar(f(tvar1_var)),
           tapp(tapp1_var, tapp2_var):
             tapp(tapp1_var,
                  map[TERMS[V, S], TERMS[W, S]](map(f), tapp2_var))
        ENDCASES
  MEASURE t BY <<


What do I have to do to get rid of this TCC? Do i really need a specific 
property of the map function for lists? 

Regards,

Sjaak