This file is generated from the following operator table: [[2,3,4,6,2,6,4,4,2],[4,2,4,5,2,3,0,7,2],[8,8,3,3,3,0,1,2,5],[8,8,2,3,7,0,1,2,5],[8,8,7,2,3,0,1,3,5],[2,4,4,7,2,2,3,4,6],[3,2,4,7,2,4,2,4,4],[8,8,3,2,7,0,1,3,5],[1,5,4,7,2,2,3,7,2]]

The magma definition

def «All4x4Tables [[2,3,4,6,2,6,4,4,2],[4,2,4,5,2,3,0,7,2],[8,8,3,3,3,0,1,2,5],[8,8,2,3,7,0,1,2,5],[8,8,7,2,3,0,1,3,5],[2,4,4,7,2,2,3,4,6],[3,2,4,7,2,4,2,4,4],[8,8,3,2,7,0,1,3,5],[1,5,4,7,2,2,3,7,2]]» : Magma (Fin 9)

Equations

• One or more equations did not get rendered due to their size.

The facts

theorem «Facts from All4x4Tables [[2,3,4,6,2,6,4,4,2],[4,2,4,5,2,3,0,7,2],[8,8,3,3,3,0,1,2,5],[8,8,2,3,7,0,1,2,5],[8,8,7,2,3,0,1,3,5],[2,4,4,7,2,2,3,4,6],[3,2,4,7,2,4,2,4,4],[8,8,3,2,7,0,1,3,5],[1,5,4,7,2,2,3,7,2]]» : ∃ (G : Type) (x : Magma G) (_ : Finite G), Equation3475 G ∧ ¬Equation3659 G ∧ ¬Equation4065 G ∧ ¬Equation4269 G ∧ ¬Equation4270 G ∧ ¬Equation4272 G ∧ ¬Equation4273 G ∧ ¬Equation4314 G ∧ ¬Equation4343 G ∧ ¬Equation4606 G ∧ ¬Equation4622 G ∧ ¬Equation4631 G ∧ ¬Equation4658 G