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

The magma definition

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

Equations

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

The facts

theorem «Facts from All4x4Tables [[1,2,4,4,0,0,0,2],[4,6,4,1,6,1,1,1],[1,3,2,2,7,2,3,3],[1,3,3,3,7,3,3,3],[4,5,5,2,4,4,4,2],[5,5,5,5,5,0,7,3],[6,6,4,6,6,0,6,6],[1,7,4,7,6,4,7,7]]» : ∃ (G : Type) (x : Magma G) (_ : Finite G), Equation834 G ∧ ¬Equation1020 G ∧ ¬Equation1224 G ∧ ¬Equation1225 G ∧ ¬Equation1229 G ∧ ¬Equation1239 G ∧ ¬Equation1241 G ∧ ¬Equation1242 G ∧ ¬Equation1249 G ∧ ¬Equation1251 G ∧ ¬Equation1252 G ∧ ¬Equation1832 G ∧ ¬Equation3253 G ∧ ¬Equation3659 G ∧ ¬Equation3864 G ∧ ¬Equation3865 G ∧ ¬Equation3867 G ∧ ¬Equation3870 G ∧ ¬Equation3878 G ∧ ¬Equation3881 G ∧ ¬Equation3887 G ∧ ¬Equation3888 G ∧ ¬Equation3915 G ∧ ¬Equation3925 G ∧ ¬Equation3928 G ∧ ¬Equation4065 G ∧ ¬Equation4269 G ∧ ¬Equation4270 G ∧ ¬Equation4293 G ∧ ¬Equation4314 G ∧ ¬Equation4583 G ∧ ¬Equation4591 G ∧ ¬Equation4598 G ∧ ¬Equation4606 G ∧ ¬Equation4608 G ∧ ¬Equation4622 G ∧ ¬Equation4631 G ∧ ¬Equation4636 G ∧ ¬Equation4647 G