# Re: [PVS-Help] what to do when consequents are logically opposite

```Hi Chunqing,

You have to be more careful when quantifiers are involved; 1 and 2 are
not logically opposite.  The opposite of 1 is

NOT (FORALL (t: {x: T| x > ALPHA(x!1) AND x < OMEGA(x!1)}):
NOT tp1!1(t, x!1))

which is logically equivalent to

EXISTS (t: {x: T| x > ALPHA(x!1) AND x < OMEGA(x!1)}):
tp1!1(t, x!1)

This would then be provable by skolemizing the FORALL, then using the
new skolem constant to instantiate the EXISTS.

pvs-bugs@csl.sri.com, so I can diagnose the problem.  I believe it is
already fixed in current versions of PVS, but I'd like to be certain.

Thanks,
Sam

CHEN Chunqing <chenchun@comp.nus.edu.sg> wrote:

> Date: Fri, 29 Sep 2006 14:49:06 +0800 (GMT-8)
> From: CHEN Chunqing <chenchun@comp.nus.edu.sg>
> To: pvs-help@csl.sri.com
> Subject: [PVS-Help] what to do when consequents are logically opposite
> Sender: pvs-help-bounces+owre=csl.sri.com@csl.sri.com
>
> Hi, all,
>
> First of all, thanks Professor Sam Owre for his quick and effective reply
> of my last question and so I can continue my adventure in PVS :)
>
> Right now I met a problem during a proof (PVS version is 3.1), the detail
> is below:
>
> [1] OO?(PROJ_1(x!1))
>   |---------
> {1} FORALL (t: {x: T| x > ALPHA(x!1) AND x < OMEGA(x!1)}):
>         NOT tp1!1(t, x!1)
> [2] FORALL (t: {x: T| x > ALPHA(x!1) AND x < OMEGA(x!1)}):
>         tp1!1(t, x!1)
>
> where tp1!1 is a function returning boolean value. To me the consequences
> 1 and 2 are logically opposite (I have specified a lemma below for it and
> checked the validated by PVS already):
>
> Uni_n_Emp_temp: LEMMA
>    (forall (y: II): forall (x: {xx: T| x > ALPHA(y) and x < OMEGA(y)}):
> NOT tp1(x, y)) OR
>    (forall (y: II): forall (x: {xx: T| x > ALPHA(y) and x < OMEGA(y)}): tp1(x, y))
> => true;
>
> Since in sequent calculus, consequences are disjunctive, right? and hence
> the above proof should be correct in my opinion. Though PVS does not
> behave the way :) Can anyone kindly enlighten me what to do in this
> situation?
>
> So I tried the command (merge-fnums (1, 2)), and thought that may solve
> the problem by merging two consequences together. However, this time PVS
> claims the following error message:
>
> ------------- start of the message ------------
> Rule? (merge-fnums (1, 2))
> No change on: (skip)
> Uni_n_Emp.2.1.2 :
>
> [1] OO?(PROJ_1(x!1))
>   |---------
> {1} FORALL (t: {x: T| x > ALPHA(x!1) AND x < OMEGA(x!1)}):
>         NOT tp1!1(t, x!1)
> [2] FORALL (t: {x: T| x > ALPHA(x!1) AND x < OMEGA(x!1)}):
>         tp1!1(t, x!1)
>
> Rule?
> Ill-formed rule/strategy: 2
> No change on: (skip)
> Error: Attempt to take the car of 2 which is not listp.
>    [condition type: simple-error]
>
> Restart actions (select using :continue):