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

[CHEN Chunqing <chenchun@xxxxxxxxxxxxxxx>]

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):
  0: Return to Top Level (an "abort" restart).
  1: Abort entirely from this process.
[1] pvs(41):
------------ end of the message ---------------

Did anyone encounter the similar problem before, and could you please 
share your experience?

Thank you in advance.

Cheers
Chunqing