# I would like to know the simpler way to prove.

```Hi. PVS users.

I would like to know the simple command without instantiation.

I proved THEOREM group1check,  group3check, group2check with (inst )

command. But, I would like to know the automatic way to prove these

theorem. How can I do it?

love : THEORY

BEGIN

persontype : TYPE = {g1_p1, g1_p2,  g2_p2, g2_p3,
g2_p4, g3_p1, g3_p2}

group1set : setof[persontype] = {x : persontype |
x =  g1_p1 OR  x = g1_p2}
group1type : TYPE = (group1set)

group3set : setof[persontype] = {x : persontype |
x =  g3_p1 OR x = g3_p2}
group3type : TYPE = (group3set)

group2set : setof[persontype] = {x : persontype |
x = g2_p2 OR x = g2_p4 OR x = g2_p3}
group2type : TYPE = (group2set)

love : TYPE = [persontype, persontype]
loveset : setof[love]= { ele : love |
ele = (g1_p1, g2_p2) OR ele = (g1_p2, g2_p4) OR
ele = (g2_p2, g2_p3) OR ele = (g2_p2, g2_p4) OR
ele = (g2_p4, g2_p3) OR ele = (g2_p4, g3_p2) OR
ele = (g2_p3, g3_p1) }
lovetype :  TYPE = (loveset)

group1check: THEOREM FORALL (a1 : group1type):
EXISTS (a2 : group2type): member((a1,a2),loveset)
%(grind :if-match nil)(inst 1 "g2_p2")(inst 1 "g2_p4")

group3check: THEOREM FORALL (a1 : group3type):
EXISTS (a2 : group2type): member((a2,a1),loveset)
%(grind :if-match nil)(inst 1 "g2_p3")(inst 1 "g2_p4")

group2check: THEOREM FORALL (a1: group2type):
EXISTS (a2 : persontype): EXISTS (a3:persontype):
member((a2,a1), loveset) AND
member((a1,a3), loveset)
%(grind :if-match nil)(inst 1 "g1_p1" "g2_p3")(assert)(inst 1 "g1_p2" "g2_p3")(assert) (inst 1 "g2_p2" "g3_p1")(assert)

END love

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

```