Magma
AutoInverseAfI
UnitalAfI
β(xβA::f(x,x)=I)
pred AutoInverse(A: set univ, f: univ->univ->univ, I: univ) {
Unital[A,f,I]
all x: A | f[x,x] = I
}
IdempotentAβ
MagmaAβ
β(aβA::aβa=a)
pred Idempotent(A: set univ, op: univ->univ->univ) {
Magma[A,op]
all a: A | op[a,a] = a
}
InverseAfIyx
LeftInverseAfIyx
RightInverseAfIyx
pred Inverse(A: set univ, f: univ->univ->univ, I,y,x: univ) {
LeftInverse[A,f,I,y,x]
RightInverse[A,f,I,y,x]
}
LeftInverseAfIyx
UnitalAfI
f(L,x)=I
pred LeftInverse(A: set univ, f: univ->univ->univ, I,L,x: univ) {
Unital[A,f,I]
f[L,x] = I
}
LeftUnitAβI
MagmaAβ
IβA
β(xβA::Iβx=x)
pred LeftUnit(A: set univ, op: univ->univ->univ, I: univ) {
Magma[A,op]
I in A
all x: A | op[I,x] = x
}
LeftZeroAfZ
MagmaAβ
IβA
β(xβA::f(Z,x)=Z)
pred LeftZero(A: set univ, f: univ->univ->univ, Z: univ) {
Magma[A,f]
Z in A
all x: A | f[Z,x] = Z
}
RightInverseAfIyx
UnitalAfI
f(x,R)=I
pred RightInverse(A: set univ, f: univ->univ->univ, I,R,x: univ) {
Unital[A,f,I]
f[x,R] = I
}
RightUnitAβI
MagmaAβ
IβA
β(xβA::x=xβI)
pred RightUnit(A: set univ, op: univ->univ->univ, I: univ) {
Magma[A,op]
I in A
all x: A | x = op[x,I]
}
RightZeroAfZ
MagmaAβ
IβA
β(xβA::f(x,Z)=Z)
pred RightZero(A: set univ, f: univ->univ->univ, Z: univ) {
Magma[A,f]
Z in A
all x: A | f[x,Z] = Z
}
SymmetricAβ
MagmaAβ
β(x,yβA::xβy=yβx)
pred Symmetric(A: set univ, op: univ->univ->univ) {
Magma[A,op]
all x,y: A | op[x,y] = op[y,x]
}
Last updated