053: Graceful Graphs

language Essence 1.3

given n : int(1..) $ The size of the wheel

letting V be domain int(0..2*n)       $ The vertices
letting E be domain int(0..3*n-1)     $ The Edges
letting Colours be domain int(0..3*n) $ The colours
letting W be domain int(0..n-1)       $ The wheel
letting C be 2*n                      $ The centre

find colouring : function(total,injective) V --> Colours
find edgeID    : function(total,injective) E --> Colours

such that
  $ Wheel is graceful
  forAll v : W .
    edgeID(v) = |colouring(v)-colouring((v+1)%n)|,

  $ satellites are graceful
  forAll v : W .
    edgeID(v+n) = |colouring(v)-colouring(v+n)|,

  $ connections to centre are graceful
  forAll v : W .
    edgeID(v+2*n) = |colouring(C)-colouring(v)|