graph 1 2 Sections Graphs Doc

Def x:A. B(x) == x:AB(x)

is mentioned by

Thm* f:(ABA). (a:A, b1,b2:B. f(a,b1) = f(a,b2) b1 = b2) (a,a':A. Dec(b:B. a' = f(a,b))) Graph(a:A -- > f(a,b) | b:B) Graph(a,a':A. b:B. a' = f(a,b))[fun-graph-rel-graph]
Thm* For any graph (x,y:V. Dec(x = y)) (x,y:V. x-the_graph- > *y x = y (z:V. z = x & x-the_graph- > z & z-the_graph- > *y))[connect-iff]
Thm* k:, L: List. 0 < ||L|| (r:. r- > L^k)[Ramsey]
Thm* k:, L: List. k-1- > L^k (i:||L||. L[i] < k)[trivial-arrows]
Thm* n,k:, c:(nk). p:(k( List)). sum(||p(j)|| | j < k) = n & (j:k, x,y:||p(j)||. x < y (p(j))[x] > (p(j))[y]) & (j:k, x:||p(j)||. (p(j))[x] < n & c((p(j))[x]) = j)[finite-partition]
Def G H == vmap:(Vertices(G)Vertices(H)), emap:(Edges(G)Edges(H)). Bij(Vertices(G); Vertices(H); vmap) & Bij(Edges(G); Edges(H); emap) & (vmap,vmap) o Incidence(G) = Incidence(H) o emap[graph-isomorphic]
Def dfsl-traversal(the_graph;L;s) == df-traversal(the_graph;s) & (i:Vertices(the_graph). (inl(i) s) L-the_graph- > *i) & ((i:Vertices(the_graph). L-the_graph- > *i non-trivial-loop(the_graph;i)) (L1,L2:Vertices(the_graph) List. L = (L1 @ L2) (s1,s2:traversal(the_graph). s = (s2 @ s1) traversal(the_graph) & paren(Vertices(the_graph);s1) & paren(Vertices(the_graph);s2) & (j:Vertices(the_graph). ((inl(j) s1) L1-the_graph- > *j) & ((inl(j) s2) L2-the_graph- > *j & L1-the_graph- > *j)))))[dfsl-traversal]
Def non-trivial-loop(G;i) == j:Vertices(G). j = i & i-G- > *j & j-G- > *i[non-trivial-loop]
Def x-the_graph- > *y == p:Vertices(the_graph) List. path(the_graph;p) & p[0] = x & last(p) = y[connect]
Def x-the_graph- > y == e:Edges(the_graph). Incidence(the_graph)(e) = < x,y > [edge]
Def paren(T;s) == s = nil (T+T) List (t:T, s':(T+T) List. s = ([inl(t)] @ s' @ [inr(t)]) & paren(T;s')) (s',s'':(T+T) List. ||s'|| < ||s|| & ||s''|| < ||s|| & s = (s' @ s'') & paren(T;s') & paren(T;s'')) (recursive)[paren]
Def r- > L^k == n:. rn (G:({s:(n List)| ||s|| = k & (x,y:||s||. x < y s[x] < s[y]) }||L||). c:||L||, f:(L[c]n). increasing(f;L[c]) & (s:L[c] List. ||s|| = k (x,y:||s||. x < y s[x] < s[y]) G(map(f;s)) = c))[arrows]

In prior sections: core int 2 num thy 1 fun 1 mb nat mb list 1 mb list 2 graph 1 1

Try larger context: Graphs

graph 1 2 Sections Graphs Doc