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

[PVS-Help] Expressing cube root in PVS


I'm trying to prove some stuff in PVS involving cube roots and am 
currently using the ^^ notation, i.e. a^^(1/3) for expressing the root, 
but was wondering whether there is a generic root function in PVS that 
would allow one to deal with arbitrary roots, e.g. root(a,n)? I haven't 
found it in the libraries, but, perhaps, there is an undocumented facility?

Thanks a lot in advance for your help,