[PVS-Help] Some problems in using PVS 3.2

[Nikhil Kikkeri <nikhil@xxxxxxxxxxxx>]

Hi--

I do not know where to start but I'll try to be concise about the problem I am 
facing. What I saying might be appear vague, but any solution at this point 
would be helpful

I have a big library of PVS files which were written in PVS 2.3 a couple of 
years ago. For the purpose of our work we decided to migrate everything to 
PVS 3.2.

Just today I discovered some problems that might be associated with that. Or 
it might be the case that it is a totally different issue.

There are many circuits that are recursively described over the size of the 
input "n" which is a posnat. These were proved using induct "n".  However I 
found out that most of these proofs when re-run in PVS 3.2 generate more 
sub-goals that what originally existed (for example 3 instead of 2).

Ordinarily one could redo the proofs again manually and complete them. I tried 
doing that but I faced a couple of other problems. For example 
"bv2nat_concat" failed to replace the terms. For example in the consequent I 
had

bv2nat(fill[1](FALSE) o fill[1](x))

If I say (use "bv2nat_concat") I get in the antecedent

bv2nat[2](fill[1](FALSE) o fill[1](x)) = bv2nat[1](fill[1](FALSE))*exp2(1) + 
bv2nat[1](fill[1](x))

which is correct but the replace does not do anything. Also normally stating 
(use "bv2nat_concat") does not produce the expressions with the parameters in 
them. So this is the first time I have seen something like it.

Doing C-u M-x show-expanded-sequent and then using that for the replace does 
not seem to work either.

Thank you in advance.

Best regards
-Nikhil



-- 
Depart not from the path which fate has assigned you.