Equation 3588 to Equations of order greater than…

DefinitionEquation 3588#

Equation 3588 is the law \(0 \diamond 1 \simeq 2 \diamond ((0 \diamond 1) \diamond 2)\) (or the equation \(x \diamond y = z \diamond ((x \diamond y) \diamond z)\)).

Lean

Formalized as Equation3588.

Sources
LeanEquation3588
Uses 1 · Used by 2
Statement usesMagma
Used by3994 implies 3588 for finite models · 3994 does not imply 3588 for infinite models

Our project located this law as one member of an “Austin pair”; see Finite implications and infinite models.

DefinitionEquation 3722#

Equation 3722 is the law \(0 \diamond 1 \simeq (0 \diamond 1) \diamond (0 \diamond 1)\) (or the equation \(x \diamond y = (x \diamond y) \diamond (x \diamond y)\)).

Lean

Formalized as Equation3722.

Sources
LeanEquation3722
Uses 1 · Used by 1
Statement usesMagma
Used by3744 implies 3722, 381

Appears in Putnam 1978, Problem A4, part (a). It is self-dual.

DefinitionEquation 3744#

Equation 3744 is the law \(0 \diamond 1 \simeq (0 \diamond 2) \diamond (3 \diamond 1)\) (or the equation \(x \diamond y = (x \diamond z) \diamond (w \diamond y)\)).

Lean

Formalized as Equation3744.

Sources
LeanEquation3744
Uses 1 · Used by 1
Statement usesMagma
Used by3744 implies 3722, 381

This law is called a “bypass operation” in Putnam 1978, Problem A4. It is self-dual. See 3744 implies 3722, 381.

Our project located this law as one member of an “Austin pair”; see Finite implications and infinite models.

DefinitionEquation 4315#

Equation 4315 is the law \(0 \diamond (1 \diamond 0) \simeq 0 \diamond (1 \diamond 2)\) (or the equation \(x \diamond (y \diamond x) = x \diamond (y \diamond z)\)).

Lean

Formalized as Equation4315.

Sources
LeanEquation4315
Uses 1 · Used by 1
Statement usesMagma
Used by1659 does not imply 4315

DefinitionEquation 4512#

Equation 4512 is the law \(0 \diamond (1 \diamond 2) \simeq (0 \diamond 1) \diamond 2\) (or the equation \(x \diamond (y \diamond z) = (x \diamond y) \diamond z\)).

Lean

Formalized as Equation4512.

Sources
LeanEquation4512
Uses 1 · Used by 1
Statement usesMagma
Used byConsequences of 1571

The associative law. It is self-dual.

DefinitionEquation 4513#

Equation 4513 is the law \(0 \diamond (1 \diamond 2) \simeq (0 \diamond 1) \diamond 3\) (or the equation \(x \diamond (y \diamond z) = (x \diamond y) \diamond w\)).

Lean

Formalized as Equation4513.

Sources
LeanEquation4513
Uses 1
Statement usesMagma

DefinitionEquation 4522#

Equation 4522 is the law \(0 \diamond (1 \diamond 2) \simeq (0 \diamond 3) \diamond 4\) (or the equation \(x \diamond (y \diamond z) = (x \diamond w) \diamond u\)).

Lean

Formalized as Equation4522.

Sources
LeanEquation4522
Uses 1
Statement usesMagma

Dual to E4579.

DefinitionEquation 4564#

Equation 4564 is the law \(0 \diamond (1 \diamond 2) \simeq (3 \diamond 1) \diamond 2\) (or the equation \(x \diamond (y \diamond z) = (w \diamond y) \diamond z\)).

Lean

Formalized as Equation4564.

Sources
LeanEquation4564
Uses 1
Statement usesMagma

Dual to E4513.

DefinitionEquation 4579#

Equation 4579 is the law \(0 \diamond (1 \diamond 2) \simeq (3 \diamond 4) \diamond 2\) (or the equation \(x \diamond (y \diamond z) = (w \diamond u) \diamond z\)).

Lean

Formalized as Equation4579.

Sources
LeanEquation4579
Uses 1
Statement usesMagma

Dual to E4522.

DefinitionEquation 4582#

Equation 4582 is the law \(0 \diamond (1 \diamond 2) \simeq (3 \diamond 4) \diamond 5\) (or the equation \(x \diamond (y \diamond z) = (w \diamond u) \diamond v\)).

Lean

Formalized as Equation4582.

Sources
LeanEquation4582
Uses 1
Statement usesMagma

This law asserts that all triple constants (regardless of bracketing) are constant.

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.