(3steps total) PrintForm Definitions Lemmas graph 1 3 Sections Graphs Doc

At: vertex-count-less 2

1. the_graph: Graph
2. the_obj: GraphObject(the_graph)
3. P: Vertices(the_graph)
4. Q: Vertices(the_graph)
5. x:Vertices(the_graph). P(x) Q(x)
6. x:Vertices(the_graph). P(x) & Q(x)
7. z: Vertices(the_graph) List
8. z1: Vertices(the_graph) List
9. no_repeats(Vertices(the_graph);z1)
10. x:Vertices(the_graph). (x z1) Q(x)
11. no_repeats(Vertices(the_graph);z)
12. x:Vertices(the_graph). (x z) P(x)
x:Vertices(the_graph). (x z) & (x z1)

By:
ParallelOp 6
THEN
ParallelOp 7
THEN
EasyHyp
THEN
ParallelOp 7
THEN
EasyHyp


Generated subgoals:

None

About:
listboolassertfunctionimpliesandallexists

(3steps total) PrintForm Definitions Lemmas graph 1 3 Sections Graphs Doc