# Differences

This shows you the differences between two versions of the page.

equations [2017/10/02 10:44]
jipsen
equations [2017/10/02 10:57] (current)
jipsen
Line 65: Line 65:
def involutive              := ∀x,     h(h x) = x def involutive              := ∀x,     h(h x) = x
-def inverse_ops             := ∀x,     h(k x) = x+def inverse_operations      := ∀x,     h(k x) = x
def left_absorption         := ∀x,     h(k x) = k x def left_absorption         := ∀x,     h(k x) = k x
def right_absorption        := ∀x,     h(k x) = h x def right_absorption        := ∀x,     h(k x) = h x
Line 74: Line 74:
def left_zero               := ∀x,     0⬝x = 0 def left_zero               := ∀x,     0⬝x = 0
def right_zero              := ∀x,     x⬝0 = 0 def right_zero              := ∀x,     x⬝0 = 0
-def left_projection         := ∀x y,   x⬝y = h x
-def right_projection        := ∀x y,   x⬝y = h y
-def squareconstant          := ∀x,     x⬝x = 1
-def square_unary            := ∀x,     x⬝x = h x
-def left_const_mult         := ∀x,     1⬝x = h x
-def right_const_mult        := ∀x,     x⬝1 = h x
-def commutative             := ∀x y,   x⬝y = y⬝x
def left_inverse            := ∀x,     x⁻¹⬝x = 1 def left_inverse            := ∀x,     x⁻¹⬝x = 1
def right_inverse           := ∀x,     x⬝x⁻¹ = 1 def right_inverse           := ∀x,     x⬝x⁻¹ = 1
+def left_const_mult         := ∀x,     c⬝x = h x
+def right_const_mult        := ∀x,     x⬝c = h x
+def square_constant         := ∀x,     x⬝x = c
+def square_unary            := ∀x,     x⬝x = h x
def left_unary_identity     := ∀x,     (h x)⬝x = x def left_unary_identity     := ∀x,     (h x)⬝x = x
def right_unary_identity    := ∀x,     x⬝(h x) = x def right_unary_identity    := ∀x,     x⬝(h x) = x
-def associative             := ∀x y z, x⬝(y⬝z) = (x⬝y)⬝z +def left_unary_const_mult   := ∀x,    h(c⬝x) = c⬝(h x
-def left_commutative        := ∀x y z, x⬝(y⬝z) = y⬝(x⬝z+def right_unary_const_mult  := ∀x,    h(x⬝c) = (h x)⬝c
-def right_commutative       := ∀x y z, (x⬝y)⬝z = (x⬝z)⬝y +def commutative             := ∀x y,  x⬝y = y⬝x
-def interassociative1       := ∀x y z, x⬝(y+z) = (x⬝y)+z +def left_unary_projection   := ∀x y,  x⬝y = h x
-def interassociative2       := ∀x y z, x⬝(y+z) = (x+y)⬝z+def right_unary_projection  := ∀x y,  x⬝y = h y
def left_idempotent         := ∀x y,   x⬝(x⬝y) = x⬝y def left_idempotent         := ∀x y,   x⬝(x⬝y) = x⬝y
def right_idempotent        := ∀x y,   (x⬝y)⬝y = x⬝y def right_idempotent        := ∀x y,   (x⬝y)⬝y = x⬝y
Line 100: Line 97:
def left_subtraction        := ∀x y,   x⬝(x+y) = y def left_subtraction        := ∀x y,   x⬝(x+y) = y
def right_subtraction       := ∀x y,   (y+x)⬝x = y def right_subtraction       := ∀x y,   (y+x)⬝x = y
-def left_distributive       := ∀x y z, x⬝(y+z) = (x⬝y)+(x⬝z)
-def right_distributive      := ∀x y z, (x+y)⬝z = (x⬝z)+(y⬝z)
-def left_self_distributive  := ∀x y z, x⬝(y⬝z) = (x⬝y)⬝(x⬝z)
-def right_self_distributive := ∀x y z, (x⬝y)⬝z = (x⬝z)⬝(y⬝z)
def unary_commutative       := ∀x y,   (h x)⬝(h y) = (h y)⬝(h x) def unary_commutative       := ∀x y,   (h x)⬝(h y) = (h y)⬝(h x)
def unary_involutive        := ∀x y,   h(x⬝y) = (h y)⬝(h x) def unary_involutive        := ∀x y,   h(x⬝y) = (h y)⬝(h x)
def interdistributive       := ∀x y,   h(x⬝y) = (h x)+(h y) def interdistributive       := ∀x y,   h(x⬝y) = (h x)+(h y)
def unary_distributive      := ∀x y,   h(x⬝y) = (h x)⬝(h y) def unary_distributive      := ∀x y,   h(x⬝y) = (h x)⬝(h y)
-def left_unary_const_mult   := ∀x,     h(1⬝x) = 1⬝(h x)
-def right_unary_const_mult  := ∀x,     h(x⬝1) = (h x)⬝1
def left_twisted            := ∀x y,   (h(x⬝y))⬝x = x⬝(h y) def left_twisted            := ∀x y,   (h(x⬝y))⬝x = x⬝(h y)
def right_twisted           := ∀x y,   x⬝(h(y⬝x)) = (h y)⬝x def right_twisted           := ∀x y,   x⬝(h(y⬝x)) = (h y)⬝x
Line 119: Line 110:
def right_absorbtive        := ∀x y,   (h(x⬝y))⬝(h y) = h(x⬝y) def right_absorbtive        := ∀x y,   (h(x⬝y))⬝(h y) = h(x⬝y)
def flexible                := ∀x y,   (x⬝y)⬝x = x⬝(y⬝x) def flexible                := ∀x y,   (x⬝y)⬝x = x⬝(y⬝x)
-def entropic                := ∀x y z w, (x⬝y)(z⬝w) = (x⬝z)(y⬝w+def associative             := ∀x y z, x⬝(y⬝z) = (x⬝y)⬝z
-def paramedial              := ∀x y z w, (x⬝y)⬝(z⬝w) = (w⬝y)⬝(z⬝x)+def left_commutative        := ∀x y z, x⬝(y⬝z) = y⬝(x⬝z)
+def right_commutative       := ∀x y z, (x⬝y)⬝z = (x⬝z)⬝y
+def interassociative1       := ∀x y z, x⬝(y+z) = (x⬝y)+z
+def interassociative2       := ∀x y z, x⬝(y+z) = (x+y)⬝z
+def left_distributive       := ∀x y z, x⬝(y+z) = (x⬝y)+(x⬝z)
+def right_distributive      := ∀x y z, (x+y)⬝z = (x⬝z)+(y⬝z)
+def left_self_distributive  := ∀x y z, x⬝(y⬝z) = (x⬝y)⬝(x⬝z)
+def right_self_distributive := ∀x y z, (x⬝y)⬝z = (x⬝z)⬝(y⬝z)
def Moufang1                := ∀x y z, ((x⬝y)⬝x)⬝z = x⬝(y⬝(x⬝z)) def Moufang1                := ∀x y z, ((x⬝y)⬝x)⬝z = x⬝(y⬝(x⬝z))
def Moufang2                := ∀x y z, ((x⬝y)⬝z)⬝y = x⬝(y⬝(z⬝y)) def Moufang2                := ∀x y z, ((x⬝y)⬝z)⬝y = x⬝(y⬝(z⬝y))
def Moufang3                := ∀x y z, (x⬝y)⬝(z⬝x) = (x⬝(y⬝z))⬝x def Moufang3                := ∀x y z, (x⬝y)⬝(z⬝x) = (x⬝(y⬝z))⬝x
def Moufang4                := ∀x y z, (x⬝y)⬝(z⬝x) = x⬝((y⬝z)⬝x) def Moufang4                := ∀x y z, (x⬝y)⬝(z⬝x) = x⬝((y⬝z)⬝x)
+def entropic                := ∀x y z w, (x⬝y)⬝(z⬝w) = (x⬝z)⬝(y⬝w)
+def paramedial              := ∀x y z w, (x⬝y)⬝(z⬝w) = (w⬝y)⬝(z⬝x)
+
end identities end identities
</code> </code>