Documentation

equational_theories.Generated.All4x4Tables.Refutation37

This file is generated from the following operator table: [[1,2,0,16,3,4,13,2,0,1,8,8,9,1,4,9,14],[13,5,8,7,6,12,5,5,9,13,4,4,4,2,12,4,11],[0,9,1,4,14,16,8,9,1,0,13,13,2,0,16,2,3],[14,11,3,0,15,15,7,11,4,14,12,12,6,16,15,6,0],[16,7,4,0,0,15,6,7,14,16,11,11,12,3,15,12,15],[3,6,14,15,0,0,12,6,16,3,7,7,11,4,0,11,15],[9,4,2,6,12,11,5,4,8,9,4,4,5,13,11,5,7],[13,5,8,7,6,12,5,5,9,13,4,4,4,2,12,4,11],[1,13,0,14,16,3,9,13,1,1,2,2,8,0,3,8,4],[1,2,0,16,3,4,13,2,0,1,8,8,9,1,4,9,14],[2,5,9,11,7,6,4,5,13,2,5,5,4,8,6,4,12],[2,5,9,11,7,6,4,5,13,2,5,5,4,8,6,4,12],[8,4,13,12,11,7,4,4,2,8,5,5,5,9,7,5,6],[0,8,1,3,4,14,2,8,0,0,9,9,13,1,14,13,16],[3,6,14,15,0,0,12,6,16,3,7,7,11,4,0,11,15],[8,4,13,12,11,7,4,4,2,8,5,5,5,9,7,5,6],[4,12,16,15,15,0,11,12,3,4,6,6,7,14,0,7,0]]

The magma definition

source
def «All4x4Tables [[1,2,0,16,3,4,13,2,0,1,8,8,9,1,4,9,14],[13,5,8,7,6,12,5,5,9,13,4,4,4,2,12,4,11],[0,9,1,4,14,16,8,9,1,0,13,13,2,0,16,2,3],[14,11,3,0,15,15,7,11,4,14,12,12,6,16,15,6,0],[16,7,4,0,0,15,6,7,14,16,11,11,12,3,15,12,15],[3,6,14,15,0,0,12,6,16,3,7,7,11,4,0,11,15],[9,4,2,6,12,11,5,4,8,9,4,4,5,13,11,5,7],[13,5,8,7,6,12,5,5,9,13,4,4,4,2,12,4,11],[1,13,0,14,16,3,9,13,1,1,2,2,8,0,3,8,4],[1,2,0,16,3,4,13,2,0,1,8,8,9,1,4,9,14],[2,5,9,11,7,6,4,5,13,2,5,5,4,8,6,4,12],[2,5,9,11,7,6,4,5,13,2,5,5,4,8,6,4,12],[8,4,13,12,11,7,4,4,2,8,5,5,5,9,7,5,6],[0,8,1,3,4,14,2,8,0,0,9,9,13,1,14,13,16],[3,6,14,15,0,0,12,6,16,3,7,7,11,4,0,11,15],[8,4,13,12,11,7,4,4,2,8,5,5,5,9,7,5,6],[4,12,16,15,15,0,11,12,3,4,6,6,7,14,0,7,0]]» :
Magma (Fin 17)
Equations
  • One or more equations did not get rendered due to their size.
Instances For

    The facts

    source
    theorem «Facts from All4x4Tables [[1,2,0,16,3,4,13,2,0,1,8,8,9,1,4,9,14],[13,5,8,7,6,12,5,5,9,13,4,4,4,2,12,4,11],[0,9,1,4,14,16,8,9,1,0,13,13,2,0,16,2,3],[14,11,3,0,15,15,7,11,4,14,12,12,6,16,15,6,0],[16,7,4,0,0,15,6,7,14,16,11,11,12,3,15,12,15],[3,6,14,15,0,0,12,6,16,3,7,7,11,4,0,11,15],[9,4,2,6,12,11,5,4,8,9,4,4,5,13,11,5,7],[13,5,8,7,6,12,5,5,9,13,4,4,4,2,12,4,11],[1,13,0,14,16,3,9,13,1,1,2,2,8,0,3,8,4],[1,2,0,16,3,4,13,2,0,1,8,8,9,1,4,9,14],[2,5,9,11,7,6,4,5,13,2,5,5,4,8,6,4,12],[2,5,9,11,7,6,4,5,13,2,5,5,4,8,6,4,12],[8,4,13,12,11,7,4,4,2,8,5,5,5,9,7,5,6],[0,8,1,3,4,14,2,8,0,0,9,9,13,1,14,13,16],[3,6,14,15,0,0,12,6,16,3,7,7,11,4,0,11,15],[8,4,13,12,11,7,4,4,2,8,5,5,5,9,7,5,6],[4,12,16,15,15,0,11,12,3,4,6,6,7,14,0,7,0]]» :
    ∃ (G : Type) (x : Magma G) (_ : Finite G), Equation3545 G ∧ ¬Equation3862 G ∧ ¬Equation4065 G ∧ ¬Equation4283 G ∧ ¬Equation4290 G ∧ ¬Equation4320 G ∧ ¬Equation4380 G ∧ ¬Equation4598 G ∧ ¬Equation4605 G ∧ ¬Equation4635 G