[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[PVS-Help] question about term rewriting
Dear PVS users,
I am exploring PVS' term rewriting capabilities and have stumbled across
a phenomenon which I cannot make sense of. See the following theory:
n: VAR rational
sub: THEOREM n-n = 0
% (rewrite "sub") fails
testsub: THEOREM false and 1/0 - 1/0 = 0
% (rewrite "sub") succeeds
testsub2: THEOREM true or 1/0 - 1/0 = 0
In the case of testsub, (rewrite "sub") fails, because a TCC is
generated that presumably prevents instantiating sub with an ill-typed
term. That makes sense to me.
In the case of testsub2 however, (rewrite "sub") does not generate a
TCC, and sub seems to be used to rewrite 1/0 - 1/0 to 0.
First off, I am wondering why rewriting fails in the case of testsub and
succeeds in the case of testsub2. The examples seem to be fairly equivalent.
Second, I am wondering how (rewrite "sub") solves (or avoids stating)
the TCC in the case of testsub2. Is it the observation that you can
assume the negation of the first disjunct when rewriting the second
disjunct? Or is it something even more fancy?
I appreciate any explanation or pointer.
Thanks in advance,