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

[PVS-Help] split command problem

    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!