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

[PVS-Help] split command problem




hi,all:
    Recently when I try to prove the sequence :
   [-1] A!1(el(i!1))
   [-2] el(i!1) = x!1 OR X!1(x!1)
     |---------
   [1] A!1(x!1)
I use the (split) command and the sequence is devided to 2 branches. The first branch with antecedent el(i!1) = x!1 is easy to prove.But the second branch can not be proved. I think anyone of these subgoal be proved would complete the proof but PVS compel me to complete both of the them.Could anybody tell me why and what to do. Thanks!
 




网易邮箱,中国第一大电子邮件服务商