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

How can I prove this?

Hi. PVS users, 
I always thank you for your kindness.
 
A month ago, I specified oldmember and proved theorem t1 
by (grind) in PVS.  

Nowadays, I change from oldmember to newmember(recursive form) 
and theorem t2. How can I prove theorem t2? 

poset : THEORY

  BEGIN

  atom : TYPE = {a,b,c,d,e,f}  
  elem : TYPE = [atom,atom]
  tset : TYPE = setof[elem] 
  
  fm(e:elem): atom = proj_1(e) 
  lm(e:elem): atom = proj_2(e)

  oldmember(p:elem,s:tset): bool = 
   (member(p,s) OR 
     EXISTS (a1,a2:elem):
      (member(a1,s) & member(a2,s) & 
        fm(a2) = lm(a1) & fm(a1) = fm(p) & lm(a2) = lm(p))) 

  newmember(p:elem,s:tset): INDUCTIVE bool = 
   (member(p,s) OR 
     EXISTS (a1,a2:elem):
      (newmember(a1,s) & newmember(a2,s) & 
        fm(a2) = lm(a1) & fm(a1) = fm(p) & lm(a2) = lm(p))) 

   dset: set[elem] = {e:elem | e=(a,b) or e = (b,c)}
   
   t1 :THEOREM  NOT EXISTS(a1,a2:atom) :  
                 (oldmember((a1,a2),dset) and 
                  oldmember((a2,a1),dset)) 

   t2 : THEOREM  NOT EXISTS(a1,a2:atom) :  
                 (newmember((a1,a2),dset) and 
                  newmember((a2,a1),dset)) 

  END poset4




-- 
Kim, Tae-ho
thkim@salmosa.kaist.ac.kr
http://salmosa.kaist.ac.kr/~thkim