[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,