# 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

```