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

[PVS-Help] how to prove such a simple lemma?

Hello all,
I just met a so simple lemma, but don't know how to prove it. Who could help me?
P,Q: VAR [size:{a:nat| a>=3}, [below[size] ->set[nat]]]
test: LEMMA   P`1=Q`1+1 AND FORALL (i:below(P`1)),(j:below(Q`1)): P`2(i)=Q`2(j)
                          IMPLIES EXISTS (i,j:below(P`1)): P`2(i)=P`2(j)
since the size of Q is 1 less than the size of P, so this lemma should hold. I think I should use epsilons, but don't know how to apply this command.
many thanks!