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

The magma definition

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

Equations

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

The facts

theorem «Facts from All4x4Tables [[2,8,7,2,8,8,2,7,7],[1,1,0,6,6,6,1,0,0],[3,3,0,6,6,6,3,0,0],[1,1,0,6,6,6,1,0,0],[3,3,5,4,4,4,3,5,5],[2,8,7,2,8,8,2,7,7],[3,3,5,4,4,4,3,5,5],[2,8,7,2,8,8,2,7,7],[1,1,5,4,4,4,1,5,5]]» : ∃ (G : Type) (x : Magma G) (_ : Finite G), Equation168 G ∧ ¬Equation3461 G ∧ ¬Equation3462 G ∧ ¬Equation3521 G ∧ ¬Equation3522 G ∧ ¬Equation3864 G ∧ ¬Equation3880 G ∧ ¬Equation3915 G ∧ ¬Equation3952 G ∧ ¬Equation4268 G ∧ ¬Equation4314 G ∧ ¬Equation4606 G ∧ ¬Equation4666 G