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

The magma definition

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

Equations

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

The facts

theorem «Facts from All4x4Tables [[1,2,5,6,4,3,7,0],[4,3,0,7,1,2,6,5],[2,1,7,0,3,4,5,6],[0,6,4,2,5,7,3,1],[7,5,2,4,6,0,1,3],[6,0,3,1,7,5,4,2],[3,4,6,5,2,1,0,7],[5,7,1,3,0,6,2,4]]» : ∃ (G : Type) (x : Magma G) (_ : Finite G), Equation1587 G ∧ ¬Equation411 G ∧ ¬Equation614 G ∧ ¬Equation817 G ∧ ¬Equation1020 G ∧ ¬Equation1229 G ∧ ¬Equation1241 G ∧ ¬Equation1248 G ∧ ¬Equation1252 G ∧ ¬Equation1276 G ∧ ¬Equation1278 G ∧ ¬Equation1429 G ∧ ¬Equation1434 G ∧ ¬Equation1488 G ∧ ¬Equation1515 G ∧ ¬Equation1519 G ∧ ¬Equation1629 G ∧ ¬Equation1832 G ∧ ¬Equation2035 G ∧ ¬Equation2238 G ∧ ¬Equation2441 G ∧ ¬Equation2647 G ∧ ¬Equation2650 G ∧ ¬Equation2652 G ∧ ¬Equation2660 G ∧ ¬Equation2662 G ∧ ¬Equation2699 G ∧ ¬Equation2710 G ∧ ¬Equation2746 G ∧ ¬Equation2847 G ∧ ¬Equation3050 G ∧ ¬Equation3253 G ∧ ¬Equation3456 G ∧ ¬Equation3659 G ∧ ¬Equation3862 G ∧ ¬Equation4065 G ∧ ¬Equation4270 G ∧ ¬Equation4273 G ∧ ¬Equation4275 G ∧ ¬Equation4283 G ∧ ¬Equation4290 G ∧ ¬Equation4320 G ∧ ¬Equation4380 G ∧ ¬Equation4585 G ∧ ¬Equation4588 G ∧ ¬Equation4590 G ∧ ¬Equation4598 G ∧ ¬Equation4605 G ∧ ¬Equation4635 G