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

can you give me command to prove test??



Hi,everyone:

 I am just new beginner in PVS, I found the example in maillist ,but I cann't prove it,after I used 
(grind) command, it need to prove :

test :  

{-1}  b!1(x!1)
  |-------
{1}   a!1(x!1)


I don't know how to do it,can you give me some advice. the follow is the example given by John



foo[T: TYPE]:THEORY
BEGIN

set1: TYPE = finite_set[T]
set2: TYPE = {t: finite_set[T]| FORALL (s:set1): subset?(t,s)}

a: VAR set1
b: VAR set2

test: LEMMA subset?(b,a)

END foo

You can then prove test from the type predicate on b.



best regards