非可換環を探す

noncomm_ring.als

sig R {
  plus : R -> one R,
	opp : R,
	mult : R -> one R
}
one sig O extends R {}
one sig I extends R {}
 
fact Rplus_abelian {
	all x,y,z : R | x.plus[y].plus[z] = x.plus[y.plus[z]]
	all x : R | x.plus[O] = x
	all x : R | x.plus[x.opp] = O
	all x,y : R | x.plus[y] = y.plus[x]
}
fact Rmult_monoid {
	all x,y,z : R | x.mult[y].mult[z] = x.mult[y.mult[z]]
	all x : R | x.mult[I] = x
	all x : R | I.mult[x] = x
}
fact Rdist {
	all x,y,z : R | x.plus[y].mult[z] = x.mult[z].plus[y.mult[z]]
	all x,y,z : R | x.mult[y.plus[z]] = x.mult[y].plus[x.mult[z]]
}

fact Rnoncomm {
	some x,y : R | x.mult[y] != y.mult[x]
}

run {} for 8
run {} for 7