/* graph coloring */
/*datatype colors = red | green | blue | yellow | white | black. */
/*datatype nodes = node of nat colors. */  /* node numbers are represented by nat */
/*datatype edges = edge of nat nat. */

/*function diffcolors: colors * (list nat) * (list nodes)-> bool.*/
diffcolors C [] N := true.
diffcolors C [I|L] N := if (eqcol C (color I N)) then false else (diffcolors C L N).

/*function color: nat * (list nodes) -> colors.*/
color I [node(J,C) | L] := if (I = J) then C else (color I L).

/*function neighbors: nat * (list edges) -> (list nat).*/
neighbors I [] := [].
neighbors I [edge(J,K) | E] := if (I = K) then [J | neighbors I E] else
                               if (I = J) then [K | neighbors I E] else
                                        neighbors I E.

/*function eqcol: colors * colors -> bool.*/
eqcol C1 C2 := (allowed C1, allowed C2,(C1=C2)). /* here result direction cuts early*/

/*function allowed: colors -> bool.*/
allowed red   := true.
allowed green := true.
allowed blue  := true.

/*function check: (list nodes) * (list nodes) * (list edges) -> bool.*/
check [] N E := true.
check [node(I,C) | L] N E := (diffcolors C (neighbors I E) N, check L N E).

/* example: shuffle exchange network with 16 nodes; 3 colors needed. goal: */
goal [C0,C1,C2,C3,C4,C5,C6,C7,C8,C9,C10,C11,C12,C13,C14,C15] :=
   if
      ((Nodes = [node(0,C0), node(1,C1), node(2,C2), node(3,C3), node(4,C4),
                  node(5,C5), node(6,C6), node(7,C7), node(8,C8), node(9,C9),
                  node(10,C10), node(11,C11), node(12,C12), node(13,C13),
                  node(14,C14), node(15,C15)]),
       (Edges = [edge(0, 1), edge(2, 3), edge(4, 5), edge(6, 7), edge(8, 9),
                 edge(10, 11), edge(12, 13), edge(14, 15),
                 edge(1, 2), edge(2, 4), edge(4, 8), edge(8, 1),
                 edge(3, 6), edge(6, 12), edge(12, 9), edge(9, 3),
                 edge(5, 10), edge(10, 5),
                 edge(7, 14), edge(14, 13), edge(13, 11), edge(11, 7)]),
       check Nodes Nodes Edges) then true.

/* goal :  goal X  */