This file is generated from the following operator table: [[0,1,1],[2,1,2],[0,0,2]]

The magma definition

def «All4x4Tables [[0,1,1],[2,1,2],[0,0,2]]» : Magma (Fin 3)

Equations

• «All4x4Tables [[0,1,1],[2,1,2],[0,0,2]]» = { op := MemoFinOp.extractWrapper 3 [65792, 131330, 131072] _proof_1✝ }

The facts

theorem «Facts from All4x4Tables [[0,1,1],[2,1,2],[0,0,2]]» : ∃ (G : Type) (x : Magma G) (_ : Finite G), Equation1481 G ∧ Equation1489 G ∧ Equation2337 G ∧ Equation2533 G ∧ Equation2787 G ∧ ¬Equation264 G ∧ ¬Equation283 G ∧ ¬Equation1025 G ∧ ¬Equation1516 G ∧ ¬Equation1847 G ∧ ¬Equation2243 G ∧ ¬Equation2253 G ∧ ¬Equation2263 G ∧ ¬Equation2300 G ∧ ¬Equation2446 G ∧ ¬Equation2449 G ∧ ¬Equation2466 G ∧ ¬Equation2496 G ∧ ¬Equation2543 G ∧ ¬Equation2649 G ∧ ¬Equation2709 G ∧ ¬Equation2804 G ∧ ¬Equation3058 G ∧ ¬Equation3197 G ∧ ¬Equation3316 G ∧ ¬Equation3343 G ∧ ¬Equation3346 G ∧ ¬Equation3353 G ∧ ¬Equation3519 G ∧ ¬Equation3546 G ∧ ¬Equation3556 G ∧ ¬Equation3749 G ∧ ¬Equation3752 G ∧ ¬Equation3759 G ∧ ¬Equation3867 G ∧ ¬Equation3952 G ∧ ¬Equation3962 G ∧ ¬Equation4128 G ∧ ¬Equation4165 G ∧ ¬Equation4269 G ∧ ¬Equation4291 G ∧ ¬Equation4320 G ∧ ¬Equation4406 G ∧ ¬Equation4435 G ∧ ¬Equation4445 G ∧ ¬Equation4480 G ∧ ¬Equation4606 G