SemiBase

A certified basis of 2 identities

This list of identities is a basis, proved in Lean, of 396 semigroups of order six, all of which generate the variety V[15004]. Removing the identities that follow from the others leaves 2 identities (Vampire); the variety page shows the shortest known basis.

Identifier sb-5f13964b2be86e16 in the data of the bases-min seal.

Certified for

[6, 15004] [6, 15009] [6, 15013] [6, 15018] [6, 15020] [6, 15021] [6, 15022] [6, 15023] [6, 15025] [6, 15026] [6, 15032] [6, 15036] [6, 15043] [6, 15045] [6, 15046] [6, 15047] [6, 15048] [6, 15050] [6, 15053] [6, 15055] [6, 15056] [6, 15057] [6, 15061] [6, 15063] [6, 15065] [6, 15069] [6, 15074] [6, 15076] [6, 15077] [6, 15078] [6, 15079] [6, 15081] [6, 15082] [6, 15089] [6, 15092] [6, 15093] [6, 15094] [6, 15095] [6, 15096] [6, 15100] [6, 15101] [6, 15106] [6, 15111] [6, 15115] [6, 15120] [6, 15122] [6, 15123] [6, 15125] [6, 15127] [6, 15128] [6, 15129] [6, 15130] [6, 15132] [6, 15133] [6, 15134] [6, 15135] [6, 15136] [6, 15137] [6, 15138] [6, 15139] [6, 15141] [6, 15144] [6, 15145] [6, 15146] [6, 15147] [6, 15148] [6, 15149] [6, 15151] [6, 15152] [6, 15153] [6, 15155] [6, 15157] [6, 15158] [6, 15159] [6, 15160] [6, 15164] [6, 15165] [6, 15166] [6, 15167] [6, 15170] [6, 15171] [6, 15176] [6, 15178] [6, 15181] [6, 15187] [6, 15191] [6, 15192] [6, 15193] [6, 15197] [6, 15201] [6, 15207] [6, 15208] [6, 15209] [6, 15210] [6, 15212] [6, 15213] [6, 15214] [6, 15217] [6, 15220] [6, 15221] [6, 15227] [6, 15229] [6, 15230] [6, 15231] [6, 15233] [6, 15234] [6, 15235] [6, 15237] [6, 15242] [6, 15243] [6, 15244] [6, 15245] [6, 15250] [6, 15251] [6, 15252] [6, 15262] [6, 15263] [6, 15269] [6, 15273] [6, 15279] [6, 15280] [6, 15281] [6, 15283] [6, 15284] [6, 15287] [6, 15288] [6, 15289] [6, 15290] [6, 15291] [6, 15292] [6, 15293] [6, 15294] [6, 15295] [6, 15296] [6, 15297] [6, 15298] [6, 15299] [6, 15300] [6, 15301] [6, 15302] [6, 15306] [6, 15307] [6, 15308] [6, 15309] [6, 15312] [6, 15313] [6, 15315] [6, 15316] [6, 15317] [6, 15321] [6, 15322] [6, 15323] [6, 15324] [6, 15328] [6, 15329] [6, 15330] [6, 15333] [6, 15335] [6, 15336] [6, 15337] [6, 15338] [6, 15339] [6, 15340] [6, 15345] [6, 15346] [6, 15347] [6, 15348] [6, 15349] [6, 15351] [6, 15352] [6, 15356] [6, 15358] [6, 15360] [6, 15365] [6, 15368] [6, 15370] [6, 15375] [6, 15377] [6, 15378] [6, 15383] [6, 15386] [6, 15388] [6, 15389] [6, 15397] [6, 15400] [6, 15401] [6, 15406] [6, 15407] [6, 15408] [6, 15409] [6, 15410] [6, 15411] [6, 15412] [6, 15413] [6, 15415] [6, 15416] [6, 15417] [6, 15420] [6, 15421] [6, 15422] [6, 15427] [6, 15428] [6, 15429] [6, 15431] [6, 15432] [6, 15433] [6, 15434] [6, 15435] [6, 15436] [6, 15437] [6, 15440] [6, 15441] [6, 15442] [6, 15443] [6, 15444] [6, 15445] [6, 15446] [6, 15448] [6, 15449] [6, 15450] [6, 15451] [6, 15453] [6, 15454] [6, 15460] [6, 15463] [6, 15466] [6, 15469] [6, 15472] [6, 15473] [6, 15474] [6, 15475] [6, 15476] [6, 15481] [6, 15486] [6, 15489] [6, 15494] [6, 15496] [6, 15497] [6, 15498] [6, 15499] [6, 15501] [6, 15502] [6, 15504] [6, 15510] [6, 15511] [6, 15512] [6, 15513] [6, 15515] [6, 15517] [6, 15518] [6, 15522] [6, 15525] [6, 15527] [6, 15529] [6, 15532] [6, 15535] [6, 15537] [6, 15539] [6, 15540] [6, 15541] [6, 15542] [6, 15546] [6, 15547] [6, 15550] [6, 15553] [6, 15554] [6, 15555] [6, 15556] [6, 15557] [6, 15558] [6, 15560] [6, 15561] [6, 15562] [6, 15563] [6, 15564] [6, 15565] [6, 15567] [6, 15568] [6, 15571] [6, 15572] [6, 15573] [6, 15574] [6, 15578] [6, 15579] [6, 15585] [6, 15589] [6, 15590] [6, 15591] [6, 15595] [6, 15598] [6, 15602] [6, 15606] [6, 15607] [6, 15611] [6, 15614] [6, 15618] [6, 15619] [6, 15620] [6, 15621] [6, 15624] [6, 15626] [6, 15628] [6, 15629] [6, 15631] [6, 15633] [6, 15640] [6, 15647] [6, 15648] [6, 15649] [6, 15652] [6, 15658] [6, 15663] [6, 15668] [6, 15672] [6, 15677] [6, 15679] [6, 15680] [6, 15681] [6, 15682] [6, 15684] [6, 15685] [6, 15690] [6, 15694] [6, 15701] [6, 15703] [6, 15704] [6, 15705] [6, 15706] [6, 15707] [6, 15709] [6, 15710] [6, 15711] [6, 15715] [6, 15717] [6, 15721] [6, 15726] [6, 15728] [6, 15729] [6, 15730] [6, 15731] [6, 15733] [6, 15734] [6, 15739] [6, 15742] [6, 15743] [6, 15744] [6, 15745] [6, 15749] [6, 15754] [6, 15759] [6, 15763] [6, 15768] [6, 15770] [6, 15771] [6, 15773] [6, 15775] [6, 15776] [6, 15777] [6, 15778] [6, 15780] [6, 15781] [6, 15785] [6, 15786] [6, 15789] [6, 15791] [6, 15792] [6, 15793] [6, 15794] [6, 15796] [6, 15797] [6, 15798] [6, 15799] [6, 15800] [6, 15801] [6, 15802] [6, 15803] [6, 15805] [6, 15806] [6, 15807] [6, 15808] [6, 15809] [6, 15811] [6, 15812] [6, 15815] [6, 15816] [6, 15819] [6, 15820] [6, 15826] [6, 15827] [6, 15831] [6, 15834] [6, 15838] [6, 15839] [6, 15848] [6, 15849] [6, 15853]

The identities

  1. x ≈ x²
  2. xy ≈ xyx