language Essence 1.3

$The Ramsey number R(k,l) is the smallest number such that$ if we two-colour the edges of complete graph of this size,
$there always exists a monochromatic subgraph of either k or l nodes.$ In other words (from Wikipedia):
$The Ramsey number, R(k,l), gives the solution to the party problem,$ which asks the minimum number of guests, R(k,l), that must be invited
$so that at least k will know each other$      or at least l will not know each other.

$Here, we are modelling the Ramsey-graph problem which is the problem of finding counter-examples.$ For a given k,l, and num_vertices: find a colouring of the complete graph
$which does not have a blue-subgraph nor a red-subgraph. given k, l, num_vertices : int$ due to symmetry R(k, l) = R(l,k)
where k <= l

$complete graph, to we can calculate the number of edges letting num_edges be num_vertices * (num_vertices - 1)$ we are two-colouring
letting Colour be new type enum {red, blue}

letting Vertex be domain int(1..num_vertices)

find graph : function (size num_edges) (Vertex, Vertex) --> Colour

$the graph is complete such that forAll i,j : Vertex . i < j -> (i,j) in defined(graph) /\ graph((i,j)) = graph((j,i)), forAll i : Vertex . !((i,i) in defined(graph))$ there isn't a red-subgraph of size k
such that
forAll subgraph_vertices : set (size k) of Vertex .
!(forAll {i,j} subsetEq subgraph_vertices . graph((i,j)) = red)

\$ there isn't a blue-subgraph of size l
such that
forAll subgraph_vertices : set (size l) of Vertex .
!(forAll {i,j} subsetEq subgraph_vertices . graph((i,j)) = blue)