Thm* f:(A B A). ( 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:( n  k). 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: . r n  ( 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] |