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