Nuprl - Proof: vertex-count-le

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

For any graph the_obj:GraphObject(the_graph), P,Q:(V). (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)) ||A||||B||

Generated subgoal:

1 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. z: Vertices(the_graph) List
7. z1: Vertices(the_graph) List
8. no_repeats(Vertices(the_graph);z1)
9. x:Vertices(the_graph). (x z1) Q(x)
10. no_repeats(Vertices(the_graph);z)
11. x:Vertices(the_graph). (x z) P(x)
12. x: Vertices(the_graph)
13. (x z)
(x z1) 1 step

About:

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