sig Universum { op: Universum set -> set Universum // (x->y->z in op) <=> (x*y = z) }{} one sig e in Universum {}{} pred H { // Closure: x*y = z all x:Universum | all y:Universum | some z:Universum | x->y->z in op // Associativity: (x*y)*z = x*(y*z) all x:Universum | all y:Universum | all z:Universum | all xy:Universum | all yz:Universum | all xyz:Universum | all xyz':Universum | ( (x->y->xy in op) and (xy->z->xyz in op) // (x*y)*z and (y->z->yz in op) and (x->yz->xyz' in op) // x*(y*z) ) => xyz = xyz' // Identity: x*e = x = e*x all x:Universum | (x->e->x in op) and (e->x->x in op) // Inverse: x*y = e = y*x all x:Universum | some y:Universum | (x->y->e in op) and (y->x->e in op) } run H for 3 Universum