[PVS-Help] "1 = 0" pvs problem

[lingzhao <maolzh@xxxxxxxxx>]

Hi,


I am using pvs, but sometimes I encountered some problems. 

When I was trying to prove a lemma in pvs, I found one proof sequence as
below:


        [-1]  (x!1 = 0)
        [-2]  (s0!1(1) = 2)
        [-3]  s0!1(0) = 1
        [-4]  m!1 = 0
        {-5}  (0 = 2)
        [-6]  (s1!1 = s0!1 WITH [(0) := 3])
          |-------
        [1]   1 = 0
        
        Rule? (assert)
        Simplifying, rewriting, and recording with decision procedures,
        
        This completes the proof of update_privilege.1.1.


After I typed a "assert" rule in pvs, it proves!

The problem is that the consequent formula " [1]   1 = 0 " is
absolutely not right, but why pvs assert that it can be proved by the
antecedent formulas?

Thanks,
Lingzhao