Magma

$\textbf{Magma} \; A \; \otimes$

---

$\textbf{Function} \; (A \times A) \; A \; \otimes$

---

pred Magma(A: set univ, op: univ->univ->univ) {
  op in (A->A)-> one A
}

$\textbf{AutoInverse} \; A \; f \; I$

---

$\textbf{Unital} \; A \; f\; I$

$\forall(x \in 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
}

$\textbf{Idempotent} \; A \; \otimes$

---

$\textbf{Magma} \; A \; \otimes$

$\forall(a \in A :: a \otimes a = a)$

---

pred Idempotent(A: set univ, op: univ->univ->univ) {
  Magma[A,op]
  all a: A | op[a,a] = a
}

$\textbf{Inverse} \; A \; f \; I \; y \; x$

---

$\textbf{LeftInverse} \; A \; f \; I \; y \; x$

$\textbf{RightInverse} \; A \; f \; I \; y \; x$

---

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]
}

$\textbf{LeftInverse} \; A \; f \; I \; y \; x$

---

$\textbf{Unital} \; A \; f \; I$

$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
}

$\textbf{LeftUnit} \; A \; \otimes \; I$

---

$\textbf{Magma} \; A \; \otimes$

$I \in A$

$\forall(x \in A :: I \otimes 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
}

$\textbf{LeftZero} \; A \; f \; Z$

---

$\textbf{Magma} \; A \; \otimes$

$I \in A$

$\forall(x \in 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
}

$\textbf{RightInverse} \; A \; f \; I \; y \; x$

---

$\textbf{Unital} \; A \; f \; I$

$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
}

$\textbf{RightUnit} \; A \; \otimes \; I$

---

$\textbf{Magma} \; A \; \otimes$

$I \in A$

$\forall(x \in A :: x = x \otimes 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]
}

$\textbf{RightZero} \; A \; f \; Z$

---

$\textbf{Magma} \; A \; \otimes$

$I \in A$

$\forall(x \in 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
}

$\textbf{Symmetric} \; A \; \otimes$

---

$\textbf{Magma} \; A \; \otimes$

$\forall(x,y \in A :: x \otimes y = y \otimes x)$

---

pred Symmetric(A: set univ, op: univ->univ->univ) {
  Magma[A,op]
  all x,y: A | op[x,y] = op[y,x]
}

$\textbf{Unital} \; A \; \otimes \; I$

---

$\textbf{LeftUnit} \; A \; \otimes \; I$

$\textbf{RightUnit} \; A \; \otimes \; I$

---

pred Unital(A: set univ, op: univ->univ->univ, I: univ) {
  LeftUnit[A,op,I]
  RightUnit[A,op,I]
}

$\textbf{Zero} \; A \; f \; Z$

---

$\textbf{LeftZero} \; A \; f \; Z$

$\textbf{RightZero} \; A \; f \; Z$

---

pred Zero(A: set univ, f: univ->univ->univ, Z: univ) {
  LeftZero[A,f,Z]
  RightZero[A,f,Z]
}