017: Ramsey Numbers

language Essence 1.3
$ Ramsey's theorem
$ Decide if a complete graph K_n  with edges coloured with c colours must have a monochromatic triangle
$ Keeps edges in both directions

given n : int(1..20)
given colours : int(1..10)

letting num_edges be  (n * (n-1)) 

$ could made these an unamed type
letting  Colour be domain int(1..colours)
letting  Vertex be domain int(1..n)

find graph : relation (size num_edges)  of ( Colour * Vertex * Vertex  )

such that

$ make sure the it's a complete graph
forAll i : Vertex .
    |(toSet(graph(_,i,_) ))| = (n - 1) /\
    |(toSet(graph(_,_,i) ))| = (n - 1) /\
    |(toSet(graph(_,i,i) ))| = 0,

forAll i, j :  Vertex , i != j . 
   |(toSet(graph(_,i,j) ))|  = 1 /\ 
   |(toSet(graph(_,j,i) ))|  = 1 /\
   graph(_,i,j) = graph(_,j,i),


$ check for a  monochromatic triangle
forAll i : Vertex .
    forAll (c,e1) in toSet(graph(_, i, _) ) .
        forAll tuple (t) in  toSet(graph(c, i, _) )  , t != e1 .
            !graph(c, t, e1)