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

At: vertex-count-less
For any graph the_obj:GraphObject(the_graph), P,Q:(V). (x:V. P(x) Q(x)) (x:V. P(x) & Q(x)) vertex-count(the_obj;x.P(x)) < vertex-count(the_obj;x.Q(x))
By:
Auto
THEN
Unfold `vertex-count` 0
THEN
Inst Thm* For any graph the_obj:GraphObject(the_graph), P:(V). no_repeats(V;vertex-subset(the_obj;x.P(x))) & (x:V. (x vertex-subset(the_obj;x.P(x))) P(x)) [the_graph;the_obj;P]
THEN
MoveToConcl -1
THEN
GenConclAtAddr [1;1;2]
THEN
Thin -1
THEN
Inst Thm* For any graph the_obj:GraphObject(the_graph), P:(V). no_repeats(V;vertex-subset(the_obj;x.P(x))) & (x:V. (x vertex-subset(the_obj;x.P(x))) P(x)) [the_graph;the_obj;Q]
THEN
MoveToConcl -1
THEN
GenConclAtAddr [1;1;2]
THEN
Thin -1
THEN
BackThru Thm* A,B:T List. no_repeats(T;A) (x:T. (x A) (x B)) (x:T. (x A) & (x B)) ||A|| < ||B||
Generated subgoals:

11. 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)
13. x: Vertices(the_graph)
14. (x z)
(x z1)		1 step
 
21. 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)		1 step

About:
listboolassertless_thanfunctionuniverseimpliesandallexists

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