regularSubgroup.als

sig Element{}

one sig Group{
	elements: set Element,
	unit: one elements,
	mult: elements -> elements -> one elements,
	inv: elements -> one elements
}

fact NoRedundantElements{
	all e: Element | e in Group.elements
}

fact UnitLaw1{
	all a: Group.elements | Group.mult [a] [Group.unit] = a
}

fact UnitLaw2{
	all a: Group.elements |
	Group.mult [Group.unit] [a] = a
}

fact AssociativeLaw{
	all a: Group.elements | all b: Group.elements | all c:Group.elements |
	Group.mult [Group.mult [a] [b]] [c] = Group.mult [a] [Group.mult [b] [c]]
}

fact InvLaw1{
	all a: Group.elements | Group.mult [Group.inv[a]] [a] = Group.unit
}

assert InvLaw2 {
	all a: Group.elements | Group.mult [a] [Group.inv[a]] = Group.unit
}

//check InvLaw2

//run {}

assert Commutativity{
	all a: Group.elements | all b: Group.elements | Group.mult [a] [b] = Group.mult [b] [a]
}

assert Anticommutativity{
	some a: Group.elements | some b: Group.elements | Group.mult [a] [b] != Group.mult [b] [a]
}

//check Commutativity for 5
//check Commutativity for 6

//check Anticommutativity for 6 Element

//run {} for exactly 6 Element

pred subgroup (g: set Element, h: set Element){
	(all a: g | a in h) and
	(Group.unit in g) and
	(all a, b: g | Group.mult [a] [b] in g) and
	(all a: g | Group.inv[a] in g)
}

pred regularSubgroup(n: set Element, g: set Element){
	subgroup [n, g] and
	(all n0: n, g0: g | Group.mult [Group.mult [g0] [n0]] [Group.inv[g0]] in n)
}

// run {some g: set Element | regularSubgroup [g] [Group.elements]}

pred main(n1: set Element, n2: set Element){
	let g = Group.elements |
	regularSubgroup [n1, g] and
	(some g0: g | (not g0 in n1)) and
	regularSubgroup [n2, n1] and
	(some n10: n1 | (not n10 in n2)) and
	(not regularSubgroup [n2, g])
}

//run main for 7
run main for 8