[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[PVS-Help] problem when proving false in forall clause

Dear all,

Currently I am using PVS (version 3.1) in my research. I encounter an 
interesting problem when proving the following lemma:

False_n_emp: LEMMA (forall (y : {z : nat | z < 20}): FALSE) = FALSE;

After I tried the command "grind", the result is:

{-1} (forall (y: {z : nat | z < 20}): FALSE)

that is to say, there is no consequent, and I have no idea what to do 
next. So could you kindly enlighten me how to solve the problem and what 
causes the problem?

Actually, it is strange when I modified the above lemma to:

False_n_emp: LEMMA (forall (y: {z : nat | z < 20}): TRUE) = TRUE;

This time, PVS can prove it by single command "grind".

Does anyone meet the similar problem before, and could you please share 
your experience?

Thank you in advance and looking forward to your reply.