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) |