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

The magma definition

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

Equations

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

The facts

theorem «Facts from All4x4Tables [[0,2,1,4,3,6,5,8,7],[3,1,5,0,7,2,8,4,6],[4,6,2,8,0,7,1,5,3],[7,5,8,3,6,1,4,0,2],[8,7,6,5,4,3,2,1,0],[6,8,4,7,2,5,0,3,1],[5,3,7,1,8,0,6,2,4],[2,4,0,6,1,8,3,7,5],[1,0,3,2,5,4,7,6,8]]» : ∃ (G : Type) (x : Magma G) (_ : Finite G), Equation2700 G ∧ ¬Equation2709 G ∧ ¬Equation2736 G ∧ ¬Equation2910 G ∧ ¬Equation2912 G ∧ ¬Equation4658 G