[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[PVS-Help] (grind :theories real_props) enters infinite loop
I have the following theories:
((power(1 / (square_root(2)), 4)) = (1 / 4)
((power(1, 4)) / (power(square_root(2), 4))) = (1 / 4))
ctx_exponents defines power and square_root and provides many
rewriting rules for them. The definitions of power and square_root
are based on the Nasa PVS library.
The command (grind :theories real_props) proves the lemma
However if in contextname4__example I import contextname4
instead of ctx__exponents, then the same proof command
enters an infinite loop.
The theories on which this is based are quite large, but I
can provide them if needed to reproduce the problem.
Any help would be much appreciated.