[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 :
[-2] el(i!1) = x!1 OR X!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!