Lean Kernel Arena / perf/magma-string-n4

Countermodel certificate for an equational-theories implication, closed by decide. A magma on Fin 4 with the operation table encoded as a String satisfies x ◇ x = y ◇ ((x ◇ (y ◇ z)) ◇ z) but not x ◇ x = x ◇ (((y ◇ x) ◇ y) ◇ z). The smallest magma of the family (4^3 tuples); the cost is dominated by decoding each table entry out of the string on every lookup.

From a corpus of certificates generated for the SAIR math distillation challenge (equational theories track). The small end of the string-table family; magma-string-pair-n9 is the same workload at a larger scale.