Nuprl - Proof: vertex-subset-properties 1 1

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

1. the_graph: Graph
2. the_obj: GraphObject(the_graph)
3. P: Vertices(the_graph)
4. x,y:Vertices(the_graph). the_obj.eq(x,y) x = y
5. T:Type, s:T, x:Vertices(the_graph), f:(TVertices(the_graph)T). L:Vertices(the_graph) List. (y:Vertices(the_graph). x-the_graph- > y (y L)) & the_obj.eacc(f,s,x) = list_accum(s',x'.f(s',x');s;L)
6. T:Type, s:T, f:(TVertices(the_graph)T). L:Vertices(the_graph) List. no_repeats(Vertices(the_graph);L) & (y:Vertices(the_graph). (y L)) & the_obj.vacc(f,s) = list_accum(s',x'.f(s',x');s;L)
7. L: Vertices(the_graph) List
8. no_repeats(Vertices(the_graph);L)
9. y:Vertices(the_graph). (y L)

no_repeats(Vertices(the_graph);list_accum(s',x'.(l,x. if P(x) [x / l] else l fi)(s',x');nil;L)) & (x:Vertices(the_graph). (x list_accum(s',x'.(l,x. if P(x) [x / l] else l fi)(s',x');nil;L)) P(x))

By: All ReduceSOAps THEN RWO Thm* P:(T), L2,L1:T List. list_accum(l,x.if P(x) [x / l] else l fi;L1;L2) ~ (rev(filter(P;L2)) @ L1) 0 THEN RWO Thm* as:T List. (as @ nil) = as 0 THEN RWO Thm* x:T, L:T List. (x rev(L)) (x L) 0 THEN RWO Thm* P:(T), L:T List, x:T. (x filter(P;L)) (x L) & P(x) 0 THEN RWO Thm* L:T List. no_repeats(T;rev(L)) no_repeats(T;L) 0 THEN EasyHyp

Generated subgoal:

1 5. T:Type, s:T, x:Vertices(the_graph), f:(TVertices(the_graph)T). L:Vertices(the_graph) List. (y:Vertices(the_graph). x-the_graph- > y (y L)) & the_obj.eacc(f,s,x) = list_accum(s',x'.f(s',x');s;L)
6. T:Type, s:T, f:(TVertices(the_graph)T). L:Vertices(the_graph) List. no_repeats(Vertices(the_graph);L) & (y:Vertices(the_graph). (y L)) & the_obj.vacc(f,s) = list_accum(s',x'.f(s',x');s;L)
7. L: Vertices(the_graph) List
8. no_repeats(Vertices(the_graph);L)
9. y:Vertices(the_graph). (y L)
no_repeats(Vertices(the_graph);filter(P;L)) 1 step

About:

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