Download
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
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)